mcrl2::lts::detail::bisim_dnj::state_info_entry

class mcrl2::lts::detail::bisim_dnj::state_info_entry

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

Public attributes

block_t *block

block where the state belongs

iterator_or_counter<succ_iter_t> current_out_slice

iterator to first outgoing transition to the bunch of interest

This iterator generally points to the an outgoing non-inert transition of the state, to the first transition in an out-slice. If the bottom state has a transition in the splitter bunch (for a specific refinement), this out-slice contains the transitions in the splitter. The iterator helps to decide quickly whether a bottom state has a transition in the splitter.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.

union mcrl2::lts::detail::bisim_dnj::state_info_entry::not__t not_
permutation_iter_t pos

position of the state in the permutation array

iterator_or_counter<pred_iter_t> 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 inert incoming transitions, and as the pointer to the first incoming inert transition that already has been initialised.

iterator_or_counter<succ_iter_t> 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.

bisim_gjkw::check_complexity::state_dnj_counter_t work_counter

public-static-attrib

state_info_const_iter_t s_i_begin

pointer at the first non-dummy entry in the state_info array

state_info_const_iter_t s_i_end

pointer past the last non-dummy entry in the state_info array

Public member functions

std::string debug_id() const

print a state identification for debugging

std::string debug_id_short() const

print a short state identification for debugging

bool surely_has_no_transition_in(const bunch_t *bunch) const
bool surely_has_no_transition_in(const bunch_t *bunch) const

quick check to find out whether the state has no transition in bunch

If the current_out_slice pointer happens to be set to the new bunch NewBu (which is the immediate successor of the most recent splitter bunch bunch), the function can quickly find out whether the state has a transition in bunch. Note that here, we will need that the dummy transition at the beginning of part_tr.pred has a source state iterator that can be dereferenced.

Parameters:

  • bunch bunch of interest

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

bool surely_has_transition_in(const bunch_t *bunch) const
bool surely_has_transition_in(const bunch_t *bunch) const

quick check to find out whether the state has a transition in bunch

If the current_out_slice pointer happens to be set to the bunch the function can quickly find out whether the state has a transition in bunch.

Parameters:

  • bunch bunch of interest

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