mCRL2
|
stores information about a constellation More...
#include <liblts_bisim_gjkw.h>
Public Member Functions | |
constln_t (state_type sort_key_, permutation_iter_t begin_, permutation_iter_t end_, B_to_C_iter_t postprocess_none) | |
constructor | |
~constln_t () | |
destructor | |
const constln_t * | get_nontrivial_next () const |
provides the next non-trivial constellation | |
void | make_trivial () |
makes a constellation trivial (i. e. removes it from the respective list) | |
void | make_nontrivial () |
makes a constellation non-trivial (i. e. inserts it into the respective list) | |
bool | is_trivial () const |
returns true iff the constellation is trivial | |
permutation_const_iter_t | begin () const |
constant iterator to the first state in the constellation | |
permutation_iter_t | begin () |
iterator to the first state in the constellation | |
void | set_begin (permutation_iter_t new_begin) |
set the iterator to the first state in the constellation | |
permutation_const_iter_t | end () const |
constant iterator past the last state in the constellation | |
permutation_iter_t | end () |
iterator past the last state in the constellation | |
void | set_end (permutation_iter_t new_end) |
set the iterator past the last state in the constellation | |
state_type | size () const |
returns number of states in the constellation | |
bool | operator< (const constln_t &other) const |
compares two constellations for ordering them | |
bool | operator> (const constln_t &other) const |
bool | operator<= (const constln_t &other) const |
bool | operator>= (const constln_t &other) const |
block_t * | split_off_small_block () |
split off a single block from the constellation | |
std::string | debug_id () const |
print a constellation identification for debugging | |
Static Public Member Functions | |
static constln_t * | get_some_nontrivial () |
provides an arbitrary non-trivial constellation | |
Public Attributes | |
B_to_C_iter_t | postprocess_begin |
iterator to the first transition into this constellation that needs postprocessing | |
B_to_C_iter_t | postprocess_end |
iterator past the last transition into this constellation that needs postprocessing | |
const state_type | sort_key |
sort key to order constellation-related information | |
Private Attributes | |
permutation_iter_t | int_end |
iterator past the last state in the constellation | |
permutation_iter_t | int_begin |
iterator to the first state in the constellation | |
constln_t * | nontrivial_next |
next constellation in the list of non-trivial constellations | |
Static Private Attributes | |
static constln_t * | nontrivial_first = nullptr |
first constellation in the list of non-trivial constellations | |
stores information about a constellation
A constellation corresponds to a slice in the permutation array; its boundaries are also block boundaries. As the number of constellations is initially unknown, we will allocate it dynamically.
Definition at line 811 of file liblts_bisim_gjkw.h.