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

stores information about a single state More...

#include <liblts_bisim_dnj.h>

Classes

union  bl_t
 block where the state belongs More...
 

Public Member Functions

template<class LTS_TYPE >
std::string debug_id_short (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a short state identification for debugging
 
template<class LTS_TYPE >
std::string debug_id (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a state identification for debugging
 

Public Attributes

iterator_or_counter< pred_entry * > pred_inert
 iterator to first inert incoming transition
 
iterator_or_counter< succ_entry * > succ_inert
 iterator to first inert outgoing transition
 
union mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t bl
 
permutation_entrypos
 position of the state in the permutation array
 
iterator_or_counter< succ_entry * > untested_to_U_eqv
 number of inert transitions to non-U-states
 
bisim_gjkw::check_complexity::state_dnj_counter_t work_counter
 

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).

Definition at line 913 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ debug_id()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::bisim_dnj::state_info_entry::debug_id ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print a state identification for debugging

Definition at line 975 of file liblts_bisim_dnj.h.

◆ debug_id_short()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::bisim_dnj::state_info_entry::debug_id_short ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print a short state identification for debugging

Definition at line 966 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ bl

union mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t mcrl2::lts::detail::bisim_dnj::state_info_entry::bl

◆ pos

permutation_entry* mcrl2::lts::detail::bisim_dnj::state_info_entry::pos

position of the state in the permutation array

Definition at line 946 of file liblts_bisim_dnj.h.

◆ pred_inert

iterator_or_counter<pred_entry*> mcrl2::lts::detail::bisim_dnj::state_info_entry::pred_inert

iterator to first inert incoming transition

Non-inert incoming transitions of the state are stored just before the element where this iterator points to.

During initialisation, this field also doubles up as a counter for the number of incoming transitions, and as the pointer to the first incoming inert transition that already has been initialised.

Definition at line 923 of file liblts_bisim_dnj.h.

◆ succ_inert

iterator_or_counter<succ_entry*> mcrl2::lts::detail::bisim_dnj::state_info_entry::succ_inert

iterator to first inert outgoing transition

Non-inert outgoing transitions of the state are stored just before the element where this iterator points to.

During initialisation, this field also doubles up as a counter for the number of inert outgoing transitions, and as the pointer to the first outgoing inert transition that already has been initialised.

Definition at line 932 of file liblts_bisim_dnj.h.

◆ untested_to_U_eqv

iterator_or_counter<succ_entry*> mcrl2::lts::detail::bisim_dnj::state_info_entry::untested_to_U_eqv

number of inert transitions to non-U-states

Actually, as we cannot easily count how many inert outgoing transitions this state has, we initialize this pointer to succ_inert.begin. Every time we find an outgoing transition to a U-state, we increase this iterator; as soon as it no longer points to an outgoing transition of this state, we have found all inert outgoing transitions. This requires that after the inert outgoing transitions there is a transition that starts in another state, or there is a dummy transition.

During initialisation, this field also doubles up as a counter for the number of non-inert outgoing transitions, and as the pointer to the first outgoing transition that already has been initialised. Therefore it cannot be a const succ_entry*.

Definition at line 962 of file liblts_bisim_dnj.h.

◆ work_counter

bisim_gjkw::check_complexity::state_dnj_counter_t mcrl2::lts::detail::bisim_dnj::state_info_entry::work_counter
mutable

Definition at line 981 of file liblts_bisim_dnj.h.


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