mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_dnj::part_state_t Class Reference

refinable partition data structure More...

#include <liblts_bisim_dnj.h>

Public Member Functions

 part_state_t (state_type const num_states)
 constructor
 
state_type state_size () const
 calculate the size of the state space
 
const block_tblock (state_type const s) const
 find the block of a state
 
template<class LTS_TYPE >
void print_part (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print the partition per block
 
template<class LTS_TYPE >
void assert_consistency (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 asserts that the partition of states is consistent
 

Public Attributes

permutation_t permutation
 permutation array
 
bisim_gjkw::fixed_vector< state_info_entrystate_info
 array with all other information about states
 
state_type nr_of_blocks
 total number of blocks with unique sequence number allocated
 

Private Member Functions

template<class LTS_TYPE >
void print_block (const block_t *const B, const char *const message, const permutation_entry *begin_print, const permutation_entry *const end_print, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a slice of the partition (typically a block)
 

Detailed Description

refinable partition data structure

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

Definition at line 1218 of file liblts_bisim_dnj.h.

Constructor & Destructor Documentation

◆ part_state_t()

mcrl2::lts::detail::bisim_dnj::part_state_t::part_state_t ( state_type const  num_states)
inline

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_statesnumber of states in the LTS

Definition at line 1241 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ assert_consistency()

template<class LTS_TYPE >
void mcrl2::lts::detail::bisim_dnj::part_state_t::assert_consistency ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

asserts that the partition of states is consistent

It also requires that no states are marked.

Parameters
partitionerLTS partitioner (used to print more details)

Definition at line 1359 of file liblts_bisim_dnj.h.

◆ block()

const block_t * mcrl2::lts::detail::bisim_dnj::part_state_t::block ( state_type const  s) const
inline

find the block of a state

Parameters
snumber of the state
Returns
a pointer to the block where state s resides in

Definition at line 1286 of file liblts_bisim_dnj.h.

◆ print_block()

template<class LTS_TYPE >
void mcrl2::lts::detail::bisim_dnj::part_state_t::print_block ( const block_t *const  B,
const char *const  message,
const permutation_entry begin_print,
const permutation_entry *const  end_print,
const bisim_partitioner_dnj< LTS_TYPE > &  partitioner 
) const
inlineprivate

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
messagetext printed as a title if the slice is not empty
begin_printiterator to the beginning of the slice
end_printiterator past the end of the slice
partitionerLTS partitioner (used to print more details)

Definition at line 1300 of file liblts_bisim_dnj.h.

◆ print_part()

template<class LTS_TYPE >
void mcrl2::lts::detail::bisim_dnj::part_state_t::print_part ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print the partition per block

The function prints all blocks in order. For each block, it lists its states, separated into nonbottom and bottom states.

Parameters
partitionerLTS partitioner (used to print more details)

Definition at line 1335 of file liblts_bisim_dnj.h.

◆ state_size()

state_type mcrl2::lts::detail::bisim_dnj::part_state_t::state_size ( ) const
inline

calculate the size of the state space

Returns
the number of states in the LTS

Definition at line 1280 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ nr_of_blocks

state_type mcrl2::lts::detail::bisim_dnj::part_state_t::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.

Definition at line 1233 of file liblts_bisim_dnj.h.

◆ permutation

permutation_t mcrl2::lts::detail::bisim_dnj::part_state_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.

Definition at line 1225 of file liblts_bisim_dnj.h.

◆ state_info

bisim_gjkw::fixed_vector<state_info_entry> mcrl2::lts::detail::bisim_dnj::part_state_t::state_info

array with all other information about states

Definition at line 1228 of file liblts_bisim_dnj.h.


The documentation for this class was generated from the following file: