mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE > Class Template Reference

#include <liblts_ready_sim.h>

Inheritance diagram for mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >:
mcrl2::lts::detail::sim_partitioner< LTS_TYPE >

Public Member Functions

 ready_sim_partitioner (LTS_TYPE &l)
 
void partitioning_algorithm () override
 
 ~ready_sim_partitioner ()
 
- Public Member Functions inherited from mcrl2::lts::detail::sim_partitioner< LTS_TYPE >
 sim_partitioner (LTS_TYPE &l)
 
virtual ~sim_partitioner ()
 
virtual void partitioning_algorithm ()
 
std::vector< mcrl2::lts::transition > get_transitions () const
 
std::size_t num_eq_classes () const
 
std::size_t get_eq_class (std::size_t s) const
 
bool in_preorder (std::size_t s, std::size_t t) const
 
bool in_same_class (std::size_t s, std::size_t t) const
 

Private Member Functions

void ready2sim_reduction ()
 
void refinei ()
 
void updatei ()
 
std::string print_structure (hash_table2 *struc)
 

Private Attributes

hash_table2 * exists2
 
hash_table2 * forall2
 

Additional Inherited Members

- Protected Member Functions inherited from mcrl2::lts::detail::sim_partitioner< LTS_TYPE >
void partitioning_algorithmG ()
 
void initialise_datastructures ()
 
void refine (bool &change)
 
void update ()
 
void touch (std::size_t a, std::size_t alpha)
 
void untouch (std::size_t alpha)
 
void reverse_topological_sort (std::vector< std::size_t > &Sort)
 
void dfs_visit (std::size_t u, std::vector< bool > &visited, std::vector< std::size_t > &Sort)
 
void initialise_Sigma (std::size_t gamma, std::size_t l)
 
void initialise_Pi (std::size_t gamma, std::size_t l)
 
void filter (std::size_t S, std::vector< std::vector< bool > > &R, bool B)
 
void cleanup (std::size_t alpha, std::size_t beta)
 
void initialise_pre_EA ()
 
void induce_P_on_Pi ()
 
std::string print_Sigma_P ()
 
std::string print_Pi_Q ()
 
std::string print_Sigma ()
 
std::string print_Pi ()
 
std::string print_relation (std::size_t s, std::vector< std::vector< bool > > &R)
 
std::string print_block (std::size_t b)
 
std::string print_structure (hash_table3 *struc)
 
std::string print_reverse_topological_sort (const std::vector< std::size_t > &Sort)
 
- Protected Attributes inherited from mcrl2::lts::detail::sim_partitioner< LTS_TYPE >
LTS_TYPE & aut
 
mcrl2::lts::outgoing_transitions_per_state_action_t trans_index
 
std::size_t s_Sigma = 0UL
 
std::size_t s_Pi = 0UL
 
std::vector< bool > state_touched
 
std::vector< bool > block_touched
 
std::vector< state_bucket > state_buckets
 
std::vector< std::size_t > block_Pi
 
std::vector< std::size_t > parent
 
std::vector< std::vector< std::size_t > > children
 
std::vector< ptrdiff_t > contents_t
 
std::vector< ptrdiff_t > contents_u
 
std::vector< std::vector< bool > > stable
 
hash_table3 * exists
 
hash_table3 * forall
 
std::vector< std::vector< std::size_t > > pre_exists
 
std::vector< std::vector< std::size_t > > pre_forall
 
hash_table3 * match
 
std::vector< std::vector< bool > > P
 
std::vector< std::vector< bool > > Q
 
std::vector< std::size_t > touched_blocks
 
std::vector< std::size_t > contents
 

Detailed Description

template<class LTS_TYPE>
class mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >

Definition at line 21 of file liblts_ready_sim.h.

Constructor & Destructor Documentation

◆ ready_sim_partitioner()

template<class LTS_TYPE >
mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::ready_sim_partitioner ( LTS_TYPE &  l)
inline

Definition at line 24 of file liblts_ready_sim.h.

◆ ~ready_sim_partitioner()

template<class LTS_TYPE >
mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::~ready_sim_partitioner

Destroys this partitioner.

Definition at line 292 of file liblts_ready_sim.h.

Member Function Documentation

◆ partitioning_algorithm()

template<class LTS_TYPE >
void mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::partitioning_algorithm
overridevirtual

Computes the ready-simulation equivalence classes and preorder relations of the LTS

Reimplemented from mcrl2::lts::detail::sim_partitioner< LTS_TYPE >.

Definition at line 121 of file liblts_ready_sim.h.

◆ print_structure()

template<class LTS_TYPE >
std::string mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::print_structure ( hash_table2 *  struc)
private

Definition at line 277 of file liblts_ready_sim.h.

◆ ready2sim_reduction()

template<class LTS_TYPE >
void mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::ready2sim_reduction
private

Drives the partition pair <Universal,Id> into appropriate ready partition-pair for furhter input into GCPP.

Precondition
: true

Definition at line 107 of file liblts_ready_sim.h.

◆ refinei()

template<class LTS_TYPE >
void mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::refinei
private

Splits Universal partition into classes alpha where either { N } A<-l- alpha or not { N } <-l- alpha for some L

Precondition
: initialise_datastructures called.

Definition at line 132 of file liblts_ready_sim.h.

◆ updatei()

template<class LTS_TYPE >
void mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::updatei
private

Definition at line 202 of file liblts_ready_sim.h.

Member Data Documentation

◆ exists2

template<class LTS_TYPE >
hash_table2* mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::exists2
private

Definition at line 39 of file liblts_ready_sim.h.

◆ forall2

template<class LTS_TYPE >
hash_table2* mcrl2::lts::detail::ready_sim_partitioner< LTS_TYPE >::forall2
private

Definition at line 40 of file liblts_ready_sim.h.

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