stores information about a block More...

#include <liblts_bisim_gjkw.h>

Public Member Functions
	block_t (constln_t *const constln_, permutation_iter_t const begin_, permutation_iter_t const end_)
	constructor

	~block_t ()

void	assign_seqnr ()
	assigns a unique sequence number

state_type	seqnr () const

bool	is_refinable () const
	checks whether the block is refinable

bool	make_refinable ()
	makes a block refinable (i. e. inserts it into the respective list)

void	make_nonrefinable ()
	makes a block non-refinable (i. e. removes it from the respective list)

state_type	size () const
	provides the number of states in the block

state_type	marked_bottom_size () const
	provides the number of marked bottom states in the block

state_type	marked_size () const
	provides the number of marked states in the block

state_type	unmarked_bottom_size () const
	provides the number of unmarked bottom states in the block

bool	operator< (const block_t &other) const
	compares two blocks for ordering them

const constln_t *	constln () const
	constellation where the block belongs to

constln_t *	constln ()

void	set_constln (constln_t *new_constln)

B_to_C_descriptor *	FromRed (const constln_t *SpC)
	read FromRed

void	SetFromRed (B_to_C_desc_iter_t new_fromred)
	set FromRed to an existing element in to_constln

permutation_const_iter_t	begin () const
	iterator to the first state in the block

permutation_iter_t	begin ()

void	set_begin (permutation_iter_t new_begin)

permutation_const_iter_t	end () const
	iterator past the last state in the block

permutation_iter_t	end ()

void	set_end (permutation_iter_t new_end)

permutation_const_iter_t	nonbottom_begin () const
	iterator to the first non-bottom state in the block

permutation_iter_t	nonbottom_begin ()

permutation_const_iter_t	nonbottom_end () const
	iterator past the last non-bottom state in the block

permutation_iter_t	nonbottom_end ()

void	set_nonbottom_end (permutation_iter_t new_nonbottom_end)

permutation_const_iter_t	bottom_begin () const
	iterator to the first bottom state in the block

permutation_iter_t	bottom_begin ()

void	set_bottom_begin (permutation_iter_t new_bottom_begin)

permutation_const_iter_t	bottom_end () const
	iterator past the last bottom state in the block

permutation_iter_t	bottom_end ()

permutation_const_iter_t	unmarked_nonbottom_begin () const
	iterator to the first unmarked non-bottom state in the block

permutation_iter_t	unmarked_nonbottom_begin ()

permutation_const_iter_t	unmarked_nonbottom_end () const
	iterator past the last unmarked non-bottom state in the block

permutation_iter_t	unmarked_nonbottom_end ()

void	set_unmarked_nonbottom_end (permutation_iter_t new_unmarked_nonbottom_end)

permutation_const_iter_t	marked_nonbottom_begin () const
	iterator to the first marked non-bottom state in the block

permutation_iter_t	marked_nonbottom_begin ()

void	set_marked_nonbottom_begin (permutation_iter_t new_marked_nonbottom_begin)

permutation_const_iter_t	marked_nonbottom_end () const
	iterator one past the last marked non-bottom state in the block

permutation_iter_t	marked_nonbottom_end ()

permutation_const_iter_t	unmarked_bottom_begin () const
	iterator to the first unmarked bottom state in the block

permutation_iter_t	unmarked_bottom_begin ()

permutation_const_iter_t	unmarked_bottom_end () const
	iterator past the last unmarked bottom state in the block

permutation_iter_t	unmarked_bottom_end ()

void	set_unmarked_bottom_end (permutation_iter_t new_unmarked_bottom_end)

permutation_const_iter_t	marked_bottom_begin () const
	iterator to the first marked bottom state in the block

permutation_iter_t	marked_bottom_begin ()

void	set_marked_bottom_begin (permutation_iter_t new_marked_bottom_begin)

permutation_const_iter_t	marked_bottom_end () const
	iterator past the last marked bottom state in the block

permutation_iter_t	marked_bottom_end ()

B_to_C_const_iter_t	inert_begin () const
	iterator to the first inert transition of the block

B_to_C_iter_t	inert_begin ()

void	set_inert_begin (B_to_C_iter_t new_inert_begin)

B_to_C_const_iter_t	inert_end () const
	iterator past the last inert transition of the block

B_to_C_iter_t	inert_end ()

void	set_inert_end (B_to_C_iter_t new_inert_end)

void	set_inert_begin_and_end (B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)

bool	mark_nonbottom (state_info_ptr s)
	mark a non-bottom state

bool	mark (state_info_ptr s)
	mark a state

block_t *	split_off_blue (permutation_iter_t blue_nonbottom_end)
	refine the block (the blue subblock is smaller)

block_t *	split_off_red (permutation_iter_t red_nonbottom_begin)
	refine the block (the red subblock is smaller)

std::string	debug_id () const
	print a block identification for debugging

Static Public Member Functions
static block_t *	get_some_refinable ()
	provides an arbitrary refinable block

static permutation_const_iter_t	permutation_begin ()
	provide an iterator to the beginning of the permutation array

Public Attributes
B_to_C_desc_list	to_constln
	list of B_to_C with transitions from this block

check_complexity::block_counter_t	work_counter

Static Public Attributes
static state_type	nr_of_blocks = 0
	total number of blocks with unique sequence number allocated

Private Attributes
permutation_iter_t	int_end
	iterator past the last state of the block

permutation_iter_t	int_begin
	iterator to the first state of the block

permutation_iter_t	int_marked_nonbottom_begin
	iterator to the first marked non-bottom state of the block

permutation_iter_t	int_bottom_begin
	iterator to the first bottom state of the block

permutation_iter_t	int_marked_bottom_begin
	iterator to the first marked bottom state of the block

B_to_C_iter_t	int_inert_begin
	iterator to the first inert transition of the block

B_to_C_iter_t	int_inert_end
	iterator past the last inert transition of the block

constln_t *	int_constln
	constellation to which the block belongs

block_t *	refinable_next
	next block in the list of refinable blocks

state_type	int_seqnr
	unique sequence number of this block

Static Private Attributes
static block_t *	refinable_first = nullptr
	first block in the list of refinable blocks

static permutation_const_iter_t	perm_begin

Friends
class	part_state_t

Detailed Description

stores information about a block

A block corresponds to a slice of the permutation array. As the number of blocks is initially unknown, we will allocate instances of this class dynamically.

The slice in the permutation array containing the states of the block is subdivided into the following subslices (in this order):

unmarked non-bottom states
marked non-bottom states (initially empty)
unmarked bottom states
marked bottom states (initially empty)

A state should be marked iff it is a predecessor of the current splitter (through a strong transition). The marking is later extended to the red states; that are the states with a weak transition to the splitter.

(During the execution of some functions, more slices are subdivided further; however, as these subdivisions are local to a single function, they are not stored here.)

The blocks keep track of the total number of blocks allocated and number themselves sequentially using the static member nr_of_blocks. It is therefore impossible to have multiple refinements running at the same time.

Definition at line 403 of file liblts_bisim_gjkw.h.

The documentation for this class was generated from the following files:

lts/include/mcrl2/lts/detail/liblts_bisim_gjkw.h
lts/source/liblts_bisim_gjkw.cpp

Public Member Functions

Static Public Member Functions

Public Attributes

Static Public Attributes

Private Attributes

Static Private Attributes

Friends

Detailed Description