# 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