information about a block More...

#include <liblts_bisim_gj.h>

Classes
union	btc_R

union	constellation_or_first_unmarked_bottom_state

Public Member Functions
	block_type (state_in_block_pointer *beginning_of_states, constellation_index new_c)

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

Public Attributes
union mcrl2::lts::detail::bisimulation_gj::block_type::constellation_or_first_unmarked_bottom_state	c

state_in_block_pointer *	start_bottom_states

state_in_block_pointer *	start_non_bottom_states

state_in_block_pointer *	end_states
	pointer past the last state in the block

union mcrl2::lts::detail::bisimulation_gj::block_type::btc_R	block

check_complexity::block_gj_counter_t	work_counter

Detailed Description

information about a block

Definition at line 1056 of file liblts_bisim_gj.h.

Constructor & Destructor Documentation

◆ block_type()

mcrl2::lts::detail::bisimulation_gj::block_type::block_type	(	state_in_block_pointer *	beginning_of_states,
		constellation_index	new_c
	)

inline

Definition at line 1129 of file liblts_bisim_gj.h.

Member Function Documentation

◆ debug_id()

template<class LTS_TYPE >

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

inline

print a block identification for debugging

Definition at line 1140 of file liblts_bisim_gj.h.

Member Data Documentation

◆ block

union mcrl2::lts::detail::bisimulation_gj::block_type::btc_R mcrl2::lts::detail::bisimulation_gj::block_type::block

◆ c

union mcrl2::lts::detail::bisimulation_gj::block_type::constellation_or_first_unmarked_bottom_state mcrl2::lts::detail::bisimulation_gj::block_type::c

◆ end_states

state_in_block_pointer* mcrl2::lts::detail::bisimulation_gj::block_type::end_states

pointer past the last state in the block

Definition at line 1094 of file liblts_bisim_gj.h.

◆ start_bottom_states

state_in_block_pointer* mcrl2::lts::detail::bisimulation_gj::block_type::start_bottom_states

first state of the block in m_states_in_blocks States in [start_bottom_states, start_non_bottom_states) are bottom states in the block

Definition at line 1087 of file liblts_bisim_gj.h.

◆ start_non_bottom_states

state_in_block_pointer* mcrl2::lts::detail::bisimulation_gj::block_type::start_non_bottom_states

first non-bottom state of the block in m_states_in_blocks States in [start_non_bottom_states, end_states) are non-bottom states in the block. If m_branching==false, we have start_non_bottom_states==end_states.

Definition at line 1092 of file liblts_bisim_gj.h.

◆ work_counter

check_complexity::block_gj_counter_t mcrl2::lts::detail::bisimulation_gj::block_type::work_counter

mutable

Definition at line 1156 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

Classes

Public Member Functions

Public Attributes