Line data Source code
1 : // Author(s): Gijs Kant
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/bqnf_visitor.h
10 : /// \brief Visitor class for PBESs in Bounded Quantifier Normal Form (BQNF):
11 : /// BQNF :== forall d: D . b => BQNF | exists d: D . b && BQNF | CONJ
12 : /// CONJ :== And_{k: K} f_k && And_{i: I} forall v: D_I . g_i => DISJ^i
13 : /// DISJ^i :== Or_{l: L_i} f_{il} || Or_{j: J_i} exists w: D_{ij} . g_{ij} && X_{ij}(e_{ij})
14 : ///
15 : /// DEPRECATED
16 : #ifndef MCRL2_PBES_DETAIL_BQNF_VISITOR_H
17 : #define MCRL2_PBES_DETAIL_BQNF_VISITOR_H
18 :
19 : #include "mcrl2/pbes/pbes_functions.h"
20 :
21 : namespace mcrl2 {
22 :
23 : namespace pbes_system {
24 :
25 : namespace detail {
26 :
27 : /// \brief The current indent level. Used for debug output.
28 : static int indent_count = 0;
29 : /// \brief Increases the current indent level.
30 26 : static void inc_indent()
31 : {
32 26 : indent_count++;
33 26 : }
34 : /// \brief Decreases the current indent level.
35 26 : static void dec_indent()
36 : {
37 26 : indent_count--;
38 26 : }
39 :
40 : /// \brief Indents according to the current indent level.
41 0 : static void indent()
42 : {
43 0 : for(int i=0;i<indent_count;i++)
44 : {
45 0 : std::clog << " ";
46 : }
47 0 : }
48 :
49 : /// \brief A visitor class for PBES equations in BQNF. There is a visit_<node>
50 : /// function for each type of node. By default these functions do nothing, but check
51 : /// that the PBES equations are indeed in BQNF, so they
52 : /// must be overridden in order to add behaviour.
53 : struct bqnf_visitor
54 : {
55 : /// \brief flag that indicates if debug output should be printed.
56 : bool debug;
57 :
58 : /// \brief Returns a string representation of the type of the root node of the expression.
59 : /// \param e a PBES expression
60 : /// \return a string representation of the type of the root node of the expression.
61 0 : static std::string print_brief(const pbes_expression& e)
62 : {
63 0 : if (is_propositional_variable_instantiation(e)) {
64 0 : return std::string("PropVar ") + std::string(atermpp::down_cast<propositional_variable_instantiation>(e).name());
65 0 : } else if (is_simple_expression(e)) {
66 0 : return "SimpleExpr";
67 0 : } else if (is_and(e)) {
68 0 : return "And";
69 0 : } else if (is_or(e)) {
70 0 : return "Or";
71 0 : } else if (is_imp(e)) {
72 0 : return "Imp";
73 0 : } else if (is_forall(e)) {
74 0 : return std::string("ForAll(")+core::pp(atermpp::down_cast<forall>(e).variables())+std::string(")");
75 0 : } else if (is_exists(e)) {
76 0 : return std::string("Exists(")+core::pp(atermpp::down_cast<exists>(e).variables())+std::string(")");
77 : } else {
78 0 : return "Unknown type";
79 : }
80 : }
81 :
82 : /// \brief Determines if an expression if of the form
83 : /// phi /\ psi where phi is a simple expression
84 : /// and psi is an arbitrary expression.
85 : /// \param e an expression
86 : /// \return true if e is of the form phi /\ psi.
87 : static bool is_inner_and(const pbes_expression& e)
88 : {
89 : bool result = true;
90 : if (!(is_propositional_variable_instantiation(e) || is_simple_expression(e))) {
91 : if (is_and(e)) {
92 : pbes_expression l = pbes_system::accessors::left(e);
93 : pbes_expression r = pbes_system::accessors::right(e);
94 : if (is_simple_expression(l)) {
95 : result = is_inner_and(r);
96 : } else {
97 : result = false;
98 : }
99 : } else {
100 : result = false;
101 : }
102 : }
103 : return result;
104 : }
105 :
106 : /// \brief Determines if an expression if of the form
107 : /// phi => psi or of the form phi \/ psi where phi is a simple expression
108 : /// and psi is an arbitrary expression.
109 : /// \param e an expression
110 : /// \return true if e is of the form phi => psi or phi \/ psi.
111 : static bool is_inner_implies(const pbes_expression& e)
112 : {
113 : bool result = true;
114 : if (!(is_propositional_variable_instantiation(e) || is_simple_expression(e))) {
115 : if (is_or(e) || is_imp(e)) {
116 : pbes_expression l = pbes_system::accessors::left(e);
117 : pbes_expression r = pbes_system::accessors::right(e);
118 : if (is_simple_expression(l)) {
119 : result = is_inner_implies(r);
120 : } else {
121 : result = false;
122 : }
123 : } else {
124 : result = false;
125 : }
126 : }
127 : return result;
128 : }
129 :
130 : /// \brief Destructor.
131 3 : virtual ~bqnf_visitor()
132 3 : { }
133 :
134 : /// \brief Constructor.
135 2 : bqnf_visitor():
136 2 : debug(false)
137 2 : { }
138 :
139 : /// \brief Visits a simple expression.
140 : /// An expression is simple if it does not contain propositional variables.
141 : /// \param sigma fixpoint symbol (unused in this class)
142 : /// \param var propositional variable (unused in this class)
143 : /// \param e a PBES expression
144 : /// \return true if the expression e is a simple expression.
145 2 : virtual bool visit_simple_expression(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
146 : {
147 2 : bool result = true;
148 2 : if (is_data(e) || is_true(e) || is_false(e)) {
149 2 : result = true;
150 0 : } else if (is_not(e)) {
151 0 : pbes_expression n = pbes_system::accessors::arg(e);
152 0 : result &= visit_simple_expression(sigma, var, n);
153 0 : } else if (is_and(e) || is_or(e) || is_imp(e)) {
154 0 : pbes_expression l = pbes_system::accessors::left(e);
155 0 : pbes_expression r = pbes_system::accessors::right(e);
156 0 : result &= visit_simple_expression(sigma, var, l);
157 0 : result &= visit_simple_expression(sigma, var, r);
158 0 : } else if (is_forall(e) || is_exists(e)) {
159 0 : pbes_expression a = pbes_system::accessors::arg(e);
160 0 : result &= visit_simple_expression(sigma, var, a);
161 0 : } else if (is_propositional_variable_instantiation(e)) {
162 0 : if (debug) {
163 0 : indent(); std::clog << "Not a simple expression!" << std::endl;
164 : } else {
165 0 : throw(std::runtime_error("Not a simple expression!"));
166 : }
167 : } else {
168 0 : throw(std::runtime_error("Unknown type of expression!"));
169 : }
170 2 : if (debug) {
171 0 : indent(); std::clog << "visit_simple_expression: " << pp(e) << ": " << (result?"true":"false") << std::endl;
172 : }
173 2 : return result;
174 : }
175 :
176 : /// \brief Visits a propositional variable expression.
177 : /// \param sigma fixpoint symbol (unused in this class)
178 : /// \param var propositional variable (unused in this class)
179 : /// \param e PBES expression
180 : /// \return true if the expression is a propositional variable or a simple expression.
181 3 : virtual bool visit_propositional_variable(const fixpoint_symbol& /*sigma*/, const propositional_variable& /*var*/, const pbes_expression& e)
182 : {
183 3 : inc_indent();
184 3 : bool result = true;
185 3 : if (is_propositional_variable_instantiation(e) || is_simple_expression(e)) {
186 : // std::clog << pp(e) << std::endl;
187 : } else {
188 0 : result = false;
189 0 : if (debug) {
190 0 : indent(); std::clog << "Not a propositional variable or simple expression:" << core::pp(e) << std::endl;
191 : } else {
192 0 : throw(std::runtime_error("Not a propositional variable or simple expression!"));
193 : }
194 : }
195 3 : if (debug) {
196 0 : indent(); std::clog << " visit_propositional_variable: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
197 : }
198 3 : dec_indent();
199 3 : return result;
200 : }
201 :
202 : /// \brief Visits a conjunctive expression within an inner existential quantifier expression.
203 : /// \param sigma fixpoint symbol (unused in this class)
204 : /// \param var propositional variable (unused in this class)
205 : /// \param e a PBES expression
206 : /// \return true if the expression e conforms to BQNF.
207 3 : virtual bool visit_inner_and(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
208 : {
209 3 : inc_indent();
210 3 : bool result = true;
211 3 : if (is_and(e)) {
212 0 : pbes_expression l = pbes_system::accessors::left(e);
213 0 : pbes_expression r = pbes_system::accessors::right(e);
214 0 : if (is_simple_expression(l)) {
215 0 : result &= visit_simple_expression(sigma, var, l);
216 : // std::clog << pp(l) << " /\\ " << std::endl;
217 0 : result &= visit_inner_and(sigma, var, r);
218 : } else {
219 0 : result &= visit_propositional_variable(sigma, var, e);
220 : }
221 0 : } else {
222 3 : result &= visit_propositional_variable(sigma, var, e);
223 : }
224 3 : if (debug) {
225 0 : indent(); std::clog << " visit_inner_and: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
226 : }
227 3 : dec_indent();
228 3 : return result;
229 : }
230 :
231 : /// \brief Visits a bounded existential quantifier expression within a disjunctive expression.
232 : /// \param sigma fixpoint symbol (unused in this class)
233 : /// \param var propositional variable (unused in this class)
234 : /// \param e a PBES expression
235 : /// \return true if the expression e conforms to BQNF.
236 3 : virtual bool visit_inner_bounded_exists(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
237 : {
238 3 : inc_indent();
239 3 : pbes_expression qexpr = e;
240 3 : data::variable_list qvars;
241 3 : while (is_exists(qexpr)) {
242 0 : qvars = qvars + atermpp::down_cast<exists>(qexpr).variables();
243 0 : qexpr = pbes_system::accessors::arg(qexpr);
244 : }
245 3 : bool result = visit_inner_and(sigma, var, qexpr);
246 3 : if (debug) {
247 0 : indent(); std::clog << "visit_inner_bounded_exists: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
248 : }
249 3 : dec_indent();
250 3 : return result;
251 3 : }
252 :
253 : /// \brief Visits a disjunctive expression.
254 : /// \param sigma fixpoint symbol (unused in this class)
255 : /// \param var propositional variable (unused in this class)
256 : /// \param e a PBES expression
257 : /// \return true if the expression e conforms to BQNF.
258 3 : virtual bool visit_or(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
259 : {
260 3 : inc_indent();
261 3 : bool result = true;
262 3 : if (is_or(e) || is_imp(e)) {
263 0 : pbes_expression l = pbes_system::accessors::left(e);
264 0 : pbes_expression r = pbes_system::accessors::right(e);
265 0 : result &= visit_or(sigma, var, l);
266 0 : result &= visit_or(sigma, var, r);
267 0 : } else {
268 3 : result &= visit_inner_bounded_exists(sigma, var, e);
269 : }
270 3 : if (debug) {
271 0 : indent(); std::clog << "visit_or: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
272 : }
273 3 : dec_indent();
274 3 : return result;
275 : }
276 :
277 : /// \brief Visits a bounded universal quantifier expression within a conjunctive expression.
278 : /// \param sigma fixpoint symbol (unused in this class)
279 : /// \param var propositional variable (unused in this class)
280 : /// \param e a PBES expression
281 : /// \return true if the expression e conforms to BQNF.
282 3 : virtual bool visit_inner_bounded_forall(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
283 : {
284 3 : inc_indent();
285 3 : pbes_expression qexpr = e;
286 3 : data::variable_list qvars;
287 3 : while (is_forall(qexpr)) {
288 0 : qvars = qvars + atermpp::down_cast<forall>(qexpr).variables();
289 0 : qexpr = pbes_system::accessors::arg(qexpr);
290 : }
291 3 : bool result = true;
292 3 : if (is_or(qexpr) || is_imp(qexpr)) {
293 2 : pbes_expression l = pbes_system::accessors::left(qexpr);
294 2 : pbes_expression r = pbes_system::accessors::right(qexpr);
295 2 : if (is_simple_expression(l)) {
296 2 : result &= visit_simple_expression(sigma, var, l);
297 : // std::clog << pp(l) << (is_or(qexpr) ? " \\/ " : " => ") << std::endl;
298 2 : result &= visit_or(sigma, var, r);
299 : } else {
300 0 : result &= visit_or(sigma, var, qexpr);
301 : }
302 2 : } else {
303 1 : result &= visit_or(sigma, var, qexpr);
304 : }
305 3 : if (debug) {
306 0 : indent(); std::clog << "visit_inner_bounded_forall: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
307 : }
308 3 : dec_indent();
309 3 : return result;
310 3 : }
311 :
312 : /// \brief Visits a conjunctive expression.
313 : /// \param sigma fixpoint symbol (unused in this class)
314 : /// \param var propositional variable (unused in this class)
315 : /// \param e a PBES expression
316 : /// \return true if the expression e conforms to BQNF.
317 4 : virtual bool visit_and(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
318 : {
319 4 : inc_indent();
320 4 : bool result = true;
321 4 : if (is_and(e)) {
322 1 : pbes_expression l = pbes_system::accessors::left(e);
323 1 : pbes_expression r = pbes_system::accessors::right(e);
324 1 : result &= visit_and(sigma, var, l);
325 : // std::clog << " /\\ " << std::endl;
326 1 : result &= visit_and(sigma, var, r);
327 1 : } else {
328 3 : result &= visit_inner_bounded_forall(sigma, var, e);
329 : }
330 4 : if (debug) {
331 0 : indent(); std::clog << "visit_and: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
332 : }
333 4 : dec_indent();
334 4 : return result;
335 : }
336 :
337 : /// \brief Visits a bounded universal quantifier expression.
338 : /// \param sigma fixpoint symbol (unused in this class)
339 : /// \param var propositional variable (unused in this class)
340 : /// \param e a PBES expression
341 : /// \return true if the expression e conforms to BQNF.
342 1 : virtual bool visit_bounded_forall(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
343 : {
344 1 : inc_indent();
345 1 : assert(is_forall(e));
346 1 : pbes_expression qexpr = e;
347 1 : data::variable_list qvars;
348 2 : while (is_forall(qexpr)) {
349 1 : qvars = qvars + atermpp::down_cast<forall>(qexpr).variables();
350 1 : qexpr = pbes_system::accessors::arg(qexpr);
351 : }
352 : //std::clog << " Bounded forall: " << pp(qvars) << " . " << std::endl;
353 1 : bool result = true;
354 1 : if (is_or(qexpr) || is_imp(qexpr)) {
355 0 : pbes_expression l = pbes_system::accessors::left(qexpr);
356 0 : pbes_expression r = pbes_system::accessors::right(qexpr);
357 0 : if (is_simple_expression(l)) {
358 0 : result &= visit_simple_expression(sigma, var, l);
359 : // std::clog << pp(l) << (is_or(qexpr) ? " \\/ " : " => ") << std::endl;
360 0 : result &= visit_bqnf_expression(sigma, var, r);
361 : } else {
362 0 : result &= visit_bqnf_expression(sigma, var, qexpr);
363 : }
364 0 : } else {
365 1 : result &= visit_bqnf_expression(sigma, var, qexpr);
366 : }
367 1 : if (debug) {
368 0 : indent(); std::clog << "visit_bounded_forall: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
369 : }
370 1 : dec_indent();
371 1 : return result;
372 1 : }
373 :
374 : /// \brief Visits a bounded existential quantifier expression.
375 : /// \param sigma fixpoint symbol (unused in this class)
376 : /// \param var propositional variable (unused in this class)
377 : /// \param e a PBES expression
378 : /// \return true if the expression e conforms to BQNF.
379 0 : virtual bool visit_bounded_exists(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
380 : {
381 0 : inc_indent();
382 0 : assert(is_exists(e));
383 0 : pbes_expression qexpr = e;
384 0 : data::variable_list qvars;
385 0 : while (is_exists(qexpr)) {
386 0 : qvars = qvars + atermpp::down_cast<exists>(qexpr).variables();
387 0 : qexpr = pbes_system::accessors::arg(qexpr);
388 : }
389 0 : bool result = true;
390 0 : if (is_and(qexpr)) {
391 0 : pbes_expression l = pbes_system::accessors::left(qexpr);
392 0 : pbes_expression r = pbes_system::accessors::right(qexpr);
393 0 : if (is_simple_expression(l)) {
394 0 : result &= visit_simple_expression(sigma, var, l);
395 0 : result &= visit_bqnf_expression(sigma, var, r);
396 : } else {
397 0 : result &= visit_bqnf_expression(sigma, var, qexpr);
398 : }
399 0 : } else {
400 0 : result &= visit_bqnf_expression(sigma, var, qexpr);
401 : }
402 0 : if (debug) {
403 0 : indent(); std::clog << "visit_bounded_exists: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
404 : }
405 0 : dec_indent();
406 0 : return result;
407 0 : }
408 :
409 : /// \brief Visits a bounded quantifier expression.
410 : /// \param sigma fixpoint symbol (unused in this class)
411 : /// \param var propositional variable (unused in this class)
412 : /// \param e a PBES expression
413 : /// \return true if the expression e conforms to BQNF.
414 1 : virtual bool visit_bounded_quantifier(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
415 : {
416 1 : inc_indent();
417 1 : bool result = true;
418 1 : if (is_forall(e)) {
419 1 : result &= visit_bounded_forall(sigma, var, e);
420 0 : } else if (is_exists(e)) {
421 0 : result &= visit_bounded_exists(sigma, var, e);
422 : } else {
423 : // should not be possible
424 0 : throw(std::runtime_error("Not a quantifier expression!"));
425 : }
426 1 : if (debug) {
427 0 : indent(); std::clog << "visit_bounded_quantifier: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
428 : }
429 1 : dec_indent();
430 1 : return result;
431 : }
432 :
433 : /// \brief Visits a BQNF expression.
434 : /// \param sigma fixpoint symbol (unused in this class)
435 : /// \param var propositional variable (unused in this class)
436 : /// \param e a PBES expression
437 : /// \return true if the expression e is in BQNF.
438 5 : virtual bool visit_bqnf_expression(const fixpoint_symbol& sigma, const propositional_variable& var, const pbes_expression& e)
439 : {
440 5 : inc_indent();
441 5 : bool result = true;
442 5 : if (is_simple_expression(e)) {
443 2 : result = true;
444 3 : } else if (is_forall(e) || is_exists(e)) {
445 1 : result &= visit_bounded_quantifier(sigma, var, e);
446 : } else {
447 2 : result &= visit_and(sigma, var, e);
448 : }
449 5 : if (debug) {
450 0 : indent(); std::clog << "visit_bqnf_expression: " << print_brief(e) << ": " << (result?"true":"false") << std::endl;
451 : }
452 5 : dec_indent();
453 5 : return result;
454 : }
455 :
456 : /// \brief Visits a BQNF expression.
457 : /// In the current BQNF visitor sigma and var parameters are added for use in bqnf2ppg_rewriter.
458 : /// This functions adds dummy values for sigma and var.
459 : /// \param e a PBES expression
460 : /// \return true if the expression e is in BQNF.
461 4 : virtual bool visit_bqnf_expression(const pbes_expression& e)
462 : {
463 4 : bool result = visit_bqnf_expression(fixpoint_symbol::nu(), propositional_variable(core::identifier_string("X"), data::variable_list()), e);
464 4 : return result;
465 : }
466 :
467 : /// \brief Visits a BQNF equation.
468 : /// \param eqn a PBES equation
469 : /// \return true if the right hand side of the equation is in BQNF.
470 0 : virtual bool visit_bqnf_equation(const pbes_equation& eqn)
471 : {
472 0 : if (debug) std::clog << "visit_bqnf_equation." << std::endl;
473 0 : const fixpoint_symbol& sigma = eqn.symbol();
474 0 : const propositional_variable& var = eqn.variable();
475 0 : const pbes_expression& e = eqn.formula();
476 0 : bool result = visit_bqnf_expression(sigma, var, e);
477 0 : if (debug) std::clog << "visit_bqnf_equation: equation " << var.name() << " is " << (result ? "" : "NOT ") << "in BQNF." << std::endl;
478 0 : return result;
479 : }
480 :
481 : /// \brief Visits a BQNF equation in debug mode.
482 : /// \param eqn a PBES equation
483 : /// \return true if the right hand side of the equation is in BQNF.
484 0 : virtual bool visit_bqnf_equation_debug(const pbes_equation& eqn)
485 : {
486 0 : debug = true;
487 0 : return visit_bqnf_equation(eqn);
488 : }
489 :
490 : };
491 :
492 : } // namespace detail
493 :
494 : } // namespace pbes_system
495 :
496 : } // namespace mcrl2
497 :
498 : #endif // MCRL2_PBES_DETAIL_BQNF_VISITOR_H
|
