mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE > Class Template Reference

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, KeyHasherextra_kripke_states
 
std::unordered_map< label_type, state_typeaction_block_map
 
std::vector< state_typenoninert_out_per_state
 
std::vector< state_typeinert_out_per_state
 
std::vector< state_typenoninert_in_per_state
 
std::vector< state_typeinert_in_per_state
 
std::vector< state_typenoninert_out_per_block
 
std::vector< state_typeinert_out_per_block
 
std::vector< state_typestates_per_block
 
state_type nr_of_nonbottom_states
 

Detailed Description

template<class LTS_TYPE>
class mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >

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.


The documentation for this class was generated from the following files: