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

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

#include <liblts_bisim_dnj.h>

Public Member Functions

template<class LTS_TYPE >
std::string debug_id_short (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a short transition identification for debugging
 
template<class LTS_TYPE >
std::string debug_id (const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const
 print a transition identification for debugging
 

Public Attributes

action_block_entryaction_block
 circular iterator to link the four transition arrays
 
state_info_entrysource
 source state of the transition
 
state_info_entrytarget
 target state of the transition
 
bisim_gjkw::check_complexity::trans_dnj_counter_t work_counter
 

Detailed Description

information about a transition sorted per target state

As I expect the transitions in this array to be moved least often, I store the information on source and target state in this entry. (It could be stored in any of the four arrays describing the transition; through the circular iterators, the information would be available anyway.)

Definition at line 1540 of file liblts_bisim_dnj.h.

Member Function Documentation

◆ debug_id()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::bisim_dnj::pred_entry::debug_id ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print a transition identification for debugging

Definition at line 1563 of file liblts_bisim_dnj.h.

◆ debug_id_short()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::bisim_dnj::pred_entry::debug_id_short ( const bisim_partitioner_dnj< LTS_TYPE > &  partitioner) const
inline

print a short transition identification for debugging

Definition at line 1554 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ action_block

action_block_entry* mcrl2::lts::detail::bisim_dnj::pred_entry::action_block

circular iterator to link the four transition arrays

Definition at line 1544 of file liblts_bisim_dnj.h.

◆ source

state_info_entry* mcrl2::lts::detail::bisim_dnj::pred_entry::source

source state of the transition

Definition at line 1547 of file liblts_bisim_dnj.h.

◆ target

state_info_entry* mcrl2::lts::detail::bisim_dnj::pred_entry::target

target state of the transition

Definition at line 1550 of file liblts_bisim_dnj.h.

◆ work_counter

bisim_gjkw::check_complexity::trans_dnj_counter_t mcrl2::lts::detail::bisim_dnj::pred_entry::work_counter
mutable

Definition at line 1580 of file liblts_bisim_dnj.h.


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