12#ifndef MCRL2_PBES_PBES_EQUATION_H
13#define MCRL2_PBES_PBES_EQUATION_H
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
fixpoint_symbol & symbol()
Returns the fixpoint symbol of the equation.
pbes_expression term_type
The expression type of the equation.
fixpoint_symbol symbol_type
The symbol type of the equation.
void swap(pbes_equation &other)
Swaps the contents.
propositional_variable variable_type
The variable type of the equation.
pbes_equation(const fixpoint_symbol &symbol, const propositional_variable &variable, const pbes_expression &expr)
Constructor.
bool is_solved() const
Returns true if the predicate formula on the right hand side contains no predicate variables.
fixpoint_symbol m_symbol
The fixpoint symbol of the equation.
propositional_variable m_variable
The variable on the left hand side of the equation.
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
bool operator<(const pbes_equation &other) const
A comparison operator on pbes equations. \detail The comparison is on the addresses of aterm objects ...
propositional_variable & variable()
Returns the pbes variable of the equation.
pbes_expression m_formula
The expression on the right hand side of the equation.
pbes_equation()=default
Constructor.
pbes_expression & formula()
Returns the predicate formula on the right hand side of the equation.
const propositional_variable & variable() const
Returns the pbes variable of the equation.
\brief A propositional variable declaration
The class fixpoint_symbol.
const atermpp::function_symbol & function_symbol_PBEqn()
bool operator!=(const pbes_equation &x, const pbes_equation &y)
void normalize_sorts(T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
void find_free_variables(const T &x, OutputIterator o)
std::vector< pbes_equation > pbes_equation_vector
\brief vector of pbes_equations
bool has_propositional_variables(const pbes_expression &x)
std::ostream & operator<<(std::ostream &os, const absinthe_strategy strategy)
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
bool is_well_typed(const pbes_equation &eqn)
atermpp::term_list< pbes_equation > pbes_equation_list
\brief list of pbes_equations
atermpp::aterm pbes_equation_to_aterm(const pbes_equation &eqn)
Conversion to atermaPpl.
void swap(fixpoint_symbol &t1, fixpoint_symbol &t2)
\brief swap overload
std::string pp(const fixpoint_symbol &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
The class pbes_expression.
Add your file description here.