Line data Source code
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 : //
9 : /// \file mcrl2/pbes/pbes.h
10 : /// \brief The class pbes.
11 :
12 : #ifndef MCRL2_PBES_PBES_H
13 : #define MCRL2_PBES_PBES_H
14 :
15 : #include "mcrl2/data/detail/equal_sorts.h"
16 : #include "mcrl2/pbes/pbes_equation.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : /// \brief The main namespace for the PBES library.
22 : namespace pbes_system
23 : {
24 :
25 : class pbes;
26 : void complete_data_specification(pbes&);
27 :
28 : // template function overloads
29 : std::string pp(const pbes& x);
30 : void normalize_sorts(pbes& x, const data::sort_specification& sortspec);
31 : void translate_user_notation(pbes_system::pbes& x);
32 : std::set<data::sort_expression> find_sort_expressions(const pbes_system::pbes& x);
33 : std::set<data::variable> find_all_variables(const pbes_system::pbes& x);
34 : std::set<data::variable> find_free_variables(const pbes_system::pbes& x);
35 : std::set<data::function_symbol> find_function_symbols(const pbes_system::pbes& x);
36 :
37 : bool is_well_typed_equation(const pbes_equation& eqn,
38 : const std::set<data::sort_expression>& declared_sorts,
39 : const std::set<data::variable>& declared_global_variables,
40 : const data::data_specification& data_spec
41 : );
42 :
43 : bool is_well_typed_pbes(const std::set<data::sort_expression>& declared_sorts,
44 : const std::set<data::variable>& declared_global_variables,
45 : const std::set<data::variable>& occurring_global_variables,
46 : const std::set<propositional_variable>& declared_variables,
47 : const std::set<propositional_variable_instantiation>& occ,
48 : const propositional_variable_instantiation& init,
49 : const data::data_specification& data_spec
50 : );
51 :
52 : atermpp::aterm_appl pbes_to_aterm(const pbes& p);
53 :
54 : /// \brief parameterized boolean equation system
55 : // <PBES> ::= PBES(<DataSpec>, <GlobVarSpec>, <PBEqnSpec>, <PBInit>)
56 : // <PBEqnSpec> ::= PBEqnSpec(<PBEqn>*)
57 : class pbes
58 : {
59 : public:
60 : typedef pbes_equation equation_type;
61 :
62 : protected:
63 : /// \brief The data specification
64 : data::data_specification m_data;
65 :
66 : /// \brief The sequence of pbes equations
67 : std::vector<pbes_equation> m_equations;
68 :
69 : /// \brief The set of global variables
70 : std::set<data::variable> m_global_variables;
71 :
72 : /// \brief The initial state
73 : propositional_variable_instantiation m_initial_state;
74 :
75 : /// \brief Returns the predicate variables appearing in the left hand side of an equation.
76 : /// \return The predicate variables appearing in the left hand side of an equation.
77 284 : std::set<propositional_variable> compute_declared_variables() const
78 : {
79 284 : std::set<propositional_variable> result;
80 1428 : for (const pbes_equation& eqn: equations())
81 : {
82 1144 : result.insert(eqn.variable());
83 : }
84 284 : return result;
85 0 : }
86 :
87 : /// \brief Checks if the propositional variable instantiation v appears with the right type in the
88 : /// sequence of propositional variable declarations [first, last).
89 : /// \param first Start of a sequence of propositional variable declarations
90 : /// \param last End of a sequence of propositional variable declarations
91 : /// \param v A propositional variable instantation
92 : /// \param data_spec A data specification.
93 : /// \return True if the type of \p v is matched correctly
94 : /// \param v A propositional variable instantiation
95 : template <typename Iter>
96 181 : bool is_declared_in(Iter first, Iter last, const propositional_variable_instantiation& v, const data::data_specification& data_spec) const
97 : {
98 196 : for (Iter i = first; i != last; ++i)
99 : {
100 196 : if (i->name() == v.name() && data::detail::equal_sorts(i->parameters(), v.parameters(), data_spec))
101 : {
102 181 : return true;
103 : }
104 : }
105 0 : return false;
106 : }
107 :
108 : public:
109 : /// \brief Constructor.
110 1009 : pbes() = default;
111 :
112 : /// \brief Constructor.
113 : /// \param data A data specification
114 : /// \param equations A sequence of pbes equations
115 : /// \param initial_state A propositional variable instantiation
116 42 : pbes(data::data_specification const& data,
117 : const std::vector<pbes_equation>& equations,
118 : propositional_variable_instantiation initial_state)
119 42 : :
120 42 : m_data(data),
121 42 : m_equations(equations),
122 42 : m_initial_state(initial_state)
123 : {
124 42 : m_global_variables = pbes_system::find_free_variables(*this);
125 42 : assert(core::detail::check_rule_PBES(pbes_to_aterm(*this)));
126 42 : assert(is_well_typed());
127 42 : }
128 :
129 : /// \brief Constructor.
130 : /// \param data A data specification
131 : /// \param equations A sequence of pbes equations
132 : /// \param global_variables A sequence of free variables
133 : /// \param initial_state A propositional variable instantiation
134 141 : pbes(data::data_specification const& data,
135 : const std::set<data::variable>& global_variables,
136 : const std::vector<pbes_equation>& equations,
137 : propositional_variable_instantiation initial_state)
138 141 : :
139 141 : m_data(data),
140 141 : m_equations(equations),
141 141 : m_global_variables(global_variables),
142 141 : m_initial_state(initial_state)
143 : {
144 141 : assert(core::detail::check_rule_PBES(pbes_to_aterm(*this)));
145 141 : assert(is_well_typed());
146 141 : }
147 :
148 : /// \brief Returns the data specification.
149 : /// \return The data specification of the pbes
150 2920 : const data::data_specification& data() const
151 : {
152 2920 : return m_data;
153 : }
154 :
155 : /// \brief Returns the data specification.
156 : /// \return The data specification of the pbes
157 4168 : data::data_specification& data()
158 : {
159 4168 : return m_data;
160 : }
161 :
162 : /// \brief Returns the equations.
163 : /// \return The equations.
164 3618 : const std::vector<pbes_equation>& equations() const
165 : {
166 3618 : return m_equations;
167 : }
168 :
169 : /// \brief Returns the equations.
170 : /// \return The equations.
171 8189 : std::vector<pbes_equation>& equations()
172 : {
173 8189 : return m_equations;
174 : }
175 :
176 : /// \brief Returns the declared free variables of the pbes.
177 : /// \return The declared free variables of the pbes.
178 2263 : const std::set<data::variable>& global_variables() const
179 : {
180 2263 : return m_global_variables;
181 : }
182 :
183 : /// \brief Returns the declared free variables of the pbes.
184 : /// \return The declared free variables of the pbes.
185 1615 : std::set<data::variable>& global_variables()
186 : {
187 1615 : return m_global_variables;
188 : }
189 :
190 : /// \brief Returns the initial state.
191 : /// \return The initial state.
192 1914 : const propositional_variable_instantiation& initial_state() const
193 : {
194 1914 : return m_initial_state;
195 : }
196 :
197 : /// \brief Returns the initial state.
198 : /// \return The initial state.
199 3761 : propositional_variable_instantiation& initial_state()
200 : {
201 3761 : return m_initial_state;
202 : }
203 :
204 : /// \brief Returns the set of binding variables of the pbes.
205 : /// This is the set variables that occur on the left hand side of an equation.
206 : /// \return The set of binding variables of the pbes.
207 204 : std::set<propositional_variable> binding_variables() const
208 : {
209 : using namespace std::rel_ops; // for definition of operator!= in terms of operator==
210 :
211 204 : std::set<propositional_variable> result;
212 796 : for (const pbes_equation& eqn: equations())
213 : {
214 592 : result.insert(eqn.variable());
215 : }
216 204 : return result;
217 0 : }
218 :
219 : /// \brief Returns the set of occurring propositional variable instantiations of the pbes.
220 : /// This is the set of variables that occur in the right hand side of an equation.
221 : /// \return The occurring propositional variable instantiations of the pbes
222 : std::set<propositional_variable_instantiation> occurring_variable_instantiations() const;
223 :
224 : /// \brief Returns the set of occurring propositional variable declarations of the pbes, i.e.
225 : /// the propositional variable declarations that occur in the right hand side of an equation.
226 : /// \return The occurring propositional variable declarations of the pbes
227 205 : std::set<propositional_variable> occurring_variables() const
228 : {
229 205 : std::set<propositional_variable> result;
230 205 : std::set<propositional_variable_instantiation> occ = occurring_variable_instantiations();
231 205 : std::map<core::identifier_string, propositional_variable> declared_variables;
232 800 : for (const pbes_equation& eqn: equations())
233 : {
234 595 : declared_variables[eqn.variable().name()] = eqn.variable();
235 : }
236 1408 : for (const propositional_variable_instantiation& v: occ)
237 : {
238 1203 : result.insert(declared_variables[v.name()]);
239 : }
240 410 : return result;
241 205 : }
242 :
243 : /// \brief True if the pbes is closed
244 : /// \return Returns true if all occurring variables are binding variables, and the initial state variable is a binding variable.
245 181 : bool is_closed() const
246 : {
247 181 : std::set<propositional_variable> bnd = binding_variables();
248 181 : std::set<propositional_variable> occ = occurring_variables();
249 362 : return std::includes(bnd.begin(), bnd.end(), occ.begin(), occ.end()) && is_declared_in(bnd.begin(), bnd.end(), initial_state(), data());
250 181 : }
251 :
252 : /// \brief Checks if the PBES is well typed
253 : /// \return True if
254 : /// <ul>
255 : /// <li>the sorts occurring in the free variables of the equations are declared in the data specification</li>
256 : /// <li>the sorts occurring in the binding variable parameters are declared in the data specification </li>
257 : /// <li>the sorts occurring in the quantifier variables of the equations are declared in the data specification </li>
258 : /// <li>the binding variables of the equations have unique names (well formedness)</li>
259 : /// <li>the global variables occurring in the equations are declared in global_variables()</li>
260 : /// <li>the global variables occurring in the equations with the same name are identical</li>
261 : /// <li>the declared global variables and the quantifier variables occurring in the equations have different names</li>
262 : /// <li>the predicate variable instantiations occurring in the equations match with their declarations</li>
263 : /// <li>the predicate variable instantiation occurring in the initial state matches with the declaration</li>
264 : /// <li>the data specification is well typed</li>
265 : /// </ul>
266 : /// N.B. Conflicts between the types of instantiations and declarations of binding variables are not checked!
267 284 : bool is_well_typed() const
268 : {
269 284 : std::set<data::sort_expression> declared_sorts = data::detail::make_set(data().sorts());
270 284 : const std::set<data::variable>& declared_global_variables = global_variables();
271 284 : std::set<data::variable> occurring_global_variables = pbes_system::find_free_variables(*this);
272 284 : std::set<propositional_variable> declared_variables = compute_declared_variables();
273 284 : std::set<propositional_variable_instantiation> occ = occurring_variable_instantiations();
274 :
275 : // check 1), 4), 5), 6), 8) and 9)
276 284 : if (!is_well_typed_pbes(declared_sorts, declared_global_variables, occurring_global_variables, declared_variables, occ, initial_state(), data()))
277 : {
278 0 : return false;
279 : }
280 :
281 : // check 2), 3) and 7)
282 1428 : for (const pbes_equation& eqn: equations())
283 : {
284 1144 : if (!is_well_typed_equation(eqn, declared_sorts, declared_global_variables, data()))
285 : {
286 0 : return false;
287 : }
288 : }
289 :
290 : // check 10)
291 284 : return data().is_well_typed();
292 284 : }
293 : };
294 :
295 : //--- start generated class pbes ---//
296 : // prototype declaration
297 : std::string pp(const pbes& x);
298 :
299 : /// \\brief Outputs the object to a stream
300 : /// \\param out An output stream
301 : /// \\param x Object x
302 : /// \\return The output stream
303 : inline
304 0 : std::ostream& operator<<(std::ostream& out, const pbes& x)
305 : {
306 0 : return out << pbes_system::pp(x);
307 : }
308 : //--- end generated class pbes ---//
309 :
310 :
311 : /// \brief Adds all sorts that appear in the PBES \a p to the data specification of \a p.
312 : /// \param p a PBES.
313 : inline
314 606 : void complete_data_specification(pbes& p)
315 : {
316 606 : std::set<data::sort_expression> s = pbes_system::find_sort_expressions(p);
317 606 : p.data().add_context_sorts(s);
318 606 : }
319 :
320 : /// \brief Equality operator on PBESs
321 : /// \return True if the PBESs have exactly the same internal representation. Note
322 : /// that this is in general not a very useful test.
323 : // TODO: improve the comparison
324 : inline
325 8 : bool operator==(const pbes& p1, const pbes& p2)
326 : {
327 8 : return pbes_to_aterm(p1) == pbes_to_aterm(p2);
328 : }
329 :
330 : } // namespace pbes_system
331 :
332 : } // namespace mcrl2
333 :
334 : #endif // MCRL2_PBES_PBES_H
|
