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