- Generated by
1.9.7
|
mCRL2
|
information about a block More...
#include <liblts_bisim_gj_lazy_BLC.h>
Classes | |
| union | start_non_bottom_states_or_state_in_reduced_LTS |
Public Member Functions | |
| block_type_lb (const block_type_lb &other) | |
| copy constructor. Required by MSCV. | |
| block_type_lb (state_in_block_pointer_lb *start_bottom, state_in_block_pointer_lb *start_non_bottom, state_in_block_pointer_lb *end, constellation_type_lb &new_c, BLC_source_type &new_bbs, char new_small_subblock_counter) | |
| constructor | |
| template<class LTS_TYPE > | |
| std::string | debug_id_short (const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &partitioner) const |
| print a short block identification for debugging | |
| template<class LTS_TYPE > | |
| std::string | debug_id (const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &partitioner) const |
| print a block identification for debugging | |
Public Attributes | |
| constellation_type_lb * | constellation |
| constellation that the block is in | |
| state_in_block_pointer_lb * | start_bottom_states |
| union mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::start_non_bottom_states_or_state_in_reduced_LTS | sta |
| state_in_block_pointer_lb * | end_states |
| pointer past the last state in the block | |
| BLC_source_type * | block_BLC_source |
| superblock for BLC sets that this block is part of | |
| state_index | refinement_info = null_state |
| pointer to refinement data structure | |
| char | contains_new_bottom_states = false |
| a boolean that is true iff the block contains new bottom states | |
| char | small_subblock_counter |
| a boolean that is true iff the block is a small subblock | |
| check_complexity::block_gj_counter_t | work_counter |
information about a block
A block is mainly described through the set of states it contains. For this we have fixed_vector<state_in_block_pointer_lb> m_states_in_blocks, where states are kept grouped by block. The fields start_bottom_states, sta.rt_non_bottom_states and end_states are pointers into that array.
Some fields get a second life (to save memory) during initialisation or during finalising; that is the purpose of the unions.
A block should be trivially destructible because we want it to be allocated using the pool allocator simple_list<BLC_indicators_lb>::get_pool(). This is why there are no iterator fields.
Definition at line 564 of file liblts_bisim_gj_lazy_BLC.h.
|
inline |
copy constructor. Required by MSCV.
Definition at line 613 of file liblts_bisim_gj_lazy_BLC.h.
|
inline |
constructor
Definition at line 637 of file liblts_bisim_gj_lazy_BLC.h.
|
inline |
print a block identification for debugging
Definition at line 666 of file liblts_bisim_gj_lazy_BLC.h.
|
inline |
print a short block identification for debugging
Definition at line 653 of file liblts_bisim_gj_lazy_BLC.h.
| BLC_source_type* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::block_BLC_source |
superblock for BLC sets that this block is part of
When a block is split, this superblock is not split, so the BLC sets do not need to be split.
Definition at line 602 of file liblts_bisim_gj_lazy_BLC.h.
| constellation_type_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::constellation |
constellation that the block is in
Definition at line 567 of file liblts_bisim_gj_lazy_BLC.h.
| char mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::contains_new_bottom_states = false |
a boolean that is true iff the block contains new bottom states
If a block contains new bottom states, it will be ignored until stabilizeB() handles all blocks with new bottom states. Such a block must also be added to the list m_blocks_with_new_bottom_states.
Definition at line 628 of file liblts_bisim_gj_lazy_BLC.h.
| state_in_block_pointer_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::end_states |
pointer past the last state in the block
Definition at line 597 of file liblts_bisim_gj_lazy_BLC.h.
| state_index mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::refinement_info = null_state |
pointer to refinement data structure
When a block needs refinement, information about how to initialize the states is stored in the refinement data structure. The pointer mostly points to an element of the list of blocks that need refinement. When the block does not need to be refined, this value is nullptr.
Definition at line 610 of file liblts_bisim_gj_lazy_BLC.h.
| char mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::small_subblock_counter |
a boolean that is true iff the block is a small subblock
If a block has become a small subblock of an earlier split, it is allowed to go through its states and transitions once. This is exploited to avoid the costly handling of NewBotSt.
Definition at line 634 of file liblts_bisim_gj_lazy_BLC.h.
| union mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::start_non_bottom_states_or_state_in_reduced_LTS mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::sta |
| state_in_block_pointer_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_type_lb::start_bottom_states |
first state of the block in m_states_in_blocks States in [start_bottom_states, sta.rt_non_bottom_states) are bottom states in the block
Definition at line 572 of file liblts_bisim_gj_lazy_BLC.h.
|
mutable |
Definition at line 674 of file liblts_bisim_gj_lazy_BLC.h.
1.9.7