stores information about a single state More...

#include <liblts_bisim_gjkw.h>

Public Member Functions
const constln_t *	constln () const
	get constellation where the state belongs

constln_t *	constln ()

succ_const_iter_t	current_constln () const

succ_iter_t	current_constln ()

void	set_current_constln (succ_iter_t const new_current_constln)

pred_const_iter_t	pred_begin () const
	iterator to first incoming transition

pred_iter_t	pred_begin ()

void	set_pred_begin (pred_iter_t new_in_begin)

pred_const_iter_t	pred_end () const
	iterator past the last incoming transition

pred_iter_t	pred_end ()

void	set_pred_end (pred_iter_t new_in_end)

pred_const_iter_t	noninert_pred_begin () const
	iterator to first non-inert incoming transition

pred_iter_t	noninert_pred_begin ()

pred_const_iter_t	noninert_pred_end () const
	iterator past the last non-inert incoming transition

pred_iter_t	noninert_pred_end ()

pred_const_iter_t	inert_pred_begin () const
	iterator to first inert incoming transition

pred_iter_t	inert_pred_begin ()

void	set_inert_pred_begin (pred_iter_t new_inert_in_begin)

pred_const_iter_t	inert_pred_end () const
	iterator one past the last inert incoming transition

pred_iter_t	inert_pred_end ()

succ_const_iter_t	succ_begin () const
	iterator to first outgoing transition

succ_iter_t	succ_begin ()

void	set_succ_begin (succ_iter_t new_out_begin)

succ_const_iter_t	succ_end () const
	iterator past the last outgoing transition

succ_iter_t	succ_end ()

void	set_succ_end (succ_iter_t new_out_end)

succ_const_iter_t	inert_succ_begin () const
	iterator to first inert outgoing transition

succ_iter_t	inert_succ_begin ()

void	set_inert_succ_begin (succ_iter_t const new_inert_out_begin)

succ_const_iter_t	inert_succ_end () const
	iterator past the last inert outgoing transition

succ_iter_t	inert_succ_end ()

void	set_inert_succ_begin_and_end (succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)

bool	surely_has_transition_to (const constln_t *SpC) const

bool	surely_has_no_transition_to (const constln_t *SpC) const

std::string	debug_id_short () const
	print a short state identification for debugging

std::string	debug_id () const
	print a state identification for debugging

bool	surely_has_transition_to (const constln_t *const SpC) const
	quick check to find out whether the state has a transition to `SpC`

bool	surely_has_no_transition_to (const constln_t *const SpC) const
	quick check to find out whether the state has no transition to `SpC`

Public Attributes
block_t *	block
	block where the state belongs

permutation_iter_t	pos
	position of the state in the permutation array

state_type	notblue
	number of inert transitions to non-blue states

check_complexity::state_counter_t	work_counter

Private Attributes
pred_iter_t	state_in_begin
	iterator to first incoming transition

succ_iter_t	state_out_begin
	iterator to first outgoing transition

pred_iter_t	state_inert_in_begin
	iterator to first inert incoming transition

succ_iter_t	state_inert_out_begin
	iterator to first inert outgoing transition

succ_iter_t	state_inert_out_end
	iterator past the last inert outgoing transition

succ_iter_t	int_current_constln
	iterator to first outgoing transition to the constellation of interest

Static Private Attributes
static state_info_const_ptr	s_i_begin
	pointer at the first entry in the `state_info` array

static state_info_const_ptr	s_i_end
	pointer past the last actual entry in the `state_info` array

Friends
class	part_state_t

Detailed Description

stores information about a single state

This class stores all other information about a state that the partition needs. In particular: the block where the state belongs and the position in the permutation array (i. e. the inverse of the permutation).

A state_info_entry only works correctly if it is part of an array where there is one more state_info_entry. The reason is that iterators past the last transition are not actually stored here, as they are equal to the iterator to the first transition of the next state. The array will contain one additional `‘state’' that is only used for these pointers.

Definition at line 163 of file liblts_bisim_gjkw.h.

Member Function Documentation

◆ surely_has_no_transition_to()

bool surely_has_no_transition_to ( const constln_t *const SpC ) const

inline

quick check to find out whether the state has no transition to SpC

If the current constellation pointer happens to be set to SpC or its successor, the function can quickly find out whether the state has a transition to SpC. The function should not be called for the constellation in which the state resides.

Parameters

SpC	constellation of interest

Returns: true if the state is known to have no transition to SpC

Definition at line 2071 of file liblts_bisim_gjkw.h.

◆ surely_has_transition_to()

bool surely_has_transition_to ( const constln_t *const SpC ) const

inline

quick check to find out whether the state has a transition to SpC

If the current constellation pointer happens to be set to SpC, the function can quickly find out whether the state has a transition to SpC. The function should not be called for the constellation in which the state resides.

Parameters

SpC	constellation of interest

Returns: true if the state is known to have a transition to SpC

Definition at line 2043 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

Public Attributes

Private Attributes

Static Private Attributes

Friends

Detailed Description

Member Function Documentation

◆ surely_has_no_transition_to()

◆ surely_has_transition_to()