mcrl2::lts::detail::bisim_dnj::bunch_t

class mcrl2::lts::detail::bisim_dnj::bunch_t

bunch of transitions

Like a slice, at the end of the algorithm there will be a bunch for every transition in the bisimulation quotient. Therefore, we should try to minimize the size of a bunch as much as possible.

Public attributes

action_block_entry *begin
action_block_entry *end
union mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t next_nontrivial_and_label
bisim_gjkw::check_complexity::bunch_dnj_counter_t work_counter

Public member functions

bunch_t(action_block_entry *new_begin, action_block_entry *new_end)
std::string debug_id(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

print a bunch identification for debugging

std::string debug_id_short(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const
bool is_trivial() const

returns true iff the bunch is trivial

If this bunch is the last in the list of non-trivial bunches, the convention is that the next pointer points to this bunch itself (to distinguish it from nullptr).

int max_work_counter(const bisim_partitioner_dnj<LTS_TYPE> &partitioner) const

calculates the maximal allowed value for work counters associated with this bunch

Work counters may only be nonzero if this bunch is a single-action bunch, i. e. all its transitions have the same action label. Also, only then the size can be calculated as end - begin.

void split_off_small_action_block_slice(part_trans_t &part_tr, bunch_t *bunch_T_a_B)

split off a single action_block-slice from the bunch

The function splits the current bunch after its first action_block-slice or before its last action_block-slice, whichever is smaller. It creates a new bunch for the split-off slice and returns a pointer to the new bunch. The caller has to adapt the block_bunch-slices.The function splits the current bunch after its first action_block-slice or before its last action_block-slice, whichever is smaller. It creates a new bunch for the split-off slice and returns a pointer to the new bunch. The caller has to adapt the block_bunch-slices.

Parameters:

  • part_tr the data structure containing information about the partition of transitions (needed to find the list of non-trivial bunches)

Returns: pointer to a new bunch containing one small action_block-slice that was originally in this bunch