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_entry *	action_block = nullptr
	circular iterator to link the four transition arrays

state_info_entry *	source = nullptr
	source state of the transition

state_info_entry *	target = nullptr
	target state of the transition

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 856 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 879 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 870 of file liblts_bisim_dnj.h.

Member Data Documentation

◆ action_block

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

circular iterator to link the four transition arrays

Definition at line 860 of file liblts_bisim_dnj.h.

◆ source

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

source state of the transition

Definition at line 863 of file liblts_bisim_dnj.h.

◆ target

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

target state of the transition

Definition at line 866 of file liblts_bisim_dnj.h.

◆ work_counter

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

mutable

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

Public Member Functions

Public Attributes