12#ifndef MCRL2_PBES_BUILDER_H
13#define MCRL2_PBES_BUILDER_H
25template <
typename Derived>
43template <
template <
class>
class Builder,
class Derived>
56 static_cast<Derived&
>(*this).enter(x);
58 static_cast<Derived&
>(*this).leave(x);
63 static_cast<Derived&
>(*this).enter(x);
65 static_cast<Derived&
>(*this).apply(result_variable, x.
variable());
68 static_cast<Derived&
>(*this).apply(result_formula, x.
formula());
70 static_cast<Derived&
>(*this).leave(x);
75 static_cast<Derived&
>(*this).enter(x);
77 static_cast<Derived&
>(*this).update(x.
equations());
79 static_cast<Derived&
>(*this).apply(result_initial_state, x.
initial_state());
81 static_cast<Derived&
>(*this).leave(x);
88 static_cast<Derived&
>(*this).enter(x);
90 static_cast<Derived&
>(*this).leave(x);
97 static_cast<Derived&
>(*this).enter(x);
99 static_cast<Derived&
>(*this).leave(x);
106 static_cast<Derived&
>(*this).enter(x);
108 static_cast<Derived&
>(*this).leave(x);
115 static_cast<Derived&
>(*this).enter(x);
117 static_cast<Derived&
>(*this).leave(x);
124 static_cast<Derived&
>(*this).enter(x);
126 static_cast<Derived&
>(*this).leave(x);
133 static_cast<Derived&
>(*this).enter(x);
135 static_cast<Derived&
>(*this).leave(x);
142 static_cast<Derived&
>(*this).enter(x);
144 static_cast<Derived&
>(*this).leave(x);
151 static_cast<Derived&
>(*this).enter(x);
154 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
158 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
162 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
166 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
170 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
174 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
178 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
182 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
186 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
190 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
192 static_cast<Derived&
>(*this).leave(x);
198template <
typename Derived>
206template <
template <
class>
class Builder,
class Derived>
217 static_cast<Derived&
>(*this).enter(x);
219 static_cast<Derived&
>(*this).apply(result_formula, x.
formula());
221 static_cast<Derived&
>(*this).leave(x);
226 static_cast<Derived&
>(*this).enter(x);
227 static_cast<Derived&
>(*this).update(x.
equations());
229 static_cast<Derived&
>(*this).apply(result_initial_state, x.
initial_state());
231 static_cast<Derived&
>(*this).leave(x);
238 static_cast<Derived&
>(*this).enter(x);
240 static_cast<Derived&
>(*this).leave(x);
247 static_cast<Derived&
>(*this).enter(x);
249 static_cast<Derived&
>(*this).leave(x);
256 static_cast<Derived&
>(*this).enter(x);
258 static_cast<Derived&
>(*this).leave(x);
265 static_cast<Derived&
>(*this).enter(x);
267 static_cast<Derived&
>(*this).leave(x);
274 static_cast<Derived&
>(*this).enter(x);
276 static_cast<Derived&
>(*this).leave(x);
283 static_cast<Derived&
>(*this).enter(x);
285 static_cast<Derived&
>(*this).leave(x);
292 static_cast<Derived&
>(*this).enter(x);
294 static_cast<Derived&
>(*this).leave(x);
301 static_cast<Derived&
>(*this).enter(x);
304 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
308 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
312 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
316 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
320 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
324 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
328 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
332 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
336 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
340 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
342 static_cast<Derived&
>(*this).leave(x);
348template <
typename Derived>
355template <
template <
class>
class Builder,
class Derived>
368 static_cast<Derived&
>(*this).enter(x);
370 static_cast<Derived&
>(*this).leave(x);
375 static_cast<Derived&
>(*this).enter(x);
377 static_cast<Derived&
>(*this).apply(result_variable, x.
variable());
380 static_cast<Derived&
>(*this).apply(result_formula, x.
formula());
382 static_cast<Derived&
>(*this).leave(x);
387 static_cast<Derived&
>(*this).enter(x);
389 static_cast<Derived&
>(*this).update(x.
equations());
391 static_cast<Derived&
>(*this).apply(result_initial_state, x.
initial_state());
393 static_cast<Derived&
>(*this).leave(x);
400 static_cast<Derived&
>(*this).enter(x);
402 static_cast<Derived&
>(*this).leave(x);
409 static_cast<Derived&
>(*this).enter(x);
411 static_cast<Derived&
>(*this).leave(x);
418 static_cast<Derived&
>(*this).enter(x);
420 static_cast<Derived&
>(*this).leave(x);
427 static_cast<Derived&
>(*this).enter(x);
429 static_cast<Derived&
>(*this).leave(x);
436 static_cast<Derived&
>(*this).enter(x);
438 static_cast<Derived&
>(*this).leave(x);
445 static_cast<Derived&
>(*this).enter(x);
447 static_cast<Derived&
>(*this).leave(x);
454 static_cast<Derived&
>(*this).enter(x);
456 static_cast<Derived&
>(*this).leave(x);
463 static_cast<Derived&
>(*this).enter(x);
466 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
470 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
474 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
478 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
482 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
486 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
490 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
494 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
498 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
502 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
504 static_cast<Derived&
>(*this).leave(x);
510template <
typename Derived>
518template <
template <
class>
class Builder,
class Derived>
529 static_cast<Derived&
>(*this).enter(x);
531 static_cast<Derived&
>(*this).apply(result_formula, x.
formula());
533 static_cast<Derived&
>(*this).leave(x);
538 static_cast<Derived&
>(*this).enter(x);
539 static_cast<Derived&
>(*this).update(x.
equations());
540 static_cast<Derived&
>(*this).leave(x);
548 static_cast<Derived&
>(*this).enter(x);
550 static_cast<Derived&
>(*this).leave(x);
558 static_cast<Derived&
>(*this).enter(x);
560 static_cast<Derived&
>(*this).leave(x);
567 static_cast<Derived&
>(*this).enter(x);
569 static_cast<Derived&
>(*this).leave(x);
576 static_cast<Derived&
>(*this).enter(x);
578 static_cast<Derived&
>(*this).leave(x);
585 static_cast<Derived&
>(*this).enter(x);
587 static_cast<Derived&
>(*this).leave(x);
594 static_cast<Derived&
>(*this).enter(x);
596 static_cast<Derived&
>(*this).leave(x);
603 static_cast<Derived&
>(*this).enter(x);
605 static_cast<Derived&
>(*this).leave(x);
612 static_cast<Derived&
>(*this).enter(x);
615 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
619 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::variable>(x));
623 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
627 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
631 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
635 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
639 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
643 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
647 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
651 static_cast<Derived&
>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
653 static_cast<Derived&
>(*this).leave(x);
659template <
typename Derived>
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
const propositional_variable & variable() const
Returns the pbes variable of the equation.
parameterized boolean equation system
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
const std::vector< pbes_equation > & equations() const
Returns the equations.
\brief A propositional variable instantiation
const core::identifier_string & name() const
\brief A propositional variable declaration
const core::identifier_string & name() const
add your file description here.
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_untyped_data_parameter(const atermpp::aterm &x)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void make_propositional_variable(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_not(const atermpp::aterm &x)
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm &x)
bool is_or(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
void make_propositional_variable_instantiation(atermpp::aterm &t, const ARGUMENTS &... args)
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
expression builder that visits all sub expressions
void update(T &x, typename atermpp::disable_if_container< T >::type *=nullptr)
void apply(atermpp::term_list< T > &result, const atermpp::term_list< U > &x)
void apply(T &result, const pbes_system::imp &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::or_ &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::not_ &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::forall &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::imp &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::or_ &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::or_ &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void apply(T &result, const pbes_system::propositional_variable &x)
void apply(T &result, const pbes_system::imp &x)
void update(pbes_system::pbes_equation &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(T &result, const pbes_system::imp &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::propositional_variable &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::or_ &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void apply(T &result, const data::data_expression &x)
core::builder< Derived > super