mCRL2
Loading...
Searching...
No Matches
pbes_equation.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_PBES_PBES_EQUATION_H
13#define MCRL2_PBES_PBES_EQUATION_H
14
18
19namespace mcrl2
20{
21
22namespace pbes_system
23{
24
25class pbes_equation;
26atermpp::aterm pbes_equation_to_aterm(const pbes_equation& eqn);
27bool is_well_typed(const pbes_equation& eqn);
29
32{
33 protected:
36
39
42
43 public:
46
49
52
54 pbes_equation() = default;
55
61 :
64 m_formula(expr)
65 {
66 }
67
70 const fixpoint_symbol& symbol() const
71 {
72 return m_symbol;
73 }
74
78 {
79 return m_symbol;
80 }
81
85 {
86 return m_variable;
87 }
88
92 {
93 return m_variable;
94 }
95
98 const pbes_expression& formula() const
99 {
100 return m_formula;
101 }
102
106 {
107 return m_formula;
108 }
109
111 // (Comment Wieger: is_const would be a better name)
113 bool is_solved() const;
114
116 void swap(pbes_equation& other)
117 {
118 using std::swap;
119 swap(m_symbol, other.m_symbol);
120 swap(m_variable, other.m_variable);
121 swap(m_formula, other.m_formula);
122 }
123
128 bool operator<(const pbes_equation& other) const
129 {
130 return (m_formula < other.m_formula) ||
131 ((m_formula == other.m_formula &&
132 (m_variable < other.m_variable ||
133 (m_variable == other.m_variable &&
134 m_symbol < other.m_symbol))));
135 }
136};
137
138//--- start generated class pbes_equation ---//
141
143typedef std::vector<pbes_equation> pbes_equation_vector;
144
145// prototype declaration
146std::string pp(const pbes_equation& x);
147
152inline
153std::ostream& operator<<(std::ostream& out, const pbes_equation& x)
154{
155 return out << pbes_system::pp(x);
156}
157
159inline void swap(pbes_equation& t1, pbes_equation& t2)
160{
161 t1.swap(t2);
162}
163//--- end generated class pbes_equation ---//
164
165inline bool
167{
168 return x.symbol() == y.symbol() &&
169 x.variable() == y.variable() &&
170 x.formula() == y.formula();
171}
172
173inline bool
175{
176 return !(x == y);
177}
178
181inline
183{
185}
186
187// template function overloads
188std::string pp(const pbes_equation_vector& x);
190std::set<data::variable> find_free_variables(const pbes_system::pbes_equation& x);
191
192} // namespace pbes_system
193
194} // namespace mcrl2
195
196#endif // MCRL2_PBES_PBES_EQUATION_H
A list of aterm objects.
Definition aterm_list.h:24
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.
Definition pbes.cpp:103
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)
Definition find.h:87
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.
Definition pbes.h:325
bool is_well_typed(const pbes_equation &eqn)
Definition pbes.cpp:77
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)
Definition pbes.cpp:37
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462
The class pbes_expression.
Add your file description here.