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

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

const block_t *block(state_type s) const

find the block of a state


  • s number of the state

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

part_state_t(state_type num_states)


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


  • num_states number of states in the LTS
state_type state_size() const

calculate the size of the state space

Returns: the number of states in the LTS



The destructor also deallocates the blocks, as they are not directly referenced from anywhere.

Public static member functions

static void assert_consistency(bool branching)

asserts that the partition of states is consistent

It also requires that no states are marked.

void print_part()

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.


  • part_tr partition for the transitions