mCRL2
|
helps with initialising the refinable partition data structure More...
#include <liblts_bisim_gjkw.h>
Classes | |
class | Key |
class | KeyHasher |
Public Member Functions | |
bisim_partitioner_gjkw_initialise_helper (LTS_TYPE &l, bool branching, bool preserve_divergence) | |
constructor of the helper class | |
void | init_transitions (part_state_t &part_st, part_trans_t &part_tr, bool branching, bool preserve_divergence) |
initialise the state in part_st and the transitions in part_tr | |
void | replace_transition_system (const part_state_t &part_st, ONLY_IF_DEBUG(bool branching,) bool preserve_divergence) |
Replaces the transition relation of the current LTS by the transitions of the bisimulation-reduced transition system. | |
state_type | get_nr_of_states () const |
provides the number of states in the Kripke structure | |
trans_type | get_nr_of_transitions () const |
provides the number of transitions in the Kripke structure | |
Private Attributes | |
LTS_TYPE & | aut |
state_type | nr_of_states |
const state_type | orig_nr_of_states |
trans_type | nr_of_transitions |
std::unordered_map< Key, state_type, KeyHasher > | extra_kripke_states |
std::unordered_map< label_type, state_type > | action_block_map |
std::vector< state_type > | noninert_out_per_state |
std::vector< state_type > | inert_out_per_state |
std::vector< state_type > | noninert_in_per_state |
std::vector< state_type > | inert_in_per_state |
std::vector< state_type > | noninert_out_per_block |
std::vector< state_type > | inert_out_per_block |
std::vector< state_type > | states_per_block |
state_type | nr_of_nonbottom_states |
helps with initialising the refinable partition data structure
Before allocating memory for the refinable partition data structure, the number of states and transitions (including extra states generated by the translation from labelled transition system to Kripke structure) has to be known. This class serves to calculate these numbers.
The helper class also initialises the variables used by check_complexity to find the number of states and transitions in time complexity checks.
Definition at line 1676 of file liblts_bisim_gjkw.h.