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>


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

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