mCRL2
|
#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_indicators > | to_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 | |
Definition at line 562 of file liblts_bisim_gj.h.
|
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.
|
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.
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.
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.