mcrl2::lts::detail::bisim_dnj::block_t

class mcrl2::lts::detail::bisim_dnj::block_t

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 bottom statesmarked bottom states (initially empty)unmarked non-bottom statesmarked non-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, blocks 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.

Public attributes

permutation_iter_t begin

iterator to the first state of the block

permutation_iter_t end

iterator past the last state of the block

permutation_iter_t marked_bottom_begin

iterator to the first marked bottom state of the block

permutation_iter_t marked_nonbottom_begin

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

permutation_iter_t nonbottom_begin

iterator to the first non-bottom state of the block

const state_type seqnr

unique sequence number of this block

After the stuttering equivalence algorithm has terminated, this number is used as a state number in the quotient LTS.

std::list<block_bunch_slice_t> stable_block_bunch

list of stable block_bunch-slices with transitions from this block

bisim_gjkw::check_complexity::block_dnj_counter_t work_counter

public-static-attrib

state_type nr_of_blocks

total number of blocks with unique sequence number allocated

Upon starting the stuttering equivalence algorithm, the number of blocks must be zero.

Public member functions

block_t(const permutation_iter_t &new_begin, const permutation_iter_t &new_end)

constructor

The constructor initialises the block to: all states are bottom states, no state is marked.

Parameters:

  • new_begin initial iterator to the first state of the block
  • new_end initial iterator past the last state of the block
state_type bottom_size() const

provides the number of bottom states in the block

std::string debug_id() const

print a block identification for debugging

bool mark(const permutation_iter_t &s)

mark a state

Marking is done by moving the state to the slice of the marked bottom or non-bottom states of the block.

Parameters:

  • s the state that has to be marked

Returns: true if the state was not marked before

bool mark_nonbottom(const permutation_iter_t &s)

mark a non-bottom state

Marking is done by moving the state to the slice of the marked non-bottom states of the block.

Parameters:

  • s the non-bottom state that has to be marked

Returns: true if the state was not marked before

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 nonbottom_size() const

provides the number of non-bottom states in the block

void print_block(const char *message, permutation_const_iter_t begin_print, const permutation_const_iter_t &end_print) const

print a slice of the partition (typically a block)

If the slice indicated by the parameters is not empty, the message and the states in this slice will be printed.

Parameters:

  • message text printed as a title if the slice is not empty
  • begin_print iterator to the beginning of the slice
  • end_print iterator past the end of the slice
state_type size() const

provides the number of states in the block

block_t* split_off_block(enum new_block_mode_t const new_block_mode)

refine a block

This function is called after a refinement function has found where to split the block into unmarked (blue) and marked (red) states. It creates a new block for the smaller subblock.

Parameters:

  • new_block_mode indicates whether the blue or the red block should be the new one. (This parameter is necessary in case the two halves have exactly the same size.)

Returns: pointer to the new block

state_type unmarked_bottom_size() const

provides the number of unmarked bottom states in the block

state_type unmarked_nonbottom_size() const

provides the number of unmarked nonbottom states in the block