information about a state More...

#include <liblts_bisim_gj_lazy_BLC.h>

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

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

Public Attributes
block_type_lb *	block = null_block_lb
	block of the state

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

outgoing_transitions_it_lb	start_outgoing_transitions
	first outgoing transition

state_in_block_pointer_lb *	ref_states_in_blocks = nullptr
	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
	counter used during `four_way_splitB()`

check_complexity::state_gj_counter_t	work_counter

Detailed Description

information about a state

Definition at line 325 of file liblts_bisim_gj_lazy_BLC.h.

Member Function Documentation

◆ debug_id()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj_lazy_BLC::state_type_gj_lb::debug_id ( const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > & partitioner ) const

inline

print a state identification for debugging

Definition at line 355 of file liblts_bisim_gj_lazy_BLC.h.

◆ debug_id_short()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj_lazy_BLC::state_type_gj_lb::debug_id_short ( const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > & partitioner ) const

inline

print a short state identification for debugging

Definition at line 346 of file liblts_bisim_gj_lazy_BLC.h.

Member Data Documentation

◆ block

block_type_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::state_type_gj_lb::block = null_block_lb

block of the state

Definition at line 328 of file liblts_bisim_gj_lazy_BLC.h.

◆ counter

transition_index mcrl2::lts::detail::bisimulation_gj_lazy_BLC::state_type_gj_lb::counter =undefined

counter used during four_way_splitB()

If this counter is set to undefined (0), the state is considered to be not yet visited. A visited state has a positive counter, consisting of marked( subblock it is expected to move to ) + number of outgoing block-inert transitions that are not yet visited.

Definition at line 342 of file liblts_bisim_gj_lazy_BLC.h.