mCRL2
|
#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_pointer * | rt_non_bottom_states |
state_index | te_in_reduced_LTS |
used during finalizing for the state index in the reduced LTS | |
Definition at line 538 of file liblts_bisim_gj.h.
|
inline |
Definition at line 554 of file liblts_bisim_gj.h.
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.
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.