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 bisimulationreduced 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 1655 of file liblts_bisim_gjkw.h.