mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser Struct Reference

#include <parelm.h>

Inheritance diagram for mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser:
mcrl2::pbes_system::pbes_expression_traverser< parelm_dependency_traverser > mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >

Public Types

using super = pbes_expression_traverser< parelm_dependency_traverser >
 
- Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
using super = Traverser< Derived >
 

Public Member Functions

 parelm_dependency_traverser (graph &G_, const std::map< core::identifier_string, std::size_t > &propvar_offsets_)
 
void enter (const forall &x)
 
void leave (const forall &x)
 
void enter (const exists &x)
 
void leave (const exists &x)
 
void apply (const propositional_variable_instantiation &x)
 
void apply (const pbes_equation &eqn)
 
- Public Member Functions inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
void apply (const pbes_system::pbes_equation &x)
 
void apply (const pbes_system::pbes &x)
 
void apply (const pbes_system::propositional_variable_instantiation &x)
 
void apply (const pbes_system::not_ &x)
 
void apply (const pbes_system::and_ &x)
 
void apply (const pbes_system::or_ &x)
 
void apply (const pbes_system::imp &x)
 
void apply (const pbes_system::forall &x)
 
void apply (const pbes_system::exists &x)
 
void apply (const pbes_system::pbes_expression &x)
 

Public Attributes

graph & G
 
const std::map< core::identifier_string, std::size_t > & propvar_offsets
 
core::identifier_string X
 
data::variable_list Xparams
 
std::multiset< data::variable > bound_variables
 

Detailed Description

Definition at line 57 of file parelm.h.

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ parelm_dependency_traverser()

mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::parelm_dependency_traverser ( graph &  G_,
const std::map< core::identifier_string, std::size_t > &  propvar_offsets_ 
)
inline

Definition at line 71 of file parelm.h.

Member Function Documentation

◆ apply() [1/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::apply ( const pbes_equation &  eqn)
inline

Definition at line 133 of file parelm.h.

◆ apply() [2/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::apply ( const propositional_variable_instantiation &  x)
inline

Definition at line 107 of file parelm.h.

◆ enter() [1/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::enter ( const exists &  x)
inline

Definition at line 91 of file parelm.h.

◆ enter() [2/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::enter ( const forall &  x)
inline

Definition at line 75 of file parelm.h.

◆ leave() [1/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::leave ( const exists &  x)
inline

Definition at line 99 of file parelm.h.

◆ leave() [2/2]

void mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::leave ( const forall &  x)
inline

Definition at line 83 of file parelm.h.

Member Data Documentation

◆ bound_variables

std::multiset<data::variable> mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::bound_variables

Definition at line 69 of file parelm.h.

◆ G

graph& mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::G

Definition at line 64 of file parelm.h.

◆ propvar_offsets

const std::map<core::identifier_string, std::size_t>& mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::propvar_offsets

Definition at line 65 of file parelm.h.

◆ X

core::identifier_string mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::X

Definition at line 67 of file parelm.h.

◆ Xparams

data::variable_list mcrl2::pbes_system::pbes_parelm_algorithm::parelm_dependency_traverser::Xparams

Definition at line 68 of file parelm.h.


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