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)
 ~part_state_t ()
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


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: