information about a state More...

#include <liblts_bisim_gj.h>

Public Member Functions
template<class LTS_TYPE >
std::string	debug_id_short (const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
	print a short state identification for debugging

template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_gj< LTS_TYPE > &partitioner) const
	print a state identification for debugging

Public Attributes
block_index	block =0
	block of the state

std::vector< transition >::iterator	start_incoming_transitions
	first incoming transition

outgoing_transitions_it	start_outgoing_transitions
	first outgoing transition

state_in_block_pointer *	ref_states_in_blocks
	pointer to the corresponding entry in m_states_in_blocks

transition_index	no_of_outgoing_block_inert_transitions =0
	number of outgoing block-inert transitions

transition_index	counter =undefined

check_complexity::state_gj_counter_t	work_counter

Detailed Description

information about a state

Definition at line 876 of file liblts_bisim_gj.h.

Member Function Documentation

◆ debug_id()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj::state_type_gj::debug_id ( const bisim_partitioner_gj< LTS_TYPE > & partitioner ) const

inline

print a state identification for debugging

Definition at line 909 of file liblts_bisim_gj.h.

◆ debug_id_short()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj::state_type_gj::debug_id_short ( const bisim_partitioner_gj< LTS_TYPE > & partitioner ) const

inline

print a short state identification for debugging

Definition at line 900 of file liblts_bisim_gj.h.

Member Data Documentation

◆ block

block_index mcrl2::lts::detail::bisimulation_gj::state_type_gj::block =0

block of the state

Definition at line 879 of file liblts_bisim_gj.h.

◆ counter

transition_index mcrl2::lts::detail::bisimulation_gj::state_type_gj::counter =undefined

counter used during splitting If this counter is set to undefined (-1), it is considered to be not yet visited. If this counter is set to Rmarked (-2), the state is considered to be in the R-subblock. If this counter is a positive number, it is the number of outgoing block-inert transitions that have not yet been handled. If this counter is 0, the state is considered to be in the U-subblock.

Definition at line 896 of file liblts_bisim_gj.h.

◆ no_of_outgoing_block_inert_transitions

transition_index mcrl2::lts::detail::bisimulation_gj::state_type_gj::no_of_outgoing_block_inert_transitions =0

number of outgoing block-inert transitions

Definition at line 887 of file liblts_bisim_gj.h.

◆ ref_states_in_blocks

state_in_block_pointer* mcrl2::lts::detail::bisimulation_gj::state_type_gj::ref_states_in_blocks

pointer to the corresponding entry in m_states_in_blocks

Definition at line 885 of file liblts_bisim_gj.h.

◆ start_incoming_transitions

std::vector<transition>::iterator mcrl2::lts::detail::bisimulation_gj::state_type_gj::start_incoming_transitions

first incoming transition

Definition at line 881 of file liblts_bisim_gj.h.

◆ start_outgoing_transitions

outgoing_transitions_it mcrl2::lts::detail::bisimulation_gj::state_type_gj::start_outgoing_transitions

first outgoing transition

Definition at line 883 of file liblts_bisim_gj.h.

◆ work_counter

check_complexity::state_gj_counter_t mcrl2::lts::detail::bisimulation_gj::state_type_gj::work_counter

mutable

Definition at line 914 of file liblts_bisim_gj.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_gj.h

Public Member Functions

Public Attributes