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.)

Public attributes

permutation_entry *begin

iterator to the first state of the block

permutation_entry *end

iterator past the last state of the block

permutation_entry *marked_bottom_begin

iterator to the first marked bottom state of the block

permutation_entry *marked_nonbottom_begin

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

permutation_entry *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.

simple_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 member functions

block_t(permutation_entry *new_begin, permutation_entry *new_end, state_type new_seqnr)

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
  • new_seqnr is the sequence number of the new block
state_type bottom_size() const

provides the number of bottom states in the block

std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

print a block identification for debugging

bool mark(permutation_entry *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 iff the state was not marked before

bool mark_nonbottom(permutation_entry *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 iff 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 size() const

provides the number of states in the block

void split_off_block(enum new_block_mode_t const new_block_mode, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_t *const new_block)

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.)
  • new_seqnr is the sequence number of the new block

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