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/modal_formula/print.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_PRINT_H
13 : #define MCRL2_MODAL_FORMULA_PRINT_H
14 :
15 : #include "mcrl2/lps/print.h"
16 : #include "mcrl2/modal_formula/traverser.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace action_formulas {
21 :
22 0 : constexpr inline int precedence(const forall&) { return 21; }
23 0 : constexpr inline int precedence(const exists&) { return 21; }
24 0 : constexpr inline int precedence(const imp&) { return 22; }
25 0 : constexpr inline int precedence(const or_&) { return 23; }
26 1 : constexpr inline int precedence(const and_&) { return 24; }
27 0 : constexpr inline int precedence(const at&) { return 25; }
28 7 : constexpr inline int precedence(const not_&) { return 26; }
29 7 : inline int precedence(const action_formula& x)
30 : {
31 7 : if (is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
32 7 : else if (is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
33 7 : else if (is_imp(x)) { return precedence(atermpp::down_cast<imp>(x)); }
34 7 : else if (is_or(x)) { return precedence(atermpp::down_cast<or_>(x)); }
35 7 : else if (is_and(x)) { return precedence(atermpp::down_cast<and_>(x)); }
36 7 : else if (is_at(x)) { return precedence(atermpp::down_cast<at>(x)); }
37 7 : else if (is_not(x)) { return precedence(atermpp::down_cast<not_>(x)); }
38 5 : return core::detail::max_precedence;
39 : }
40 :
41 : // only defined for binary operators
42 0 : inline bool is_left_associative(const imp&) { return false; }
43 0 : inline bool is_left_associative(const or_&) { return true; }
44 0 : inline bool is_left_associative(const and_&) { return true; }
45 : inline bool is_left_associative(const action_formula& x)
46 : {
47 : if (is_imp(x)) { return is_left_associative(atermpp::down_cast<imp>(x)); }
48 : else if (is_or(x)) { return is_left_associative(atermpp::down_cast<or_>(x)); }
49 : else if (is_and(x)) { return is_left_associative(atermpp::down_cast<and_>(x)); }
50 : return false;
51 : }
52 :
53 0 : inline bool is_right_associative(const imp&) { return true; }
54 0 : inline bool is_right_associative(const or_&) { return true; }
55 0 : inline bool is_right_associative(const and_&) { return true; }
56 : inline bool is_right_associative(const action_formula& x)
57 : {
58 : if (is_imp(x)) { return is_right_associative(atermpp::down_cast<imp>(x)); }
59 : else if (is_or(x)) { return is_right_associative(atermpp::down_cast<or_>(x)); }
60 : else if (is_and(x)) { return is_right_associative(atermpp::down_cast<and_>(x)); }
61 : return false;
62 : }
63 :
64 : namespace detail
65 : {
66 :
67 : template <typename Derived>
68 : struct printer: public action_formulas::add_traverser_sort_expressions<lps::detail::printer, Derived>
69 : {
70 : typedef action_formulas::add_traverser_sort_expressions<lps::detail::printer, Derived> super;
71 :
72 : using super::enter;
73 : using super::leave;
74 : using super::apply;
75 : using super::derived;
76 : using super::print_abstraction;
77 : using super::print_list;
78 : using super::print_action_declarations;
79 : using super::print_expression;
80 : using super::print_unary_left_operation;
81 : using super::print_binary_operation;
82 :
83 14 : void apply(const action_formulas::true_& x)
84 : {
85 14 : derived().enter(x);
86 14 : derived().print("true");
87 14 : derived().leave(x);
88 14 : }
89 :
90 0 : void apply(const action_formulas::false_& x)
91 : {
92 0 : derived().enter(x);
93 0 : derived().print("false");
94 0 : derived().leave(x);
95 0 : }
96 :
97 5 : void apply(const action_formulas::not_& x)
98 : {
99 5 : derived().enter(x);
100 5 : print_unary_left_operation(x, "!");
101 5 : derived().leave(x);
102 5 : }
103 :
104 1 : void apply(const action_formulas::and_& x)
105 : {
106 1 : derived().enter(x);
107 1 : print_binary_operation(x, " && ");
108 1 : derived().leave(x);
109 1 : }
110 :
111 0 : void apply(const action_formulas::or_& x)
112 : {
113 0 : derived().enter(x);
114 0 : print_binary_operation(x, " || ");
115 0 : derived().leave(x);
116 0 : }
117 :
118 0 : void apply(const action_formulas::imp& x)
119 : {
120 0 : derived().enter(x);
121 0 : print_binary_operation(x, " => ");
122 0 : derived().leave(x);
123 0 : }
124 :
125 0 : void apply(const action_formulas::forall& x)
126 : {
127 0 : derived().enter(x);
128 0 : print_abstraction(x, "forall");
129 0 : derived().leave(x);
130 0 : }
131 :
132 0 : void apply(const action_formulas::exists& x)
133 : {
134 0 : derived().enter(x);
135 0 : print_abstraction(x, "exists");
136 0 : derived().leave(x);
137 0 : }
138 :
139 0 : void apply(const action_formulas::at& x)
140 : {
141 0 : derived().enter(x);
142 0 : derived().apply(x.operand());
143 0 : derived().print(" @ ");
144 0 : print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
145 0 : derived().leave(x);
146 0 : }
147 :
148 52 : void apply(const action_formulas::multi_action& x)
149 : {
150 52 : derived().enter(x);
151 52 : if (x.actions().empty())
152 : {
153 0 : derived().print("tau");
154 : }
155 : else
156 : {
157 52 : print_list(x.actions(), "", "", "|");
158 : }
159 52 : derived().leave(x);
160 52 : }
161 : };
162 :
163 : } // namespace detail
164 :
165 : /// \brief Prints the object t to a stream.
166 : template <typename T>
167 0 : void pp(const T& t, std::ostream& out)
168 : {
169 0 : core::detail::apply_printer<action_formulas::detail::printer> printer(out);
170 0 : printer.apply(t);
171 0 : }
172 :
173 : /// \brief Returns a string representation of the object t.
174 : template <typename T>
175 0 : std::string pp(const T& t)
176 : {
177 0 : std::ostringstream out;
178 0 : action_formulas::pp(t, out);
179 0 : return out.str();
180 0 : }
181 :
182 : } // namespace action_formulas
183 :
184 : namespace regular_formulas {
185 :
186 0 : constexpr inline int precedence(const seq&) { return 31; }
187 0 : constexpr inline int precedence(const alt&) { return 32; }
188 0 : constexpr inline int precedence(const trans&) { return 33; }
189 3 : constexpr inline int precedence(const trans_or_nil&) { return 33; }
190 3 : inline int precedence(const regular_formula& x)
191 : {
192 3 : if (is_seq(x)) { return precedence(atermpp::down_cast<seq>(x)); }
193 3 : else if (is_alt(x)) { return precedence(atermpp::down_cast<alt>(x)); }
194 3 : else if (is_trans(x)) { return precedence(atermpp::down_cast<trans>(x)); }
195 3 : else if (is_trans_or_nil(x)) { return precedence(atermpp::down_cast<trans_or_nil>(x)); }
196 3 : return core::detail::max_precedence;
197 : }
198 :
199 : // only defined for binary operators
200 0 : inline bool is_left_associative(const seq&) { return false; }
201 0 : inline bool is_left_associative(const alt&) { return true; }
202 : inline bool is_left_associative(const regular_formula& x)
203 : {
204 : if (is_seq(x)) { return is_left_associative(atermpp::down_cast<seq>(x)); }
205 : else if (is_alt(x)) { return is_left_associative(atermpp::down_cast<alt>(x)); }
206 : return false;
207 : }
208 :
209 0 : inline bool is_right_associative(const seq&) { return true; }
210 0 : inline bool is_right_associative(const alt&) { return true; }
211 : inline bool is_right_associative(const regular_formula& x)
212 : {
213 : if (is_seq(x)) { return is_right_associative(atermpp::down_cast<seq>(x)); }
214 : else if (is_alt(x)) { return is_right_associative(atermpp::down_cast<alt>(x)); }
215 : return false;
216 : }
217 :
218 : namespace detail
219 : {
220 :
221 : template <typename Derived>
222 : struct printer: public regular_formulas::add_traverser_sort_expressions<action_formulas::detail::printer, Derived>
223 : {
224 : typedef regular_formulas::add_traverser_sort_expressions<action_formulas::detail::printer, Derived> super;
225 :
226 : using super::enter;
227 : using super::leave;
228 : using super::apply;
229 : using super::derived;
230 : using super::print_action_declarations;
231 :
232 : using super::print_expression;
233 : using super::print_unary_left_operation;
234 : using super::print_unary_right_operation;
235 : using super::print_binary_operation;
236 :
237 0 : void apply(const regular_formulas::seq& x)
238 : {
239 0 : derived().enter(x);
240 0 : print_binary_operation(x, " . ");
241 0 : derived().leave(x);
242 0 : }
243 :
244 0 : void apply(const regular_formulas::alt& x)
245 : {
246 0 : derived().enter(x);
247 0 : print_binary_operation(x, " + ");
248 0 : derived().leave(x);
249 0 : }
250 :
251 0 : void apply(const regular_formulas::trans& x)
252 : {
253 0 : derived().enter(x);
254 0 : print_unary_right_operation(x, "+");
255 0 : derived().leave(x);
256 0 : }
257 :
258 3 : void apply(const regular_formulas::trans_or_nil& x)
259 : {
260 3 : derived().enter(x);
261 3 : print_unary_right_operation(x, "*");
262 3 : derived().leave(x);
263 3 : }
264 :
265 0 : void apply(const regular_formulas::untyped_regular_formula& x)
266 : {
267 0 : derived().enter(x);
268 0 : print_expression(x.left(), false);
269 0 : derived().print(" " + std::string(x.name()) + " ");
270 0 : print_expression(x.right(), false);
271 0 : derived().leave(x);
272 0 : }
273 : };
274 :
275 : } // namespace detail
276 :
277 : /// \brief Prints the object t to a stream.
278 : template <typename T>
279 0 : void pp(const T& t, std::ostream& out)
280 : {
281 0 : core::detail::apply_printer<regular_formulas::detail::printer> printer(out);
282 0 : printer.apply(t);
283 0 : }
284 :
285 : /// \brief Returns a string representation of the object t.
286 : template <typename T>
287 0 : std::string pp(const T& t)
288 : {
289 0 : std::ostringstream out;
290 0 : regular_formulas::pp(t, out);
291 0 : return out.str();
292 0 : }
293 :
294 : } // namespace regular_formulas
295 :
296 : namespace state_formulas {
297 :
298 47 : constexpr inline int precedence(const mu&) { return 41; }
299 2 : constexpr inline int precedence(const nu&) { return 41; }
300 3 : constexpr inline int precedence(const forall&) { return 42; }
301 0 : constexpr inline int precedence(const exists&) { return 42; }
302 0 : constexpr inline int precedence(const infimum&) { return 42; }
303 0 : constexpr inline int precedence(const supremum&) { return 42; }
304 10 : constexpr inline int precedence(const imp&) { return 45; }
305 28 : constexpr inline int precedence(const or_&) { return 46; }
306 45 : constexpr inline int precedence(const and_&) { return 47; }
307 0 : constexpr inline int precedence(const plus&) { return 43; }
308 0 : constexpr inline int precedence(const const_multiply&) { return 44; }
309 0 : constexpr inline int precedence(const const_multiply_alt&) { return 44; }
310 58 : constexpr inline int precedence(const must&) { return 48; }
311 40 : constexpr inline int precedence(const may&) { return 48; }
312 20 : constexpr inline int precedence(const not_&) { return 50; }
313 228 : inline int precedence(const state_formula& x)
314 : {
315 228 : if (is_mu(x)) { return precedence(atermpp::down_cast<mu>(x)); }
316 181 : else if (is_nu(x)) { return precedence(atermpp::down_cast<nu>(x)); }
317 179 : else if (is_forall(x)) { return precedence(atermpp::down_cast<forall>(x)); }
318 176 : else if (is_exists(x)) { return precedence(atermpp::down_cast<exists>(x)); }
319 176 : else if (is_infimum(x)) { return precedence(atermpp::down_cast<infimum>(x)); }
320 176 : else if (is_supremum(x)) { return precedence(atermpp::down_cast<supremum>(x)); }
321 176 : else if (is_imp(x)) { return precedence(atermpp::down_cast<imp>(x)); }
322 176 : else if (is_or(x)) { return precedence(atermpp::down_cast<or_>(x)); }
323 171 : else if (is_and(x)) { return precedence(atermpp::down_cast<and_>(x)); }
324 165 : else if (is_plus(x)) { return precedence(atermpp::down_cast<plus>(x)); }
325 165 : else if (is_const_multiply(x)) { return precedence(atermpp::down_cast<const_multiply>(x)); }
326 165 : else if (is_const_multiply_alt(x)) { return precedence(atermpp::down_cast<const_multiply_alt>(x)); }
327 165 : else if (is_must(x)) { return precedence(atermpp::down_cast<must>(x)); }
328 151 : else if (is_may(x)) { return precedence(atermpp::down_cast<may>(x)); }
329 135 : else if (is_not(x)) { return precedence(atermpp::down_cast<not_>(x)); }
330 131 : return core::detail::max_precedence;
331 : }
332 :
333 : // only defined for binary operators
334 0 : inline bool is_left_associative(const imp&) { return false; }
335 0 : inline bool is_left_associative(const or_&) { return true; }
336 0 : inline bool is_left_associative(const and_&) { return true; }
337 0 : inline bool is_left_associative(const plus&) { return true; }
338 0 : inline bool is_left_associative(const const_multiply&) { return true; }
339 : inline bool is_left_associative(const const_multiply_alt&) { return true; }
340 : inline bool is_left_associative(const state_formula& x)
341 : {
342 : if (is_imp(x)) { return is_left_associative(atermpp::down_cast<imp>(x)); }
343 : else if (is_or(x)) { return is_left_associative(atermpp::down_cast<or_>(x)); }
344 : else if (is_and(x)) { return is_left_associative(atermpp::down_cast<and_>(x)); }
345 : else if (is_plus(x)) { return is_left_associative(atermpp::down_cast<plus>(x)); }
346 : else if (is_const_multiply(x)) { return is_left_associative(atermpp::down_cast<const_multiply>(x)); }
347 : else if (is_const_multiply_alt(x)) { return is_left_associative(atermpp::down_cast<const_multiply_alt>(x)); }
348 : return false;
349 : }
350 :
351 0 : inline bool is_right_associative(const imp&) { return true; }
352 0 : inline bool is_right_associative(const or_&) { return true; }
353 5 : inline bool is_right_associative(const and_&) { return true; }
354 0 : inline bool is_right_associative(const plus&) { return true; }
355 0 : inline bool is_right_associative(const const_multiply&) { return true; }
356 : inline bool is_right_associative(const const_multiply_alt&) { return true; }
357 : inline bool is_right_associative(const state_formula& x)
358 : {
359 : if (is_imp(x)) { return is_right_associative(atermpp::down_cast<imp>(x)); }
360 : else if (is_or(x)) { return is_right_associative(atermpp::down_cast<or_>(x)); }
361 : else if (is_and(x)) { return is_right_associative(atermpp::down_cast<and_>(x)); }
362 : else if (is_plus(x)) { return is_right_associative(atermpp::down_cast<plus>(x)); }
363 : else if (is_const_multiply(x)) { return is_right_associative(atermpp::down_cast<const_multiply>(x)); }
364 : else if (is_const_multiply_alt(x)) { return is_right_associative(atermpp::down_cast<const_multiply_alt>(x)); }
365 : return false;
366 : }
367 :
368 : namespace detail
369 : {
370 :
371 : template <typename Derived>
372 : struct printer: public state_formulas::add_traverser_sort_expressions<regular_formulas::detail::printer, Derived>
373 : {
374 : typedef state_formulas::add_traverser_sort_expressions<regular_formulas::detail::printer, Derived> super;
375 :
376 : using super::enter;
377 : using super::leave;
378 : using super::apply;
379 : using super::derived;
380 : using super::print_abstraction;
381 : using super::print_variables;
382 : using super::print_list;
383 : using super::print_action_declarations;
384 :
385 : using super::print_expression;
386 : using super::print_unary_left_operation;
387 : using super::print_binary_operation;
388 : using super::print_unary_operand;
389 :
390 : // Determines whether or not data expressions should be wrapped inside 'val'.
391 : std::vector<bool> val;
392 :
393 190 : void disable_val()
394 : {
395 190 : val.push_back(false);
396 190 : }
397 :
398 190 : void enable_val()
399 : {
400 190 : assert(!val.empty());
401 190 : val.pop_back();
402 190 : }
403 :
404 103 : void apply(const data::data_expression& x)
405 : {
406 103 : bool print_val = val.empty();
407 103 : derived().enter(x);
408 103 : if (print_val)
409 : {
410 24 : disable_val();
411 24 : derived().print("val(");
412 : }
413 103 : super::apply(x);
414 103 : if (print_val)
415 : {
416 24 : derived().print(")");
417 24 : enable_val();
418 : }
419 103 : derived().leave(x);
420 103 : }
421 :
422 78 : void apply(const state_formulas::true_& x)
423 : {
424 78 : derived().enter(x);
425 78 : derived().print("true");
426 78 : derived().leave(x);
427 78 : }
428 :
429 23 : void apply(const state_formulas::false_& x)
430 : {
431 23 : derived().enter(x);
432 23 : derived().print("false");
433 23 : derived().leave(x);
434 23 : }
435 :
436 16 : void apply(const state_formulas::not_& x)
437 : {
438 16 : derived().enter(x);
439 16 : print_unary_left_operation(x, "!");
440 16 : derived().leave(x);
441 16 : }
442 :
443 0 : void apply(const state_formulas::minus& x)
444 : {
445 0 : derived().enter(x);
446 0 : print_unary_left_operation(x, "-");
447 0 : derived().leave(x);
448 0 : }
449 :
450 39 : void apply(const state_formulas::and_& x)
451 : {
452 39 : derived().enter(x);
453 39 : print_binary_operation(x, " && ");
454 39 : derived().leave(x);
455 39 : }
456 :
457 23 : void apply(const state_formulas::or_& x)
458 : {
459 23 : derived().enter(x);
460 23 : print_binary_operation(x, " || ");
461 23 : derived().leave(x);
462 23 : }
463 :
464 10 : void apply(const state_formulas::imp& x)
465 : {
466 10 : derived().enter(x);
467 10 : print_binary_operation(x, " => ");
468 10 : derived().leave(x);
469 10 : }
470 :
471 0 : void apply(const state_formulas::plus& x)
472 : {
473 0 : derived().enter(x);
474 0 : print_binary_operation(x, " + ");
475 0 : derived().leave(x);
476 0 : }
477 :
478 0 : void apply(const state_formulas::const_multiply& x)
479 : {
480 0 : derived().enter(x);
481 0 : print_binary_operation(x, " * ");
482 0 : derived().leave(x);
483 0 : }
484 :
485 0 : void apply(const state_formulas::const_multiply_alt& x)
486 : {
487 0 : derived().enter(x);
488 0 : derived().apply(x.left());
489 0 : derived().print("*");
490 0 : derived().apply(x.right());
491 : // print_expression(x.right(), false);
492 0 : derived().leave(x);
493 0 : }
494 :
495 11 : void apply(const state_formulas::forall& x)
496 : {
497 11 : derived().enter(x);
498 11 : print_abstraction(x, "forall");
499 11 : derived().leave(x);
500 11 : }
501 :
502 5 : void apply(const state_formulas::exists& x)
503 : {
504 5 : derived().enter(x);
505 5 : print_abstraction(x, "exists");
506 5 : derived().leave(x);
507 5 : }
508 :
509 3 : void apply(const state_formulas::infimum& x)
510 : {
511 3 : derived().enter(x);
512 3 : print_abstraction(x, "inf");
513 3 : derived().leave(x);
514 3 : }
515 :
516 3 : void apply(const state_formulas::supremum& x)
517 : {
518 3 : derived().enter(x);
519 3 : print_abstraction(x, "sup");
520 3 : derived().leave(x);
521 3 : }
522 :
523 44 : void apply(const state_formulas::must& x)
524 : {
525 44 : derived().enter(x);
526 44 : derived().print("[");
527 44 : disable_val();
528 44 : derived().apply(x.formula());
529 44 : enable_val();
530 44 : derived().print("]");
531 44 : print_unary_operand(x, x.operand());
532 44 : derived().leave(x);
533 44 : }
534 :
535 24 : void apply(const state_formulas::may& x)
536 : {
537 24 : derived().enter(x);
538 24 : derived().print("<");
539 24 : disable_val();
540 24 : derived().apply(x.formula());
541 24 : enable_val();
542 24 : derived().print(">");
543 24 : print_unary_operand(x, x.operand());
544 24 : derived().leave(x);
545 24 : }
546 :
547 0 : void apply(const state_formulas::yaled& x)
548 : {
549 0 : derived().enter(x);
550 0 : derived().print("yaled");
551 0 : derived().leave(x);
552 0 : }
553 :
554 0 : void apply(const state_formulas::yaled_timed& x)
555 : {
556 0 : disable_val();
557 0 : derived().enter(x);
558 0 : derived().print("yaled");
559 0 : derived().print(" @ ");
560 0 : print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
561 0 : derived().leave(x);
562 0 : enable_val();
563 0 : }
564 :
565 0 : void apply(const state_formulas::delay& x)
566 : {
567 0 : derived().enter(x);
568 0 : derived().print("delay");
569 0 : derived().leave(x);
570 0 : }
571 :
572 2 : void apply(const state_formulas::delay_timed& x)
573 : {
574 2 : disable_val();
575 2 : derived().enter(x);
576 2 : derived().print("delay");
577 2 : derived().print(" @ ");
578 2 : print_expression(x.time_stamp(), precedence(x.time_stamp()) < core::detail::max_precedence);
579 2 : derived().leave(x);
580 2 : enable_val();
581 2 : }
582 :
583 83 : void apply(const state_formulas::variable& x)
584 : {
585 83 : disable_val();
586 83 : derived().enter(x);
587 83 : derived().apply(x.name());
588 83 : print_list(x.arguments(), "(", ")", ", ", false);
589 83 : derived().leave(x);
590 83 : enable_val();
591 83 : }
592 :
593 : // TODO: merge this function with the version in data/print.h (?)
594 96 : void print_assignments(const data::assignment_list& assignments)
595 : {
596 96 : if (assignments.empty())
597 : {
598 83 : return;
599 : }
600 13 : disable_val();
601 13 : derived().print("(");
602 29 : for (auto i = assignments.begin(); i != assignments.end(); ++i)
603 : {
604 16 : if (i != assignments.begin())
605 : {
606 3 : derived().print(", ");
607 : }
608 16 : derived().apply(i->lhs());
609 16 : derived().print(": ");
610 16 : derived().apply(i->lhs().sort());
611 16 : derived().print(" = ");
612 16 : derived().apply(i->rhs());
613 : }
614 13 : derived().print(")");
615 13 : enable_val();
616 : }
617 :
618 20 : void apply(const state_formulas::nu& x)
619 : {
620 20 : derived().enter(x);
621 20 : derived().print("nu ");
622 20 : derived().apply(x.name());
623 20 : print_assignments(x.assignments());
624 20 : derived().print(". ");
625 20 : derived().apply(x.operand());
626 20 : derived().leave(x);
627 20 : }
628 :
629 76 : void apply(const state_formulas::mu& x)
630 : {
631 76 : derived().enter(x);
632 76 : derived().print("mu ");
633 76 : derived().apply(x.name());
634 76 : print_assignments(x.assignments());
635 76 : derived().print(". ");
636 76 : derived().apply(x.operand());
637 76 : derived().leave(x);
638 76 : }
639 :
640 3 : void apply(const state_formulas::state_formula_specification& x)
641 : {
642 3 : derived().enter(x);
643 3 : derived().apply(x.data());
644 3 : print_action_declarations(x.action_labels(), "act ",";\n\n", ";\n ");
645 3 : derived().print("form ");
646 3 : derived().apply(x.formula());
647 3 : derived().print(";\n");
648 3 : derived().leave(x);
649 3 : }
650 : };
651 :
652 : } // namespace detail
653 :
654 : /// \brief Prints the object t to a stream.
655 : template <typename T>
656 140 : void pp(const T& t, std::ostream& out)
657 : {
658 140 : core::detail::apply_printer<state_formulas::detail::printer> printer(out);
659 140 : printer.apply(t);
660 140 : }
661 :
662 : /// \brief Returns a string representation of the object t.
663 : template <typename T>
664 140 : std::string pp(const T& t)
665 : {
666 140 : std::ostringstream out;
667 140 : state_formulas::pp(t, out);
668 280 : return out.str();
669 140 : }
670 :
671 : } // namespace state_formulas
672 :
673 : } // namespace mcrl2
674 :
675 : #endif // MCRL2_MODAL_FORMULA_PRINT_H
676 :
|