class mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t

Information about a set of transitions with the same source block, in the same bunch.

This describes the coarser partition of transitions. In the end we will have one slice for each transition, so we should try to minimize this data structure as much as possible.Also note that these slices are part of a doubly-linked list. We cannot change this to a singly-linked list because then we would have to meticulously keep the list ordered, which is not possible when a block loses all its bottom states.

Public attributes

class mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t::bunch_stability_t bunch
block_bunch_iter_t end

pointer past the end of the transitions in the block_bunch array

bisim_gjkw::check_complexity::block_bunch_dnj_counter_t work_counter


block_bunch_const_iter_t block_bunch_begin
const block_bunch_iter_t *block_bunch_end

Public member functions

bool add_work_to_bottom_transns(enum bisim_gjkw::check_complexity::counter_type ctr, unsigned max_value, const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
block_bunch_slice_t(const block_bunch_iter_t &new_end, bunch_t *new_bunch, bool is_stable)
std::string debug_id() const
bool empty() const
bool is_stable() const
void make_stable()
void make_unstable()
block_t *source_block() const

compute the source block of the transitions in this slice