- Generated by
1.9.7
|
mCRL2
|
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_entry * | pos |
| 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 | |
| check_complexity::state_dnj_counter_t | work_counter |
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 215 of file liblts_bisim_dnj.h.
|
inline |
print a state identification for debugging
Definition at line 277 of file liblts_bisim_dnj.h.
|
inline |
print a short state identification for debugging
Definition at line 268 of file liblts_bisim_dnj.h.
| union mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t mcrl2::lts::detail::bisim_dnj::state_info_entry::bl |
| permutation_entry* mcrl2::lts::detail::bisim_dnj::state_info_entry::pos |
position of the state in the permutation array
Definition at line 248 of file liblts_bisim_dnj.h.
| 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 225 of file liblts_bisim_dnj.h.
| 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 234 of file liblts_bisim_dnj.h.
| 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 264 of file liblts_bisim_dnj.h.
|
mutable |
Definition at line 283 of file liblts_bisim_dnj.h.
1.9.7