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_iter_t begin
action_block_iter_t end
bunch_t *next_nontrivial
union mcrl2::lts::detail::bisim_dnj::bunch_t::sort_key_and_label_t sort_key_and_label
bisim_gjkw::check_complexity::bunch_dnj_counter_t work_counter


bunch_t *first_nontrivial

Public member functions

bunch_t(const action_block_iter_t &new_begin, const action_block_iter_t &new_end, trans_type new_sort_key)
std::string debug_id() const

print a bunch identification for debugging

std::string debug_id_short() 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).

void make_nontrivial()
void make_trivial()
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.

bool operator<(const bunch_t &el) const
bool operator<=(const bunch_t &el) const
bool operator>(const bunch_t &el) const
bool operator>=(const bunch_t &el) const
bunch_t *split_off_small_action_block_slice()

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.

Public static member functions

static bunch_t *get_some_nontrivial()