mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_dnj::action_block_entry Class Reference

information about a transition sorted per (action, target block) pair More...

#include <liblts_bisim_dnj.h>

Public Member Functions

action_block_entryaction_block_slice_begin (ONLY_IF_DEBUG(const action_block_entry *const action_block_begin, const action_block_entry *const action_block_orig_inert_begin))
 find the beginning of the action_block-slice
 

Public Attributes

succ_entrysucc
 circular iterator to link the four transition arrays
 
action_block_entrybegin_or_before_end
 pointer to delimit the slice of transitions in the same (action, block) pair
 

Detailed Description

information about a transition sorted per (action, target block) pair

Definition at line 1587 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ action_block_slice_begin()

action_block_entry * mcrl2::lts::detail::bisim_dnj::action_block_entry::action_block_slice_begin ( ONLY_IF_DEBUG(const action_block_entry *const action_block_begin, const action_block_entry *const action_block_orig_inert_begin)  )
inline

find the beginning of the action_block-slice

Definition at line 1610 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ begin_or_before_end

action_block_entry* mcrl2::lts::detail::bisim_dnj::action_block_entry::begin_or_before_end

pointer to delimit the slice of transitions in the same (action, block) pair

For most transitions, this pointer points to the first transition that has the same action and goes to the same block. 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 and dummy entries, the value is nullptr.

Definition at line 1606 of file liblts_bisim_dnj.h.

◆ succ

succ_entry* mcrl2::lts::detail::bisim_dnj::action_block_entry::succ

circular iterator to link the four transition arrays

This iterator can be nullptr because we need to insert dummy elements between two action_block-slices during initialisation, to make it easier for first_move_transition_to_new_action_block() to detect whether two action_block-slices belong to the same action or not.

Definition at line 1595 of file liblts_bisim_dnj.h.


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