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

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_tget_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_tsplit_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_tget_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_tnontrivial_next
 next constellation in the list of non-trivial constellations
 

Static Private Attributes

static constln_tnontrivial_first = nullptr
 first constellation in the list of non-trivial constellations
 

Detailed Description

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.


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