data structure to indicate the source states of super-BLC sets More...

#include <liblts_bisim_gj_lazy_BLC.h>

Public Member Functions
	BLC_source_type (state_in_block_pointer_lb new_start, state_in_block_pointer_lb new_end)

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

Public Attributes
state_in_block_pointer_lb *	start_BLC_source
	start of the slice in `m_states_in_blocks` containing source states

state_in_block_pointer_lb *	end_BLC_source
	end of the slice in `m_states_in_blocks` containing source states

simple_list< BLC_indicators_lb >	block_to_constellation
	list of super-BLC sets with transitions starting in these states

Detailed Description

data structure to indicate the source states of super-BLC sets

Definition at line 679 of file liblts_bisim_gj_lazy_BLC.h.

Constructor & Destructor Documentation

◆ BLC_source_type()

mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_source_type::BLC_source_type	(	state_in_block_pointer_lb *	new_start,
		state_in_block_pointer_lb *	new_end
	)

inline

Definition at line 690 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::BLC_source_type::debug_id ( const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > & partitioner ) const

inline

print a BLC-source identification for debugging

Definition at line 699 of file liblts_bisim_gj_lazy_BLC.h.

Member Data Documentation

◆ block_to_constellation

simple_list<BLC_indicators_lb> mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_source_type::block_to_constellation

list of super-BLC sets with transitions starting in these states

Definition at line 688 of file liblts_bisim_gj_lazy_BLC.h.

◆ end_BLC_source

state_in_block_pointer_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_source_type::end_BLC_source

end of the slice in m_states_in_blocks containing source states

Definition at line 685 of file liblts_bisim_gj_lazy_BLC.h.

◆ start_BLC_source

state_in_block_pointer_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_source_type::start_BLC_source

start of the slice in m_states_in_blocks containing source states

Definition at line 682 of file liblts_bisim_gj_lazy_BLC.h.

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

lts/include/mcrl2/lts/detail/liblts_bisim_gj_lazy_BLC.h

Public Member Functions

Public Attributes