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/srf_pbes.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_SRF_PBES_H
13 : #define MCRL2_PBES_SRF_PBES_H
14 :
15 : #include "mcrl2/core/detail/print_utility.h"
16 : #include "mcrl2/pbes/find.h"
17 : #include "mcrl2/pbes/join.h"
18 : #include "mcrl2/pbes/pbes_functions.h"
19 : #include "mcrl2/pbes/rewriters/pbes2data_rewriter.h"
20 :
21 : namespace mcrl2 {
22 :
23 : namespace pbes_system {
24 :
25 : namespace detail {
26 :
27 : inline
28 0 : pbes_expression make_not(const pbes_expression& x)
29 : {
30 0 : if(data::is_data_expression(x) && data::sort_bool::is_not_application(x))
31 : {
32 0 : return data::sort_bool::arg(atermpp::down_cast<data::data_expression>(x));
33 : }
34 0 : else if(is_not(x))
35 : {
36 0 : return accessors::arg(x);
37 : }
38 0 : return not_(x);
39 : }
40 :
41 : } // namespace detail
42 :
43 : class srf_summand
44 : {
45 : protected:
46 : data::variable_list m_parameters;
47 : data::data_expression m_condition;
48 : propositional_variable_instantiation m_X;
49 :
50 : public:
51 0 : srf_summand(
52 : data::variable_list parameters,
53 : const pbes_expression& condition,
54 : propositional_variable_instantiation X
55 : )
56 0 : : m_parameters(std::move(parameters)), m_condition(detail::pbes2data(condition)), m_X(std::move(X))
57 0 : {}
58 :
59 : const data::variable_list& parameters() const
60 : {
61 : return m_parameters;
62 : }
63 :
64 : data::variable_list& parameters()
65 : {
66 : return m_parameters;
67 : }
68 :
69 : const data::data_expression& condition() const
70 : {
71 : return m_condition;
72 : }
73 :
74 : data::data_expression& condition()
75 : {
76 : return m_condition;
77 : }
78 :
79 : const propositional_variable_instantiation& variable() const
80 : {
81 : return m_X;
82 : }
83 :
84 0 : propositional_variable_instantiation& variable()
85 : {
86 0 : return m_X;
87 : }
88 :
89 0 : void add_variables(const data::variable_list& variables)
90 : {
91 0 : m_parameters = variables + m_parameters;
92 0 : }
93 :
94 0 : void add_condition(const pbes_expression& f)
95 : {
96 0 : m_condition = data::lazy::and_(atermpp::down_cast<data::data_expression>(detail::pbes2data(f)), m_condition);
97 0 : }
98 :
99 0 : pbes_expression to_pbes(bool conjunctive) const
100 : {
101 0 : if (conjunctive)
102 : {
103 0 : return make_forall_(m_parameters, imp(m_condition, m_X));
104 : }
105 : else
106 : {
107 0 : return make_exists_(m_parameters, and_(m_condition, m_X));
108 : }
109 : }
110 : };
111 :
112 : inline
113 : std::ostream& operator<<(std::ostream& out, const srf_summand& summand)
114 : {
115 : return out << "variables = " << core::detail::print_list(summand.parameters()) << " f = " << summand.condition() << " X = " << summand.variable();
116 : }
117 :
118 : class srf_equation
119 : {
120 : protected:
121 : fixpoint_symbol m_sigma;
122 : propositional_variable m_variable;
123 : std::vector<srf_summand> m_summands;
124 : bool m_conjunctive;
125 :
126 : public:
127 0 : explicit srf_equation(const fixpoint_symbol& sigma, const propositional_variable& variable, std::vector<srf_summand> summands, bool conjunctive)
128 0 : : m_sigma(sigma), m_variable(variable), m_summands(std::move(summands)), m_conjunctive(conjunctive)
129 0 : {}
130 :
131 : const fixpoint_symbol& symbol() const
132 : {
133 : return m_sigma;
134 : }
135 :
136 : fixpoint_symbol& symbol()
137 : {
138 : return m_sigma;
139 : }
140 :
141 0 : const propositional_variable& variable() const
142 : {
143 0 : return m_variable;
144 : }
145 :
146 0 : propositional_variable& variable()
147 : {
148 0 : return m_variable;
149 : }
150 :
151 : const std::vector<srf_summand>& summands() const
152 : {
153 : return m_summands;
154 : }
155 :
156 0 : std::vector<srf_summand>& summands()
157 : {
158 0 : return m_summands;
159 : }
160 :
161 : bool& is_conjunctive()
162 : {
163 : return m_conjunctive;
164 : }
165 :
166 : bool is_conjunctive() const
167 : {
168 : return m_conjunctive;
169 : }
170 :
171 0 : pbes_equation to_pbes() const
172 : {
173 0 : std::vector<pbes_expression> v;
174 0 : for (const srf_summand& summand: m_summands)
175 : {
176 0 : v.push_back(summand.to_pbes(m_conjunctive));
177 : }
178 0 : pbes_expression rhs = m_conjunctive ? join_and(v.begin(), v.end()) : join_or(v.begin(), v.end());
179 0 : return pbes_equation(m_sigma, m_variable, rhs);
180 0 : }
181 :
182 : void make_total(const srf_summand& true_summand, const srf_summand& false_summand)
183 : {
184 : if (m_conjunctive)
185 : {
186 : m_summands.push_back(true_summand);
187 : }
188 : else
189 : {
190 : m_summands.push_back(false_summand);
191 : }
192 : }
193 : };
194 :
195 : inline
196 : std::ostream& operator<<(std::ostream& out, const srf_equation& eqn)
197 : {
198 : out << "srf equation" << std::endl;
199 : for (const srf_summand& summand: eqn.summands())
200 : {
201 : out << summand << std::endl;
202 : }
203 : return out;
204 : }
205 :
206 : namespace detail {
207 :
208 : std::vector<srf_summand> srf_or(
209 : const pbes_expression& phi,
210 : std::deque<pbes_equation>& equations,
211 : const pbes_equation& eqn,
212 : const data::variable_list& V,
213 : data::set_identifier_generator& id_generator,
214 : const core::identifier_string& X_true,
215 : const core::identifier_string& X_false,
216 : std::vector<srf_equation>& result
217 : );
218 :
219 : struct srf_or_traverser: public pbes_expression_traverser<srf_or_traverser>
220 : {
221 : typedef pbes_expression_traverser<srf_or_traverser> super;
222 : using super::enter;
223 : using super::leave;
224 : using super::apply;
225 :
226 : // The remaining PBES equations
227 : std::deque<pbes_equation>& equations;
228 :
229 : // The current equation
230 : const pbes_equation& eqn;
231 :
232 : const data::variable_list& V;
233 :
234 : // Used for creating new equations
235 : data::set_identifier_generator& id_generator;
236 :
237 : // The names of the true and false equations
238 : const core::identifier_string& X_true;
239 : const core::identifier_string& X_false;
240 :
241 : // The equations of the resulting srf PBES
242 : std::vector<srf_equation>& result;
243 :
244 : // The summands of the generated equation
245 : std::vector<srf_summand> summands;
246 :
247 0 : srf_or_traverser(
248 : std::deque<pbes_equation>& equations_,
249 : const pbes_equation& eqn_,
250 : const data::variable_list& V_,
251 : data::set_identifier_generator& id_generator_,
252 : const core::identifier_string& X_true_,
253 : const core::identifier_string& X_false_,
254 : std::vector<srf_equation>& result_
255 : )
256 0 : : equations(equations_), eqn(eqn_), V(V_), id_generator(id_generator_), X_true(X_true_), X_false(X_false_), result(result_)
257 0 : {}
258 :
259 0 : void apply(const and_& x)
260 : {
261 0 : if (is_simple_expression(x.left()))
262 : {
263 0 : std::size_t size = summands.size();
264 0 : apply(x.right());
265 0 : for (auto i = summands.begin() + size; i != summands.end(); ++i)
266 : {
267 0 : i->add_condition(x.left());
268 : }
269 : }
270 0 : else if (is_simple_expression(x.right()))
271 : {
272 0 : std::size_t size = summands.size();
273 0 : apply(x.left());
274 0 : for (auto i = summands.begin() + size; i != summands.end(); ++i)
275 : {
276 0 : i->add_condition(x.right());
277 : }
278 : }
279 : else
280 : {
281 0 : const propositional_variable& X = eqn.variable();
282 0 : propositional_variable X1(id_generator(X.name()), V);
283 0 : const pbes_expression& f = true_();
284 0 : equations.push_front(pbes_equation(eqn.symbol(), X1, x));
285 0 : summands.emplace_back(data::variable_list(), f, propositional_variable_instantiation(X1.name(), data::make_data_expression_list(V)));
286 0 : }
287 0 : }
288 :
289 0 : void apply(const exists& x)
290 : {
291 0 : std::vector<srf_summand> body_summands = srf_or(x.body(), equations, eqn, V + x.variables(), id_generator, X_true, X_false, result);
292 0 : for (srf_summand& summand: body_summands)
293 : {
294 0 : summand.add_variables(x.variables());
295 : }
296 0 : summands.insert(summands.end(), body_summands.begin(), body_summands.end());
297 0 : }
298 :
299 0 : void apply(const forall& x)
300 : {
301 0 : if (is_simple_expression(x.body()))
302 : {
303 0 : const pbes_expression& f = x.body();
304 0 : const propositional_variable_instantiation& X = propositional_variable_instantiation(X_true, {});
305 0 : summands.emplace_back(x.variables(), f, X);
306 0 : }
307 : else
308 : {
309 0 : const propositional_variable& X = eqn.variable();
310 0 : propositional_variable X1(id_generator(X.name()), V);
311 0 : const pbes_expression& f = true_();
312 0 : equations.push_front(pbes_equation(eqn.symbol(), X1, x));
313 0 : summands.emplace_back(data::variable_list(), f, propositional_variable_instantiation(X1.name(), data::make_data_expression_list(V)));
314 0 : }
315 0 : }
316 :
317 0 : void apply(const propositional_variable_instantiation& x)
318 : {
319 0 : const pbes_expression& f = true_();
320 0 : summands.emplace_back(data::variable_list(), f, x);
321 0 : }
322 :
323 0 : void apply(const pbes_expression& x)
324 : {
325 0 : if (is_simple_expression(x))
326 : {
327 0 : const propositional_variable_instantiation& X = propositional_variable_instantiation(X_true, {});
328 0 : const pbes_expression& f = x;
329 0 : summands.emplace_back(data::variable_list(), f, X);
330 0 : }
331 : else
332 : {
333 0 : super::apply(x);
334 : }
335 0 : }
336 :
337 0 : void apply(const not_& /* x */)
338 : {
339 0 : throw mcrl2::runtime_error("unsupported term!");
340 : }
341 :
342 0 : void apply(const imp& /* x */)
343 : {
344 0 : throw mcrl2::runtime_error("unsupported term!");
345 : }
346 : };
347 :
348 : inline
349 0 : std::vector<srf_summand> srf_or(
350 : const pbes_expression& phi,
351 : std::deque<pbes_equation>& equations,
352 : const pbes_equation& eqn,
353 : const data::variable_list& V,
354 : data::set_identifier_generator& id_generator,
355 : const core::identifier_string& X_true,
356 : const core::identifier_string& X_false,
357 : std::vector<srf_equation>& result
358 : )
359 : {
360 0 : srf_or_traverser f(equations, eqn, V, id_generator, X_true, X_false, result);
361 0 : f.apply(phi);
362 0 : return std::move(f.summands);
363 0 : }
364 :
365 : std::vector<srf_summand> srf_and(
366 : const pbes_expression& phi,
367 : std::deque<pbes_equation>& equations,
368 : const pbes_equation& eqn,
369 : const data::variable_list& V,
370 : data::set_identifier_generator& id_generator,
371 : const core::identifier_string& X_true,
372 : const core::identifier_string& X_false,
373 : std::vector<srf_equation>& result
374 : );
375 :
376 : struct srf_and_traverser: public pbes_expression_traverser<srf_and_traverser>
377 : {
378 : typedef pbes_expression_traverser<srf_and_traverser> super;
379 : using super::enter;
380 : using super::leave;
381 : using super::apply;
382 :
383 : // The remaining PBES equations
384 : std::deque<pbes_equation>& equations;
385 :
386 : // The current equation
387 : const pbes_equation& eqn;
388 :
389 : const data::variable_list& V;
390 :
391 : // Used for creating new equations
392 : data::set_identifier_generator& id_generator;
393 :
394 : // The names of the true and false equations
395 : const core::identifier_string& X_true;
396 : const core::identifier_string& X_false;
397 :
398 : // The equations of the resulting srf PBES
399 : std::vector<srf_equation>& result;
400 :
401 : // The summands of the generated equation
402 : std::vector<srf_summand> summands;
403 :
404 0 : srf_and_traverser(
405 : std::deque<pbes_equation>& equations_,
406 : const pbes_equation& eqn_,
407 : const data::variable_list& V_,
408 : data::set_identifier_generator& id_generator_,
409 : const core::identifier_string& X_true_,
410 : const core::identifier_string& X_false_,
411 : std::vector<srf_equation>& result_
412 : )
413 0 : : equations(equations_), eqn(eqn_), V(V_), id_generator(id_generator_), X_true(X_true_), X_false(X_false_), result(result_)
414 0 : {}
415 :
416 0 : void apply(const or_& x)
417 : {
418 0 : if (is_simple_expression(x.left()))
419 : {
420 0 : std::size_t size = summands.size();
421 0 : apply(x.right());
422 0 : for (auto i = summands.begin() + size; i != summands.end(); ++i)
423 : {
424 0 : i->add_condition(detail::make_not(x.left()));
425 : }
426 : }
427 0 : else if (is_simple_expression(x.right()))
428 : {
429 0 : std::size_t size = summands.size();
430 0 : apply(x.left());
431 0 : for (auto i = summands.begin() + size; i != summands.end(); ++i)
432 : {
433 0 : i->add_condition(detail::make_not(x.right()));
434 : }
435 : }
436 : else
437 : {
438 0 : const propositional_variable& X = eqn.variable();
439 0 : propositional_variable X1(id_generator(X.name()), V);
440 0 : const pbes_expression& f = true_();
441 0 : equations.push_front(pbes_equation(eqn.symbol(), X1, x));
442 0 : summands.emplace_back(data::variable_list(), f, propositional_variable_instantiation(X1.name(), data::make_data_expression_list(V)));
443 0 : }
444 0 : }
445 :
446 0 : void apply(const forall& x)
447 : {
448 0 : std::vector<srf_summand> body_summands = srf_and(x.body(), equations, eqn, V + x.variables(), id_generator, X_true, X_false, result);
449 0 : for (srf_summand& summand: body_summands)
450 : {
451 0 : summand.add_variables(x.variables());
452 : }
453 0 : summands.insert(summands.end(), body_summands.begin(), body_summands.end());
454 0 : }
455 :
456 0 : void apply(const exists& x)
457 : {
458 0 : if (is_simple_expression(x.body()))
459 : {
460 0 : const pbes_expression& f = x.body();
461 0 : const propositional_variable_instantiation& X = propositional_variable_instantiation(X_true, {});
462 0 : summands.emplace_back(x.variables(), f, X);
463 0 : }
464 : else
465 : {
466 0 : const propositional_variable& X = eqn.variable();
467 0 : propositional_variable X1(id_generator(X.name()), V);
468 0 : const pbes_expression& f = true_();
469 0 : equations.push_front(pbes_equation(eqn.symbol(), X1, x));
470 0 : summands.emplace_back(data::variable_list(), f, propositional_variable_instantiation(X1.name(), data::make_data_expression_list(V)));
471 0 : }
472 0 : }
473 :
474 0 : void apply(const propositional_variable_instantiation& x)
475 : {
476 0 : const pbes_expression& f = true_();
477 0 : summands.emplace_back(data::variable_list(), f, x);
478 0 : }
479 :
480 0 : void apply(const pbes_expression& x)
481 : {
482 0 : if (is_simple_expression(x))
483 : {
484 0 : const propositional_variable_instantiation& X = propositional_variable_instantiation(X_false, {});
485 0 : const pbes_expression& f = x;
486 0 : summands.emplace_back(data::variable_list(), detail::make_not(f), X);
487 0 : }
488 : else
489 : {
490 0 : super::apply(x);
491 : }
492 0 : }
493 :
494 0 : void apply(const not_& /* x */)
495 : {
496 0 : throw mcrl2::runtime_error("unsupported term!");
497 : }
498 :
499 0 : void apply(const imp& /* x */)
500 : {
501 0 : throw mcrl2::runtime_error("unsupported term!");
502 : }
503 : };
504 :
505 : inline
506 0 : std::vector<srf_summand> srf_and(
507 : const pbes_expression& phi,
508 : std::deque<pbes_equation>& equations,
509 : const pbes_equation& eqn,
510 : const data::variable_list& V,
511 : data::set_identifier_generator& id_generator,
512 : const core::identifier_string& X_true,
513 : const core::identifier_string& X_false,
514 : std::vector<srf_equation>& result
515 : )
516 : {
517 0 : srf_and_traverser f(equations, eqn, V, id_generator, X_true, X_false, result);
518 0 : f.apply(phi);
519 0 : return std::move(f.summands);
520 0 : }
521 :
522 : inline
523 0 : bool is_conjunctive(const pbes_expression& phi)
524 : {
525 0 : if (is_simple_expression(phi))
526 : {
527 0 : return false;
528 : }
529 0 : else if (is_propositional_variable_instantiation(phi))
530 : {
531 0 : return false;
532 : }
533 0 : else if (is_or(phi))
534 : {
535 0 : const auto& phi_ = atermpp::down_cast<or_>(phi);
536 0 : return (is_simple_expression(phi_.left()) && is_propositional_variable_instantiation(phi_.right())) ||
537 0 : (is_simple_expression(phi_.right()) && is_propositional_variable_instantiation(phi_.left()));
538 : }
539 0 : else if (is_and(phi))
540 : {
541 0 : const auto& phi_ = atermpp::down_cast<and_>(phi);
542 0 : return !((is_simple_expression(phi_.left()) && is_propositional_variable_instantiation(phi_.right())) ||
543 0 : (is_simple_expression(phi_.right()) && is_propositional_variable_instantiation(phi_.left())));
544 : }
545 0 : else if (is_exists(phi))
546 : {
547 0 : return false;
548 : }
549 0 : else if (is_forall(phi))
550 : {
551 0 : return true;
552 : }
553 0 : throw mcrl2::runtime_error("is_conjunctive: unexpected case " + pbes_system::pp(phi));
554 : }
555 :
556 : } // namespace detail
557 :
558 : // explicit representation of a pbes in SRF format
559 : class srf_pbes
560 : {
561 : protected:
562 : data::data_specification m_dataspec;
563 : std::vector<srf_equation> m_equations;
564 : propositional_variable_instantiation m_initial_state;
565 :
566 : public:
567 : srf_pbes() = default;
568 :
569 0 : srf_pbes(
570 : const data::data_specification& dataspec,
571 : std::vector<srf_equation> equations,
572 : propositional_variable_instantiation initial_state
573 : )
574 0 : : m_dataspec(dataspec), m_equations(std::move(equations)), m_initial_state(std::move(initial_state))
575 0 : {}
576 :
577 0 : const std::vector<srf_equation>& equations() const
578 : {
579 0 : return m_equations;
580 : }
581 :
582 0 : std::vector<srf_equation>& equations()
583 : {
584 0 : return m_equations;
585 : }
586 :
587 : const propositional_variable_instantiation& initial_state() const
588 : {
589 : return m_initial_state;
590 : }
591 :
592 0 : propositional_variable_instantiation& initial_state()
593 : {
594 0 : return m_initial_state;
595 : }
596 :
597 : const data::data_specification& data() const
598 : {
599 : return m_dataspec;
600 : }
601 :
602 0 : data::data_specification& data()
603 : {
604 0 : return m_dataspec;
605 : }
606 :
607 0 : pbes to_pbes() const
608 : {
609 0 : std::vector<pbes_equation> v;
610 0 : for (const srf_equation& eqn: equations())
611 : {
612 0 : v.push_back(eqn.to_pbes());
613 : }
614 0 : return pbes(m_dataspec, v, m_initial_state);
615 0 : }
616 :
617 : // Adds extra clauses to the equations to enforce that the PBES is in TSRF format
618 : // Precondition: the last two equations must be the equations corresponding to false and true
619 : void make_total()
620 : {
621 : std::size_t N = m_equations.size();
622 : const srf_summand& false_summand = m_equations[N-2].summands().front();
623 : const srf_summand& true_summand = m_equations[N-1].summands().front();
624 : for (std::size_t i = 0; i < N - 2; i++)
625 : {
626 : m_equations[i].make_total(true_summand, false_summand);
627 : }
628 : }
629 : };
630 :
631 : /// \brief Converts a PBES into standard recursive form
632 : /// \pre The pbes p must be normalized
633 : inline
634 0 : srf_pbes pbes2srf(const pbes& p)
635 : {
636 0 : data::set_identifier_generator id_generator;
637 0 : for (const core::identifier_string& id: pbes_system::find_identifiers(p))
638 : {
639 0 : id_generator.add_identifier(id);
640 0 : }
641 :
642 0 : core::identifier_string X_false = id_generator("X_false");
643 0 : core::identifier_string X_true = id_generator("X_true");
644 0 : pbes_equation eqn_false(fixpoint_symbol::mu(), propositional_variable(X_false, {}), or_(data::sort_bool::false_(), propositional_variable_instantiation(X_false, {})));
645 0 : pbes_equation eqn_true(fixpoint_symbol::nu(), propositional_variable(X_true, {}), propositional_variable_instantiation(X_true, {}));
646 :
647 0 : const auto& p_equations = p.equations();
648 0 : std::deque<pbes_equation> equations(p_equations.begin(), p_equations.end());
649 0 : equations.emplace_back(eqn_false);
650 0 : equations.emplace_back(eqn_true);
651 :
652 0 : std::vector<srf_equation> srf_equations;
653 0 : while (!equations.empty())
654 : {
655 0 : pbes_equation eqn = equations.front();
656 0 : equations.pop_front();
657 0 : bool is_conjunctive = detail::is_conjunctive(eqn.formula());
658 : std::vector<srf_summand> summands = is_conjunctive ?
659 0 : detail::srf_and(eqn.formula(), equations, eqn, eqn.variable().parameters(), id_generator, X_true, X_false, srf_equations) :
660 0 : detail::srf_or(eqn.formula(), equations, eqn, eqn.variable().parameters(), id_generator, X_true, X_false, srf_equations);
661 0 : srf_equations.emplace_back(eqn.symbol(), eqn.variable(), summands, is_conjunctive);
662 0 : }
663 :
664 0 : return srf_pbes(p.data(), std::vector<srf_equation>(srf_equations.begin(), srf_equations.end()), p.initial_state());
665 0 : }
666 :
667 : } // namespace pbes_system
668 :
669 : } // namespace mcrl2
670 :
671 : #endif // MCRL2_PBES_SRF_PBES_H
|
