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/detail/is_well_typed.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_IS_WELL_TYPED_H
13 : #define MCRL2_PBES_DETAIL_IS_WELL_TYPED_H
14 :
15 : #include "mcrl2/data/detail/data_utility.h"
16 : #include "mcrl2/pbes/traverser.h"
17 : #include <boost/iterator/transform_iterator.hpp>
18 :
19 : namespace mcrl2 {
20 :
21 : namespace pbes_system {
22 :
23 : namespace detail {
24 :
25 : /// Visitor for collecting the quantifier variables that occur in a pbes expression.
26 : struct find_quantifier_variables_traverser: public pbes_expression_traverser<find_quantifier_variables_traverser>
27 : {
28 : typedef pbes_expression_traverser<find_quantifier_variables_traverser> super;
29 : using super::enter;
30 : using super::leave;
31 : using super::apply;
32 :
33 : std::set<data::variable> result;
34 :
35 289 : void enter(const forall& x)
36 : {
37 289 : auto const& v = x.variables();
38 289 : result.insert(v.begin(), v.end());
39 289 : }
40 :
41 563 : void enter(const exists& x)
42 : {
43 563 : auto const& v = x.variables();
44 563 : result.insert(v.begin(), v.end());
45 563 : }
46 : };
47 :
48 : inline
49 1026 : std::set<data::variable> find_quantifier_variables(const pbes_expression& x)
50 : {
51 1026 : find_quantifier_variables_traverser f;
52 1026 : f.apply(x);
53 2052 : return f.result;
54 1026 : }
55 :
56 : /// \brief Visitor for determining if within the scope of a quantifier there are quantifier
57 : /// variables of free variables with the same name.
58 : struct has_quantifier_name_clashes_traverser: public pbes_expression_traverser<has_quantifier_name_clashes_traverser>
59 : {
60 : typedef pbes_expression_traverser<has_quantifier_name_clashes_traverser> super;
61 : using super::enter;
62 : using super::leave;
63 : using super::apply;
64 :
65 : std::vector<data::variable_list> quantifier_stack;
66 : bool result;
67 : data::variable name_clash; // if result is true, then this attribute contains the conflicting variable
68 :
69 0 : has_quantifier_name_clashes_traverser()
70 0 : : result(false)
71 0 : {}
72 :
73 : /// \brief Returns true if the quantifier_stack contains a data variable with the given name
74 : /// \param name A
75 : /// \return True if the quantifier_stack contains a data variable with the given name
76 0 : bool is_in_quantifier_stack(const core::identifier_string& name) const
77 : {
78 0 : for (const data::variable_list& vars: quantifier_stack)
79 : {
80 0 : if (std::find(boost::make_transform_iterator(vars.begin(), data::detail::variable_name()),
81 0 : boost::make_transform_iterator(vars.end() , data::detail::variable_name()),
82 : name
83 0 : ) != boost::make_transform_iterator(vars.end() , data::detail::variable_name())
84 : )
85 : {
86 0 : return true;
87 : }
88 : }
89 0 : return false;
90 : }
91 :
92 : /// \brief Adds variables to the quantifier stack, and adds replacements for the name clashes to replacements.
93 : /// \param variables A sequence of data variables
94 : /// \return The number of replacements that were added.
95 0 : void push(const data::variable_list& variables)
96 : {
97 0 : if (result)
98 : {
99 0 : return;
100 : }
101 0 : for (const data::variable& v: variables)
102 : {
103 0 : if (is_in_quantifier_stack(v.name()))
104 : {
105 0 : result = true;
106 0 : name_clash = v;
107 0 : return;
108 : }
109 : }
110 0 : quantifier_stack.push_back(variables);
111 : }
112 :
113 : /// \brief Pops the quantifier stack
114 0 : void pop()
115 : {
116 0 : if (result)
117 : {
118 0 : return;
119 : }
120 0 : quantifier_stack.pop_back();
121 : }
122 :
123 0 : void enter(const forall& x)
124 : {
125 0 : push(x.variables());
126 0 : }
127 :
128 0 : void leave(const forall&)
129 : {
130 0 : pop();
131 0 : }
132 :
133 0 : void enter(const exists& x)
134 : {
135 0 : push(x.variables());
136 0 : }
137 :
138 0 : void leave(const exists&)
139 : {
140 0 : pop();
141 0 : }
142 : };
143 :
144 : inline
145 : bool has_quantifier_name_clashes(const pbes_expression& x)
146 : {
147 : has_quantifier_name_clashes_traverser f;
148 : f.apply(x);
149 : return f.result;
150 : }
151 :
152 : /// \brief Checks if the equation is well typed
153 : /// \return True if
154 : /// <ul>
155 : /// <li>the binding variable parameters have unique names</li>
156 : /// <li>the names of the quantifier variables in the equation are disjoint with the binding variable parameter names</li>
157 : /// <li>within the scope of a quantifier variable in the formula, no other quantifier variables with the same name may occur</li>
158 : /// </ul>
159 : inline
160 0 : bool is_well_typed(const pbes_equation& eqn)
161 : {
162 : // check 1)
163 0 : if (data::detail::sequence_contains_duplicates(
164 0 : boost::make_transform_iterator(eqn.variable().parameters().begin(), data::detail::variable_name()),
165 0 : boost::make_transform_iterator(eqn.variable().parameters().end() , data::detail::variable_name())
166 : )
167 : )
168 : {
169 0 : mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the names of the binding variable parameters are not unique" << std::endl;
170 0 : return false;
171 : }
172 :
173 : // check 2)
174 0 : std::set<data::variable> qvariables = detail::find_quantifier_variables(eqn.formula());
175 0 : if (data::detail::sequences_do_overlap(
176 0 : boost::make_transform_iterator(eqn.variable().parameters().begin(), data::detail::variable_name()),
177 0 : boost::make_transform_iterator(eqn.variable().parameters().end() , data::detail::variable_name()),
178 : boost::make_transform_iterator(qvariables.begin() , data::detail::variable_name()),
179 : boost::make_transform_iterator(qvariables.end() , data::detail::variable_name())
180 : )
181 : )
182 : {
183 0 : mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the names of the quantifier variables and the names of the binding variable parameters are not disjoint in expression " << pbes_system::pp(eqn.formula()) << std::endl;
184 0 : return false;
185 : }
186 :
187 : // check 3)
188 0 : has_quantifier_name_clashes_traverser nvisitor;
189 0 : nvisitor.apply(eqn.formula());
190 0 : if (nvisitor.result)
191 : {
192 0 : mCRL2log(log::error) << "pbes_equation::is_well_typed() failed: the quantifier variable " << nvisitor.name_clash << " occurs within the scope of a quantifier variable with the same name." << std::endl;
193 0 : return false;
194 : }
195 :
196 0 : return true;
197 0 : }
198 :
199 : /// \brief Checks if the propositional variable instantiation v has a conflict with the
200 : /// sequence of propositional variable declarations [first, last).
201 : /// \param first Start of a sequence of propositional variable declarations
202 : /// \param last End of a sequence of propositional variable declarations
203 : /// \return True if a conflict has been detected
204 : /// \param v A propositional variable instantiation
205 : template <typename Iter>
206 2565 : bool has_conflicting_type(Iter first, Iter last, const propositional_variable_instantiation& v, const data::data_specification& data_spec)
207 : {
208 39298 : for (Iter i = first; i != last; ++i)
209 : {
210 36733 : if (i->name() == v.name() && !data::detail::equal_sorts(i->parameters(), v.parameters(), data_spec))
211 : {
212 0 : return true;
213 : }
214 : }
215 2565 : return false;
216 : }
217 :
218 : inline
219 1026 : bool is_well_typed_equation(const pbes_equation& eqn,
220 : const std::set<data::sort_expression>& declared_sorts,
221 : const std::set<data::variable>& declared_global_variables,
222 : const data::data_specification& data_spec
223 : )
224 : {
225 : // check 2)
226 1026 : const data::variable_list& variables = eqn.variable().parameters();
227 1026 : if (!data::detail::check_sorts(
228 1026 : boost::make_transform_iterator(variables.begin(), data::detail::sort_of_variable()),
229 2052 : boost::make_transform_iterator(variables.end() , data::detail::sort_of_variable()),
230 : declared_sorts
231 : )
232 : )
233 : {
234 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the binding variable "
235 0 : << eqn.variable()
236 0 : << " are not declared in the data specification "
237 0 : << data_spec
238 0 : << std::endl;
239 0 : return false;
240 : }
241 :
242 : // check 3)
243 1026 : std::set<data::variable> quantifier_variables = detail::find_quantifier_variables(eqn.formula());
244 1026 : if (!data::detail::check_sorts(
245 : boost::make_transform_iterator(quantifier_variables.begin(), data::detail::sort_of_variable()),
246 : boost::make_transform_iterator(quantifier_variables.end() , data::detail::sort_of_variable()),
247 : declared_sorts
248 : )
249 : )
250 : {
251 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the quantifier variables "
252 0 : << data::pp(quantifier_variables)
253 0 : << " are not declared in the data specification "
254 0 : << data_spec
255 0 : << std::endl;
256 0 : return false;
257 : }
258 :
259 : // check 7)
260 1026 : if (!utilities::detail::set_intersection(declared_global_variables, quantifier_variables).empty())
261 : {
262 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: the declared free variables and the quantifier variables have collisions" << std::endl;
263 0 : return false;
264 : }
265 1026 : return true;
266 1026 : }
267 :
268 : inline
269 280 : bool is_well_typed_pbes(const std::set<data::sort_expression>& declared_sorts,
270 : const std::set<data::variable>& declared_global_variables,
271 : const std::set<data::variable>& occurring_global_variables,
272 : const std::set<propositional_variable>& declared_variables,
273 : const std::set<propositional_variable_instantiation>& occ,
274 : const propositional_variable_instantiation& init,
275 : const data::data_specification& data_spec
276 : )
277 : {
278 : // check 1)
279 280 : if (!data::detail::check_sorts(
280 : boost::make_transform_iterator(declared_global_variables.begin(), data::detail::sort_of_variable()),
281 : boost::make_transform_iterator(declared_global_variables.end() , data::detail::sort_of_variable()),
282 : declared_sorts
283 : )
284 : )
285 : {
286 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: some of the sorts of the free variables "
287 0 : << data::pp(declared_global_variables)
288 0 : << " are not declared in the data specification "
289 0 : << data_spec
290 0 : << std::endl;
291 0 : return false;
292 : }
293 :
294 : // check 4)
295 1026 : auto propvar_name = [](const propositional_variable& x) { return x.name(); };
296 280 : if (data::detail::sequence_contains_duplicates(
297 : boost::make_transform_iterator(declared_variables.begin(), propvar_name),
298 : boost::make_transform_iterator(declared_variables.end() , propvar_name)
299 : )
300 : )
301 : {
302 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: the names of the binding variables are not unique" << std::endl;
303 0 : return false;
304 : }
305 :
306 : // check 5)
307 280 : if (!std::includes(declared_global_variables.begin(),
308 : declared_global_variables.end(),
309 : occurring_global_variables.begin(),
310 : occurring_global_variables.end()
311 : )
312 : )
313 : {
314 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: not all of the free variables are declared\n"
315 0 : << "free variables: " << data::pp(occurring_global_variables) << "\n"
316 0 : << "declared free variables: " << data::pp(declared_global_variables)
317 0 : << std::endl;
318 0 : return false;
319 : }
320 :
321 : // check 6)
322 280 : if (data::detail::sequence_contains_duplicates(
323 : boost::make_transform_iterator(occurring_global_variables.begin(), data::detail::variable_name()),
324 : boost::make_transform_iterator(occurring_global_variables.end() , data::detail::variable_name())
325 : )
326 : )
327 : {
328 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: the free variables have no unique names" << std::endl;
329 0 : return false;
330 : }
331 :
332 : // check 8)
333 2565 : for (const propositional_variable_instantiation& v: occ)
334 : {
335 2285 : if (has_conflicting_type(declared_variables.begin(), declared_variables.end(), v, data_spec))
336 : {
337 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: the occurring variable " << pbes_system::pp(v) << " conflicts with its declaration!" << std::endl;
338 0 : return false;
339 : }
340 : }
341 :
342 : // check 9)
343 280 : if (has_conflicting_type(declared_variables.begin(), declared_variables.end(), init, data_spec))
344 : {
345 0 : mCRL2log(log::error) << "pbes::is_well_typed() failed: the initial state " << pbes_system::pp(init) << " conflicts with its declaration!" << std::endl;
346 0 : return false;
347 : }
348 280 : return true;
349 : }
350 :
351 : } // namespace detail
352 :
353 : } // namespace pbes_system
354 :
355 : } // namespace mcrl2
356 :
357 : #endif // MCRL2_PBES_DETAIL_IS_WELL_TYPED_H
|