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

#include <liblts_bisim_gj.h>

Public Member Functions

 start_non_bottom_states_or_state_in_reduced_LTS (state_in_block_pointer *s)
 

Public Attributes

state_in_block_pointerrt_non_bottom_states
 
state_index te_in_reduced_LTS
 used during finalizing for the state index in the reduced LTS
 

Detailed Description

Definition at line 538 of file liblts_bisim_gj.h.

Constructor & Destructor Documentation

◆ start_non_bottom_states_or_state_in_reduced_LTS()

mcrl2::lts::detail::bisimulation_gj::block_type::start_non_bottom_states_or_state_in_reduced_LTS::start_non_bottom_states_or_state_in_reduced_LTS ( state_in_block_pointer s)
inline

Definition at line 554 of file liblts_bisim_gj.h.

Member Data Documentation

◆ rt_non_bottom_states

state_in_block_pointer* mcrl2::lts::detail::bisimulation_gj::block_type::start_non_bottom_states_or_state_in_reduced_LTS::rt_non_bottom_states

first non-bottom state of the block in m_states_in_blocks States in [sta.rt_non_bottom_states, end_states) are non-bottom states in the block.

If m_branching==false, we have sta.rt_non_bottom_states==end_states.

Definition at line 545 of file liblts_bisim_gj.h.

◆ te_in_reduced_LTS

state_index mcrl2::lts::detail::bisimulation_gj::block_type::start_non_bottom_states_or_state_in_reduced_LTS::te_in_reduced_LTS

used during finalizing for the state index in the reduced LTS

After partition refinement has finished, the boundary between bottom and non-bottom states is no longer needed. Therefore, we use the same space to store a block number instead. This block number is the same as the state number in the reduced LTS.

Definition at line 552 of file liblts_bisim_gj.h.


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