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  reference_aterm_stack_element
 
struct  stack_element
 

Public Types

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

Public Member Functions

 Rplus_traverser (std::array< vertex_set, 2 > &S_, detail::structure_graph_builder &graph_builder_)
 
void push (const reference_aterm_stack_element &elem)
 
stack_element pop ()
 
reference_aterm_stack_element & top ()
 
const reference_aterm_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 &x1, const pbes_expression &x2)
 

Public Attributes

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

Detailed Description

Definition at line 102 of file pbesinst_structure_graph2.h.

Member Typedef Documentation

◆ super

using mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus_traverser::super = pbes_expression_traverser<Rplus_traverser>

Definition at line 104 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 168 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 359 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 369 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 349 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 235 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 201 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 364 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 374 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 354 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 292 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 213 of file pbesinst_structure_graph2.h.

◆ less()

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

Definition at line 196 of file pbesinst_structure_graph2.h.

◆ pop()

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

Definition at line 177 of file pbesinst_structure_graph2.h.

◆ push()

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

Definition at line 172 of file pbesinst_structure_graph2.h.

◆ top() [1/2]

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

Definition at line 185 of file pbesinst_structure_graph2.h.

◆ top() [2/2]

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

Definition at line 191 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 165 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 163 of file pbesinst_structure_graph2.h.

◆ stack

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

Definition at line 166 of file pbesinst_structure_graph2.h.

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