mcrl2::lts::detail::bisim_dnj::succ_entry Class Reference

information about a transition sorted per source state More...

#include <liblts_bisim_dnj.h>

Public Member Functions
succ_entry *	out_slice_begin (ONLY_IF_DEBUG(const fixed_vector< succ_entry > &succ))
	find the beginning of the out-slice
bunch_t *	bunch () const
	find the bunch of the transition

Static Public Member Functions
template<class LTS_TYPE >
static void	add_work_to_out_slice (const bisim_partitioner_dnj< LTS_TYPE > &partitioner, const succ_entry *out_slice_begin, enum check_complexity::counter_type ctr, unsigned max_value)
	assign work to the transitions in an out-slice (i.e. the transitions from one state in a specific bunch)

Public Attributes
block_bunch_entry *	block_bunch
	circular iterator to link the four transition arrays
succ_entry *	begin_or_before_end
	pointer to delimit the slice of transitions in the same bunch

Detailed Description

information about a transition sorted per source state

Definition at line 778 of file liblts_bisim_dnj.h.

Member Data Documentation

begin_or_before_end

succ_entry* mcrl2::lts::detail::bisim_dnj::succ_entry::begin_or_before_end

pointer to delimit the slice of transitions in the same bunch

For most transitions, this pointer points to the first transition that starts in the same state and belongs to the same bunch. But if this transition is the first such transition, the pointer points to the last such transition (not one past the last, like otherwise in C and C++).

For inert transitions, the value is nullptr.

Definition at line 792 of file liblts_bisim_dnj.h.

block_bunch

block_bunch_entry* mcrl2::lts::detail::bisim_dnj::succ_entry::block_bunch

circular iterator to link the four transition arrays

Definition at line 782 of file liblts_bisim_dnj.h.

---

The documentation for this class was generated from the following file:

• lts/include/mcrl2/lts/detail/liblts_bisim_dnj.h