12#ifndef MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
13#define MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
20namespace regular_formulas
120 assert(core::detail::check_term_RegSeq(*
this));
131 seq& operator=(const
seq&) noexcept = default;
132 seq& operator=(
seq&&) noexcept = default;
136 return atermpp::down_cast<regular_formula>((*
this)[0]);
141 return atermpp::down_cast<regular_formula>((*
this)[1]);
147template <
class... ARGUMENTS>
163std::string
pp(
const seq& x);
196 assert(core::detail::check_term_RegAlt(*
this));
207 alt& operator=(const
alt&) noexcept = default;
208 alt& operator=(
alt&&) noexcept = default;
212 return atermpp::down_cast<regular_formula>((*
this)[0]);
217 return atermpp::down_cast<regular_formula>((*
this)[1]);
223template <
class... ARGUMENTS>
239std::string
pp(
const alt& x);
272 assert(core::detail::check_term_RegTrans(*
this));
288 return atermpp::down_cast<regular_formula>((*
this)[0]);
294template <
class... ARGUMENTS>
310std::string
pp(
const trans& x);
343 assert(core::detail::check_term_RegTransOrNil(*
this));
359 return atermpp::down_cast<regular_formula>((*
this)[0]);
365template <
class... ARGUMENTS>
381std::string
pp(
const trans_or_nil& x);
414 assert(core::detail::check_term_UntypedRegFrm(*
this));
424 :
regular_formula(
atermpp::aterm(core::detail::function_symbol_UntypedRegFrm(), core::identifier_string(name), left, right))
433 const core::identifier_string& name()
const
435 return atermpp::down_cast<core::identifier_string>((*
this)[0]);
440 return atermpp::down_cast<regular_formula>((*
this)[1]);
445 return atermpp::down_cast<regular_formula>((*
this)[2]);
451template <
class... ARGUMENTS>
467std::string
pp(
const untyped_regular_formula& x);
Term containing a string.
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.
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...
const atermpp::function_symbol & function_symbol_RegSeq()
const atermpp::function_symbol & function_symbol_RegTransOrNil()
const atermpp::function_symbol & function_symbol_RegTrans()
const atermpp::function_symbol & function_symbol_RegAlt()
bool check_rule_RegFrm(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedRegFrm()
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
static const atermpp::function_symbol UntypedRegFrm
static const atermpp::function_symbol RegSeq
static const atermpp::function_symbol RegTransOrNil
static const atermpp::function_symbol RegAlt
static const atermpp::function_symbol RegTrans