mCRL2
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | List of all members
mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser Struct Reference

#include <pbesinst_structure_graph2.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser:
mcrl2::pbes_system::pbes_expression_traverser< Rplus_traverser > mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >

Classes

struct  stack_element
 

Public Types

typedef pbes_expression_traverser< Rplus_traverser > super
 
- Public Types inherited from mcrl2::pbes_system::add_traverser_pbes_expressions< Traverser, Derived >
typedef Traverser< Derived > super
 

Public Member Functions

 Rplus_traverser (std::array< vertex_set, 2 > &S_, detail::structure_graph_builder &graph_builder_)
 
void push (const stack_element &elem)
 
stack_element pop ()
 
stack_element & top ()
 
const stack_element & top () const
 
void leave (const data::data_expression &x)
 
void leave (const propositional_variable_instantiation &x)
 
void leave (const and_ &)
 
void leave (const or_ &)
 
void enter (const imp &x)
 
void leave (const imp &x)
 
void enter (const exists &x)
 
void leave (const exists &x)
 
void enter (const forall &x)
 
void leave (const forall &x)
 
- 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)
 

Static Public Member Functions

static bool less (const pbes_expression &, const pbes_expression &)
 

Public Attributes

std::array< vertex_set, 2 > & S
 
detail::structure_graph_builder & graph_builder
 
atermpp::vector< stack_element > stack
 

Detailed Description

Definition at line 91 of file pbesinst_structure_graph2.h.

Member Typedef Documentation

◆ super

typedef pbes_expression_traverser<Rplus_traverser> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::super

Definition at line 93 of file pbesinst_structure_graph2.h.

Constructor & Destructor Documentation

◆ Rplus_traverser()

mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::Rplus_traverser ( std::array< vertex_set, 2 > &  S_,
detail::structure_graph_builder &  graph_builder_ 
)
inline

Definition at line 129 of file pbesinst_structure_graph2.h.

Member Function Documentation

◆ enter() [1/3]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::enter ( const exists &  x)
inline

Definition at line 329 of file pbesinst_structure_graph2.h.

◆ enter() [2/3]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::enter ( const forall &  x)
inline

Definition at line 339 of file pbesinst_structure_graph2.h.

◆ enter() [3/3]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::enter ( const imp &  x)
inline

Definition at line 319 of file pbesinst_structure_graph2.h.

◆ leave() [1/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const and_ &  )
inline

Definition at line 197 of file pbesinst_structure_graph2.h.

◆ leave() [2/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const data::data_expression &  x)
inline

Definition at line 163 of file pbesinst_structure_graph2.h.

◆ leave() [3/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const exists &  x)
inline

Definition at line 334 of file pbesinst_structure_graph2.h.

◆ leave() [4/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const forall &  x)
inline

Definition at line 344 of file pbesinst_structure_graph2.h.

◆ leave() [5/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const imp &  x)
inline

Definition at line 324 of file pbesinst_structure_graph2.h.

◆ leave() [6/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const or_ &  )
inline

Definition at line 258 of file pbesinst_structure_graph2.h.

◆ leave() [7/7]

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::leave ( const propositional_variable_instantiation &  x)
inline

Definition at line 175 of file pbesinst_structure_graph2.h.

◆ less()

static bool mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::less ( const pbes_expression &  ,
const pbes_expression &   
)
inlinestatic

Definition at line 158 of file pbesinst_structure_graph2.h.

◆ pop()

stack_element mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::pop ( )
inline

Definition at line 138 of file pbesinst_structure_graph2.h.

◆ push()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::push ( const stack_element &  elem)
inline

Definition at line 133 of file pbesinst_structure_graph2.h.

◆ top() [1/2]

stack_element & mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::top ( )
inline

Definition at line 146 of file pbesinst_structure_graph2.h.

◆ top() [2/2]

const stack_element & mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::top ( ) const
inline

Definition at line 152 of file pbesinst_structure_graph2.h.

Member Data Documentation

◆ graph_builder

detail::structure_graph_builder& mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::graph_builder

Definition at line 125 of file pbesinst_structure_graph2.h.

◆ S

std::array<vertex_set, 2>& mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::S

Definition at line 123 of file pbesinst_structure_graph2.h.

◆ stack

atermpp::vector<stack_element> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::stack

Definition at line 127 of file pbesinst_structure_graph2.h.

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