mcrl2::lts::detail::bisimulation_gj::BLC_indicators Struct Reference

#include <liblts_bisim_gj.h>

Public Member Functions
	BLC_indicators (BLC_list_iterator start, BLC_list_iterator end, bool is_stable)
bool	is_stable () const
void	make_stable ()
void	make_unstable ()
template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_gj< LTS_TYPE > &partitioner, const block_index from_block=null_block) const
	print a B_to_C slice identification for debugging

Public Attributes
BLC_list_iterator	start_same_BLC
BLC_list_iterator_or_null	start_marked_BLC
BLC_list_iterator	end_same_BLC
check_complexity::BLC_gj_counter_t	work_counter

Detailed Description

The following type gives the start and end indications of the transitions for the same block, label and constellation in the array m_BLC_transitions.

Definition at line 920 of file liblts_bisim_gj.h.

Constructor & Destructor Documentation

BLC_indicators()

mcrl2::lts::detail::bisimulation_gj::BLC_indicators::BLC_indicators ( BLC_list_iterator  start, BLC_list_iterator  end, bool  is_stable  )

inline

Definition at line 931 of file liblts_bisim_gj.h.

Member Function Documentation

debug_id()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj::BLC_indicators::debug_id ( const bisim_partitioner_gj< LTS_TYPE > &  partitioner, const block_index  from_block = null_block  ) const

inline

print a B_to_C slice identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 960 of file liblts_bisim_gj.h.

is_stable()

bool mcrl2::lts::detail::bisimulation_gj::BLC_indicators::is_stable ( ) const

inline

Definition at line 939 of file liblts_bisim_gj.h.

make_stable()

void mcrl2::lts::detail::bisimulation_gj::BLC_indicators::make_stable ( )

inline

Definition at line 947 of file liblts_bisim_gj.h.

make_unstable()

void mcrl2::lts::detail::bisimulation_gj::BLC_indicators::make_unstable ( )

inline

Definition at line 952 of file liblts_bisim_gj.h.

Member Data Documentation

end_same_BLC

BLC_list_iterator mcrl2::lts::detail::bisimulation_gj::BLC_indicators::end_same_BLC

Definition at line 929 of file liblts_bisim_gj.h.

start_marked_BLC

BLC_list_iterator_or_null mcrl2::lts::detail::bisimulation_gj::BLC_indicators::start_marked_BLC

Definition at line 928 of file liblts_bisim_gj.h.

start_same_BLC

BLC_list_iterator mcrl2::lts::detail::bisimulation_gj::BLC_indicators::start_same_BLC

Definition at line 922 of file liblts_bisim_gj.h.

work_counter

check_complexity::BLC_gj_counter_t mcrl2::lts::detail::bisimulation_gj::BLC_indicators::work_counter

mutable

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