mcrl2::lts::detail::bisim_dnj::part_state_t

class mcrl2::lts::detail::bisim_dnj::part_state_t

refinable partition data structure

This class collects all information about a partition of the states.

Public attributes

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.

permutation_t permutation

permutation array

This is the central element of the data structure: In this array, states that belong to the same block are stored in adjacent elements.

bisim_gjkw::fixed_vector<state_info_entry> state_info

array with all other information about states

We allocate 1 additional dummy ``state’’ at the end of the array, to get an illegal state that can actually be dereferenced.

Public member functions

void assert_consistency(bool branching, const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

asserts that the partition of states is consistent

It also requires that no states are marked.

const block_t *block(state_type s) const

find the block of a state

Parameters:

  • s number of the state

Returns: a pointer to the block where state s resides in

part_state_t(state_type num_states)

constructor

The constructor allocates memory and makes the permutation and state_info arrays consistent with each other, but does not actually initialise the partition. Immediately afterwards, the initialisation will be done in bisim_partitioner_dnj::create_initial_partition().

Parameters:

  • num_states number of states in the LTS
void print_block(const block_t *B, const char *message, const permutation_entry *begin_print, const permutation_entry *end_print, const bisim_partitioner_dnj<LTS_TYPE> &partitioner) 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

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

Parameters:

  • message text printed as a title if the slice is not empty
  • B block that is being printed (it is checked whether states belong to this block)
  • begin iterator to the beginning of the slice
  • end iterator past the end of the slice
void print_part(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

print the partition per block

print the partition as a tree (per constellation and block)The function prints all blocks in order. For each block, it lists its states, separated into nonbottom and bottom states.The function prints all constellations (in order); for each constellation it prints the blocks it consists of; and for each block, it lists its states, separated into nonbottom and bottom states.

Parameters:

  • part_tr partition for the transitions
state_type state_size() const

calculate the size of the state space

Returns: the number of states in the LTS