Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/detail/stategraph_pbes.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_PBES_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_PBES_H
14 :
15 : #include "mcrl2/core/detail/print_utility.h"
16 : #include "mcrl2/pbes/detail/guard_traverser.h"
17 : #include "mcrl2/pbes/detail/stategraph_simplify_rewriter.h"
18 : #include "mcrl2/pbes/detail/stategraph_utility.h"
19 :
20 : namespace mcrl2 {
21 :
22 : namespace pbes_system {
23 :
24 : namespace detail {
25 :
26 : class predicate_variable
27 : {
28 : friend class stategraph_equation;
29 :
30 : protected:
31 : propositional_variable_instantiation X;
32 : pbes_expression m_guard;
33 : data::rewriter::substitution_type m_sigma;
34 : std::map<std::size_t, data::data_expression> m_source; // source[j] = e <=> source(X, i, j) = e
35 : std::map<std::size_t, data::data_expression> m_target; // target[j] = c <=> target(X, i, j) = c
36 : std::map<std::size_t, std::size_t> m_copy; // copy[j] = k <=> copy(X, i, j) = k
37 : std::set<std::size_t> m_used; // j \in used <=> used(X, i, j)
38 : std::set<std::size_t> m_changed; // j \in changed <=> changed(X, i, j)
39 :
40 : public:
41 :
42 108 : predicate_variable(const propositional_variable_instantiation& X_, const pbes_expression& guard_)
43 108 : : X(X_), m_guard(guard_)
44 108 : {}
45 :
46 3 : const propositional_variable_instantiation& variable() const
47 : {
48 3 : return X;
49 : }
50 :
51 108 : const pbes_expression& guard() const
52 : {
53 108 : return m_guard;
54 : }
55 :
56 940 : const core::identifier_string& name() const
57 : {
58 940 : return X.name();
59 : }
60 :
61 321 : const data::rewriter::substitution_type& sigma() const
62 : {
63 321 : return m_sigma;
64 : }
65 :
66 481 : const data::data_expression_list& parameters() const
67 : {
68 481 : return X.parameters();
69 : }
70 :
71 355 : const std::map<std::size_t, data::data_expression>& source() const
72 : {
73 355 : return m_source;
74 : }
75 :
76 : // Returns source(k), or data::undefined_data_expression() if source(k) does not exist.
77 1 : data::data_expression source(std::size_t k) const
78 : {
79 : using utilities::detail::mapped_value;
80 1 : return mapped_value(m_source, k, data::undefined_data_expression());
81 : }
82 :
83 499 : const std::map<std::size_t, data::data_expression>& target() const
84 : {
85 499 : return m_target;
86 : }
87 :
88 : // Returns target(k), or data::undefined_data_expression() if target(k) does not exist.
89 3 : data::data_expression target(std::size_t k) const
90 : {
91 : using utilities::detail::mapped_value;
92 3 : return mapped_value(m_target, k, data::undefined_data_expression());
93 : }
94 :
95 439 : const std::map<std::size_t, std::size_t>& copy() const
96 : {
97 439 : return m_copy;
98 : }
99 :
100 : // Returns copy(k), or data::undefined_index() if copy(k) does not exist.
101 0 : std::size_t copy(std::size_t k) const
102 : {
103 : using utilities::detail::mapped_value;
104 0 : return mapped_value(m_copy, k, data::undefined_index());
105 : }
106 :
107 8 : const std::set<std::size_t>& used() const
108 : {
109 8 : return m_used;
110 : }
111 :
112 4 : const std::set<std::size_t>& changed() const
113 : {
114 4 : return m_changed;
115 : }
116 :
117 108 : void simplify_guard()
118 : {
119 : data::simplify_rewriter r;
120 108 : stategraph_simplify_rewriter<data::simplify_rewriter> R(r);
121 108 : m_guard = R(m_guard);
122 108 : }
123 :
124 0 : std::string print() const
125 : {
126 0 : std::ostringstream out;
127 0 : out << "predicate variable X = " << X << std::endl;
128 0 : out << "guard = " << m_guard << std::endl;
129 0 : out << "sigma = " << m_sigma << std::endl;
130 0 : out << "source = " << core::detail::print_map(m_source) << std::endl;
131 0 : out << "target = " << core::detail::print_map(m_target) << std::endl;
132 0 : out << "copy = " << core::detail::print_map(m_copy) << std::endl;
133 0 : out << "used = " << core::detail::print_set(m_used) << std::endl;
134 0 : out << "changed = " << core::detail::print_set(m_changed) << std::endl;
135 0 : return out.str();
136 0 : }
137 : };
138 :
139 : inline
140 0 : std::ostream& operator<<(std::ostream& out, const predicate_variable& x)
141 : {
142 0 : return out << x.variable();
143 : }
144 :
145 : class stategraph_equation: public pbes_equation
146 : {
147 : protected:
148 : std::vector<predicate_variable> m_predvars;
149 : std::vector<data::variable> m_parameters;
150 : pbes_expression m_condition;
151 : mutable std::vector<std::size_t> m_control_flow_parameter_indices;
152 : mutable data::variable_vector m_control_flow_parameters;
153 : mutable std::vector<std::size_t> m_data_parameter_indices;
154 : mutable data::variable_vector m_data_parameters;
155 :
156 : // Extracts all conjuncts d[i] == e from the pbes expression x, for some i in 0 ... d.size(), and with e a constant.
157 108 : void find_equality_conjuncts(const pbes_expression& x, const std::vector<data::variable>& d, std::map<data::variable, data::data_expression>& result) const
158 : {
159 108 : std::vector<pbes_expression> conjuncts;
160 108 : detail::stategraph_split_and(x, conjuncts);
161 219 : for (const pbes_expression& expr: conjuncts)
162 : {
163 111 : if (data::is_data_expression(expr))
164 : {
165 111 : const auto& v_i = atermpp::down_cast<const data::data_expression>(expr);
166 111 : if (data::is_equal_to_application(v_i))
167 : {
168 103 : const data::data_expression& left = data::binary_left1(v_i);
169 103 : const data::data_expression& right = data::binary_right1(v_i);
170 103 : if (data::is_variable(left) && std::find(d.begin(), d.end(), data::variable(left)) != d.end() && data::is_constant(right))
171 : {
172 103 : const auto& vleft = atermpp::down_cast<data::variable>(left);
173 103 : result[vleft] = right;
174 : }
175 0 : else if (data::is_variable(right) && std::find(d.begin(), d.end(), data::variable(right)) != d.end() && data::is_constant(left))
176 : {
177 0 : const auto& vright = atermpp::down_cast<data::variable>(right);
178 0 : result[vright] = left;
179 : }
180 : }
181 : // handle conjuncts b and !b, with b a variable with sort Bool
182 8 : else if (data::is_variable(v_i) && data::is_bool(v_i.sort()) && std::find(d.begin(), d.end(), data::variable(v_i)) != d.end())
183 : {
184 0 : const auto& v = atermpp::down_cast<data::variable>(v_i);
185 0 : result[v] = data::true_();
186 : }
187 8 : else if (data::is_not(v_i))
188 : {
189 0 : const data::data_expression& narg = data::sort_bool::arg(v_i);
190 0 : if (data::is_variable(narg) && data::is_bool(v_i.sort()) && std::find(d.begin(), d.end(), data::variable(narg)) != d.end())
191 : {
192 0 : const auto& v = atermpp::down_cast<data::variable>(narg);
193 0 : result[v] = data::false_();
194 : }
195 : }
196 : }
197 : }
198 108 : mCRL2log(log::trace) << " computing source: expression = " << x << ", d_X = " << core::detail::print_list(d) << ", result = " << core::detail::print_map(result) << std::endl;
199 108 : }
200 :
201 : bool is_cf(const std::map<core::identifier_string, std::vector<bool> >& is_control_flow, const core::identifier_string& X, std::size_t i) const
202 : {
203 : auto j = is_control_flow.find(X);
204 : assert(j != is_control_flow.end());
205 : const std::vector<bool>& cf = j->second;
206 : assert(i < cf.size());
207 : return cf[i];
208 : }
209 :
210 : // computes the source function for a pbes equation
211 62 : void compute_source()
212 : {
213 170 : for (predicate_variable& predvar: m_predvars)
214 : {
215 108 : std::map<data::variable, data::data_expression> sigma;
216 108 : find_equality_conjuncts(predvar.m_guard, m_parameters, sigma);
217 :
218 : // convert sigma to source
219 429 : for (std::size_t j = 0; j < m_parameters.size(); j++)
220 : {
221 321 : data::variable d_j = m_parameters[j];
222 321 : auto k = sigma.find(d_j);
223 321 : if (k != sigma.end())
224 : {
225 103 : data::data_expression e = k->second;
226 103 : predvar.m_source[j] = e;
227 103 : predvar.m_sigma[d_j] = e;
228 103 : }
229 321 : }
230 108 : }
231 62 : }
232 :
233 62 : void compute_target(data::rewriter& R)
234 : {
235 170 : for (predicate_variable& Ye: m_predvars)
236 : {
237 108 : auto const& e = Ye.parameters();
238 108 : std::size_t j_index = 0;
239 429 : for (auto j = e.begin(); j != e.end(); ++j, ++j_index)
240 : {
241 321 : data::data_expression c = R(*j, Ye.sigma());
242 321 : if (data::is_constant(c))
243 : {
244 113 : Ye.m_target[j_index] = c;
245 : }
246 321 : }
247 : }
248 62 : }
249 :
250 62 : void compute_copy()
251 : {
252 170 : for (predicate_variable& predvar: m_predvars)
253 : {
254 108 : auto const& e = predvar.X.parameters();
255 429 : for (std::size_t j = 0; j < m_parameters.size(); j++)
256 : {
257 321 : std::size_t k_index = 0;
258 1361 : for (auto k = e.begin(); k != e.end(); ++k, ++k_index)
259 : {
260 1040 : if (m_parameters[j] == *k)
261 : {
262 188 : predvar.m_copy[j] = k_index;
263 : }
264 : }
265 : }
266 : }
267 62 : }
268 :
269 62 : void compute_used()
270 : {
271 : using utilities::detail::contains;
272 :
273 62 : auto const& d_X = m_parameters;
274 170 : for (predicate_variable& Ye : m_predvars)
275 : {
276 108 : auto v = pbes_system::find_free_variables(Ye.guard());
277 429 : for (std::size_t j = 0; j < d_X.size(); j++)
278 : {
279 321 : if (contains(v, d_X[j]))
280 : {
281 104 : Ye.m_used.insert(j);
282 : }
283 321 : std::size_t p_index = 0;
284 321 : auto const& e = Ye.parameters();
285 1361 : for (auto p = e.begin(); p != e.end(); ++p, ++p_index)
286 : {
287 1040 : auto freevars = data::find_free_variables(*p);
288 1040 : if (contains(freevars, d_X[j]))
289 : {
290 272 : if ( (Ye.name() != variable().name()) || p_index != j )
291 : {
292 174 : Ye.m_used.insert(j);
293 : }
294 : }
295 1040 : }
296 : }
297 108 : }
298 62 : }
299 :
300 62 : void compute_changed()
301 : {
302 62 : auto const& d_X = m_parameters;
303 170 : for (predicate_variable& Ye: m_predvars)
304 : {
305 108 : if (Ye.name() != variable().name())
306 : {
307 71 : continue;
308 : }
309 37 : std::size_t j_index = 0;
310 37 : auto const& e = Ye.parameters();
311 164 : for (auto j = e.begin(); j != e.end(); ++j, ++j_index)
312 : {
313 127 : if (*j != d_X[j_index])
314 : {
315 78 : Ye.m_changed.insert(j_index);
316 : }
317 : }
318 : }
319 62 : }
320 :
321 : public:
322 62 : stategraph_equation(const pbes_equation& eqn, const data::rewriter& rewr)
323 62 : : pbes_equation(eqn)
324 : {
325 62 : pbes_system::detail::guard_traverser f(rewr);
326 62 : f.apply(eqn.formula());
327 62 : const std::vector<std::pair<propositional_variable_instantiation, pbes_expression>>& guards = f.expression_stack.back().guards;
328 170 : for (const auto& guard: guards)
329 : {
330 108 : m_predvars.emplace_back(guard.first, guard.second);
331 : }
332 62 : m_condition = f.expression_stack.back().condition;
333 62 : data::variable_list params = variable().parameters();
334 62 : m_parameters = std::vector<data::variable>(params.begin(), params.end());
335 62 : }
336 :
337 62 : void compute_source_target_copy(data::rewriter& R)
338 : {
339 62 : compute_source();
340 62 : compute_target(R);
341 62 : compute_copy();
342 62 : compute_used();
343 62 : compute_changed();
344 62 : }
345 :
346 : /// \brief Sets the control flow parameters of this equation
347 : /// \param CFP contains the indices of the control flow parameters of this equation
348 49 : void set_control_flow_parameters(const std::set<std::size_t>& CFP) const
349 : {
350 49 : m_control_flow_parameter_indices = std::vector<std::size_t>(CFP.begin(), CFP.end());
351 101 : for (std::size_t i: m_control_flow_parameter_indices)
352 : {
353 52 : m_control_flow_parameters.push_back(m_parameters[i]);
354 : }
355 49 : }
356 :
357 : /// \brief Sets the data parameters of this equation
358 : /// \param DP contains the indices of the control flow parameters of this equation
359 62 : void set_data_parameters(const std::set<std::size_t>& DP) const
360 : {
361 62 : m_data_parameter_indices = std::vector<std::size_t>(DP.begin(), DP.end());
362 179 : for (std::size_t i: m_data_parameter_indices)
363 : {
364 117 : m_data_parameters.push_back(m_parameters[i]);
365 : }
366 62 : }
367 :
368 0 : const data::variable_vector& control_flow_parameters() const
369 : {
370 0 : return m_control_flow_parameters;
371 : }
372 :
373 0 : const std::vector<std::size_t>& control_flow_parameter_indices() const
374 : {
375 0 : return m_control_flow_parameter_indices;
376 : }
377 :
378 : const data::variable_vector& data_parameters() const
379 : {
380 : return m_data_parameters;
381 : }
382 :
383 11 : const std::vector<std::size_t>& data_parameter_indices() const
384 : {
385 11 : return m_data_parameter_indices;
386 : }
387 :
388 : bool is_simple() const
389 : {
390 : for (const predicate_variable& predvar: m_predvars)
391 : {
392 : // TODO check this
393 : if (!pbes_system::is_false(predvar.guard()))
394 : {
395 : return false;
396 : }
397 : }
398 : return true;
399 : }
400 :
401 : const pbes_expression& simple_guard() const
402 : {
403 : return m_condition;
404 : }
405 :
406 617 : const std::vector<data::variable>& parameters() const
407 : {
408 617 : return m_parameters;
409 : }
410 :
411 438 : const std::vector<predicate_variable>& predicate_variables() const
412 : {
413 438 : return m_predvars;
414 : }
415 :
416 62 : std::vector<predicate_variable>& predicate_variables()
417 : {
418 62 : return m_predvars;
419 : }
420 :
421 : std::string print() const
422 : {
423 : std::ostringstream out;
424 : out << "equation = " << print_equation(*this) << std::endl;
425 : out << "guards:" << std::endl;
426 : for (const predicate_variable& predvar: m_predvars)
427 : {
428 : out << "variable = " << predvar.variable() << " guard = " << predvar.guard() << std::endl;
429 : }
430 : out << "simple = " << std::boolalpha << is_simple() << std::endl;
431 : return out.str();
432 : }
433 :
434 0 : std::string print_source_target_copy() const
435 : {
436 0 : std::ostringstream out;
437 0 : std::string X(variable().name());
438 0 : for (std::size_t i = 0; i < m_predvars.size(); i++)
439 : {
440 0 : out << " predvar[" << i << "] = " << m_predvars[i] << " guard = " << m_predvars[i].guard() << std::endl;
441 :
442 : // source
443 0 : auto const& source = m_predvars[i].source();
444 0 : for (const auto& j: source)
445 : {
446 0 : out << " source(" << X << ", " << i << ", " << j.first << ") = " << j.second << std::endl;
447 : }
448 :
449 : // sigma
450 0 : out << " sigma = " << m_predvars[i].sigma() << std::endl;
451 :
452 : // target
453 0 : const std::map<std::size_t, data::data_expression>& target = m_predvars[i].target();
454 0 : for (const auto& j: target)
455 : {
456 0 : out << " target(" << X << ", " << i << ", " << j.first << ") = " << j.second << std::endl;
457 : }
458 :
459 : // copy
460 0 : auto const& copy = m_predvars[i].copy();
461 0 : for (const auto& j: copy)
462 : {
463 0 : out << " copy(" << X << ", " << i << ", " << j.first << ") = " << j.second << std::endl;
464 : }
465 0 : out << " used = " << core::detail::print_set(m_predvars[i].used()) << std::endl;
466 0 : out << " changed = " << core::detail::print_set(m_predvars[i].changed()) << std::endl;
467 : }
468 0 : return out.str();
469 0 : }
470 :
471 : // Removes the values from e that correspond to a data parameter
472 0 : data::data_expression_list project(const data::data_expression_list& e) const
473 : {
474 0 : assert(e.size() == m_parameters.size());
475 0 : data::data_expression_vector result;
476 0 : for (std::size_t i: m_control_flow_parameter_indices)
477 : {
478 0 : result.push_back(nth_element(e, i));
479 : }
480 0 : return data::data_expression_list(result.begin(), result.end());
481 0 : }
482 : };
483 :
484 : // explicit representation of a pbes in STATEGRAPH format
485 : class stategraph_pbes
486 : {
487 : protected:
488 : data::data_specification m_data;
489 : std::vector<stategraph_equation> m_equations;
490 : std::set<data::variable> m_global_variables;
491 : propositional_variable_instantiation m_initial_state;
492 :
493 : public:
494 27 : stategraph_pbes() = default;
495 :
496 : /// \brief Constructor
497 : /// \pre The pbes p must be in STATEGRAPH format
498 27 : stategraph_pbes(const pbes& p, const data::rewriter& rewr)
499 27 : : m_data(p.data()), m_global_variables(p.global_variables()), m_initial_state(p.initial_state())
500 : {
501 27 : const std::vector<pbes_equation>& equations = p.equations();
502 89 : for (const pbes_equation& equation: equations)
503 : {
504 62 : m_equations.emplace_back(equation, rewr);
505 : }
506 27 : }
507 :
508 434 : const std::vector<stategraph_equation>& equations() const
509 : {
510 434 : return m_equations;
511 : }
512 :
513 166 : std::vector<stategraph_equation>& equations()
514 : {
515 166 : return m_equations;
516 : }
517 :
518 : const std::set<data::variable>& global_variables() const
519 : {
520 : return m_global_variables;
521 : }
522 :
523 : std::set<data::variable>& global_variables()
524 : {
525 : return m_global_variables;
526 : }
527 :
528 35 : const propositional_variable_instantiation& initial_state() const
529 : {
530 35 : return m_initial_state;
531 : }
532 :
533 0 : const data::data_specification& data() const
534 : {
535 0 : return m_data;
536 : }
537 :
538 : data::data_expression source(std::size_t k, std::size_t i, std::size_t n) const
539 : {
540 : auto const& eqn = equations()[k];
541 : auto const& sigma = eqn.predicate_variables()[i].sigma();
542 : data::variable d_n = eqn.parameters()[n];
543 : data::data_expression x = sigma(d_n);
544 : if (x == d_n)
545 : {
546 : return data::undefined_data_expression();
547 : }
548 : else
549 : {
550 : return x;
551 : }
552 : }
553 :
554 27 : void compute_source_target_copy()
555 : {
556 27 : data::rewriter R(m_data);
557 89 : for (stategraph_equation& eqn: equations())
558 : {
559 62 : eqn.compute_source_target_copy(R);
560 : }
561 27 : }
562 :
563 0 : std::string print_source_target_copy() const
564 : {
565 0 : std::ostringstream out;
566 0 : for (const stategraph_equation& eqn: equations())
567 : {
568 0 : out << "equation = " << print_equation(eqn) << std::endl;
569 0 : out << eqn.print_source_target_copy() << std::endl;
570 : }
571 0 : return out.str();
572 0 : }
573 : };
574 :
575 : inline
576 422 : std::vector<stategraph_equation>::const_iterator find_equation(const stategraph_pbes& p, const core::identifier_string& X, bool warn = true)
577 : {
578 422 : auto const& equations = p.equations();
579 712 : for (auto i = equations.begin(); i != equations.end(); ++i)
580 : {
581 712 : if (i->variable().name() == X)
582 : {
583 422 : return i;
584 : }
585 : }
586 0 : if (warn)
587 : {
588 0 : mCRL2log(log::debug) << "find_equation: could not find predicate variable " << X << std::endl;
589 : }
590 0 : return equations.end();
591 : }
592 :
593 : } // namespace detail
594 :
595 : } // namespace pbes_system
596 :
597 : } // namespace mcrl2
598 :
599 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_PBES_H
|
