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

#include <lps2pbes_rhs.h>

Inheritance diagram for mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >:
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 >

Public Types

typedef rhs_traverser< Derived, TermTraits, Parameters > super
 
typedef TermTraits tr
 
- Public Types inherited from mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >
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_structured_traverser (Parameters &parameters, const data::variable_list &variables_, const fixpoint_symbol &sigma_, std::vector< pbes_equation > &equations_, TermTraits tr)
 
data::variable_list rhs_structured_compute_variables (const state_formulas::state_formula &x, const std::multiset< data::variable > &variables) const
 
void enter (const state_formulas::forall &x)
 
void leave (const state_formulas::forall &x)
 
void enter (const state_formulas::exists &x)
 
void leave (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)
 
void apply (const state_formulas::must &x)
 
void apply (const state_formulas::may &x)
 
void leave (const data::data_expression &x)
 
void leave (const state_formulas::true_ &)
 
void leave (const state_formulas::false_ &)
 
void leave (const state_formulas::and_ &)
 
void leave (const state_formulas::or_ &)
 
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::not_ &)
 
void apply (const state_formulas::imp &)
 
void apply (const state_formulas::forall &x)
 
void apply (const state_formulas::exists &x)
 
void apply (const state_formulas::must &x)
 
void apply (const state_formulas::may &x)
 
void apply (const state_formulas::nu &x)
 
void apply (const state_formulas::mu &x)
 
void push (const pbes_expression &x)
 
pbes_expression & top ()
 
const pbes_expression & top () const
 
pbes_expression pop ()
 
bool is_timed () const
 
template<typename MustMayExpression >
void apply_may_must (const MustMayExpression &x, bool is_must)
 
Derived & derived ()
 
- Public Member Functions inherited from mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >
 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

std::multiset< data::variable > variables
 
const fixpoint_symbol & sigma
 
std::vector< pbes_equation > & equations
 
Parameters & parameters
 
- Public Attributes inherited from mcrl2::pbes_system::detail::rhs_traverser< Derived, TermTraits, Parameters >
Parameters & parameters
 
std::vector< pbes_expression > result_stack
 

Detailed Description

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

Definition at line 524 of file lps2pbes_rhs.h.

Member Typedef Documentation

◆ super

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

Definition at line 526 of file lps2pbes_rhs.h.

◆ tr

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

Definition at line 527 of file lps2pbes_rhs.h.

Constructor & Destructor Documentation

◆ rhs_structured_traverser()

template<typename Derived , typename TermTraits , typename Parameters >
mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >::rhs_structured_traverser ( Parameters &  parameters,
const data::variable_list &  variables_,
const fixpoint_symbol &  sigma_,
std::vector< pbes_equation > &  equations_,
TermTraits  tr 
)
inline

Definition at line 544 of file lps2pbes_rhs.h.

Member Function Documentation

◆ apply() [1/10]

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/10]

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/10]

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/10]

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/10]

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

Definition at line 615 of file lps2pbes_rhs.h.

◆ apply() [6/10]

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() [7/10]

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() [8/10]

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

Definition at line 610 of file lps2pbes_rhs.h.

◆ apply() [9/10]

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() [10/10]

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_structured_traverser< Derived, TermTraits, Parameters >::apply_may_must_result ( const pbes_expression &  p)
inline

Definition at line 599 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_structured_traverser< Derived, TermTraits, Parameters >::apply_may_must_rhs ( const MustMayExpression &  x)
inline

Definition at line 593 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.

◆ enter() [1/2]

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

Definition at line 577 of file lps2pbes_rhs.h.

◆ enter() [2/2]

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

Definition at line 563 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/12]

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/12]

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/12]

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/12]

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/12]

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

Definition at line 583 of file lps2pbes_rhs.h.

◆ leave() [6/12]

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() [7/12]

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

Definition at line 569 of file lps2pbes_rhs.h.

◆ leave() [8/12]

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() [9/12]

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() [10/12]

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() [11/12]

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() [12/12]

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.

◆ 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.

◆ rhs_structured_compute_variables()

template<typename Derived , typename TermTraits , typename Parameters >
data::variable_list mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >::rhs_structured_compute_variables ( const state_formulas::state_formula &  x,
const std::multiset< data::variable > &  variables 
) const
inline

Definition at line 556 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

◆ equations

template<typename Derived , typename TermTraits , typename Parameters >
std::vector<pbes_equation>& mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >::equations

Definition at line 542 of file lps2pbes_rhs.h.

◆ 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.

◆ sigma

template<typename Derived , typename TermTraits , typename Parameters >
const fixpoint_symbol& mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >::sigma

Definition at line 541 of file lps2pbes_rhs.h.

◆ variables

template<typename Derived , typename TermTraits , typename Parameters >
std::multiset<data::variable> mcrl2::pbes_system::detail::rhs_structured_traverser< Derived, TermTraits, Parameters >::variables

Definition at line 540 of file lps2pbes_rhs.h.

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