mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type Struct Reference

information about a block that needs to be refined More...

#include <liblts_bisim_gj_lazy_BLC.h>

Public Member Functions
	block_that_needs_refinement_type (block_type_lb &B, BLC_indicators_lb *a_large_splitter=nullptr)
	constructor
state_index	bottom_size (enum subblocks coroutine)
	calculate the size of the bottom states that are in subblock coroutine
template<class LTS_TYPE >
std::string	debug_id (const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &partitioner) const

Public Attributes
std::array< state_in_block_pointer_lb *, 4 >	start_bottom_states
	distribution of bottom states
std::array< std::vector< state_in_block_pointer_lb >, 3 >	potential_non_bottom_states
	potential non-bottom states
std::vector< state_in_block_pointer_lb >	potential_non_bottom_states_HitSmall
BLC_indicators_lb *	large_splitter
	large splitter

Detailed Description

information about a block that needs to be refined

Because we will refine multiple blocks at a time, we need to store the information about ReachAlw, AvoidSml, AvoidLrg, pot-ReachAlw and HitSmall elsewhere. These sets are constructed from the super-BLC set for all blocks in the super-BLC source at the same time.

Definition at line 732 of file liblts_bisim_gj_lazy_BLC.h.

Constructor & Destructor Documentation

block_that_needs_refinement_type()

mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::block_that_needs_refinement_type ( block_type_lb &  B, BLC_indicators_lb *  a_large_splitter = nullptr  )

inline

constructor

The constructor initializes AvoidSml to contain all bottom states (the default). The block's pointer to refinement_info is also initialized. Note that there is no destructor that would set refinement_info to nullptr again.

Definition at line 776 of file liblts_bisim_gj_lazy_BLC.h.

Member Function Documentation

bottom_size()

state_index mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::bottom_size ( enum subblocks  coroutine )

inline

calculate the size of the bottom states that are in subblock coroutine

Definition at line 788 of file liblts_bisim_gj_lazy_BLC.h.

debug_id()

template<class LTS_TYPE >

std::string mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::debug_id ( const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &  partitioner ) const

inline

Definition at line 798 of file liblts_bisim_gj_lazy_BLC.h.

Member Data Documentation

large_splitter

BLC_indicators_lb* mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::large_splitter

large splitter

The large splitter is needed because one cannot go through all its transitions before the coroutines start. Note that it may happen that large_splitter==nullptr, in particular if one splits under transitions that have just become constellation-inert, and during stabilizeB() if the super-BLC set is small.

Definition at line 762 of file liblts_bisim_gj_lazy_BLC.h.

potential_non_bottom_states

std::array<std::vector<state_in_block_pointer_lb>, 3> mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::potential_non_bottom_states

potential non-bottom states

These vectors contain non-bottom states that have been found when going through predecessors of a subblock.

Definition at line 753 of file liblts_bisim_gj_lazy_BLC.h.

potential_non_bottom_states_HitSmall

std::vector<state_in_block_pointer_lb> mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::potential_non_bottom_states_HitSmall

Definition at line 754 of file liblts_bisim_gj_lazy_BLC.h.

start_bottom_states

std::array<state_in_block_pointer_lb*, 4> mcrl2::lts::detail::bisimulation_gj_lazy_BLC::block_that_needs_refinement_type::start_bottom_states

distribution of bottom states

Bottom states are distributed over the subblocks by placing them in a specific slice of the bottom states of block bi: at the beginning there will be ReachAlw-bottom states, then AvoidLrg-bottom states and at the end AvoidSml-bottom states. The iterators indicate the place where every slice starts; at the same time, this is the end of the previous slice.

contains the beginning of the parts of the bottom states: start_bottom_states[ReachAlw] ... start_bottom_states[ReachAlw+1] contains the states that are guaranteed to be in ReachAlw start_bottom_states[AvoidSml] ... start_bottom_states[AvoidSml+1] contains the states that might remain in AvoidSml start_bottom_states[AvoidLrg] ... start_bottom_states[AvoidLrg+1] contains the states that are guaranteed to be in AvoidLrg

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