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/modal_formula/typecheck.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_TYPECHECK_H
13 : #define MCRL2_MODAL_FORMULA_TYPECHECK_H
14 :
15 : #include "mcrl2/lps/typecheck.h"
16 : #include "mcrl2/modal_formula/detail/state_variable_context.h"
17 : #include "mcrl2/modal_formula/is_monotonous.h"
18 : #include "mcrl2/modal_formula/normalize_sorts.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace action_formulas
24 : {
25 :
26 : namespace detail
27 : {
28 :
29 : struct typecheck_builder: public action_formula_builder<typecheck_builder>
30 : {
31 : typedef action_formula_builder<typecheck_builder> super;
32 : using super::apply;
33 :
34 : data::data_type_checker& m_data_type_checker;
35 : data::detail::variable_context m_variable_context;
36 : const process::detail::action_context& m_action_context;
37 :
38 230 : typecheck_builder(data::data_type_checker& data_typechecker,
39 : const data::detail::variable_context& variable_context,
40 : const process::detail::action_context& action_context
41 : )
42 230 : : m_data_type_checker(data_typechecker),
43 230 : m_variable_context(variable_context),
44 230 : m_action_context(action_context)
45 230 : {}
46 :
47 171 : process::action typecheck_action(const core::identifier_string& name, const data::data_expression_list& parameters)
48 : {
49 171 : return process::typecheck_action(name, parameters, m_data_type_checker, m_variable_context, m_action_context);
50 : }
51 :
52 : template <class T>
53 0 : void apply(T& result, const data::data_expression& x)
54 : {
55 0 : result = m_data_type_checker.typecheck_data_expression(x, data::sort_bool::bool_(), m_variable_context);
56 0 : }
57 :
58 : template <class T>
59 0 : void apply(T& result, const action_formulas::at& x)
60 : {
61 0 : data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
62 0 : make_at(result, [&](action_formula& r){ (*this).apply(r, x.operand()); }, new_time);
63 0 : }
64 :
65 : template <class T>
66 179 : void apply(T& result, const process::untyped_multi_action& x)
67 : {
68 : // If x has size 1, first try to type check it as a data expression.
69 179 : if (x.actions().size() == 1)
70 : {
71 171 : const data::untyped_data_parameter& y = x.actions().front();
72 : try
73 : {
74 171 : result = data::typecheck_untyped_data_parameter(m_data_type_checker, y.name(), y.arguments(), data::sort_bool::bool_(), m_variable_context);
75 0 : return;
76 : }
77 171 : catch (mcrl2::runtime_error& )
78 : {
79 : // skip
80 : }
81 : }
82 : // Type check it as a multi action
83 179 : process::action_list new_arguments;
84 529 : for (const data::untyped_data_parameter& a: x.actions())
85 : {
86 171 : new_arguments.push_front(typecheck_action(a.name(), a.arguments()));
87 : }
88 179 : new_arguments = atermpp::reverse(new_arguments);
89 179 : result = action_formulas::multi_action(new_arguments);
90 179 : }
91 :
92 : template <class T>
93 3 : void apply(T& result, const action_formulas::forall& x)
94 : {
95 : try
96 : {
97 3 : auto m_variable_context_copy = m_variable_context;
98 3 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
99 3 : action_formula body;
100 3 : (*this).apply(body, x.body());
101 3 : m_variable_context = m_variable_context_copy;
102 3 : result = forall(x.variables(), body);
103 3 : }
104 0 : catch (mcrl2::runtime_error& e)
105 : {
106 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + action_formulas::pp(x));
107 : }
108 3 : }
109 :
110 : template <class T>
111 2 : void apply(T& result, const action_formulas::exists& x)
112 : {
113 : try
114 : {
115 2 : auto m_variable_context_copy = m_variable_context;
116 2 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
117 2 : action_formula body;
118 2 : (*this).apply(body, x.body());
119 2 : m_variable_context = m_variable_context_copy;
120 2 : result = exists(x.variables(), body);
121 2 : }
122 0 : catch (mcrl2::runtime_error& e)
123 : {
124 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + action_formulas::pp(x));
125 : }
126 2 : }
127 : };
128 :
129 : inline
130 230 : typecheck_builder make_typecheck_builder(
131 : data::data_type_checker& data_typechecker,
132 : const data::detail::variable_context& variables,
133 : const process::detail::action_context& actions
134 : )
135 : {
136 230 : return typecheck_builder(data_typechecker, variables, actions);
137 : }
138 :
139 : } // namespace detail
140 :
141 : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
142 : action_formula typecheck_action_formula(const action_formula& x,
143 : const data::data_specification& dataspec,
144 : const VariableContainer& variables,
145 : const ActionLabelContainer& actions
146 : )
147 : {
148 : data::data_type_checker data_typechecker(dataspec);
149 : data::detail::variable_context variable_context;
150 : variable_context.add_context_variables(variables, data_typechecker);
151 : process::detail::action_context action_context;
152 : action_context.add_context_action_labels(actions, data_typechecker);
153 : action_formula result;
154 : detail::make_typecheck_builder(data_typechecker, variable_context, action_context).
155 : apply(result, action_formulas::normalize_sorts(x, data_typechecker.typechecked_data_specification()));
156 : return result;
157 : }
158 :
159 : inline
160 : action_formula typecheck_action_formula(const action_formula& x, const lps::stochastic_specification& lpsspec)
161 : {
162 : return typecheck_action_formula(x, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
163 : }
164 :
165 : } // namespace action_formulas
166 :
167 : namespace regular_formulas
168 : {
169 :
170 : namespace detail
171 : {
172 :
173 : struct typecheck_builder: public regular_formula_builder<typecheck_builder>
174 : {
175 : typedef regular_formula_builder<typecheck_builder> super;
176 : using super::apply;
177 :
178 : data::data_type_checker& m_data_type_checker;
179 : const data::detail::variable_context& m_variable_context;
180 : const process::detail::action_context& m_action_context;
181 :
182 225 : typecheck_builder(data::data_type_checker& data_typechecker,
183 : const data::detail::variable_context& variables,
184 : const process::detail::action_context& actions
185 : )
186 225 : : m_data_type_checker(data_typechecker),
187 225 : m_variable_context(variables),
188 225 : m_action_context(actions)
189 225 : {}
190 :
191 0 : data::data_expression make_fbag_union(const data::data_expression& left, const data::data_expression& right)
192 : {
193 0 : const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
194 0 : const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
195 0 : return data::sort_fbag::union_(cs.element_sort(), left, right);
196 0 : }
197 :
198 0 : data::data_expression make_bag_union(const data::data_expression& left, const data::data_expression& right)
199 : {
200 0 : const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
201 0 : const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
202 0 : return data::sort_bag::union_(cs.element_sort(), left, right);
203 0 : }
204 :
205 0 : data::data_expression make_fset_union(const data::data_expression& left, const data::data_expression& right)
206 : {
207 0 : const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
208 0 : const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
209 0 : return data::sort_fset::union_(cs.element_sort(), left, right);
210 0 : }
211 :
212 0 : data::data_expression make_set_union(const data::data_expression& left, const data::data_expression& right)
213 : {
214 0 : const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
215 0 : const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
216 0 : return data::sort_set::union_(cs.element_sort(), left, right);
217 0 : }
218 :
219 0 : data::data_expression make_plus(const data::data_expression& left, const data::data_expression& right)
220 : {
221 0 : if (data::sort_real::is_real(left.sort()) || data::sort_real::is_real(right.sort()))
222 : {
223 0 : return data::sort_real::plus(left, right);
224 : }
225 0 : else if (data::sort_int::is_int(left.sort()) || data::sort_int::is_int(right.sort()))
226 : {
227 0 : return data::sort_int::plus(left, right);
228 : }
229 0 : else if (data::sort_nat::is_nat(left.sort()) || data::sort_nat::is_nat(right.sort()))
230 : {
231 0 : return data::sort_nat::plus(left, right);
232 : }
233 0 : else if (data::sort_pos::is_pos(left.sort()) || data::sort_pos::is_pos(right.sort()))
234 : {
235 0 : return data::sort_pos::plus(left, right);
236 : }
237 0 : else if (data::sort_bag::is_union_application(left) || data::sort_bag::is_union_application(right))
238 : {
239 0 : return make_bag_union(left, right);
240 : }
241 0 : else if (data::sort_fbag::is_union_application(left) || data::sort_fbag::is_union_application(right))
242 : {
243 0 : return make_fbag_union(left, right);
244 : }
245 0 : else if (data::sort_set::is_union_application(left) || data::sort_set::is_union_application(right))
246 : {
247 0 : return make_set_union(left, right);
248 : }
249 0 : else if (data::sort_fset::is_union_application(left) || data::sort_fset::is_union_application(right))
250 : {
251 0 : return make_fset_union(left, right);
252 : }
253 0 : throw mcrl2::runtime_error("could not typecheck " + data::pp(left) + " + " + data::pp(right));
254 : }
255 :
256 0 : data::data_expression make_element_at(const data::data_expression& left, const data::data_expression& right) const
257 : {
258 0 : const data::sort_expression& s = atermpp::down_cast<data::application>(left).head().sort();
259 0 : const data::container_sort& cs = atermpp::down_cast<data::container_sort>(s);
260 0 : return data::sort_list::element_at(cs.element_sort(), left, right);
261 0 : }
262 :
263 : template <class T>
264 5 : void apply(T& result, const regular_formulas::untyped_regular_formula& x)
265 : {
266 5 : regular_formula left;
267 5 : (*this).apply(left, x.left());
268 5 : regular_formula right;
269 5 : (*this).apply(right, x.right());
270 5 : if (data::is_data_expression(left) && data::is_data_expression(right))
271 : {
272 0 : if (x.name() == core::identifier_string("."))
273 : {
274 0 : result = make_element_at(atermpp::down_cast<data::data_expression>(left), atermpp::down_cast<data::data_expression>(right));
275 : }
276 : else
277 : {
278 0 : result = make_plus(atermpp::down_cast<data::data_expression>(left), atermpp::down_cast<data::data_expression>(right));
279 : }
280 : }
281 : else
282 : {
283 5 : if (x.name() == core::identifier_string("."))
284 : {
285 3 : result = seq(left, right);
286 : }
287 : else
288 : {
289 2 : result = alt(left, right);
290 : }
291 : }
292 5 : }
293 :
294 : /* Has to be a regular formula as result.... */
295 : // template <class T>A
296 230 : void apply(regular_formula& result, const action_formulas::action_formula& x)
297 : {
298 230 : action_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(result, x);
299 230 : }
300 : };
301 :
302 : inline
303 225 : typecheck_builder make_typecheck_builder(
304 : data::data_type_checker& data_typechecker,
305 : const data::detail::variable_context& variables,
306 : const process::detail::action_context& actions
307 : )
308 : {
309 225 : return typecheck_builder(data_typechecker, variables, actions);
310 : }
311 :
312 : } // namespace detail
313 :
314 : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
315 : regular_formula typecheck_regular_formula(const regular_formula& x,
316 : const data::data_specification& dataspec,
317 : const VariableContainer& variables,
318 : const ActionLabelContainer& actions
319 : )
320 : {
321 : data::data_type_checker data_typechecker(dataspec);
322 : data::detail::variable_context variable_context;
323 : variable_context.add_context_variables(variables, data_typechecker);
324 : process::detail::action_context action_context;
325 : action_context.add_context_action_labels(actions, data_typechecker);
326 : regular_formula result;
327 : detail::make_typecheck_builder(data_typechecker, variable_context, action_context).
328 : apply(result, regular_formulas::normalize_sorts(x, data_typechecker.typechecked_data_specification()));
329 : return result;
330 : }
331 :
332 : inline
333 : regular_formula typecheck_regular_formula(const regular_formula& x, const lps::stochastic_specification& lpsspec)
334 : {
335 : return typecheck_regular_formula(x, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
336 : }
337 :
338 : } // namespace regular_formulas
339 :
340 : namespace state_formulas
341 : {
342 :
343 : namespace detail
344 : {
345 :
346 : struct typecheck_builder: public state_formula_builder<typecheck_builder>
347 : {
348 : typedef state_formula_builder<typecheck_builder> super;
349 : using super::apply;
350 :
351 : data::data_type_checker& m_data_type_checker;
352 : data::detail::variable_context m_variable_context;
353 : const process::detail::action_context& m_action_context;
354 : detail::state_variable_context m_state_variable_context;
355 : const bool m_formula_is_quantitative; // If true, allow real values, otherwise restrict to a boolean formula.
356 :
357 179 : typecheck_builder(data::data_type_checker& data_typechecker,
358 : const data::detail::variable_context& variable_context,
359 : const process::detail::action_context& action_context,
360 : const detail::state_variable_context& state_variable_context,
361 : const bool formula_is_quantitative
362 : )
363 179 : : m_data_type_checker(data_typechecker),
364 179 : m_variable_context(variable_context),
365 179 : m_action_context(action_context),
366 179 : m_state_variable_context(state_variable_context),
367 179 : m_formula_is_quantitative(formula_is_quantitative)
368 179 : {}
369 :
370 : template <class T>
371 26 : void apply(T& result, const data::data_expression& x)
372 : {
373 26 : if (m_formula_is_quantitative)
374 : {
375 : try
376 : {
377 1 : result = m_data_type_checker.typecheck_data_expression(x, data::sort_real::real_(), m_variable_context);
378 : }
379 0 : catch (mcrl2::runtime_error& e1)
380 : {
381 : try
382 : {
383 0 : result = m_data_type_checker.typecheck_data_expression(x, data::sort_bool::bool_(), m_variable_context);
384 : }
385 0 : catch (mcrl2::runtime_error& e2)
386 : {
387 0 : throw mcrl2::runtime_error("Fail to type data expression as bool or real: " + pp(x) + ".\n" +
388 0 : e1.what() + "\n" +
389 0 : e2.what());
390 : }
391 : }
392 : }
393 : else
394 : {
395 25 : result = m_data_type_checker.typecheck_data_expression(x, data::sort_bool::bool_(), m_variable_context);
396 : }
397 26 : }
398 :
399 : template <class T>
400 19 : void apply(T& result, const state_formulas::forall& x)
401 : {
402 19 : if (m_formula_is_quantitative)
403 : {
404 0 : throw mcrl2::runtime_error("Forall is not allowed to capture values in a quantitative modal formula " + state_formulas::pp(x) + ". Use inf for infimum instead. ");
405 : }
406 : else
407 : {
408 : try
409 : {
410 19 : auto m_variable_context_copy = m_variable_context;
411 19 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
412 19 : state_formula body;
413 19 : (*this).apply(body, x.body());
414 19 : m_variable_context = m_variable_context_copy;
415 19 : result = forall(x.variables(), body);
416 19 : }
417 0 : catch (mcrl2::runtime_error& e)
418 : {
419 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
420 : }
421 : }
422 19 : }
423 :
424 : template <class T>
425 8 : void apply(T& result, const state_formulas::exists& x)
426 : {
427 8 : if (m_formula_is_quantitative)
428 : {
429 0 : throw mcrl2::runtime_error("Exists is not allowed to capture values in a quantitative modal formula " + state_formulas::pp(x) + ". Use sup for supremum instead. ");
430 : }
431 : else
432 : {
433 : try
434 : {
435 8 : auto m_variable_context_copy = m_variable_context;
436 8 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
437 8 : state_formula body;
438 8 : (*this).apply(body, x.body());
439 8 : m_variable_context = m_variable_context_copy;
440 8 : result = exists(x.variables(), body);
441 8 : }
442 0 : catch (mcrl2::runtime_error& e)
443 : {
444 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
445 : }
446 : }
447 8 : }
448 :
449 : template <class T>
450 2 : void apply(T& result, const state_formulas::infimum& x)
451 : {
452 2 : if (!m_formula_is_quantitative)
453 : {
454 0 : throw mcrl2::runtime_error("Infimum is not allowed in an ordinary, non quantitative modal formula " + state_formulas::pp(x) + ". Use forall instead. ");
455 : }
456 : else
457 : {
458 : try
459 : {
460 2 : auto m_variable_context_copy = m_variable_context;
461 2 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
462 2 : state_formula body;
463 2 : (*this).apply(body, x.body());
464 2 : m_variable_context = m_variable_context_copy;
465 2 : result = infimum(x.variables(), body);
466 2 : }
467 0 : catch (mcrl2::runtime_error& e)
468 : {
469 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
470 : }
471 : }
472 2 : }
473 :
474 : template <class T>
475 1 : void apply(T& result, const state_formulas::supremum& x)
476 : {
477 1 : if (!m_formula_is_quantitative)
478 : {
479 0 : throw mcrl2::runtime_error("Supremum is not allowed in an ordinary, non quantitative modal formula " + state_formulas::pp(x) + ". Use exists instead. ");
480 : }
481 : else
482 : {
483 : try
484 : {
485 1 : auto m_variable_context_copy = m_variable_context;
486 1 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
487 1 : state_formula body;
488 1 : (*this).apply(body, x.body());
489 1 : m_variable_context = m_variable_context_copy;
490 1 : result = supremum(x.variables(), body);
491 1 : }
492 0 : catch (mcrl2::runtime_error& e)
493 : {
494 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
495 : }
496 : }
497 1 : }
498 :
499 : template <class T>
500 1 : void apply(T& result, const state_formulas::sum& x)
501 : {
502 1 : if (!m_formula_is_quantitative)
503 : {
504 0 : throw mcrl2::runtime_error("Sum is not allowed in an ordinary, non quantitative modal formula " + state_formulas::pp(x) + ". ");
505 : }
506 : else
507 : {
508 : try
509 : {
510 1 : auto m_variable_context_copy = m_variable_context;
511 1 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
512 1 : state_formula body;
513 1 : (*this).apply(body, x.body());
514 1 : m_variable_context = m_variable_context_copy;
515 1 : result = sum(x.variables(), body);
516 1 : }
517 0 : catch (mcrl2::runtime_error& e)
518 : {
519 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + state_formulas::pp(x));
520 : }
521 : }
522 1 : }
523 :
524 : template <class T>
525 88 : void apply(T& result, const state_formulas::may& x)
526 : {
527 88 : regular_formulas::regular_formula formula;
528 88 : regular_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(formula, x.formula());
529 88 : state_formula operand;
530 88 : (*this).apply(operand, x.operand());
531 88 : make_may(result, formula, operand);
532 88 : }
533 :
534 : template <class T>
535 137 : void apply(T& result, const state_formulas::must& x)
536 : {
537 137 : regular_formulas::regular_formula formula;
538 137 : regular_formulas::detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context).apply(formula, x.formula());
539 137 : state_formula operand;
540 137 : (*this).apply(operand, x.operand());
541 134 : make_must(result, formula, operand);
542 140 : }
543 :
544 : template <class T>
545 3 : void apply(T& result, const state_formulas::delay_timed& x)
546 : {
547 3 : data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
548 3 : make_delay_timed(result, new_time);
549 3 : }
550 :
551 : template <class T>
552 1 : void apply(T& result, const state_formulas::yaled_timed& x)
553 : {
554 1 : data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
555 1 : make_yaled_timed(result, new_time);
556 1 : }
557 :
558 143 : state_formula apply_untyped_parameter(const core::identifier_string& name, const data::data_expression_list& arguments)
559 : {
560 143 : data::sort_expression_list expected_sorts = m_state_variable_context.matching_state_variable_sorts(name, arguments);
561 142 : data::data_expression_list new_arguments;
562 142 : auto q1 = expected_sorts.begin();
563 142 : auto q2 = arguments.begin();
564 150 : for (; q1 != expected_sorts.end(); ++q1, ++q2)
565 : {
566 8 : new_arguments.push_front(m_data_type_checker.typecheck_data_expression(*q2, *q1, m_variable_context));
567 : }
568 142 : new_arguments = atermpp::reverse(new_arguments);
569 284 : return state_formulas::variable(name, new_arguments);
570 142 : }
571 :
572 : template <class T>
573 0 : void apply(T& result, const state_formulas::variable& x)
574 : {
575 0 : result = apply_untyped_parameter(x.name(), x.arguments());
576 0 : }
577 :
578 : template <class T>
579 143 : void apply(T& result, const data::untyped_data_parameter& x)
580 : {
581 143 : result = apply_untyped_parameter(x.name(), x.arguments());
582 142 : }
583 :
584 168 : data::variable_list assignment_variables(const data::assignment_list& x) const
585 : {
586 168 : std::vector<data::variable> result;
587 183 : for (const data::assignment& a: x)
588 : {
589 15 : result.push_back(a.lhs());
590 : }
591 336 : return data::variable_list(result.begin(), result.end());
592 168 : }
593 :
594 : template <typename MuNuFormula>
595 168 : state_formula apply_mu_nu(const MuNuFormula& x, bool is_mu)
596 : {
597 168 : data::assignment_list new_assignments = m_data_type_checker.typecheck_assignment_list(x.assignments(), m_variable_context);
598 :
599 : // add the assignment variables to the context
600 168 : auto m_variable_context_copy = m_variable_context;
601 168 : data::variable_list x_variables = assignment_variables(x.assignments());
602 168 : m_variable_context.add_context_variables(x_variables, m_data_type_checker);
603 :
604 : // add x to the state variable context
605 168 : auto m_state_variable_context_copy = m_state_variable_context;
606 168 : m_state_variable_context.add_state_variable(x.name(), x_variables, m_data_type_checker);
607 :
608 : // typecheck the operand
609 168 : state_formula new_operand;
610 168 : (*this).apply(new_operand, x.operand());
611 :
612 : // restore the context
613 166 : m_variable_context = m_variable_context_copy;
614 166 : m_state_variable_context = m_state_variable_context_copy;
615 :
616 166 : if (is_mu)
617 : {
618 99 : return mu(x.name(), new_assignments, new_operand);
619 : }
620 : else
621 : {
622 67 : return nu(x.name(), new_assignments, new_operand);
623 : }
624 176 : }
625 :
626 : template <class T>
627 68 : void apply(T& result, const state_formulas::nu& x)
628 : {
629 68 : result = apply_mu_nu(x, false);
630 67 : }
631 :
632 : template <class T>
633 100 : void apply(T& result, const state_formulas::mu& x)
634 : {
635 100 : result = apply_mu_nu(x, true);
636 99 : }
637 :
638 : template <class T>
639 36 : void apply(T& result, const state_formulas::not_& x)
640 : {
641 36 : if (m_formula_is_quantitative)
642 : {
643 0 : throw mcrl2::runtime_error("No ! allowed in a quantitative modal formula " + state_formulas::pp(x) + ".");
644 : }
645 : else
646 : {
647 36 : apply(result, static_cast<not_>(x).operand());
648 36 : make_not_(result, result);
649 : }
650 36 : }
651 :
652 : template <class T>
653 0 : void apply(T& result, const state_formulas::minus& x)
654 : {
655 0 : if (!m_formula_is_quantitative)
656 : {
657 0 : throw mcrl2::runtime_error("No unary minus (-) allowed in a boolean modal formula " + state_formulas::pp(x) + ".");
658 : }
659 : else
660 : {
661 0 : apply(result, static_cast<minus>(x).operand());
662 0 : make_minus(result, result);
663 : }
664 0 : }
665 :
666 : template <class T>
667 0 : void apply(T& result, const state_formulas::plus& x)
668 : {
669 0 : if (!m_formula_is_quantitative)
670 : {
671 0 : throw mcrl2::runtime_error("No addition (+) allowed in a boolean modal formula " + state_formulas::pp(x) + ".");
672 : }
673 : else
674 : {
675 0 : apply(result, static_cast<plus>(x).left());
676 0 : state_formula rhs;
677 0 : apply(rhs, static_cast<plus>(x).right());
678 0 : make_plus(result, result, rhs);
679 0 : }
680 0 : }
681 :
682 : template <class T>
683 1 : void apply(T& result, const state_formulas::const_multiply& x)
684 : {
685 1 : if (!m_formula_is_quantitative)
686 : {
687 0 : throw mcrl2::runtime_error("No multiplication with a constant allowed in a boolean modal formula " + state_formulas::pp(x) + ".");
688 : }
689 : else
690 : {
691 1 : data::data_expression constant = m_data_type_checker.typecheck_data_expression(static_cast<const_multiply>(x).left(), data::sort_real::real_(), m_variable_context);
692 1 : state_formula rhs;
693 1 : apply(rhs, static_cast<const_multiply>(x).right());
694 1 : make_const_multiply(result, constant, rhs);
695 1 : }
696 1 : }
697 :
698 : template <class T>
699 1 : void apply(T& result, const state_formulas::const_multiply_alt& x)
700 : {
701 1 : if (!m_formula_is_quantitative)
702 : {
703 0 : throw mcrl2::runtime_error("No multiplication with a constant allowed in a boolean modal formula " + state_formulas::pp(x) + ".");
704 : }
705 : else
706 : {
707 1 : state_formula lhs;
708 1 : apply(lhs, static_cast<const_multiply_alt>(x).left());
709 1 : data::data_expression constant = m_data_type_checker.typecheck_data_expression(static_cast<const_multiply_alt>(x).right(), data::sort_real::real_(), m_variable_context);
710 1 : make_const_multiply_alt(result, lhs, constant);
711 1 : }
712 1 : }
713 : };
714 :
715 : inline
716 179 : typecheck_builder make_typecheck_builder(
717 : data::data_type_checker& data_typechecker,
718 : const data::detail::variable_context& variable_context,
719 : const process::detail::action_context& action_context,
720 : const detail::state_variable_context& state_variable_context,
721 : const bool formula_is_quantitative
722 : )
723 : {
724 179 : return typecheck_builder(data_typechecker, variable_context, action_context, state_variable_context, formula_is_quantitative);
725 : }
726 :
727 : } // namespace detail
728 :
729 : class state_formula_type_checker
730 : {
731 : protected:
732 : data::data_type_checker m_data_type_checker;
733 : data::detail::variable_context m_variable_context;
734 : process::detail::action_context m_action_context;
735 : detail::state_variable_context m_state_variable_context;
736 : const bool m_formula_is_quantitative;
737 :
738 : public:
739 : /** \brief Constructor for a state_formula type checker.
740 : * \param[in] dataspec The data specification against which state formulas are checked.
741 : * \param[in] action_labels The data labels that can occur in a state formula.
742 : * \param[in] variables A container containing variables that can occur in state formulas.
743 : **/
744 : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
745 179 : state_formula_type_checker(const data::data_specification& dataspec,
746 : const bool formula_is_quantitative,
747 : const ActionLabelContainer& action_labels = ActionLabelContainer(),
748 : const VariableContainer& variables = VariableContainer()
749 : )
750 179 : : m_data_type_checker(dataspec),
751 179 : m_formula_is_quantitative(formula_is_quantitative)
752 : {
753 179 : m_variable_context.add_context_variables(variables, m_data_type_checker);
754 179 : m_action_context.add_context_action_labels(action_labels, m_data_type_checker);
755 179 : }
756 :
757 : //check correctness of the state formula as follows:
758 : //1) determine the types of actions according to the definitions
759 : // in spec
760 : //2) determine the types of data expressions according to the
761 : // definitions in spec
762 : //3) check for name conflicts of data variable declarations in
763 : // forall, exists, mu and nu quantifiers
764 : //4) check for monotonicity of fixpoint variables
765 179 : state_formula typecheck_state_formula(const state_formula& x)
766 : {
767 179 : mCRL2log(log::verbose) << "type checking state formula..." << std::endl;
768 179 : state_formula result;
769 181 : detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_action_context, m_state_variable_context, m_formula_is_quantitative).
770 180 : apply(result, state_formulas::normalize_sorts(x, m_data_type_checker.typechecked_data_specification()));
771 178 : return result;
772 1 : }
773 : };
774 :
775 : /** \brief Type check a state formula.
776 : * Throws an exception if something went wrong.
777 : * \param[in] x A state formula that has not been type checked.
778 : * \param[in] dataspec The data specification against which the formulas is checked.
779 : * \param[in] action_labels A declaration of action labels that can be used in the state formulas.
780 : * \param[in] variables A container with global data variables.
781 : * \post formula is type checked.
782 : **/
783 : template <typename VariableContainer, typename ActionLabelContainer>
784 179 : state_formula typecheck_state_formula(const state_formula& x,
785 : const bool formula_is_quantitative,
786 : const data::data_specification& dataspec = data::data_specification(),
787 : const ActionLabelContainer& action_labels = ActionLabelContainer(),
788 : const VariableContainer& variables = VariableContainer()
789 : )
790 : {
791 : try
792 : {
793 179 : state_formula_type_checker type_checker(dataspec, formula_is_quantitative, action_labels, variables);
794 357 : return type_checker.typecheck_state_formula(x);
795 179 : }
796 2 : catch (mcrl2::runtime_error& e)
797 : {
798 1 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula " + state_formulas::pp(x));
799 : }
800 : }
801 :
802 : /** \brief Type check a state formula.
803 : * Throws an exception if something went wrong.
804 : * \param[in] x A state formula that has not been type checked.
805 : * \param[in] lpsspec A linear process specifications containing data, action and global variable declarations
806 : * to be used when typechecking the formula.
807 : * \post formula is type checked.
808 : **/
809 : inline
810 174 : state_formula typecheck_state_formula(const state_formula& x,
811 : const lps::stochastic_specification& lpsspec,
812 : const bool formula_is_quantitative
813 : )
814 : {
815 174 : return typecheck_state_formula(x, formula_is_quantitative, lpsspec.data(), lpsspec.action_labels(), lpsspec.global_variables());
816 : }
817 :
818 : /// \brief Typecheck the state formula specification formspec. It is assumed that the formula is self contained,
819 : /// i.e. all actions and sorts must be declared.
820 : inline
821 : void typecheck_state_formula_specification(state_formula_specification& formspec, const bool formula_is_quantitative)
822 : {
823 : try
824 : {
825 : data::data_type_checker checker(formspec.data());
826 : data::data_specification dataspec = checker.typechecked_data_specification();
827 : state_formulas::normalize_sorts(formspec, dataspec);
828 : state_formula_type_checker type_checker(dataspec, formula_is_quantitative, formspec.action_labels(), std::vector<data::variable>());
829 : formspec.formula() = type_checker.typecheck_state_formula(formspec.formula());
830 : formspec.data() = checker.typechecked_data_specification();
831 : formspec.data().translate_user_notation();
832 : }
833 : catch (mcrl2::runtime_error& e)
834 : {
835 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula specification " + state_formulas::pp(formspec));
836 : }
837 : }
838 :
839 : /// \brief Typecheck the state formula specification formspec. It is assumed that the formula is not self contained,
840 : /// i.e. some of the actions and sorts may be declared in lpsspec.
841 : inline
842 : void typecheck_state_formula_specification(state_formula_specification& formspec, const lps::stochastic_specification& lpsspec, const bool formula_is_quantitative)
843 : {
844 : try
845 : {
846 : data::data_type_checker checker(formspec.data());
847 : data::data_specification dataspec = checker.typechecked_data_specification();
848 : state_formulas::normalize_sorts(formspec, dataspec);
849 : state_formula_type_checker type_checker(dataspec, formula_is_quantitative, lpsspec.action_labels() + formspec.action_labels(), lpsspec.global_variables());
850 : formspec.formula() = type_checker.typecheck_state_formula(formspec.formula());
851 : formspec.data() = checker.typechecked_data_specification();
852 : formspec.data().translate_user_notation();
853 : }
854 : catch (mcrl2::runtime_error& e)
855 : {
856 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check modal formula specification " + state_formulas::pp(formspec));
857 : }
858 : }
859 :
860 : } // namespace state_formulas
861 :
862 : } // namespace mcrl2
863 :
864 : #endif // MCRL2_MODAL_FORMULA_TYPECHECK_H
|
