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

#include <liblts_bisim_dnj.h>

Public Member Functions
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))
	find the beginning of the action_block-slice

Public Attributes
succ_entry *	succ
	circular iterator to link the four transition arrays

action_block_entry *	begin_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 889 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 912 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 908 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 897 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