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 ()=default
	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 = nullptr
	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

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 817 of file liblts_bisim_gjkw.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_gjkw.h
lts/source/liblts_bisim_gjkw.cpp

Public Member Functions

Static Public Member Functions

Public Attributes

Private Attributes

Static Private Attributes

Detailed Description