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/absinthe.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_ABSINTHE_H
13 : #define MCRL2_PBES_ABSINTHE_H
14 :
15 : #define MCRL2_ABSINTHE_CHECK_EXPRESSIONS
16 :
17 : #include "mcrl2/data/consistency.h"
18 : #include "mcrl2/data/detail/data_construction.h"
19 : #include "mcrl2/pbes/builder.h"
20 : #include "mcrl2/utilities/detail/separate_keyword_section.h"
21 :
22 : #ifdef MCRL2_ABSINTHE_CHECK_EXPRESSIONS
23 : #include "mcrl2/data/detail/print_parse_check.h"
24 : #endif
25 :
26 : namespace mcrl2 {
27 :
28 : namespace pbes_system {
29 :
30 : template <typename Term>
31 0 : std::string print_term(const Term& x)
32 : {
33 0 : return data::pp(x) + " " + data::pp(x);
34 : }
35 :
36 : template <typename Term>
37 0 : std::string print_symbol(const Term& x)
38 : {
39 0 : return data::pp(x) + ": " + data::pp(x.sort());
40 : }
41 :
42 : namespace detail {
43 :
44 : inline
45 : data::data_specification& absinthe_data_specification()
46 : {
47 : static data::data_specification dataspec;
48 : return dataspec;
49 : }
50 :
51 : #ifdef MCRL2_ABSINTHE_CHECK_EXPRESSIONS
52 : template <typename T>
53 : inline void absinthe_check_expression(const T& x)
54 : {
55 : data::detail::print_parse_check(x, absinthe_data_specification());
56 : }
57 : #else
58 : template <typename T>
59 : inline void absinthe_check_expression(const T&)
60 : {}
61 : #endif
62 :
63 : // Returns true if f appears as a structured sort constructor in dataspec.
64 : inline
65 2 : bool is_structured_sort_constructor(const data::data_specification& dataspec, const data::function_symbol& f)
66 : {
67 6 : for (const data::alias& a: dataspec.user_defined_aliases())
68 : {
69 4 : if (f.sort() != a.name())
70 : {
71 4 : continue;
72 : }
73 0 : const data::sort_expression& s = a.reference();
74 0 : if (data::is_structured_sort(s))
75 : {
76 0 : const auto& ss = atermpp::down_cast<data::structured_sort>(s);
77 0 : for (const data::function_symbol& g: ss.constructor_functions())
78 : {
79 0 : if (f.name() == g.name())
80 : {
81 0 : return true;
82 : }
83 0 : }
84 : }
85 : }
86 2 : return false;
87 : }
88 :
89 : inline
90 : void print_used_function_symbols(const pbes& p)
91 : {
92 : mCRL2log(log::debug) << "--- used function symbols ---" << std::endl;
93 : for (const data::function_symbol& f: pbes_system::find_function_symbols(p))
94 : {
95 : mCRL2log(log::debug) << print_symbol(f) << std::endl;
96 : }
97 : }
98 :
99 : // TODO: Is this correct if s has the shape A -> (B -> C)? Should the result be (B -> C) or C?
100 : inline
101 0 : data::sort_expression target_sort(const data::sort_expression& s)
102 : {
103 0 : if (data::is_basic_sort(s))
104 : {
105 0 : return s;
106 : }
107 0 : else if (data::is_function_sort(s))
108 : {
109 0 : const auto& fs = atermpp::down_cast<data::function_sort>(s);
110 0 : return fs.codomain();
111 : }
112 0 : else if (data::is_container_sort(s))
113 : {
114 0 : return s;
115 : }
116 0 : throw mcrl2::runtime_error("target_sort: unsupported sort " + print_term(s) + " detected!");
117 : return data::sort_expression();
118 : }
119 :
120 : } // namespace detail
121 :
122 : struct absinthe_algorithm
123 : {
124 : typedef std::map<data::sort_expression, data::sort_expression> sort_expression_substitution_map;
125 : typedef std::map<data::function_symbol, data::function_symbol> function_symbol_substitution_map;
126 : typedef std::map<data::sort_expression, data::function_symbol> abstraction_map;
127 :
128 : // Used for generating variables of sort comprehensions.
129 : data::set_identifier_generator m_generator;
130 :
131 : struct absinthe_sort_expression_builder: public sort_expression_builder<absinthe_sort_expression_builder>
132 : {
133 : typedef sort_expression_builder<absinthe_sort_expression_builder> super;
134 : using super::apply;
135 :
136 : const abstraction_map& sigmaH;
137 : const sort_expression_substitution_map& sigmaS;
138 : const function_symbol_substitution_map& sigmaF;
139 : data::set_identifier_generator& generator;
140 :
141 7 : absinthe_sort_expression_builder(const abstraction_map& sigmaA_,
142 : const sort_expression_substitution_map& sigmaS_,
143 : const function_symbol_substitution_map& sigmaF_,
144 : data::set_identifier_generator& generator_
145 : )
146 7 : : sigmaH(sigmaA_),
147 7 : sigmaS(sigmaS_),
148 7 : sigmaF(sigmaF_),
149 7 : generator(generator_)
150 7 : {}
151 :
152 : template <class T>
153 32 : void apply(T& result, const data::sort_expression& x)
154 : {
155 32 : auto i = sigmaS.find(x);
156 32 : if (i == sigmaS.end())
157 : {
158 21 : super::apply(result, x);
159 : //pbes_system::detail::absinthe_check_expression(result);
160 : }
161 : else
162 : {
163 11 : result = i->second;
164 : //pbes_system::detail::absinthe_check_expression(result);
165 : }
166 32 : }
167 :
168 : template <class T>
169 3 : void apply(T& result, const data::function_symbol& x)
170 : {
171 3 : auto i = sigmaF.find(x);
172 3 : if (i != sigmaF.end())
173 : {
174 : //pbes_system::detail::absinthe_check_expression(i->second);
175 3 : result = i->second;
176 3 : return;
177 : }
178 0 : throw mcrl2::runtime_error("function symbol " + print_symbol(x) + " not present in the function symbol mapping!");
179 : }
180 :
181 : template <class T>
182 3 : void apply(T& result, const data::application& x)
183 : {
184 3 : if (data::is_variable(x.head()))
185 : {
186 0 : data::variable v = atermpp::down_cast<data::variable>(x.head());
187 0 : data::sort_expression sort;
188 0 : super::apply(sort, v.sort());
189 0 : v = data::variable(v.name(), sort);
190 0 : result = data::detail::create_finite_set(data::application(v, x.begin(), x.end()));
191 0 : return;
192 0 : }
193 3 : else if (data::is_function_symbol(x.head()))
194 : {
195 3 : super::apply(result, x);
196 3 : return;
197 : }
198 : else
199 : {
200 0 : throw mcrl2::runtime_error("don't know how to handle arbitrary expression as head: " + data::pp(x));
201 : }
202 : }
203 :
204 : template <class T>
205 0 : void apply(T& result, const data::lambda& x)
206 : {
207 0 : data::data_expression body;
208 0 : super::apply(body, x);
209 : //pbes_system::detail::absinthe_check_expression(body);
210 0 : data::sort_expression s = body.sort();
211 0 : generator.add_identifiers(data::find_identifiers(x));
212 0 : data::variable v(generator("v"), s);
213 0 : result = data::detail::create_set_comprehension(v, data::equal_to(v, body));
214 : //pbes_system::detail::absinthe_check_expression(result);
215 0 : }
216 :
217 : template <class T>
218 10 : void apply(T& result, const data::data_expression& x)
219 : {
220 10 : if (data::is_variable(x))
221 : {
222 2 : super::apply(result, x);
223 2 : result = data::detail::create_finite_set(result);
224 : //pbes_system::detail::absinthe_check_expression(result);
225 : }
226 : else
227 : {
228 : // check if it is a "ground term", i.e. it does not contain any variables
229 8 : auto i = sigmaH.find(x.sort());
230 8 : if (i != sigmaH.end() && data::find_all_variables(x).empty())
231 : {
232 4 : data::data_expression_list args = { x };
233 2 : result = data::detail::create_finite_set(data::application(i->second, args));
234 : //pbes_system::detail::absinthe_check_expression(result);
235 2 : }
236 : else
237 : {
238 : // first apply the sort and function symbol transformations
239 6 : super::apply(result, x);
240 : //pbes_system::detail::absinthe_check_expression(result);
241 : }
242 : }
243 10 : }
244 : };
245 :
246 : // Applies sigmaS to a sort expression
247 : struct sort_function
248 : {
249 : using argument_type = data::sort_expression;
250 : using result_type = data::sort_expression;
251 :
252 : absinthe_sort_expression_builder f;
253 :
254 3 : sort_function(const abstraction_map& sigmaH,
255 : const sort_expression_substitution_map& sigmaS,
256 : const function_symbol_substitution_map& sigmaF,
257 : data::set_identifier_generator& generator
258 : )
259 3 : : f(sigmaH, sigmaS, sigmaF, generator)
260 3 : {}
261 :
262 16 : data::sort_expression operator()(const data::sort_expression& x)
263 : {
264 16 : data::sort_expression sort;
265 16 : f.apply(sort, x);
266 16 : return sort;
267 0 : }
268 : };
269 :
270 : struct absinthe_data_expression_builder: public pbes_expression_builder<absinthe_data_expression_builder>
271 : {
272 : typedef pbes_expression_builder<absinthe_data_expression_builder> super;
273 : using super::apply;
274 : using super::update;
275 :
276 2 : data::variable_list make_variables(const data::data_expression_list& x, const std::string& hint, sort_function sigma) const
277 : {
278 2 : std::vector<data::variable> result;
279 2 : std::size_t i = 0;
280 4 : for (auto j = x.begin(); j != x.end(); ++i, ++j)
281 : {
282 2 : result.emplace_back(hint + utilities::number2string(i), sigma(j->sort()));
283 : }
284 4 : return data::variable_list(result.begin(), result.end());
285 2 : }
286 :
287 : const abstraction_map& sigmaH;
288 : const sort_expression_substitution_map& sigmaS;
289 : const function_symbol_substitution_map& sigmaF;
290 : data::set_identifier_generator& generator;
291 : bool m_is_over_approximation;
292 :
293 1 : data::data_expression lift(const data::data_expression& x)
294 : {
295 1 : data::data_expression result;
296 1 : absinthe_sort_expression_builder(sigmaH, sigmaS, sigmaF, generator).apply(result, x);
297 1 : return result;
298 0 : }
299 :
300 2 : data::data_expression_list lift(const data::data_expression_list& x)
301 : {
302 2 : data::data_expression_list result;
303 2 : absinthe_sort_expression_builder(sigmaH, sigmaS, sigmaF, generator).apply(result, x);
304 2 : return result;
305 0 : }
306 :
307 0 : data::variable_list lift(const data::variable_list& x)
308 : {
309 0 : data::variable_list result;
310 0 : absinthe_sort_expression_builder(sigmaH, sigmaS, sigmaF, generator).apply(result, x);
311 0 : return result;
312 0 : }
313 :
314 1 : pbes_system::propositional_variable lift(const pbes_system::propositional_variable& x)
315 : {
316 1 : pbes_system::propositional_variable result;
317 1 : absinthe_sort_expression_builder(sigmaH, sigmaS, sigmaF, generator).apply(result, x);
318 1 : return result;
319 0 : }
320 :
321 1 : absinthe_data_expression_builder(const abstraction_map& sigmaA_,
322 : const sort_expression_substitution_map& sigmaS_,
323 : const function_symbol_substitution_map& sigmaF_,
324 : data::set_identifier_generator& generator_,
325 : bool is_over_approximation)
326 1 : : sigmaH(sigmaA_),
327 1 : sigmaS(sigmaS_),
328 1 : sigmaF(sigmaF_),
329 1 : generator(generator_),
330 1 : m_is_over_approximation(is_over_approximation)
331 1 : {}
332 :
333 : template <class T>
334 1 : void apply(T& result, const data::data_expression& x)
335 : {
336 1 : data::data_expression x1 = lift(x);
337 1 : if (m_is_over_approximation)
338 : {
339 1 : result = data::detail::create_set_in(data::true_(), x1);
340 : }
341 : else
342 : {
343 0 : result = data::not_(data::detail::create_set_in(data::false_(), x1));
344 : }
345 1 : }
346 :
347 : template <class T>
348 2 : void apply(T& result, const propositional_variable_instantiation& x)
349 : {
350 2 : data::data_expression_list e = lift(x.parameters());
351 4 : data::variable_list variables = make_variables(x.parameters(), "x", sort_function(sigmaH, sigmaS, sigmaF, generator));
352 2 : data::data_expression_list::iterator i = e.begin();
353 2 : data::variable_list::iterator j = variables.begin();
354 2 : data::data_expression_vector z;
355 4 : for (; i != e.end(); ++i, ++j)
356 : {
357 2 : z.push_back(data::detail::create_set_in(*j, *i));
358 : }
359 2 : data::data_expression q = data::lazy::join_and(z.begin(), z.end());
360 2 : if (m_is_over_approximation)
361 : {
362 2 : result = make_exists_(variables, and_(q, propositional_variable_instantiation(x.name(), atermpp::container_cast<data::data_expression_list>(variables))));
363 : }
364 : else
365 : {
366 0 : result = make_forall_(variables, imp(q, propositional_variable_instantiation(x.name(), atermpp::container_cast<data::data_expression_list>(variables))));
367 : }
368 2 : }
369 :
370 : template <class T>
371 0 : void apply(T& result, const pbes_system::forall& x)
372 : {
373 0 : pbes_system::pbes_expression body;
374 0 : super::apply(body, x.body());
375 0 : result = make_forall_(lift(x.variables()), body);
376 0 : }
377 :
378 : template <class T>
379 0 : void apply(T& result, const pbes_system::exists& x)
380 : {
381 0 : pbes_system::pbes_expression body;
382 0 : super::apply(body, x.body());
383 0 : result = make_exists_(lift(x.variables()), body);
384 0 : }
385 :
386 1 : void update(pbes_system::pbes_equation& x)
387 : {
388 1 : x.variable() = lift(x.variable());
389 1 : pbes_system::pbes_expression result;
390 1 : super::apply(result, x.formula());
391 1 : x.formula() = result;
392 1 : }
393 :
394 1 : void update(pbes_system::pbes& x)
395 : {
396 1 : super::update(x.equations());
397 1 : pbes_expression kappa;
398 1 : apply(kappa, x.initial_state());
399 2 : core::identifier_string name("GeneratedZ");
400 1 : propositional_variable Z(name, data::variable_list());
401 1 : x.equations().emplace_back(fixpoint_symbol::mu(), Z, kappa);
402 1 : x.initial_state() = propositional_variable_instantiation(name, data::data_expression_list());
403 1 : }
404 : };
405 :
406 : sort_expression_substitution_map parse_sort_expression_mapping(const std::string& text, const data::data_specification& dataspec)
407 : {
408 : sort_expression_substitution_map result;
409 :
410 : for (const std::string& line: utilities::regex_split(text, "\\n"))
411 : {
412 : std::vector<std::string> words = utilities::regex_split(line, ":=");
413 : if (words.size() == 2)
414 : {
415 : data::sort_expression lhs = data::parse_sort_expression(words[0], dataspec);
416 : data::sort_expression rhs = data::parse_sort_expression(words[1], dataspec);
417 : result[lhs] = rhs;
418 : }
419 : }
420 : return result;
421 : }
422 :
423 : // Parse the right hand sides of the function symbol mapping in text, and add them to dataspec if needed
424 1 : void parse_right_hand_sides(const std::string& text, data::data_specification& dataspec)
425 : {
426 1 : std::string dataspec_text = data::pp(dataspec);
427 4 : for (const std::string& line: utilities::regex_split(text, "\\n"))
428 : {
429 6 : std::vector<std::string> words = utilities::regex_split(line, ":=");
430 3 : if (words.size() == 2)
431 : {
432 2 : data::function_symbol f = data::parse_function_symbol(words[1], dataspec_text);
433 2 : if (!pbes_system::detail::is_structured_sort_constructor(dataspec, f))
434 : {
435 2 : dataspec.add_mapping(f);
436 : }
437 2 : }
438 4 : }
439 1 : }
440 :
441 1 : function_symbol_substitution_map parse_function_symbol_mapping(const std::string& text, const data::data_specification& dataspec)
442 : {
443 1 : function_symbol_substitution_map result;
444 1 : std::string dataspec_text = data::pp(dataspec);
445 :
446 4 : for (const std::string& line: utilities::regex_split(text, "\\n"))
447 : {
448 6 : std::vector<std::string> words = utilities::regex_split(line, ":=");
449 3 : if (words.size() == 2)
450 : {
451 2 : data::function_symbol lhs = data::parse_function_symbol(words[0], dataspec_text);
452 2 : std::string s = words[1];
453 2 : s = utilities::regex_replace(";\\s*$", "", s);
454 2 : data::function_symbol rhs = data::parse_function_symbol(s, dataspec_text);
455 2 : result[lhs] = rhs;
456 2 : }
457 4 : }
458 2 : return result;
459 1 : }
460 :
461 : // text is a data_specification; extract the user defined mappings
462 1 : abstraction_map parse_abstraction_map(const std::string& text)
463 : {
464 1 : abstraction_map result;
465 1 : data::data_specification dataspec = data::parse_data_specification(text);
466 2 : for (const data::function_symbol& i: dataspec.user_defined_mappings())
467 : {
468 1 : const auto& f = atermpp::down_cast<data::function_sort>(i.sort());
469 1 : if (f.domain().size() != 1)
470 : {
471 0 : throw mcrl2::runtime_error("cannot abstract the function " + data::pp(i) + " since the arity of the domain is not equal to one!");
472 : }
473 1 : result[f.domain().front()] = i;
474 : }
475 2 : return result;
476 1 : }
477 :
478 : // creates a finite set containing one data expression
479 : struct make_data_expression_set
480 : {
481 : data::data_expression operator()(const data::data_expression& x) const
482 : {
483 : data::sort_expression s = x.sort();
484 : data::data_expression result = data::sort_fset::empty(s);
485 : result = data::sort_fset::cons_(s, x, result);
486 : return result;
487 : }
488 : };
489 :
490 : // transforms the sort expression s to Set(s)
491 : struct make_set
492 : {
493 8 : data::sort_expression operator()(const data::sort_expression& s) const
494 : {
495 8 : return data::sort_set::set_(s);
496 : }
497 : };
498 :
499 : // function that transforms a function symbol
500 : struct lift_function_symbol_1_2
501 : {
502 : std::map<std::string, std::string> unprintable;
503 : std::set<std::string> suffix_with_sort;
504 :
505 3 : lift_function_symbol_1_2()
506 3 : {
507 3 : unprintable["&&"] = "and";
508 3 : unprintable["||"] = "or";
509 3 : unprintable["!"] = "not";
510 3 : unprintable["#"] = "len";
511 3 : unprintable["."] = "element_at";
512 3 : unprintable["+"] = "plus";
513 3 : unprintable["-"] = "minus";
514 3 : unprintable[">"] = "greater";
515 3 : unprintable["<"] = "less";
516 3 : unprintable[">="] = "ge";
517 3 : unprintable["<="] = "le";
518 3 : unprintable["=="] = "eq";
519 3 : unprintable["!="] = "neq";
520 3 : unprintable["[]"] = "emptylist";
521 3 : unprintable["++"] = "concat";
522 3 : unprintable["<|"] = "snoc";
523 3 : unprintable["|>"] = "cons";
524 3 : unprintable["@cNat"] = "cNat";
525 3 : unprintable["@cDub"] = "cDub";
526 3 : unprintable["@c0"] = "c0";
527 3 : unprintable["@c1"] = "c1";
528 3 : unprintable["@func_update"] = "func_update";
529 3 : unprintable["@cInt"] = "cInt";
530 3 : unprintable["@cNeg"] = "cNeg";
531 :
532 3 : suffix_with_sort.insert("[]");
533 3 : suffix_with_sort.insert("|>");
534 3 : }
535 :
536 2 : std::string print_cleaned(const data::sort_expression& s) const
537 : {
538 2 : std::string result = data::pp(s);
539 2 : result = utilities::regex_replace("\\(", "_", result);
540 2 : result = utilities::regex_replace("\\)", "_", result);
541 2 : result = utilities::regex_replace("#", "_", result);
542 2 : result = utilities::regex_replace("->", "_", result);
543 2 : result = utilities::remove_whitespace(result);
544 2 : return result;
545 0 : }
546 :
547 :
548 3 : data::function_symbol operator()(const data::function_symbol& f, sort_function sigma) const
549 : {
550 : using utilities::detail::contains;
551 :
552 : //mCRL2log(log::debug) << "lift_function_symbol_1_2 f = " << print_symbol(f) << std::endl;
553 3 : std::string name = std::string(f.name());
554 :
555 3 : bool print_sort = contains(suffix_with_sort, std::string(f.name()));
556 3 : auto i = unprintable.find(name);
557 3 : if (i != unprintable.end())
558 : {
559 2 : name = i->second;
560 : }
561 3 : name = "Generated_" + name;
562 3 : if (print_sort)
563 : {
564 2 : name = name + print_cleaned(f.sort());
565 : }
566 :
567 3 : const data::sort_expression& s = f.sort();
568 3 : if (data::is_basic_sort(s))
569 : {
570 2 : return data::function_symbol(name, sigma(s));
571 : }
572 2 : else if (data::is_function_sort(s))
573 : {
574 : // Apply sigmaS recursively to s
575 : // f: tail: List(Nat) -> List(Nat)
576 : // result: generated_tail: List(AbsNat) -> Set(List(AbsNat))
577 1 : data::function_sort fs = atermpp::down_cast<data::function_sort>(sigma(s));
578 2 : return data::function_symbol(name, data::function_sort(fs.domain(), make_set()(fs.codomain())));
579 1 : }
580 1 : else if (data::is_container_sort(s))
581 : {
582 : // Apply sigmaS recursively to s
583 : // Example: List(Nat) -> List(AbsNat)
584 2 : return data::function_symbol(name, sigma(s));
585 : }
586 0 : throw mcrl2::runtime_error("absinthe algorithm: unsupported sort " + print_term(s) + " detected!");
587 : return data::function_symbol();
588 3 : }
589 : };
590 :
591 : // function that lifts a function symbol
592 : struct lift_function_symbol_2_3
593 : {
594 5 : data::function_symbol operator()(const data::function_symbol& f) const
595 : {
596 : using namespace data;
597 : //mCRL2log(log::debug) << "lift_function_symbol_2_3 f = " << print_symbol(f) << std::endl;
598 10 : std::string name = "Lift" + utilities::trim_copy(std::string(f.name()));
599 5 : const sort_expression &s = f.sort();
600 5 : if (is_basic_sort(s))
601 : {
602 2 : return function_symbol(name, make_set()(s));
603 : }
604 4 : else if (is_function_sort(s))
605 : {
606 3 : const auto& fs = atermpp::down_cast<data::function_sort>(s);
607 3 : const sort_expression_list& sl = fs.domain();
608 6 : return function_symbol(name, function_sort(sort_expression_list(sl.begin(),sl.end(), make_set()), fs.codomain()));
609 : }
610 1 : else if (is_container_sort(s))
611 : {
612 2 : return data::function_symbol(name, make_set()(s));
613 : }
614 0 : throw mcrl2::runtime_error("absinthe algorithm (lift): unsupported sort " + print_term(s) + " detected!");
615 5 : }
616 : };
617 :
618 : // function that generates an equation from a function symbol and it's corresponding 'generated' version
619 : struct lift_equation_1_2
620 : {
621 : lift_equation_1_2() = default;
622 :
623 0 : std::vector<data::variable> make_variables(const data::sort_expression_list& sorts, const std::string& hint, sort_function sigma) const
624 : {
625 0 : std::vector<data::variable> result;
626 0 : std::size_t i = 0;
627 0 : for (auto j = sorts.begin(); j != sorts.end(); ++i, ++j)
628 : {
629 0 : result.emplace_back(hint + utilities::number2string(i), sigma(*j));
630 : }
631 0 : return result;
632 0 : }
633 :
634 : // sigmaH is used for checking consistency of the user input
635 1 : data::data_equation operator()(const data::function_symbol& f1, const data::function_symbol& f2, sort_function sigma, const abstraction_map& sigmaH) const
636 : {
637 1 : mCRL2log(log::debug) << "lift_equation_1_2 f1 = " << print_symbol(f1) << " f2 = " << print_symbol(f2) << std::endl;
638 1 : data::variable_list variables;
639 1 : const data::data_expression& condition = data::true_();
640 1 : data::data_expression lhs;
641 1 : data::data_expression rhs;
642 :
643 1 : data::sort_expression s1 = f1.sort();
644 : //data::function_symbol f1a(f1.name(), sigma(s1));
645 :
646 1 : if (data::is_basic_sort(s1))
647 : {
648 1 : lhs = f2;
649 1 : data::function_symbol f1_sigma(f1.name(), sigma(f1.sort()));
650 :
651 1 : auto i = sigmaH.find(f1.sort());
652 1 : if (i == sigmaH.end())
653 : {
654 0 : rhs = f1_sigma;
655 : }
656 : else
657 : {
658 1 : data::function_symbol h = i->second;
659 1 : rhs = data::application(h, f1);
660 : //pbes_system::detail::absinthe_check_expression(rhs);
661 1 : }
662 1 : }
663 0 : else if (data::is_function_sort(s1))
664 : {
665 0 : data::function_sort fs1(f1.sort());
666 0 : data::function_sort fs2(f2.sort());
667 :
668 : // check validity
669 0 : if (data::is_function_update_application(f1))
670 : {
671 : // TODO: add check that the domain of the updated function does not contain abstraction sorts
672 : }
673 0 : else if (fs1.domain() != fs2.domain())
674 : {
675 0 : throw std::runtime_error("can not generalize functions with abstraction sorts in the domain: " + data::pp(f1) + ": " + data::pp(s1));
676 : }
677 :
678 0 : data::variable_vector x = make_variables(fs2.domain(), "x", sigma);
679 0 : variables = data::variable_list(x.begin(),x.end());
680 0 : lhs = data::application(f2, x.begin(), x.end());
681 0 : data::application f_x(f1, x.begin(), x.end());
682 :
683 0 : data::function_symbol f1_sigma(f1.name(), sigma(f1.sort()));
684 :
685 0 : auto i = sigmaH.find(detail::target_sort(f1.sort()));
686 0 : if (i == sigmaH.end())
687 : {
688 0 : data::application f1_sigma_x(f1_sigma, x.begin(), x.end());
689 0 : rhs = data::detail::create_finite_set(f_x);
690 : //pbes_system::detail::absinthe_check_expression(rhs);
691 0 : }
692 : else
693 : {
694 0 : data::function_symbol h = i->second;
695 0 : rhs = data::detail::create_finite_set(data::application(h, f_x));
696 : //pbes_system::detail::absinthe_check_expression(rhs);
697 0 : }
698 0 : }
699 0 : else if (data::is_container_sort(s1))
700 : {
701 : // Example:
702 : // f1: [] : List(Nat)
703 : // f2: generated_emptylist : List(AbsNat)
704 : // eqn: generated_emptylist = [] met [] : List(AbsNat)
705 : // tail: List(AbsNat) -> List(Nat)
706 0 : lhs = f2;
707 0 : data::function_symbol f1_sigma(f1.name(), sigma(f1.sort()));
708 0 : rhs = f1_sigma;
709 : //pbes_system::detail::absinthe_check_expression(rhs);
710 0 : }
711 : else
712 : {
713 0 : throw mcrl2::runtime_error("absinthe algorithm (lift_equation_1_2): unsupported sort " + print_term(s1) + " detected!");
714 : }
715 :
716 1 : if (lhs.sort() != rhs.sort())
717 : {
718 0 : throw mcrl2::runtime_error("absinthe algorithm (lift_equation_1_2): lhs.sort() and rhs.sort are not equal: " + data::pp(lhs.sort()) + " <-> " + data::pp(rhs.sort()));
719 : }
720 :
721 2 : return data::data_equation(variables, condition, lhs, rhs);
722 1 : }
723 : };
724 :
725 : // function that generates an equation from a function symbol and it's corresponding lifted version
726 : struct lift_equation_2_3
727 : {
728 : lift_equation_2_3() = default;
729 :
730 6 : std::vector<data::variable> make_variables(const data::sort_expression_list& sorts, const std::string& hint, sort_function sigma) const
731 : {
732 6 : std::vector<data::variable> result;
733 6 : std::size_t i = 0;
734 16 : for (auto j = sorts.begin(); j != sorts.end(); ++i, ++j)
735 : {
736 10 : result.emplace_back(hint + utilities::number2string(i), sigma(*j));
737 : }
738 6 : return result;
739 0 : }
740 :
741 : // Let x = [x1:D1, ..., xn:Dn] and X = [X1:Set(D1), ..., Xn:Set(Dn)]. Returns the expression
742 : //
743 : // (x1 in X1 /\ ... /\ xn in Xn)
744 3 : data::data_expression enumerate_domain(const std::vector<data::variable>& x, const std::vector<data::variable>& X) const
745 : {
746 3 : std::vector<data::data_expression> a;
747 3 : auto i = x.begin();
748 3 : auto j = X.begin();
749 8 : for (; i != x.end(); ++i, ++j)
750 : {
751 5 : a.push_back(data::detail::create_set_in(*i, *j));
752 : }
753 3 : data::data_expression body = data::lazy::join_and(a.begin(), a.end());
754 6 : return body;
755 3 : }
756 :
757 5 : data::data_equation operator()(const data::function_symbol& f2, const data::function_symbol& f3, sort_function sigma) const
758 : {
759 : //mCRL2log(log::debug) << "lift_equation_2_3 f2 = " << print_symbol(f2) << " f3 = " << print_symbol(f3) << std::endl;
760 5 : data::variable_list variables;
761 5 : const data::data_expression& condition = data::true_();
762 5 : data::data_expression lhs;
763 5 : data::data_expression rhs;
764 :
765 5 : const data::sort_expression& s2 = f2.sort();
766 :
767 5 : if (data::is_basic_sort(s2))
768 : {
769 1 : lhs = f3;
770 1 : rhs = data::detail::create_finite_set(f2);
771 : }
772 4 : else if (data::is_function_sort(s2))
773 : {
774 3 : data::function_sort fs2(f2.sort());
775 3 : data::function_sort fs3(f3.sort());
776 :
777 3 : if (!data::is_container_sort(fs2.codomain()))
778 : {
779 0 : throw mcrl2::runtime_error("The codomain " + data::pp(fs2.codomain()) + " of function " + data::pp(f2.name()) + " should be a container sort!");
780 : }
781 :
782 : // TODO: generate these variables in a proper way
783 6 : std::vector<data::variable> x = make_variables(fs2.domain(), "x", sigma);
784 6 : std::vector<data::variable> X = make_variables(fs3.domain(), "X", sigma);
785 :
786 3 : variables = data::variable_list(X.begin(), X.end());
787 3 : lhs = data::application(f3, X.begin(), X.end());
788 6 : data::variable y("y", data::detail::get_set_sort(atermpp::down_cast<data::container_sort>(fs2.codomain())));
789 3 : data::data_expression Y = data::application(f2, x.begin(), x.end());
790 6 : data::data_expression body = data::and_(enumerate_domain(x, X), data::detail::create_set_in(y, Y));
791 3 : rhs = data::detail::create_set_comprehension(y, data::exists(x, body));
792 3 : }
793 1 : else if (data::is_container_sort(s2))
794 : {
795 1 : lhs = f3;
796 1 : rhs = data::detail::create_finite_set(f2);
797 : }
798 : else
799 : {
800 0 : throw mcrl2::runtime_error("absinthe algorithm (lift_equation_2_3): unsupported sort " + print_term(s2) + " detected!");
801 : }
802 10 : return data::data_equation(variables, condition, lhs, rhs);
803 5 : }
804 : };
805 :
806 : template <typename Map>
807 0 : std::string print_mapping(const Map& m)
808 : {
809 0 : std::ostringstream out;
810 0 : for (auto i = m.begin(); i != m.end(); ++i)
811 : {
812 0 : out << i->first << " -> " << i->second << std::endl;
813 : }
814 0 : return out.str();
815 0 : }
816 :
817 1 : void check_consistency(const data::sort_expression& s, const data::sort_expression& t, const data::function_symbol& f, sort_expression_substitution_map& sigmaS) const
818 : {
819 1 : sort_expression_substitution_map::const_iterator i = sigmaS.find(s);
820 1 : if (i != sigmaS.end() && i->second != t)
821 : {
822 0 : throw mcrl2::runtime_error("inconsistent abstraction " + data::pp(s) + " := " + data::pp(t) + " detected in the abstraction of " + print_symbol(f) + " (elsewhere it is abstracted as " + data::pp(s) + " := " + data::pp(i->second) + ").");
823 : }
824 : else
825 : {
826 1 : sigmaS[s] = t;
827 : }
828 1 : }
829 :
830 : // Let f1: s1 x ... sn -> s and f2: t1 x ... tn -> t
831 : // This function checks if the correspondence si -> ti conflicts with sigmaS.
832 1 : void check_consistency(const data::function_symbol& f1, const data::function_symbol& f2, sort_expression_substitution_map& sigmaS) const
833 : {
834 1 : const data::sort_expression& s1 = f1.sort();
835 1 : const data::sort_expression& s2 = f2.sort();
836 :
837 1 : if (data::is_basic_sort(s1))
838 : {
839 1 : check_consistency(s1, s2, f1, sigmaS);
840 : }
841 0 : else if (data::is_function_sort(s1))
842 : {
843 0 : data::function_sort fs1(s1);
844 0 : data::function_sort fs2(s2);
845 :
846 0 : const data::sort_expression_list& domain1 = fs1.domain();
847 0 : const data::sort_expression_list& domain2 = fs2.domain();
848 :
849 0 : data::sort_expression_list::iterator i1 = domain1.begin();
850 0 : data::sort_expression_list::iterator i2 = domain2.begin();
851 :
852 0 : for (; i1 != domain1.end(); ++i1, ++i2)
853 : {
854 0 : check_consistency(*i1, *i2, f1, sigmaS);
855 : }
856 : // check_consistency(fs1.codomain(), fs2.codomain(), f1, sigmaS);
857 0 : }
858 : // else if (data::is_container_sort(s1))
859 : // {
860 : // }
861 1 : }
862 :
863 : // add lifted mappings and equations to the data specification
864 1 : void lift_data_specification(const pbes& p, const abstraction_map& sigmaH, const sort_expression_substitution_map& sigmaS, function_symbol_substitution_map& sigmaF, data::data_specification& dataspec)
865 : {
866 : using utilities::detail::has_key;
867 :
868 1 : sort_expression_substitution_map sigmaS_consistency = sigmaS; // is only used for consistency checking
869 1 : sort_function sigma(sigmaH, sigmaS, sigmaF, m_generator);
870 :
871 : // add lifted versions of used function symbols that are not specified by the user to sigmaF, and adds them to the data specification as well
872 1 : std::set<data::function_symbol> used_function_symbols = pbes_system::find_function_symbols(p);
873 :
874 : // add List containers for user defined sorts, since they are used in the translation
875 1 : const data::basic_sort_vector& sorts = dataspec.user_defined_sorts();
876 1 : for (const data::basic_sort& sort: sorts)
877 : {
878 0 : data::sort_expression s = data::container_sort(data::list_container(), sort);
879 0 : dataspec.add_context_sort(s);
880 0 : }
881 :
882 : // add constructor functions of List containers of abstracted sorts to sigmaF
883 2 : for (const auto& i: sigmaH)
884 : {
885 2 : data::sort_expression s = data::container_sort(data::list_container(), i.first);
886 1 : dataspec.add_context_sort(s);
887 1 : data::function_symbol_vector list_constructors = dataspec.constructors(s);
888 3 : for (const data::function_symbol& f1: list_constructors)
889 : {
890 2 : data::function_symbol f2 = lift_function_symbol_1_2()(f1, sigma);
891 2 : sigmaF[f1] = f2;
892 2 : dataspec.add_mapping(f2);
893 2 : mCRL2log(log::debug) << "adding list constructor " << f1 << " to sigmaF" << std::endl;
894 2 : }
895 1 : }
896 :
897 4 : for (const data::function_symbol& f1: used_function_symbols)
898 : {
899 3 : mCRL2log(log::debug) << "lifting function symbol: " << f1 << std::endl;
900 3 : if (!has_key(sigmaF, f1))
901 : {
902 1 : data::function_symbol f2 = lift_function_symbol_1_2()(f1, sigma);
903 1 : mCRL2log(log::debug) << "lifted function symbol: " << f1 << " to " << f2 << std::endl;
904 1 : check_consistency(f1, f2, sigmaS_consistency);
905 1 : sigmaF[f1] = f2;
906 1 : dataspec.add_mapping(f2);
907 :
908 1 : data::data_equation eq = lift_equation_1_2()(f1, f2, sigma, sigmaH);
909 1 : mCRL2log(log::debug) << "adding equation: " << eq << std::endl;
910 1 : dataspec.add_equation(eq);
911 1 : }
912 : }
913 :
914 6 : for (auto& i : sigmaF)
915 : {
916 : // data::function_symbol f1 = i->first;
917 5 : data::function_symbol f2 = i.second;
918 5 : data::function_symbol f3 = lift_function_symbol_2_3()(f2);
919 :
920 5 : mCRL2log(log::debug) << "adding mapping: " << f3 << " " << f3.sort() << std::endl;
921 5 : dataspec.add_mapping(f3);
922 :
923 : // update sigmaF
924 5 : i.second = f3;
925 :
926 : // make an equation for the lifted function symbol f
927 5 : data::data_equation eq = lift_equation_2_3()(f2, f3, sigma);
928 5 : mCRL2log(log::debug) << "adding equation: " << eq << std::endl;
929 5 : dataspec.add_equation(eq);
930 5 : }
931 1 : }
932 :
933 : void print_fsvec(const data::function_symbol_vector& v, const std::string& msg) const
934 : {
935 : mCRL2log(log::debug) << "--- " << msg << std::endl;
936 : for (const data::function_symbol& f: v)
937 : {
938 : mCRL2log(log::debug) << print_symbol(f) << std::endl;
939 : }
940 : }
941 :
942 : void print_fsmap(const function_symbol_substitution_map& v, const std::string& msg) const
943 : {
944 : mCRL2log(log::debug) << "--- " << msg << std::endl;
945 : for (const auto& i: v)
946 : {
947 : mCRL2log(log::debug) << print_symbol(i.first) << " --> " << print_symbol(i.second) << std::endl;
948 : }
949 : }
950 :
951 : void enable_logging()
952 : {
953 : log::logger::set_reporting_level(log::debug);
954 : }
955 :
956 1 : void run(pbes& p, const std::string& abstraction_text, bool is_over_approximation)
957 : {
958 : // split the string abstraction_text into four different parts
959 1 : std::string function_symbol_mapping_text;
960 1 : std::string user_sorts_text;
961 1 : std::string user_equations_text;
962 1 : std::string abstraction_mapping_text;
963 1 : std::string pbes_sorts_text;
964 :
965 1 : std::string text = abstraction_text;
966 10 : std::vector<std::string> all_keywords = { "sort", "var", "eqn", "map", "cons", "absfunc", "absmap" };
967 1 : std::pair<std::string, std::string> q;
968 :
969 1 : q = utilities::detail::separate_keyword_section(text, "sort", all_keywords);
970 1 : user_sorts_text = q.first;
971 1 : text = q.second;
972 :
973 1 : q = utilities::detail::separate_keyword_section(text, "absmap", all_keywords);
974 :
975 1 : abstraction_mapping_text = q.first;
976 1 : text = q.second;
977 :
978 : // must be the last one!
979 1 : q = utilities::detail::separate_keyword_section(text, "absfunc", all_keywords);
980 1 : function_symbol_mapping_text = q.first;
981 1 : user_equations_text = q.second;
982 :
983 : // extract pbes sorts
984 1 : std::string ptext = data::pp(p.data());
985 1 : q = utilities::detail::separate_keyword_section(ptext, "sort", all_keywords);
986 1 : pbes_sorts_text = q.first;
987 :
988 : // 0) split user_dataspec_text into user_sorts_text and user_equations_text
989 1 : mCRL2log(log::debug) << "--- user sorts ---\n" << user_sorts_text << std::endl;
990 1 : mCRL2log(log::debug) << "--- user equations ---\n" << user_equations_text << std::endl;
991 1 : mCRL2log(log::debug) << "--- function mapping ---\n" << function_symbol_mapping_text << std::endl;
992 1 : mCRL2log(log::debug) << "--- abstraction mapping ---\n" << abstraction_mapping_text << std::endl;
993 1 : mCRL2log(log::debug) << "--- pbes sorts ---\n" << pbes_sorts_text << std::endl;
994 :
995 1 : if (abstraction_mapping_text.find("absmap") != 0)
996 : {
997 0 : throw mcrl2::runtime_error("the abstraction mapping may not be empty!");
998 : }
999 :
1000 : // 1) create the data specification dataspec, which consists of user_sorts_text, abstract_mapping_text and p.data()
1001 2 : data::data_specification dataspec = data::parse_data_specification(data::pp(p.data()) + "\n" + user_sorts_text + "\n" + abstraction_mapping_text.substr(3));
1002 1 : mCRL2log(log::debug) << "--- data specification 1) ---\n" << dataspec << std::endl;
1003 :
1004 : // 2) parse the right hand sides of the function symbol mapping, and add them to dataspec
1005 1 : parse_right_hand_sides(function_symbol_mapping_text, dataspec);
1006 1 : mCRL2log(log::debug) << "--- data specification 2) ---\n" << dataspec << std::endl;
1007 :
1008 : // 3) add user_equations_text to dataspec
1009 1 : dataspec = data::parse_data_specification(data::pp(dataspec) + "\n" + user_equations_text);
1010 1 : mCRL2log(log::debug) << "--- data specification 3) ---\n" << dataspec << std::endl;
1011 :
1012 : // abstraction functions (specified by the user)
1013 2 : abstraction_map sigmaH = parse_abstraction_map(pbes_sorts_text + "\n" + user_sorts_text + "\n" + abstraction_mapping_text.substr(3));
1014 :
1015 : // sort expressions replacements (extracted from sigmaH)
1016 1 : sort_expression_substitution_map sigmaS;
1017 2 : for (auto i = sigmaH.begin(); i != sigmaH.end(); ++i)
1018 : {
1019 1 : data::function_symbol f = i->second;
1020 1 : const data::function_sort& fs = atermpp::down_cast<data::function_sort>(f.sort());
1021 1 : sigmaS[i->first] = fs.codomain();
1022 1 : }
1023 1 : mCRL2log(log::debug) << "\n--- sort expression mapping ---\n" << print_mapping(sigmaS) << std::endl;
1024 :
1025 : // function symbol replacements (specified by the user)
1026 1 : function_symbol_substitution_map sigmaF = parse_function_symbol_mapping(function_symbol_mapping_text, dataspec);
1027 1 : mCRL2log(log::debug) << "\n--- function symbol mapping ---\n" << print_mapping(sigmaF) << std::endl;
1028 :
1029 1 : m_generator.add_identifiers(data::function_and_mapping_identifiers(p.data()));
1030 1 : m_generator.add_identifiers(data::function_and_mapping_identifiers(dataspec));
1031 :
1032 : // 4) add lifted sorts, mappings and equations to dataspec
1033 : // before: the mapping sigmaF is f1 -> f2
1034 : // after: the mapping sigmaF is f1 -> f3
1035 : // after: f2 and f3 have been added to dataspec
1036 : // after: equations for f3 have been added to dataspec
1037 : // generate mapping f1 -> f2 for missing function symbols
1038 1 : lift_data_specification(p, sigmaH, sigmaS, sigmaF, dataspec);
1039 1 : mCRL2log(log::debug) << "--- data specification 4) ---\n" << dataspec << std::endl;
1040 :
1041 1 : mCRL2log(log::debug) << "\n--- function symbol mapping after lifting ---\n" << print_mapping(sigmaF) << std::endl;
1042 :
1043 1 : mCRL2log(log::debug) << "--- pbes before ---\n" << p << std::endl;
1044 :
1045 1 : p.data() = dataspec;
1046 :
1047 : // then transform the data expressions and the propositional variable instantiations
1048 1 : absinthe_data_expression_builder(sigmaH, sigmaS, sigmaF, m_generator, is_over_approximation).update(p);
1049 :
1050 1 : mCRL2log(log::debug) << "--- pbes after ---\n" << p << std::endl;
1051 1 : }
1052 : };
1053 :
1054 : } // namespace pbes_system
1055 :
1056 : } // namespace mcrl2
1057 :
1058 : #endif // MCRL2_PBES_ABSINTHE_H
|
