mCRL2
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | List of all members
mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters > Struct Template Reference

#include <lps2pbes_rhs.h>

Inheritance diagram for mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >:
mcrl2::state_formulas::state_formula_traverser< Derived > mcrl2::state_formulas::add_traverser_state_formula_expressions< state_formulas::state_formula_traverser_base, Derived > mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >

Public Types

typedef state_formulas::state_formula_traverser< Derived > super
 
typedef TermTraits tr
 
typedef tr::term_type pbes_expression
 
- Public Types inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< state_formulas::state_formula_traverser_base, Derived >
typedef state_formulas::state_formula_traverser_base< Derived > super
 

Public Member Functions

 rhs_traverser (Parameters &parameters_, TermTraits)
 
Derived & derived ()
 
void push (const pbes_expression &x)
 
pbes_expression & top ()
 
const pbes_expression & top () const
 
pbes_expression pop ()
 
void push_variables (const data::variable_list &variables)
 
void pop_variables (const data::variable_list &variables)
 
bool is_timed () const
 
void leave (const data::data_expression &x)
 
void leave (const state_formulas::true_ &)
 
void leave (const state_formulas::false_ &)
 
void apply (const state_formulas::not_ &)
 
void leave (const state_formulas::and_ &)
 
void leave (const state_formulas::or_ &)
 
void apply (const state_formulas::imp &)
 
void apply (const state_formulas::forall &x)
 
void apply (const state_formulas::exists &x)
 
template<typename MustMayExpression >
pbes_expression apply_may_must_rhs (const MustMayExpression &x)
 
pbes_expression apply_may_must_result (const pbes_expression &p)
 
template<typename MustMayExpression >
void apply_may_must (const MustMayExpression &x, bool is_must)
 
void apply (const state_formulas::must &x)
 
void apply (const state_formulas::may &x)
 
void leave (const state_formulas::yaled &)
 
void leave (const state_formulas::yaled_timed &x)
 
void leave (const state_formulas::delay &)
 
void leave (const state_formulas::delay_timed &x)
 
void leave (const state_formulas::variable &x)
 
void apply (const state_formulas::nu &x)
 
void apply (const state_formulas::mu &x)
 
- Public Member Functions inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< state_formulas::state_formula_traverser_base, Derived >
void apply (const state_formulas::true_ &x)
 
void apply (const state_formulas::false_ &x)
 
void apply (const state_formulas::not_ &x)
 
void apply (const state_formulas::minus &x)
 
void apply (const state_formulas::and_ &x)
 
void apply (const state_formulas::or_ &x)
 
void apply (const state_formulas::imp &x)
 
void apply (const state_formulas::plus &x)
 
void apply (const state_formulas::const_multiply &x)
 
void apply (const state_formulas::const_multiply_alt &x)
 
void apply (const state_formulas::forall &x)
 
void apply (const state_formulas::exists &x)
 
void apply (const state_formulas::infimum &x)
 
void apply (const state_formulas::supremum &x)
 
void apply (const state_formulas::sum &x)
 
void apply (const state_formulas::must &x)
 
void apply (const state_formulas::may &x)
 
void apply (const state_formulas::yaled &x)
 
void apply (const state_formulas::yaled_timed &x)
 
void apply (const state_formulas::delay &x)
 
void apply (const state_formulas::delay_timed &x)
 
void apply (const state_formulas::variable &x)
 
void apply (const state_formulas::nu &x)
 
void apply (const state_formulas::mu &x)
 
void apply (const state_formulas::state_formula_specification &x)
 
void apply (const state_formulas::state_formula &x)
 

Public Attributes

Parameters & parameters
 
std::vector< pbes_expression > result_stack
 

Detailed Description

template<typename Derived, typename TermTraits, typename Parameters>
struct mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >

Definition at line 203 of file lps2pbes_rhs.h.

Member Typedef Documentation

◆ pbes_expression

template<typename Derived , typename TermTraits , typename Parameters >
typedef tr::term_type mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::pbes_expression

Definition at line 207 of file lps2pbes_rhs.h.

◆ super

template<typename Derived , typename TermTraits , typename Parameters >
typedef state_formulas::state_formula_traverser<Derived> mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::super

Definition at line 205 of file lps2pbes_rhs.h.

◆ tr

template<typename Derived , typename TermTraits , typename Parameters >
typedef TermTraits mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::tr

Definition at line 206 of file lps2pbes_rhs.h.

Constructor & Destructor Documentation

◆ rhs_traverser()

template<typename Derived , typename TermTraits , typename Parameters >
mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::rhs_traverser ( Parameters &  parameters_,
TermTraits   
)
inline

Definition at line 216 of file lps2pbes_rhs.h.

Member Function Documentation

◆ apply() [1/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::exists &  x)
inline

Definition at line 317 of file lps2pbes_rhs.h.

◆ apply() [2/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::forall &  x)
inline

Definition at line 307 of file lps2pbes_rhs.h.

◆ apply() [3/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::imp &  )
inline

Definition at line 302 of file lps2pbes_rhs.h.

◆ apply() [4/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::may &  x)
inline

Definition at line 388 of file lps2pbes_rhs.h.

◆ apply() [5/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::mu &  x)
inline

Definition at line 475 of file lps2pbes_rhs.h.

◆ apply() [6/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::must &  x)
inline

Definition at line 383 of file lps2pbes_rhs.h.

◆ apply() [7/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::not_ &  )
inline

Definition at line 283 of file lps2pbes_rhs.h.

◆ apply() [8/8]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply ( const state_formulas::nu &  x)
inline

Definition at line 462 of file lps2pbes_rhs.h.

◆ apply_may_must()

template<typename Derived , typename TermTraits , typename Parameters >
template<typename MustMayExpression >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply_may_must ( const MustMayExpression &  x,
bool  is_must 
)
inline

Definition at line 342 of file lps2pbes_rhs.h.

◆ apply_may_must_result()

template<typename Derived , typename TermTraits , typename Parameters >
pbes_expression mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply_may_must_result ( const pbes_expression &  p)
inline

Definition at line 335 of file lps2pbes_rhs.h.

◆ apply_may_must_rhs()

template<typename Derived , typename TermTraits , typename Parameters >
template<typename MustMayExpression >
pbes_expression mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::apply_may_must_rhs ( const MustMayExpression &  x)
inline

Definition at line 329 of file lps2pbes_rhs.h.

◆ derived()

template<typename Derived , typename TermTraits , typename Parameters >
Derived & mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::derived ( )
inline

Definition at line 220 of file lps2pbes_rhs.h.

◆ is_timed()

template<typename Derived , typename TermTraits , typename Parameters >
bool mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::is_timed ( ) const
inline

Definition at line 263 of file lps2pbes_rhs.h.

◆ leave() [1/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const data::data_expression &  x)
inline

Definition at line 268 of file lps2pbes_rhs.h.

◆ leave() [2/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::and_ &  )
inline

Definition at line 288 of file lps2pbes_rhs.h.

◆ leave() [3/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::delay &  )
inline

Definition at line 421 of file lps2pbes_rhs.h.

◆ leave() [4/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::delay_timed &  x)
inline

Definition at line 426 of file lps2pbes_rhs.h.

◆ leave() [5/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::false_ &  )
inline

Definition at line 278 of file lps2pbes_rhs.h.

◆ leave() [6/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::or_ &  )
inline

Definition at line 295 of file lps2pbes_rhs.h.

◆ leave() [7/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::true_ &  )
inline

Definition at line 273 of file lps2pbes_rhs.h.

◆ leave() [8/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::variable &  x)
inline

Definition at line 449 of file lps2pbes_rhs.h.

◆ leave() [9/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::yaled &  )
inline

Definition at line 393 of file lps2pbes_rhs.h.

◆ leave() [10/10]

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::leave ( const state_formulas::yaled_timed &  x)
inline

Definition at line 398 of file lps2pbes_rhs.h.

◆ pop()

template<typename Derived , typename TermTraits , typename Parameters >
pbes_expression mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::pop ( )
inline

Definition at line 240 of file lps2pbes_rhs.h.

◆ pop_variables()

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::pop_variables ( const data::variable_list &  variables)
inline

Definition at line 255 of file lps2pbes_rhs.h.

◆ push()

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::push ( const pbes_expression &  x)
inline

Definition at line 225 of file lps2pbes_rhs.h.

◆ push_variables()

template<typename Derived , typename TermTraits , typename Parameters >
void mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::push_variables ( const data::variable_list &  variables)
inline

Definition at line 247 of file lps2pbes_rhs.h.

◆ top() [1/2]

template<typename Derived , typename TermTraits , typename Parameters >
pbes_expression & mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::top ( )
inline

Definition at line 230 of file lps2pbes_rhs.h.

◆ top() [2/2]

template<typename Derived , typename TermTraits , typename Parameters >
const pbes_expression & mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::top ( ) const
inline

Definition at line 235 of file lps2pbes_rhs.h.

Member Data Documentation

◆ parameters

template<typename Derived , typename TermTraits , typename Parameters >
Parameters& mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::parameters

Definition at line 213 of file lps2pbes_rhs.h.

◆ result_stack

template<typename Derived , typename TermTraits , typename Parameters >
std::vector<pbes_expression> mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >::result_stack

Definition at line 214 of file lps2pbes_rhs.h.

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