mCRL2
Loading...
Searching...
No Matches
Part_state

data structures for states More...

Namespaces

namespace  mcrl2::lts::detail::bisim_gjkw
 

Classes

class  mcrl2::lts::detail::bisim_dnj::state_info_entry
 stores information about a single state More...
 
class  mcrl2::lts::detail::bisim_dnj::permutation_entry
 entry in the permutation array More...
 
class  mcrl2::lts::detail::bisim_dnj::block_t
 stores information about a block More...
 
class  mcrl2::lts::detail::bisim_dnj::part_state_t
 refinable partition data structure More...
 
class  mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >
 implements the main algorithm for the stutter equivalence quotient More...
 
class  permutation_t
 stores a permutation of the states, ordered by block More...
 

Typedefs

typedef bisim_gjkw::fixed_vector< permutation_entrymcrl2::lts::detail::bisim_dnj::permutation_t
 
typedef simple_list< block_bunch_slice_t >::iterator mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_t
 
typedef simple_list< block_bunch_slice_t >::const_iterator mcrl2::lts::detail::bisim_dnj::block_bunch_slice_const_iter_t
 
typedef simple_list< block_bunch_slice_t >::iterator_or_null mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_or_null_t
 

Enumerations

enum  mcrl2::lts::detail::bisim_dnj::new_block_mode_t { mcrl2::lts::detail::bisim_dnj::new_block_is_U , mcrl2::lts::detail::bisim_dnj::new_block_is_R }
 

Detailed Description

data structures for states

data structures for a refinable partition

States are stored in a refinable partition data structure. The actual state information will not be moved around, but only entries in a separate permutation array. Entries is this array are grouped per block, so that the states in a block can be described as a slice in the permutation array.

The following definitions provide a refinable partition data structure. The basic idea is that we store a permutation of the states (in a permutation_t array), so that states belonging to the same block are adjacent, and also that blocks belonging to the same constellation are adjacent.

The basic structure therefore consists of the classes:

state_info_ptr - an entry in the permutation array; it contains a pointer to a state_info_entry. permutation_t - an array of permutation_entries. constln_t - contains information about a constellation, in particular which slice of permutation_t contains its states. block_t - contains information about a block, in particular which slice of permutation_t contains its states, and its constellation. state_info_entry - contains information about a state, in particular its position in the permutation_t array and its block. state_info_t - an array of state_info_entries. part_state_t - the complete data structure combining state_info_t and permutation_t.

This basic structure is extended as follows:

Typedef Documentation

◆ block_bunch_slice_const_iter_t

◆ block_bunch_slice_iter_or_null_t

◆ block_bunch_slice_iter_t

◆ permutation_t

Enumeration Type Documentation

◆ new_block_mode_t

Enumerator
new_block_is_U 
new_block_is_R 

Definition at line 905 of file liblts_bisim_dnj.h.