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 fixed_vector< permutation_entry >	mcrl2::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 iterator_or_null_t< block_bunch_slice_t >	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:

Because we combine this data structure with a partition of the transitions, a state_info_entry also contains information which slice of the incoming and outgoing, inert and non-inert transitions belong to the state. In many cases the slice of this state ends exactly where the slice of the next state begins, so we can find the end of this state's slice by looking at the next state's state_info_entry. Therefore, state_info_ptr actually contains a pointer to a state_info_entry with the additional guarantee that this is not the last entry in state_info_t. (To make this a small bit more type safe, we could change the type state_info_ptr to something like `‘pointer to an array with two state_info_entries’', typedef state_info_entry (*state_info_ptr)[2];. Still, that would allow unsafe pointer juggling.)
A block_t also contains information about its outgoing inert transitions.
A state_info_entry also contains information used during refine() or process_new_bottom().