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/guard_traverser.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_GUARD_TRAVERSER_H
13 : #define MCRL2_PBES_DETAIL_GUARD_TRAVERSER_H
14 :
15 : #include "mcrl2/data/rewriter.h"
16 : #include "mcrl2/pbes/pbes_functions.h"
17 : #include "mcrl2/pbes/rewrite.h"
18 : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
19 :
20 : #ifdef MCRL2_PBES_STATEGRAPH_CHECK_GUARDS
21 : #include "mcrl2/pbes/find.h"
22 : #endif
23 :
24 : namespace mcrl2 {
25 :
26 : namespace pbes_system {
27 :
28 : namespace detail {
29 :
30 : #ifdef MCRL2_PBES_STATEGRAPH_CHECK_GUARDS
31 : inline
32 : pbes_expression guard_s(const pbes_expression& x)
33 : {
34 : if (is_simple_expression(x))
35 : {
36 : return x;
37 : }
38 : else
39 : {
40 : return true_();
41 : }
42 : }
43 :
44 : inline
45 : pbes_expression guard_n(const pbes_expression& x)
46 : {
47 : if (is_simple_expression(x))
48 : {
49 : return data::optimized_not(x);
50 : }
51 : else
52 : {
53 : return true_();
54 : }
55 : }
56 :
57 : inline
58 : bool has_propositional_variable(const pbes_expression& x, const propositional_variable_instantiation& X)
59 : {
60 : std::set<propositional_variable_instantiation> xocc = find_propositional_variable_instantiations(x);
61 : return xocc.find(X) != xocc.end();
62 : }
63 :
64 : inline
65 : pbes_expression guard_impl(const propositional_variable_instantiation& X, const pbes_expression& x)
66 : {
67 : if (data::is_data_expression(x))
68 : {
69 : return false_();
70 : }
71 : else if (is_propositional_variable_instantiation(x))
72 : {
73 : return true_();
74 : }
75 : else if (pbes_system::is_true(x))
76 : {
77 : return false_();
78 : }
79 : else if (pbes_system::is_false(x))
80 : {
81 : return false_();
82 : }
83 : else if (pbes_system::is_not(x))
84 : {
85 : pbes_expression phi = pbes_system::not_(atermpp::aterm_appl(x)).operand();
86 : return data::optimized_not(guard_impl(X, phi));
87 : }
88 : else if (pbes_system::is_and(x))
89 : {
90 : pbes_expression phi = pbes_system::and_(atermpp::aterm_appl(x)).left();
91 : pbes_expression psi = pbes_system::and_(atermpp::aterm_appl(x)).right();
92 : if (has_propositional_variable(psi, X))
93 : {
94 : return data::optimized_and(guard_s(phi), guard_impl(X, psi));
95 : }
96 : else
97 : {
98 : return data::optimized_and(guard_s(psi), guard_impl(X, phi));
99 : }
100 : }
101 : else if (pbes_system::is_or(x))
102 : {
103 : pbes_expression phi = pbes_system::or_(atermpp::aterm_appl(x)).left();
104 : pbes_expression psi = pbes_system::or_(atermpp::aterm_appl(x)).right();
105 : if (has_propositional_variable(psi, X))
106 : {
107 : return data::optimized_and(guard_n(phi), guard_impl(X, psi));
108 : }
109 : else
110 : {
111 : return data::optimized_and(guard_n(psi), guard_impl(X, phi));
112 : }
113 : }
114 : else if (pbes_system::is_imp(x))
115 : {
116 : pbes_expression phi = pbes_system::imp(atermpp::aterm_appl(x)).left();
117 : pbes_expression psi = pbes_system::imp(atermpp::aterm_appl(x)).right();
118 : return guard_impl(X, or_(not_(phi), psi));
119 : }
120 : else if (pbes_system::is_forall(x))
121 : {
122 : pbes_expression phi = pbes_system::forall(atermpp::aterm_appl(x)).body();
123 : return guard_impl(X, phi);
124 : }
125 : else if (pbes_system::is_exists(x))
126 : {
127 : pbes_expression phi = pbes_system::exists(atermpp::aterm_appl(x)).body();
128 : return guard_impl(X, phi);
129 : }
130 : throw mcrl2::runtime_error("guard_impl: unknown term " + pbes_system::pp(x));
131 : return pbes_expression();
132 : }
133 :
134 : // Direct implementation of the definition, to be used for checking results.
135 : inline
136 : pbes_expression guard(const propositional_variable_instantiation& X, const pbes_expression& x)
137 : {
138 : std::multiset<propositional_variable_instantiation> xocc;
139 : find_propositional_variable_instantiations(x, std::inserter(xocc, xocc.end()));
140 : if (xocc.count(X) != 1)
141 : {
142 : throw mcrl2::runtime_error("guard is undefined for " + pbes_system::pp(X));
143 : }
144 : return guard_impl(X, x);
145 : }
146 : #endif // MCRL2_PBES_STATEGRAPH_CHECK_GUARDS
147 :
148 : struct guard_expression
149 : {
150 : std::vector<std::pair<propositional_variable_instantiation, pbes_expression> > guards;
151 : pbes_expression condition;
152 :
153 1199 : bool is_simple() const
154 : {
155 1199 : return guards.empty();
156 : }
157 :
158 186 : void add_guard(const pbes_expression& guard)
159 : {
160 186 : if (is_simple())
161 : {
162 0 : data::optimized_and(condition, guard, condition);
163 : }
164 : else
165 : {
166 374 : for (auto& g: guards)
167 : {
168 188 : data::optimized_and(g.second, guard, g.second);
169 : }
170 : }
171 186 : }
172 :
173 150 : void negate()
174 : {
175 150 : if (is_simple())
176 : {
177 150 : data::optimized_not(condition, condition);
178 : }
179 : else
180 : {
181 0 : for (auto& g: guards)
182 : {
183 0 : data::optimized_not(g.second, g.second);
184 : }
185 : }
186 150 : }
187 :
188 365 : explicit guard_expression(const pbes_expression& condition_ = pbes_system::true_())
189 365 : : condition(condition_)
190 365 : {}
191 :
192 : #ifdef MCRL2_PBES_STATEGRAPH_CHECK_GUARDS
193 : // Check if the guards were correctly computed with respect to x.
194 : template <typename PbesRewriter>
195 : bool check_guards(const pbes_expression& x, PbesRewriter R) const
196 : {
197 : mCRL2log(log::debug, "stategraph") << "check_guards: x = " << pbes_system::pp(x) << std::endl;
198 : bool result = true;
199 : for (auto i = guards.begin(); i != guards.end(); ++i)
200 : {
201 : try
202 : {
203 : const propositional_variable_instantiation& X = i->first;
204 : const pbes_expression& g1 = i->second;
205 : pbes_expression g2 = guard(X, x);
206 : if (pbes_rewrite(g1, R) != pbes_rewrite(g2, R))
207 : {
208 : result = false;
209 : mCRL2log(log::debug, "stategraph") << " g1 = " << g1 << " g2 = " << g2 << std::endl;
210 : mCRL2log(log::debug, "stategraph") << "guard error: X = " << X << " g1 = " << pbes_rewrite(g1, R) << " g2 = " << pbes_rewrite(g2, R) << std::endl;
211 : }
212 : }
213 : catch (mcrl2::runtime_error&)
214 : {
215 : // do not check multiple instances of predicate variables
216 : }
217 : }
218 : return result;
219 : }
220 : #else
221 : // Check if the guards were correctly computed with respect to x.
222 : template <typename PbesRewriter>
223 735 : bool check_guards(const pbes_expression& /* x */, PbesRewriter /* R */) const
224 : {
225 735 : return true;
226 : }
227 : #endif
228 : };
229 :
230 : inline
231 0 : std::ostream& operator<<(std::ostream& out, const guard_expression& x)
232 : {
233 0 : if (x.is_simple())
234 : {
235 0 : out << "condition = " << pbes_system::pp(x.condition) << std::endl;
236 : }
237 : else
238 : {
239 0 : for (const auto& g: x.guards)
240 : {
241 0 : out << pbes_system::pp(g.first) << " guard = " << pbes_system::pp(g.second) << std::endl;
242 : }
243 : }
244 0 : return out;
245 : }
246 :
247 : /// \brief Computes a multimap of propositional variable instantiations and the corresponding guards from a PBES expression
248 : struct guard_traverser: public pbes_expression_traverser<guard_traverser>
249 : {
250 : typedef pbes_expression_traverser<guard_traverser> super;
251 : using super::enter;
252 : using super::leave;
253 : using super::apply;
254 :
255 : simplify_data_rewriter<data::rewriter> R;
256 : std::vector<guard_expression> expression_stack;
257 :
258 83 : explicit guard_traverser(const data::rewriter& r)
259 83 : : R(r)
260 83 : {}
261 :
262 647 : void push(const guard_expression& x)
263 : {
264 647 : mCRL2log(log::trace) << "<push>" << "\n" << x << std::endl;
265 647 : expression_stack.push_back(x);
266 647 : }
267 :
268 1347 : guard_expression& top()
269 : {
270 1347 : return expression_stack.back();
271 : }
272 :
273 : const guard_expression& top() const
274 : {
275 : return expression_stack.back();
276 : }
277 :
278 564 : guard_expression pop()
279 : {
280 564 : guard_expression result = top();
281 564 : expression_stack.pop_back();
282 564 : return result;
283 : }
284 :
285 186 : void leave(const data::data_expression& x)
286 : {
287 186 : push(guard_expression(x));
288 186 : assert(top().check_guards(x, R));
289 186 : }
290 :
291 179 : void leave(const pbes_system::propositional_variable_instantiation& x)
292 : {
293 179 : guard_expression node;
294 179 : node.guards.emplace_back(x, pbes_system::true_());
295 179 : push(node);
296 179 : assert(top().check_guards(x, R));
297 179 : }
298 :
299 50 : void leave(const pbes_system::not_& x)
300 : {
301 50 : utilities::mcrl2_unused(x);
302 :
303 50 : top().negate();
304 50 : assert(top().check_guards(x, R));
305 50 : }
306 :
307 104 : void leave(const pbes_system::and_& x)
308 : {
309 104 : utilities::mcrl2_unused(x);
310 :
311 104 : guard_expression right = pop();
312 104 : guard_expression left = pop();
313 104 : pbes_expression new_condition;
314 104 : data::optimized_and(new_condition, left.condition, right.condition);
315 104 : if (left.is_simple() && right.is_simple())
316 : {
317 0 : left.condition = new_condition;
318 0 : push(left);
319 : }
320 104 : else if (left.is_simple())
321 : {
322 12 : right.add_guard(left.condition);
323 12 : right.condition = new_condition;
324 12 : push(right);
325 : }
326 92 : else if (right.is_simple())
327 : {
328 2 : left.add_guard(right.condition);
329 2 : left.condition = new_condition;
330 2 : push(left);
331 : }
332 : else
333 : {
334 90 : left.guards.insert(left.guards.end(), right.guards.begin(), right.guards.end());
335 90 : left.condition = new_condition;
336 90 : push(left);
337 : }
338 104 : assert(top().check_guards(x, R));
339 104 : }
340 :
341 78 : void leave(const pbes_system::or_& x)
342 : {
343 78 : utilities::mcrl2_unused(x);
344 :
345 78 : guard_expression right = pop();
346 78 : guard_expression left = pop();
347 78 : pbes_expression new_condition;
348 78 : data::optimized_or(new_condition, left.condition, right.condition);
349 78 : if (left.is_simple() && right.is_simple())
350 : {
351 0 : left.condition = new_condition;
352 0 : push(left);
353 : }
354 78 : else if (left.is_simple())
355 : {
356 71 : pbes_expression d;
357 71 : data::optimized_not(d, left.condition);
358 71 : right.add_guard(d);
359 71 : right.condition = new_condition;
360 71 : push(right);
361 71 : }
362 7 : else if (right.is_simple())
363 : {
364 1 : pbes_expression d;
365 1 : data::optimized_not(d, right.condition);
366 1 : left.add_guard(d);
367 1 : left.condition = new_condition;
368 1 : push(left);
369 1 : }
370 : else
371 : {
372 6 : left.guards.insert(left.guards.end(), right.guards.begin(), right.guards.end());
373 6 : left.condition = new_condition;
374 6 : push(left);
375 : }
376 78 : assert(top().check_guards(x, R));
377 78 : }
378 :
379 100 : void leave(const pbes_system::imp& x)
380 : {
381 100 : utilities::mcrl2_unused(x);
382 :
383 100 : guard_expression right = pop();
384 100 : guard_expression left = pop();
385 100 : left.negate();
386 100 : pbes_expression new_condition;
387 100 : data::optimized_or(new_condition, left.condition, right.condition);
388 100 : if (left.is_simple() && right.is_simple())
389 : {
390 0 : left.condition = new_condition;
391 0 : push(left);
392 : }
393 100 : else if (left.is_simple())
394 : {
395 100 : pbes_expression d;
396 100 : data::optimized_not(d, left.condition);
397 100 : right.add_guard(d);
398 100 : right.condition = new_condition;
399 100 : push(right);
400 100 : }
401 0 : else if (right.is_simple())
402 : {
403 0 : pbes_expression d;
404 0 : data::optimized_not(d, right.condition);
405 0 : left.add_guard(d);
406 0 : left.condition = new_condition;
407 0 : push(left);
408 0 : }
409 : else
410 : {
411 0 : left.guards.insert(left.guards.end(), right.guards.begin(), right.guards.end());
412 0 : left.condition = new_condition;
413 0 : push(left);
414 : }
415 100 : assert(top().check_guards(x, R));
416 100 : }
417 :
418 17 : void leave(const pbes_system::forall& x)
419 : {
420 : // If x is a simple expression, quantifiers need to be handled differently!
421 17 : if (top().is_simple())
422 : {
423 2 : top().condition = x;
424 : }
425 17 : assert(top().check_guards(x, R));
426 17 : }
427 :
428 0 : void leave(const pbes_system::exists& x)
429 : {
430 : // If x is a simple expression, quantifiers need to be handled differently!
431 0 : if (top().is_simple())
432 : {
433 0 : top().condition = x;
434 : }
435 0 : assert(top().check_guards(x, R));
436 0 : }
437 : };
438 :
439 : } // namespace detail
440 :
441 : } // namespace pbes_system
442 :
443 : } // namespace mcrl2
444 :
445 : #endif // MCRL2_PBES_DETAIL_GUARD_TRAVERSER_H
|
