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

refinable partition data structure More...

#include <liblts_bisim_gjkw.h>

Public Member Functions

 part_state_t (state_type n)
 constructor
 
 ~part_state_t ()
 destructor
 
void clear ()
 deallocates constellations and blocks
 
state_type state_size () const
 provide size of state space
 
const block_tblock (state_type s) const
 find block of a state
 
void print_part (const part_trans_t &part_tr) const
 print the partition as a tree (per constellation and block)
 
void print_trans () const
 print all transitions
 

Public Attributes

permutation_t permutation
 permutation array
 

Private Member Functions

void print_block (const char *message, const block_t *B, permutation_const_iter_t begin, permutation_const_iter_t end) const
 print a slice of the partition (typically a block)
 

Private Attributes

fixed_vector< state_info_entrystate_info
 array with all other information about states
 

Friends

template<class LTS_TYPE >
class bisim_partitioner_gjkw_initialise_helper
 

Detailed Description

refinable partition data structure

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

Definition at line 1015 of file liblts_bisim_gjkw.h.


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