mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb Struct Reference

#include <liblts_bisim_gj_lazy_BLC.h>

Public Member Functions
	BLC_indicators_lb (BLC_list_iterator start, BLC_list_iterator end, bool is_stable)
bool	is_stable () const
bool	has_marked_transitions () const
void	make_stable ()
void	make_unstable ()
bool	operator== (const BLC_indicators_lb &other) const
bool	operator!= (const BLC_indicators_lb &other) const
template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &partitioner) const
	print a B_to_C slice identification for debugging

Public Attributes
BLC_list_iterator	start_same_BLC
	iterator pointing to the first transition
BLC_list_iterator_or_null	start_marked_BLC
	iterator pointing to the first marked transition
BLC_list_iterator	end_same_BLC
	iterator pointing past the last transition
bool	starts_in_small_subblock = true
	is true if it is known that the super-BLC set transitions start in a small subblock
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 superblock, label and constellation in the array m_BLC_transitions.

Definition at line 368 of file liblts_bisim_gj_lazy_BLC.h.

Constructor & Destructor Documentation

BLC_indicators_lb()

mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::BLC_indicators_lb ( BLC_list_iterator  start, BLC_list_iterator  end, bool  is_stable  )

inline

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

inline

print a B_to_C slice identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 453 of file liblts_bisim_gj_lazy_BLC.h.

has_marked_transitions()

bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::has_marked_transitions ( ) const

inline

This function returns true iff the BLC set contains at least one marked transition.

Definition at line 419 of file liblts_bisim_gj_lazy_BLC.h.

is_stable()

bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::is_stable ( ) const

inline

Definition at line 409 of file liblts_bisim_gj_lazy_BLC.h.

make_stable()

void mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::make_stable ( )

inline

Definition at line 428 of file liblts_bisim_gj_lazy_BLC.h.

make_unstable()

void mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::make_unstable ( )

inline

Definition at line 433 of file liblts_bisim_gj_lazy_BLC.h.

operator!=()

bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::operator!= ( const BLC_indicators_lb &  other ) const

inline

Definition at line 445 of file liblts_bisim_gj_lazy_BLC.h.

operator==()

bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::operator== ( const BLC_indicators_lb &  other ) const

inline

Definition at line 438 of file liblts_bisim_gj_lazy_BLC.h.

Member Data Documentation

end_same_BLC

BLC_list_iterator mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::end_same_BLC

iterator pointing past the last transition

Definition at line 382 of file liblts_bisim_gj_lazy_BLC.h.

start_marked_BLC

BLC_list_iterator_or_null mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::start_marked_BLC

iterator pointing to the first marked transition

If the BLC indicator is regarded as stable, this pointer is nullptr. Otherwise, marked transitions are used during stabilizeB() to indicate transitions that can be visited before the coroutines in four_way_splitB() start. Typically, this are the transitions starting in new bottom states.

Definition at line 379 of file liblts_bisim_gj_lazy_BLC.h.

start_same_BLC

BLC_list_iterator mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::start_same_BLC

iterator pointing to the first transition

Definition at line 371 of file liblts_bisim_gj_lazy_BLC.h.

starts_in_small_subblock

bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::starts_in_small_subblock = true

is true if it is known that the super-BLC set transitions start in a small subblock

(Perhaps memory could be saved by adding a second boolean is_stable and suppressing end_same_BLC. For stable super-BLC sets, the end of the transitions is the same as end_marked_BLC. Loops going through all transitions in a (possibly unstable) super-BLC set would have to test this:

tr < start_marked_BLC || (!is_stable &&
                          tr < m_BLC_transitions.data_end() &&
                          source is in blc_src &&
                          action label agrees &&
                          target is in to_constln)

.)

Definition at line 398 of file liblts_bisim_gj_lazy_BLC.h.

work_counter

check_complexity::BLC_gj_counter_t mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::work_counter

mutable

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