mCRL2
Loading...
Searching...
No Matches
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_entryout_slice_begin (ONLY_IF_DEBUG(const bisim_gjkw::fixed_vector< succ_entry > &succ))
 find the beginning of the out-slice
 
bunch_tbunch () 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 bisim_gjkw::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_entryblock_bunch
 circular iterator to link the four transition arrays
 
succ_entrybegin_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 1476 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 1490 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 1480 of file liblts_bisim_dnj.h.


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