mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
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
 
bool has_marked_transitions () const
 
void make_stable ()
 
void make_unstable ()
 
bool operator== (const BLC_indicators &other) const
 
bool operator!= (const BLC_indicators &other) const
 
template<class LTS_TYPE >
std::string debug_id (const bisim_partitioner_gj< LTS_TYPE > &partitioner, const block_type *from_block=nullptr) 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 351 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 362 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_type *  from_block = nullptr 
) const
inline

print a B_to_C slice identification for debugging

This function is only available if compiled in Debug mode.

Definition at line 414 of file liblts_bisim_gj.h.

◆ has_marked_transitions()

bool mcrl2::lts::detail::bisimulation_gj::BLC_indicators::has_marked_transitions ( ) const
inline

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

Definition at line 380 of file liblts_bisim_gj.h.

◆ is_stable()

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

Definition at line 370 of file liblts_bisim_gj.h.

◆ make_stable()

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

Definition at line 389 of file liblts_bisim_gj.h.

◆ make_unstable()

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

Definition at line 394 of file liblts_bisim_gj.h.

◆ operator!=()

bool mcrl2::lts::detail::bisimulation_gj::BLC_indicators::operator!= ( const BLC_indicators &  other) const
inline

Definition at line 406 of file liblts_bisim_gj.h.

◆ operator==()

bool mcrl2::lts::detail::bisimulation_gj::BLC_indicators::operator== ( const BLC_indicators &  other) const
inline

Definition at line 399 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 360 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 359 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 353 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 468 of file liblts_bisim_gj.h.

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