#include <lps2pbes_par.h>

Inheritance diagram for mcrl2::pbes_system::detail::par_traverser:

Public Types
typedef state_formulas::state_formula_traverser< par_traverser >	super

Public Types inherited from mcrl2::state_formulas::add_traverser_state_formula_expressions< Traverser, Derived >
typedef Traverser< Derived >	super

Public Member Functions
	par_traverser (const core::identifier_string &X_, const data::variable_list &l_)

void	push (const data::variable_list &x)

const data::variable_list &	top () const

data::variable_list	pop ()

void	join ()

void	leave (const data::data_expression &)

void	leave (const state_formulas::true_ &)

void	leave (const state_formulas::false_ &)

void	leave (const state_formulas::not_ &)

void	leave (const state_formulas::and_ &)

void	leave (const state_formulas::or_ &)

void	leave (const state_formulas::imp &)

void	apply (const state_formulas::forall &x)

void	apply (const state_formulas::exists &x)

void	leave (const state_formulas::must &)

void	leave (const state_formulas::may &)

void	leave (const state_formulas::yaled &)

void	leave (const state_formulas::yaled_timed &)

void	leave (const state_formulas::delay &)

void	leave (const state_formulas::delay_timed &)

void	leave (const state_formulas::variable &)

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< Traverser, 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
const core::identifier_string &	X

const data::variable_list &	l

std::vector< data::variable_list >	result_stack

Detailed Description

Definition at line 25 of file lps2pbes_par.h.

Member Typedef Documentation

◆ super

typedef state_formulas::state_formula_traverser<par_traverser> mcrl2::pbes_system::detail::par_traverser::super

Definition at line 27 of file lps2pbes_par.h.

Constructor & Destructor Documentation

◆ par_traverser()

mcrl2::pbes_system::detail::par_traverser::par_traverser	(	const core::identifier_string &	X_,
		const data::variable_list &	l_
	)

inline

Definition at line 36 of file lps2pbes_par.h.

Member Function Documentation

◆ apply() [1/4]

void mcrl2::pbes_system::detail::par_traverser::apply ( const state_formulas::exists & x )

inline

Definition at line 105 of file lps2pbes_par.h.

◆ apply() [2/4]

void mcrl2::pbes_system::detail::par_traverser::apply ( const state_formulas::forall & x )

inline

Definition at line 100 of file lps2pbes_par.h.

◆ apply() [3/4]

void mcrl2::pbes_system::detail::par_traverser::apply ( const state_formulas::mu & x )

inline

Definition at line 157 of file lps2pbes_par.h.

◆ apply() [4/4]

void mcrl2::pbes_system::detail::par_traverser::apply ( const state_formulas::nu & x )

inline

Definition at line 145 of file lps2pbes_par.h.

◆ join()

void mcrl2::pbes_system::detail::par_traverser::join ( )

inline

Definition at line 58 of file lps2pbes_par.h.

◆ leave() [1/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const data::data_expression & )

inline

Definition at line 65 of file lps2pbes_par.h.

◆ leave() [2/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::and_ & )

inline

Definition at line 85 of file lps2pbes_par.h.

◆ leave() [3/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::delay & )

inline

Definition at line 130 of file lps2pbes_par.h.

◆ leave() [4/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::delay_timed & )

inline

Definition at line 135 of file lps2pbes_par.h.

◆ leave() [5/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::false_ & )

inline

Definition at line 75 of file lps2pbes_par.h.

◆ leave() [6/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::imp & )

inline

Definition at line 95 of file lps2pbes_par.h.

◆ leave() [7/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::may & )

inline

Definition at line 115 of file lps2pbes_par.h.

◆ leave() [8/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::must & )

inline

Definition at line 110 of file lps2pbes_par.h.

◆ leave() [9/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::not_ & )

inline

Definition at line 80 of file lps2pbes_par.h.

◆ leave() [10/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::or_ & )

inline

Definition at line 90 of file lps2pbes_par.h.

◆ leave() [11/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::true_ & )

inline

Definition at line 70 of file lps2pbes_par.h.

◆ leave() [12/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::variable & )

inline

Definition at line 140 of file lps2pbes_par.h.

◆ leave() [13/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::yaled & )

inline

Definition at line 120 of file lps2pbes_par.h.

◆ leave() [14/14]

void mcrl2::pbes_system::detail::par_traverser::leave ( const state_formulas::yaled_timed & )

inline

Definition at line 125 of file lps2pbes_par.h.

◆ pop()

data::variable_list mcrl2::pbes_system::detail::par_traverser::pop ( )

inline

Definition at line 50 of file lps2pbes_par.h.

◆ push()

void mcrl2::pbes_system::detail::par_traverser::push ( const data::variable_list & x )

inline

Definition at line 40 of file lps2pbes_par.h.

◆ top()

const data::variable_list & mcrl2::pbes_system::detail::par_traverser::top ( ) const

inline

Definition at line 45 of file lps2pbes_par.h.

Member Data Documentation

◆ l

const data::variable_list& mcrl2::pbes_system::detail::par_traverser::l

Definition at line 33 of file lps2pbes_par.h.

◆ result_stack

std::vector<data::variable_list> mcrl2::pbes_system::detail::par_traverser::result_stack

Definition at line 34 of file lps2pbes_par.h.

◆ X

const core::identifier_string& mcrl2::pbes_system::detail::par_traverser::X

Definition at line 32 of file lps2pbes_par.h.

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

pbes/include/mcrl2/pbes/detail/lps2pbes_par.h

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ par_traverser()

Member Function Documentation

◆ apply() [1/4]

◆ apply() [2/4]

◆ apply() [3/4]

◆ apply() [4/4]

◆ join()

◆ leave() [1/14]

◆ leave() [2/14]

◆ leave() [3/14]

◆ leave() [4/14]

◆ leave() [5/14]

◆ leave() [6/14]

◆ leave() [7/14]

◆ leave() [8/14]

◆ leave() [9/14]

◆ leave() [10/14]

◆ leave() [11/14]

◆ leave() [12/14]

◆ leave() [13/14]

◆ leave() [14/14]

◆ pop()

◆ push()

◆ top()

Member Data Documentation

◆ l

◆ result_stack

◆ X