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/pfnf_traverser.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_PFNF_TRAVERSER_H
13 : #define MCRL2_PBES_DETAIL_PFNF_TRAVERSER_H
14 :
15 : #include "mcrl2/data/rewriter.h"
16 : #include "mcrl2/pbes/replace.h"
17 : #include <numeric>
18 :
19 : #ifdef MCRL2_PFNF_VISITOR_DEBUG
20 : #include "mcrl2/data/print.h"
21 : #endif
22 :
23 : namespace mcrl2
24 : {
25 :
26 : namespace pbes_system
27 : {
28 :
29 : namespace detail
30 : {
31 :
32 : /// \brief Represents a quantifier Qv:V. If the bool is true it is a forall, otherwise an exists.
33 : typedef std::pair<bool, data::variable_list> pfnf_traverser_quantifier;
34 :
35 : struct variable_variable_substitution
36 : {
37 : std::map<data::variable, data::variable> sigma;
38 :
39 6 : data::variable operator()(const data::variable& v) const
40 : {
41 6 : std::map<data::variable, data::variable>::const_iterator i = sigma.find(v);
42 6 : if (i == sigma.end())
43 : {
44 1 : return v;
45 : }
46 5 : return i->second;
47 : }
48 :
49 4 : data::variable_list operator()(const data::variable_list& variables) const
50 : {
51 4 : std::vector<data::variable> result;
52 8 : for (const data::variable& v: variables)
53 : {
54 4 : result.push_back((*this)(v));
55 : }
56 8 : return data::variable_list(result.begin(),result.end());
57 4 : }
58 :
59 : std::string to_string() const
60 : {
61 : std::ostringstream out;
62 : out << "[";
63 : for (std::map<data::variable, data::variable>::const_iterator i = sigma.begin(); i != sigma.end(); ++i)
64 : {
65 : if (i != sigma.begin())
66 : {
67 : out << ", ";
68 : }
69 : out << data::pp(i->first) << " := " << data::pp(i->second);
70 : }
71 : out << "]";
72 : return out.str();
73 : }
74 : };
75 :
76 : struct variable_data_expression_substitution
77 : {
78 : typedef data::variable variable_type;
79 : typedef data::data_expression expression_type;
80 :
81 : const variable_variable_substitution& sigma;
82 :
83 3 : variable_data_expression_substitution(const variable_variable_substitution& sigma_)
84 3 : : sigma(sigma_)
85 3 : {}
86 :
87 2 : data::data_expression operator()(const data::variable& v) const
88 : {
89 2 : return sigma(v);
90 : }
91 : };
92 :
93 : /// \brief Represents the implication g => ( X0(e0) \/ ... \/ Xk(ek) )
94 : struct pfnf_traverser_implication
95 : {
96 : pbes_expression g;
97 : std::vector<propositional_variable_instantiation> rhs;
98 :
99 75 : pfnf_traverser_implication(const atermpp::aterm_appl& g_, const std::vector<propositional_variable_instantiation>& rhs_)
100 75 : : g(g_),
101 75 : rhs(rhs_)
102 75 : {}
103 :
104 : pfnf_traverser_implication(const atermpp::aterm_appl& x)
105 : : g(x)
106 : {}
107 :
108 : // applies a substitution to variables
109 0 : void substitute(const variable_variable_substitution& sigma)
110 : {
111 0 : for (propositional_variable_instantiation& v: rhs)
112 : {
113 0 : v = pbes_system::replace_free_variables(v, variable_data_expression_substitution(sigma));
114 : }
115 0 : g = pbes_system::replace_free_variables(g, variable_data_expression_substitution(sigma));
116 0 : }
117 :
118 : };
119 :
120 : struct pfnf_traverser_expression
121 : {
122 : pbes_expression expr;
123 : std::vector<pfnf_traverser_quantifier> quantifiers;
124 : std::vector<pfnf_traverser_implication> implications;
125 :
126 80 : pfnf_traverser_expression(const atermpp::aterm_appl& x, const std::vector<pfnf_traverser_quantifier>& quantifiers_, const std::vector<pfnf_traverser_implication>& implications_)
127 80 : : expr(x),
128 80 : quantifiers(quantifiers_),
129 80 : implications(implications_)
130 80 : {}
131 :
132 201 : pfnf_traverser_expression(const atermpp::aterm_appl& x)
133 201 : : expr(x)
134 201 : {}
135 :
136 : // applies a substitution to variables
137 3 : void substitute(const variable_variable_substitution& sigma)
138 : {
139 7 : for (pfnf_traverser_quantifier& quantifier: quantifiers)
140 : {
141 4 : quantifier.second = sigma(quantifier.second);
142 : }
143 3 : for (pfnf_traverser_implication& implication: implications)
144 : {
145 0 : implication.substitute(sigma);
146 : }
147 3 : expr = pbes_system::replace_free_variables(expr, variable_data_expression_substitution(sigma));
148 3 : }
149 : };
150 :
151 : } // namespace detail
152 :
153 : } // namespace pbes_system
154 :
155 : } // namespace mcrl2
156 :
157 : namespace mcrl2
158 : {
159 :
160 : namespace pbes_system
161 : {
162 :
163 : namespace detail
164 : {
165 :
166 : /// \brief Concatenates two containers
167 : /// \param x A container
168 : /// \param y A container
169 : /// \return The concatenation of x and y
170 : template <typename Container>
171 80 : Container concat(const Container& x, const Container& y)
172 : {
173 80 : Container result = x;
174 80 : result.insert(result.end(), y.begin(), y.end());
175 80 : return result;
176 0 : }
177 :
178 : /// \brief Applies the PFNF rewriter to a PBES expression.
179 : struct pfnf_traverser: public pbes_expression_traverser<pfnf_traverser>
180 : {
181 : typedef pbes_expression_traverser<pfnf_traverser> super;
182 : using super::enter;
183 : using super::leave;
184 : using super::apply;
185 :
186 : // makes sure there are no name clashes between quantifier variables in left and right
187 : // TODO: the efficiency can be increased by maintaining some additional data structures
188 46 : void resolve_name_clashes(pfnf_traverser_expression& left, pfnf_traverser_expression& right)
189 : {
190 46 : std::set<data::variable> left_variables;
191 46 : std::set<data::variable> right_variables;
192 46 : std::set<data::variable> name_clashes;
193 52 : for (std::vector<pfnf_traverser_quantifier>::const_iterator i = left.quantifiers.begin(); i != left.quantifiers.end(); ++i)
194 : {
195 6 : left_variables.insert(i->second.begin(), i->second.end());
196 : }
197 59 : for (std::vector<pfnf_traverser_quantifier>::const_iterator j = right.quantifiers.begin(); j != right.quantifiers.end(); ++j)
198 : {
199 26 : for (const data::variable& v: j->second)
200 : {
201 13 : right_variables.insert(v);
202 13 : if (left_variables.find(v) != left_variables.end())
203 : {
204 3 : name_clashes.insert(v);
205 : }
206 : }
207 : }
208 :
209 : #ifdef MCRL2_PFNF_VISITOR_DEBUG
210 : std::cout << "NAME CLASHES: " << core::detail::print_set(name_clashes) << std::endl;
211 : #endif
212 :
213 46 : if (!name_clashes.empty())
214 : {
215 3 : data::set_identifier_generator generator;
216 8 : for (const data::variable& v: left_variables)
217 : {
218 5 : generator.add_identifier(v.name());
219 : }
220 7 : for (const data::variable& v: right_variables)
221 : {
222 4 : generator.add_identifier(v.name());
223 : }
224 3 : variable_variable_substitution sigma;
225 6 : for (const data::variable& v: name_clashes)
226 : {
227 3 : sigma.sigma[v] = data::variable(generator(std::string(v.name())), v.sort());
228 : }
229 : #ifdef MCRL2_PFNF_VISITOR_DEBUG
230 : std::cout << "LEFT\n"; print_expression(left);
231 : std::cout << "RIGHT BEFORE\n"; print_expression(right);
232 : std::cout << "SIGMA = " << sigma.to_string() << std::endl;
233 : #endif
234 3 : right.substitute(sigma);
235 : #ifdef MCRL2_PFNF_VISITOR_DEBUG
236 : std::cout << "RIGHT AFTER\n"; print_expression(right);
237 : #endif
238 3 : }
239 46 : }
240 :
241 65 : pbes_expression make_and(const pfnf_traverser_expression& left, const pfnf_traverser_expression& right) const
242 : {
243 65 : pbes_expression result;
244 65 : data::optimized_and(result, left.expr, right.expr);
245 65 : return result;
246 0 : }
247 :
248 22 : pbes_expression make_or(const pfnf_traverser_expression& left, const pfnf_traverser_expression& right) const
249 : {
250 22 : pbes_expression result;
251 22 : data::optimized_or(result, left.expr, right.expr);
252 22 : return result;
253 0 : }
254 :
255 44 : pbes_expression make_not(const pfnf_traverser_expression& x) const
256 : {
257 44 : pbes_expression result;
258 44 : data::optimized_not(result, x.expr);
259 44 : return result;
260 0 : }
261 :
262 : /// \brief A stack containing expressions in PFNF format.
263 : std::vector<pfnf_traverser_expression> expression_stack;
264 :
265 : /// \brief A stack containing quantifier variables.
266 : std::vector<data::variable_list> quantifier_stack;
267 :
268 : /// \brief Returns the top element of the expression stack converted to a pbes expression.
269 : /// \return The top element of the expression stack converted to a pbes expression.
270 19 : pbes_expression evaluate() const
271 : {
272 19 : assert(!expression_stack.empty());
273 19 : const pfnf_traverser_expression& expr = expression_stack.back();
274 19 : pbes_expression h = expr.expr;
275 19 : pbes_expression result = h;
276 19 : const pbes_expression F = false_();
277 63 : for (const pfnf_traverser_implication& impl: expr.implications)
278 : {
279 44 : pbes_expression p;
280 : pbes_expression x = std::accumulate(impl.rhs.begin(), impl.rhs.end(), F,
281 110 : [&p](const pbes_expression& arg1, const pbes_expression& arg2) -> const pbes_expression
282 : {
283 55 : data::optimized_or(p, arg1, arg2);
284 55 : return p;
285 44 : });
286 44 : data::optimized_imp(p, impl.g, x);
287 44 : data::optimized_and(result, result, p);
288 44 : }
289 35 : for (const pfnf_traverser_quantifier& q: expr.quantifiers)
290 : {
291 16 : if (q.first)
292 : {
293 13 : result = forall(q.second, result);
294 : }
295 : else
296 : {
297 3 : result = exists(q.second, result);
298 : }
299 : }
300 38 : return result;
301 19 : }
302 :
303 : /// \brief Prints an expression
304 : /// \param expr An expression
305 : void print_expression(const pfnf_traverser_expression& expr) const
306 : {
307 : const std::vector<pfnf_traverser_quantifier>& q = expr.quantifiers;
308 : pbes_expression h = expr.expr;
309 : const std::vector<pfnf_traverser_implication>& g = expr.implications;
310 : for (const pfnf_traverser_quantifier& i: expr.quantifiers)
311 : {
312 : std::cout << (i.first ? "forall " : "exists ") << data::pp(i.second) << " ";
313 : }
314 : std::cout << (q.empty() ? "" : " . ") << pbes_system::pp(h) << "\n";
315 : for (const pfnf_traverser_implication& i: g)
316 : {
317 : std::cout << " /\\ " << pbes_system::pp(i.g) << " => ";
318 : if (i.rhs.empty())
319 : {
320 : std::cout << "true";
321 : }
322 : else
323 : {
324 : std::cout << "( ";
325 : for (std::vector<propositional_variable_instantiation>::const_iterator j = i.rhs.begin(); j != i.rhs.end(); ++j)
326 : {
327 : if (j != i.rhs.begin())
328 : {
329 : std::cout << " \\/ ";
330 : }
331 : std::cout << pbes_system::pp(*j);
332 : }
333 : std::cout << " )";
334 : std::cout << std::endl;
335 : }
336 : }
337 : std::cout << std::endl;
338 : }
339 :
340 : /// \brief Prints the expression stack
341 : /// \param msg A string
342 : void print(const std::string& msg = "") const
343 : {
344 : std::cout << "--- " << msg << std::endl;
345 : for (const pfnf_traverser_expression& expr: expression_stack)
346 : {
347 : print_expression(expr);
348 : }
349 : std::cout << "value = " << pbes_system::pp(evaluate()) << std::endl;
350 : }
351 :
352 31 : void enter(const data::data_expression& x)
353 : {
354 31 : expression_stack.push_back(pfnf_traverser_expression(x));
355 31 : }
356 :
357 0 : void enter(const not_&)
358 : {
359 0 : throw std::runtime_error("operation not should not occur");
360 : }
361 :
362 24 : void leave(const and_&)
363 : {
364 : // join the two expressions on top of the stack
365 24 : pfnf_traverser_expression right = expression_stack.back();
366 24 : expression_stack.pop_back();
367 24 : pfnf_traverser_expression left = expression_stack.back();
368 24 : expression_stack.pop_back();
369 24 : resolve_name_clashes(left, right);
370 24 : std::vector<pfnf_traverser_quantifier> q = concat(left.quantifiers, right.quantifiers);
371 24 : pbes_expression h = make_and(left, right);
372 24 : std::vector<pfnf_traverser_implication> g = concat(left.implications, right.implications);
373 : //std::cout << "AND RESULT\n"; print_expression(pfnf_traverser_expression(h, q, g));
374 24 : expression_stack.push_back(pfnf_traverser_expression(h, q, g));
375 24 : }
376 :
377 22 : void leave(const or_&)
378 : {
379 : // join the two expressions on top of the stack
380 22 : pfnf_traverser_expression right = expression_stack.back();
381 22 : expression_stack.pop_back();
382 22 : pfnf_traverser_expression left = expression_stack.back();
383 22 : expression_stack.pop_back();
384 22 : resolve_name_clashes(left, right);
385 :
386 22 : std::vector<pfnf_traverser_quantifier> q = concat(left.quantifiers, right.quantifiers);
387 :
388 22 : pbes_expression h_phi = left.expr;
389 22 : pbes_expression h_psi = right.expr;
390 44 : pbes_expression h = make_or(h_phi, h_psi);
391 :
392 22 : pbes_expression not_h_phi = make_not(left.expr);
393 22 : pbes_expression not_h_psi = make_not(right.expr);
394 :
395 22 : const std::vector<pfnf_traverser_implication>& q_phi = left.implications;
396 22 : const std::vector<pfnf_traverser_implication>& q_psi = right.implications;
397 :
398 22 : std::vector<pfnf_traverser_implication> g;
399 :
400 : // first conjunction
401 28 : for (const pfnf_traverser_implication& i: q_phi)
402 : {
403 6 : g.push_back(pfnf_traverser_implication(make_and(not_h_psi, i.g), i.rhs));
404 : }
405 :
406 : // second conjunction
407 47 : for (const pfnf_traverser_implication& i: q_psi)
408 : {
409 25 : g.push_back(pfnf_traverser_implication(make_and(not_h_phi, i.g), i.rhs));
410 : }
411 :
412 : // third conjunction
413 28 : for (const pfnf_traverser_implication& i: q_phi)
414 : {
415 16 : for (const pfnf_traverser_implication& k: q_psi)
416 : {
417 10 : g.push_back(pfnf_traverser_implication(make_and(i.g, k.g), concat(i.rhs, k.rhs)));
418 : }
419 : }
420 : //std::cout << "OR RESULT\n"; print_expression(pfnf_traverser_expression(h, q, g));
421 22 : expression_stack.push_back(pfnf_traverser_expression(h, q, g));
422 22 : }
423 :
424 0 : void enter(const imp& /*x*/)
425 : {
426 0 : throw std::runtime_error("operation imp should not occur");
427 : }
428 :
429 13 : void enter(const forall& x)
430 : {
431 13 : quantifier_stack.push_back(x.variables());
432 13 : }
433 :
434 13 : void leave(const forall&)
435 : {
436 : // push the quantifier on the expression stack
437 13 : expression_stack.back().quantifiers.push_back(std::make_pair(true, quantifier_stack.back()));
438 13 : quantifier_stack.pop_back();
439 13 : }
440 :
441 3 : void enter(const exists& x)
442 : {
443 3 : quantifier_stack.push_back(x.variables());
444 3 : }
445 :
446 3 : void leave(const exists&)
447 : {
448 : // push the quantifier on the expression stack
449 3 : expression_stack.back().quantifiers.push_back(std::make_pair(false, quantifier_stack.back()));
450 3 : quantifier_stack.pop_back();
451 3 : }
452 :
453 34 : void enter(const propositional_variable_instantiation& x)
454 : {
455 : // push the propositional variable on the expression stack
456 34 : std::vector<pfnf_traverser_quantifier> q;
457 34 : pbes_expression h = true_();
458 68 : std::vector<pfnf_traverser_implication> g(1, pfnf_traverser_implication(true_(), std::vector<propositional_variable_instantiation>(1, x)));
459 34 : expression_stack.push_back(pfnf_traverser_expression(h, q, g));
460 34 : }
461 : };
462 :
463 : } // namespace detail
464 :
465 : } // namespace pbes_system
466 :
467 : } // namespace mcrl2
468 :
469 : #endif // MCRL2_PBES_DETAIL_PFNF_TRAVERSER_H
|
