mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisimulation_gj::block_type::btc_R Union Reference

#include <liblts_bisim_gj.h>

Public Member Functions

 btc_R ()
 constructor
 

Static Public Member Functions

static bool if_R_is_nullptr_then_to_constellation_is_empty_list ()
 indicates whether the default values of the union members agree
 

Public Attributes

linked_list< BLC_indicatorsto_constellation
 list of descriptors of all BLC sets that contain transitions starting in the block
 
std::vector< state_in_block_pointer > * R
 used during initialisation for a pointer to a vector of marked states
 

Detailed Description

Definition at line 562 of file liblts_bisim_gj.h.

Constructor & Destructor Documentation

◆ btc_R()

mcrl2::lts::detail::bisimulation_gj::block_type::btc_R::btc_R ( )
inline

constructor

Note: if_R_is_nullptr_then_to_constellation_is_empty_list() depends on the fact that the constructor creates the variant field R.

Definition at line 592 of file liblts_bisim_gj.h.

Member Function Documentation

◆ if_R_is_nullptr_then_to_constellation_is_empty_list()

static bool mcrl2::lts::detail::bisimulation_gj::block_type::btc_R::if_R_is_nullptr_then_to_constellation_is_empty_list ( )
inlinestatic

indicates whether the default values of the union members agree

If this function returns false, it is necesssary to explicitly construct every block.to_constellation list during initialisation. Otherwise, it would be enough to just keep R as nullptr. The function is not a constexpr but it is optimized away completely (at least by my compiler, DNJ).

Definition at line 602 of file liblts_bisim_gj.h.

Member Data Documentation

◆ R

std::vector<state_in_block_pointer>* mcrl2::lts::detail::bisimulation_gj::block_type::btc_R::R

used during initialisation for a pointer to a vector of marked states

During initialisation (when there is only one constellation) the same space as to_constellation is actually used for something else.

In the initial refinement in create_initial_partition(), blocks are split according to which action labels they can (inertly) reach. If R!=nullptr, this block has been registered as a block where some state has a transition with the current label under investigation. Such states, if they are non-bottom, are inserted into the vector *R. If R!=nullptr, the block has also been inserted into the vector blocks_that_need_refinement (a local variable of create_initial_partition()).

Definition at line 587 of file liblts_bisim_gj.h.

◆ to_constellation

linked_list<BLC_indicators> mcrl2::lts::detail::bisimulation_gj::block_type::btc_R::to_constellation

list of descriptors of all BLC sets that contain transitions starting in the block

If the block has inert transitions, they are always in the first element of the list.

During the main/co-split phase, a main splitter immediately follows the corresponding co-splitter in the list. During stabilize(), BLC sets that are regarded as unstable are near the end of the list.

Definition at line 572 of file liblts_bisim_gj.h.


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