12#ifndef MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
13#define MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
21namespace action_formulas
137 assert(core::detail::check_term_ActTrue(*
this));
153 return x.
function() == core::detail::function_symbols::ActTrue;
157std::string pp(
const true_& x);
164std::ostream& operator<<(std::ostream& out,
const true_& x)
166 return out << action_formulas::pp(x);
190 assert(core::detail::check_term_ActFalse(*
this));
206 return x.
function() == core::detail::function_symbols::ActFalse;
210std::string pp(
const false_& x);
217std::ostream& operator<<(std::ostream& out,
const false_& x)
219 return out << action_formulas::pp(x);
243 assert(core::detail::check_term_ActNot(*
this));
259 return atermpp::down_cast<action_formula>((*
this)[0]);
265template <
class... ARGUMENTS>
277 return x.
function() == core::detail::function_symbols::ActNot;
281std::string pp(
const not_& x);
288std::ostream& operator<<(std::ostream& out,
const not_& x)
290 return out << action_formulas::pp(x);
314 assert(core::detail::check_term_ActAnd(*
this));
330 return atermpp::down_cast<action_formula>((*
this)[0]);
335 return atermpp::down_cast<action_formula>((*
this)[1]);
341template <
class... ARGUMENTS>
353 return x.
function() == core::detail::function_symbols::ActAnd;
357std::string pp(
const and_& x);
364std::ostream& operator<<(std::ostream& out,
const and_& x)
366 return out << action_formulas::pp(x);
390 assert(core::detail::check_term_ActOr(*
this));
401 or_& operator=(const
or_&) noexcept = default;
402 or_& operator=(
or_&&) noexcept = default;
406 return atermpp::down_cast<action_formula>((*
this)[0]);
411 return atermpp::down_cast<action_formula>((*
this)[1]);
417template <
class... ARGUMENTS>
429 return x.
function() == core::detail::function_symbols::ActOr;
433std::string pp(
const or_& x);
440std::ostream& operator<<(std::ostream& out,
const or_& x)
442 return out << action_formulas::pp(x);
466 assert(core::detail::check_term_ActImp(*
this));
477 imp& operator=(const
imp&) noexcept = default;
478 imp& operator=(
imp&&) noexcept = default;
482 return atermpp::down_cast<action_formula>((*
this)[0]);
487 return atermpp::down_cast<action_formula>((*
this)[1]);
493template <
class... ARGUMENTS>
505 return x.
function() == core::detail::function_symbols::ActImp;
509std::string pp(
const imp& x);
516std::ostream& operator<<(std::ostream& out,
const imp& x)
518 return out << action_formulas::pp(x);
542 assert(core::detail::check_term_ActForall(*
this));
556 const data::variable_list& variables()
const
558 return atermpp::down_cast<data::variable_list>((*
this)[0]);
563 return atermpp::down_cast<action_formula>((*
this)[1]);
569template <
class... ARGUMENTS>
581 return x.
function() == core::detail::function_symbols::ActForall;
585std::string pp(
const forall& x);
592std::ostream& operator<<(std::ostream& out,
const forall& x)
594 return out << action_formulas::pp(x);
618 assert(core::detail::check_term_ActExists(*
this));
632 const data::variable_list& variables()
const
634 return atermpp::down_cast<data::variable_list>((*
this)[0]);
639 return atermpp::down_cast<action_formula>((*
this)[1]);
645template <
class... ARGUMENTS>
657 return x.
function() == core::detail::function_symbols::ActExists;
661std::string pp(
const exists& x);
668std::ostream& operator<<(std::ostream& out,
const exists& x)
670 return out << action_formulas::pp(x);
694 assert(core::detail::check_term_ActAt(*
this));
703 at(
const at&)
noexcept =
default;
705 at& operator=(const
at&) noexcept = default;
706 at& operator=(
at&&) noexcept = default;
710 return atermpp::down_cast<action_formula>((*
this)[0]);
715 return atermpp::down_cast<data::data_expression>((*
this)[1]);
721template <
class... ARGUMENTS>
733 return x.
function() == core::detail::function_symbols::ActAt;
737std::string pp(
const at& x);
744std::ostream& operator<<(std::ostream& out,
const at& x)
746 return out << action_formulas::pp(x);
770 assert(core::detail::check_term_ActMultAct(*
this));
784 const process::action_list& actions()
const
786 return atermpp::down_cast<process::action_list>((*
this)[0]);
792template <
class... ARGUMENTS>
804 return x.
function() == core::detail::function_symbols::ActMultAct;
808std::string pp(
const multi_action& x);
817 return out << action_formulas::pp(x);
void swap(StaticGraph &a, StaticGraph &b)
aterm()
Default constructor.
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
\brief An untyped parameter
\brief An untyped multi action or data application
The main namespace for the aterm++ library.
void make_term_appl(Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor an aterm in a variable based on a function symbol and an forward iterator providing the a...
bool check_rule_ActFrm(const Term &t)
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_untyped_multi_action(const atermpp::aterm &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.