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

stores information about a single state More...

#include <liblts_bisim_gjkw.h>

Public Member Functions

const constln_tconstln () const
 get constellation where the state belongs
 
constln_tconstln ()
 
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_tblock
 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
SpCconstellation of interest
Returns
true if the state is known to have no transition to SpC

Definition at line 2047 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
SpCconstellation of interest
Returns
true if the state is known to have a transition to SpC

Definition at line 2019 of file liblts_bisim_gjkw.h.


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