mCRL2
Loading...
Searching...
No Matches
traverser.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//
9/// \file mcrl2/modal_formula/traverser.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_MODAL_FORMULA_TRAVERSER_H
13#define MCRL2_MODAL_FORMULA_TRAVERSER_H
14
15#include "mcrl2/lps/traverser.h"
16#include "mcrl2/modal_formula/state_formula_specification.h"
17
18namespace mcrl2
19{
20
21namespace action_formulas
22{
23
24/// \brief Base class for action_formula_traverser.
25template <typename Derived>
26struct action_formula_traverser_base: public core::traverser<Derived>
27{
28 using super = core::traverser<Derived>;
29 using super::apply;
30 using super::enter;
31 using super::leave;
32
33 void apply(const data::data_expression& x)
34 {
35 static_cast<Derived&>(*this).enter(x);
36 // skip
37 static_cast<Derived&>(*this).leave(x);
38 }
39
40 void apply(const data::untyped_data_parameter& x)
41 {
42 static_cast<Derived&>(*this).enter(x);
43 // skip
44 static_cast<Derived&>(*this).leave(x);
45 }
46
47 void apply(const process::untyped_multi_action& x)
48 {
49 static_cast<Derived&>(*this).enter(x);
50 // skip
51 static_cast<Derived&>(*this).leave(x);
52 }
53};
54
55//--- start generated action_formulas::add_traverser_sort_expressions code ---//
56template <template <class> class Traverser, class Derived>
57struct add_traverser_sort_expressions: public Traverser<Derived>
58{
59 using super = Traverser<Derived>;
60 using super::enter;
61 using super::leave;
62 using super::apply;
63
64 void apply(const action_formulas::true_& x)
65 {
66 static_cast<Derived&>(*this).enter(x);
67 // skip
68 static_cast<Derived&>(*this).leave(x);
69 }
70
71 void apply(const action_formulas::false_& x)
72 {
73 static_cast<Derived&>(*this).enter(x);
74 // skip
75 static_cast<Derived&>(*this).leave(x);
76 }
77
78 void apply(const action_formulas::not_& x)
79 {
80 static_cast<Derived&>(*this).enter(x);
81 static_cast<Derived&>(*this).apply(x.operand());
82 static_cast<Derived&>(*this).leave(x);
83 }
84
85 void apply(const action_formulas::and_& x)
86 {
87 static_cast<Derived&>(*this).enter(x);
88 static_cast<Derived&>(*this).apply(x.left());
89 static_cast<Derived&>(*this).apply(x.right());
90 static_cast<Derived&>(*this).leave(x);
91 }
92
93 void apply(const action_formulas::or_& x)
94 {
95 static_cast<Derived&>(*this).enter(x);
96 static_cast<Derived&>(*this).apply(x.left());
97 static_cast<Derived&>(*this).apply(x.right());
98 static_cast<Derived&>(*this).leave(x);
99 }
100
101 void apply(const action_formulas::imp& x)
102 {
103 static_cast<Derived&>(*this).enter(x);
104 static_cast<Derived&>(*this).apply(x.left());
105 static_cast<Derived&>(*this).apply(x.right());
106 static_cast<Derived&>(*this).leave(x);
107 }
108
109 void apply(const action_formulas::forall& x)
110 {
111 static_cast<Derived&>(*this).enter(x);
112 static_cast<Derived&>(*this).apply(x.variables());
113 static_cast<Derived&>(*this).apply(x.body());
114 static_cast<Derived&>(*this).leave(x);
115 }
116
117 void apply(const action_formulas::exists& x)
118 {
119 static_cast<Derived&>(*this).enter(x);
120 static_cast<Derived&>(*this).apply(x.variables());
121 static_cast<Derived&>(*this).apply(x.body());
122 static_cast<Derived&>(*this).leave(x);
123 }
124
125 void apply(const action_formulas::at& x)
126 {
127 static_cast<Derived&>(*this).enter(x);
128 static_cast<Derived&>(*this).apply(x.operand());
129 static_cast<Derived&>(*this).apply(x.time_stamp());
130 static_cast<Derived&>(*this).leave(x);
131 }
132
133 void apply(const action_formulas::multi_action& x)
134 {
135 static_cast<Derived&>(*this).enter(x);
136 static_cast<Derived&>(*this).apply(x.actions());
137 static_cast<Derived&>(*this).leave(x);
138 }
139
140 void apply(const action_formulas::action_formula& x)
141 {
142 static_cast<Derived&>(*this).enter(x);
143 if (data::is_data_expression(x))
144 {
145 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
146 }
147 else if (data::is_untyped_data_parameter(x))
148 {
149 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
150 }
151 else if (action_formulas::is_true(x))
152 {
153 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
154 }
155 else if (action_formulas::is_false(x))
156 {
157 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
158 }
159 else if (action_formulas::is_not(x))
160 {
161 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
162 }
163 else if (action_formulas::is_and(x))
164 {
165 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
166 }
167 else if (action_formulas::is_or(x))
168 {
169 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
170 }
171 else if (action_formulas::is_imp(x))
172 {
173 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
174 }
175 else if (action_formulas::is_forall(x))
176 {
177 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
178 }
179 else if (action_formulas::is_exists(x))
180 {
181 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
182 }
183 else if (action_formulas::is_at(x))
184 {
185 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
186 }
187 else if (action_formulas::is_multi_action(x))
188 {
189 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
190 }
191 else if (process::is_untyped_multi_action(x))
192 {
193 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
194 }
195 static_cast<Derived&>(*this).leave(x);
196 }
197
198};
199
200/// \\brief Traverser class
201template <typename Derived>
202struct sort_expression_traverser: public add_traverser_sort_expressions<lps::sort_expression_traverser, Derived>
203{
204};
205//--- end generated action_formulas::add_traverser_sort_expressions code ---//
206
207//--- start generated action_formulas::add_traverser_data_expressions code ---//
208template <template <class> class Traverser, class Derived>
209struct add_traverser_data_expressions: public Traverser<Derived>
210{
211 using super = Traverser<Derived>;
212 using super::enter;
213 using super::leave;
214 using super::apply;
215
216 void apply(const action_formulas::true_& x)
217 {
218 static_cast<Derived&>(*this).enter(x);
219 // skip
220 static_cast<Derived&>(*this).leave(x);
221 }
222
223 void apply(const action_formulas::false_& x)
224 {
225 static_cast<Derived&>(*this).enter(x);
226 // skip
227 static_cast<Derived&>(*this).leave(x);
228 }
229
230 void apply(const action_formulas::not_& x)
231 {
232 static_cast<Derived&>(*this).enter(x);
233 static_cast<Derived&>(*this).apply(x.operand());
234 static_cast<Derived&>(*this).leave(x);
235 }
236
237 void apply(const action_formulas::and_& x)
238 {
239 static_cast<Derived&>(*this).enter(x);
240 static_cast<Derived&>(*this).apply(x.left());
241 static_cast<Derived&>(*this).apply(x.right());
242 static_cast<Derived&>(*this).leave(x);
243 }
244
245 void apply(const action_formulas::or_& x)
246 {
247 static_cast<Derived&>(*this).enter(x);
248 static_cast<Derived&>(*this).apply(x.left());
249 static_cast<Derived&>(*this).apply(x.right());
250 static_cast<Derived&>(*this).leave(x);
251 }
252
253 void apply(const action_formulas::imp& x)
254 {
255 static_cast<Derived&>(*this).enter(x);
256 static_cast<Derived&>(*this).apply(x.left());
257 static_cast<Derived&>(*this).apply(x.right());
258 static_cast<Derived&>(*this).leave(x);
259 }
260
261 void apply(const action_formulas::forall& x)
262 {
263 static_cast<Derived&>(*this).enter(x);
264 static_cast<Derived&>(*this).apply(x.body());
265 static_cast<Derived&>(*this).leave(x);
266 }
267
268 void apply(const action_formulas::exists& x)
269 {
270 static_cast<Derived&>(*this).enter(x);
271 static_cast<Derived&>(*this).apply(x.body());
272 static_cast<Derived&>(*this).leave(x);
273 }
274
275 void apply(const action_formulas::at& x)
276 {
277 static_cast<Derived&>(*this).enter(x);
278 static_cast<Derived&>(*this).apply(x.operand());
279 static_cast<Derived&>(*this).apply(x.time_stamp());
280 static_cast<Derived&>(*this).leave(x);
281 }
282
283 void apply(const action_formulas::multi_action& x)
284 {
285 static_cast<Derived&>(*this).enter(x);
286 static_cast<Derived&>(*this).apply(x.actions());
287 static_cast<Derived&>(*this).leave(x);
288 }
289
290 void apply(const action_formulas::action_formula& x)
291 {
292 static_cast<Derived&>(*this).enter(x);
293 if (data::is_data_expression(x))
294 {
295 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
296 }
297 else if (data::is_untyped_data_parameter(x))
298 {
299 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
300 }
301 else if (action_formulas::is_true(x))
302 {
303 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
304 }
305 else if (action_formulas::is_false(x))
306 {
307 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
308 }
309 else if (action_formulas::is_not(x))
310 {
311 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
312 }
313 else if (action_formulas::is_and(x))
314 {
315 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
316 }
317 else if (action_formulas::is_or(x))
318 {
319 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
320 }
321 else if (action_formulas::is_imp(x))
322 {
323 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
324 }
325 else if (action_formulas::is_forall(x))
326 {
327 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
328 }
329 else if (action_formulas::is_exists(x))
330 {
331 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
332 }
333 else if (action_formulas::is_at(x))
334 {
335 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
336 }
337 else if (action_formulas::is_multi_action(x))
338 {
339 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
340 }
341 else if (process::is_untyped_multi_action(x))
342 {
343 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
344 }
345 static_cast<Derived&>(*this).leave(x);
346 }
347
348};
349
350/// \\brief Traverser class
351template <typename Derived>
352struct data_expression_traverser: public add_traverser_data_expressions<lps::data_expression_traverser, Derived>
353{
354};
355//--- end generated action_formulas::add_traverser_data_expressions code ---//
356
357//--- start generated action_formulas::add_traverser_action_formula_expressions code ---//
358template <template <class> class Traverser, class Derived>
359struct add_traverser_action_formula_expressions: public Traverser<Derived>
360{
361 using super = Traverser<Derived>;
362 using super::enter;
363 using super::leave;
364 using super::apply;
365
366 void apply(const action_formulas::true_& x)
367 {
368 static_cast<Derived&>(*this).enter(x);
369 // skip
370 static_cast<Derived&>(*this).leave(x);
371 }
372
373 void apply(const action_formulas::false_& x)
374 {
375 static_cast<Derived&>(*this).enter(x);
376 // skip
377 static_cast<Derived&>(*this).leave(x);
378 }
379
380 void apply(const action_formulas::not_& x)
381 {
382 static_cast<Derived&>(*this).enter(x);
383 static_cast<Derived&>(*this).apply(x.operand());
384 static_cast<Derived&>(*this).leave(x);
385 }
386
387 void apply(const action_formulas::and_& x)
388 {
389 static_cast<Derived&>(*this).enter(x);
390 static_cast<Derived&>(*this).apply(x.left());
391 static_cast<Derived&>(*this).apply(x.right());
392 static_cast<Derived&>(*this).leave(x);
393 }
394
395 void apply(const action_formulas::or_& x)
396 {
397 static_cast<Derived&>(*this).enter(x);
398 static_cast<Derived&>(*this).apply(x.left());
399 static_cast<Derived&>(*this).apply(x.right());
400 static_cast<Derived&>(*this).leave(x);
401 }
402
403 void apply(const action_formulas::imp& x)
404 {
405 static_cast<Derived&>(*this).enter(x);
406 static_cast<Derived&>(*this).apply(x.left());
407 static_cast<Derived&>(*this).apply(x.right());
408 static_cast<Derived&>(*this).leave(x);
409 }
410
411 void apply(const action_formulas::forall& x)
412 {
413 static_cast<Derived&>(*this).enter(x);
414 static_cast<Derived&>(*this).apply(x.body());
415 static_cast<Derived&>(*this).leave(x);
416 }
417
418 void apply(const action_formulas::exists& x)
419 {
420 static_cast<Derived&>(*this).enter(x);
421 static_cast<Derived&>(*this).apply(x.body());
422 static_cast<Derived&>(*this).leave(x);
423 }
424
425 void apply(const action_formulas::at& x)
426 {
427 static_cast<Derived&>(*this).enter(x);
428 static_cast<Derived&>(*this).apply(x.operand());
429 static_cast<Derived&>(*this).leave(x);
430 }
431
432 void apply(const action_formulas::multi_action& x)
433 {
434 static_cast<Derived&>(*this).enter(x);
435 // skip
436 static_cast<Derived&>(*this).leave(x);
437 }
438
439 void apply(const action_formulas::action_formula& x)
440 {
441 static_cast<Derived&>(*this).enter(x);
442 if (data::is_data_expression(x))
443 {
444 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
445 }
446 else if (data::is_untyped_data_parameter(x))
447 {
448 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
449 }
450 else if (action_formulas::is_true(x))
451 {
452 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
453 }
454 else if (action_formulas::is_false(x))
455 {
456 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
457 }
458 else if (action_formulas::is_not(x))
459 {
460 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
461 }
462 else if (action_formulas::is_and(x))
463 {
464 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
465 }
466 else if (action_formulas::is_or(x))
467 {
468 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
469 }
470 else if (action_formulas::is_imp(x))
471 {
472 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
473 }
474 else if (action_formulas::is_forall(x))
475 {
476 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
477 }
478 else if (action_formulas::is_exists(x))
479 {
480 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
481 }
482 else if (action_formulas::is_at(x))
483 {
484 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
485 }
486 else if (action_formulas::is_multi_action(x))
487 {
488 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
489 }
490 else if (process::is_untyped_multi_action(x))
491 {
492 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
493 }
494 static_cast<Derived&>(*this).leave(x);
495 }
496
497};
498
499/// \\brief Traverser class
500template <typename Derived>
501struct action_formula_traverser: public add_traverser_action_formula_expressions<action_formulas::action_formula_traverser_base, Derived>
502{
503};
504//--- end generated action_formulas::add_traverser_action_formula_expressions code ---//
505
506//--- start generated action_formulas::add_traverser_variables code ---//
507template <template <class> class Traverser, class Derived>
508struct add_traverser_variables: public Traverser<Derived>
509{
510 using super = Traverser<Derived>;
511 using super::enter;
512 using super::leave;
513 using super::apply;
514
515 void apply(const action_formulas::true_& x)
516 {
517 static_cast<Derived&>(*this).enter(x);
518 // skip
519 static_cast<Derived&>(*this).leave(x);
520 }
521
522 void apply(const action_formulas::false_& x)
523 {
524 static_cast<Derived&>(*this).enter(x);
525 // skip
526 static_cast<Derived&>(*this).leave(x);
527 }
528
529 void apply(const action_formulas::not_& x)
530 {
531 static_cast<Derived&>(*this).enter(x);
532 static_cast<Derived&>(*this).apply(x.operand());
533 static_cast<Derived&>(*this).leave(x);
534 }
535
536 void apply(const action_formulas::and_& x)
537 {
538 static_cast<Derived&>(*this).enter(x);
539 static_cast<Derived&>(*this).apply(x.left());
540 static_cast<Derived&>(*this).apply(x.right());
541 static_cast<Derived&>(*this).leave(x);
542 }
543
544 void apply(const action_formulas::or_& x)
545 {
546 static_cast<Derived&>(*this).enter(x);
547 static_cast<Derived&>(*this).apply(x.left());
548 static_cast<Derived&>(*this).apply(x.right());
549 static_cast<Derived&>(*this).leave(x);
550 }
551
552 void apply(const action_formulas::imp& x)
553 {
554 static_cast<Derived&>(*this).enter(x);
555 static_cast<Derived&>(*this).apply(x.left());
556 static_cast<Derived&>(*this).apply(x.right());
557 static_cast<Derived&>(*this).leave(x);
558 }
559
560 void apply(const action_formulas::forall& x)
561 {
562 static_cast<Derived&>(*this).enter(x);
563 static_cast<Derived&>(*this).apply(x.variables());
564 static_cast<Derived&>(*this).apply(x.body());
565 static_cast<Derived&>(*this).leave(x);
566 }
567
568 void apply(const action_formulas::exists& x)
569 {
570 static_cast<Derived&>(*this).enter(x);
571 static_cast<Derived&>(*this).apply(x.variables());
572 static_cast<Derived&>(*this).apply(x.body());
573 static_cast<Derived&>(*this).leave(x);
574 }
575
576 void apply(const action_formulas::at& x)
577 {
578 static_cast<Derived&>(*this).enter(x);
579 static_cast<Derived&>(*this).apply(x.operand());
580 static_cast<Derived&>(*this).apply(x.time_stamp());
581 static_cast<Derived&>(*this).leave(x);
582 }
583
584 void apply(const action_formulas::multi_action& x)
585 {
586 static_cast<Derived&>(*this).enter(x);
587 static_cast<Derived&>(*this).apply(x.actions());
588 static_cast<Derived&>(*this).leave(x);
589 }
590
591 void apply(const action_formulas::action_formula& x)
592 {
593 static_cast<Derived&>(*this).enter(x);
594 if (data::is_data_expression(x))
595 {
596 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
597 }
598 else if (data::is_untyped_data_parameter(x))
599 {
600 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
601 }
602 else if (action_formulas::is_true(x))
603 {
604 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
605 }
606 else if (action_formulas::is_false(x))
607 {
608 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
609 }
610 else if (action_formulas::is_not(x))
611 {
612 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
613 }
614 else if (action_formulas::is_and(x))
615 {
616 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
617 }
618 else if (action_formulas::is_or(x))
619 {
620 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
621 }
622 else if (action_formulas::is_imp(x))
623 {
624 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
625 }
626 else if (action_formulas::is_forall(x))
627 {
628 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
629 }
630 else if (action_formulas::is_exists(x))
631 {
632 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
633 }
634 else if (action_formulas::is_at(x))
635 {
636 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
637 }
638 else if (action_formulas::is_multi_action(x))
639 {
640 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
641 }
642 else if (process::is_untyped_multi_action(x))
643 {
644 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
645 }
646 static_cast<Derived&>(*this).leave(x);
647 }
648
649};
650
651/// \\brief Traverser class
652template <typename Derived>
653struct variable_traverser: public add_traverser_variables<lps::variable_traverser, Derived>
654{
655};
656//--- end generated action_formulas::add_traverser_variables code ---//
657
658//--- start generated action_formulas::add_traverser_identifier_strings code ---//
659template <template <class> class Traverser, class Derived>
660struct add_traverser_identifier_strings: public Traverser<Derived>
661{
662 using super = Traverser<Derived>;
663 using super::enter;
664 using super::leave;
665 using super::apply;
666
667 void apply(const action_formulas::true_& x)
668 {
669 static_cast<Derived&>(*this).enter(x);
670 // skip
671 static_cast<Derived&>(*this).leave(x);
672 }
673
674 void apply(const action_formulas::false_& x)
675 {
676 static_cast<Derived&>(*this).enter(x);
677 // skip
678 static_cast<Derived&>(*this).leave(x);
679 }
680
681 void apply(const action_formulas::not_& x)
682 {
683 static_cast<Derived&>(*this).enter(x);
684 static_cast<Derived&>(*this).apply(x.operand());
685 static_cast<Derived&>(*this).leave(x);
686 }
687
688 void apply(const action_formulas::and_& x)
689 {
690 static_cast<Derived&>(*this).enter(x);
691 static_cast<Derived&>(*this).apply(x.left());
692 static_cast<Derived&>(*this).apply(x.right());
693 static_cast<Derived&>(*this).leave(x);
694 }
695
696 void apply(const action_formulas::or_& x)
697 {
698 static_cast<Derived&>(*this).enter(x);
699 static_cast<Derived&>(*this).apply(x.left());
700 static_cast<Derived&>(*this).apply(x.right());
701 static_cast<Derived&>(*this).leave(x);
702 }
703
704 void apply(const action_formulas::imp& x)
705 {
706 static_cast<Derived&>(*this).enter(x);
707 static_cast<Derived&>(*this).apply(x.left());
708 static_cast<Derived&>(*this).apply(x.right());
709 static_cast<Derived&>(*this).leave(x);
710 }
711
712 void apply(const action_formulas::forall& x)
713 {
714 static_cast<Derived&>(*this).enter(x);
715 static_cast<Derived&>(*this).apply(x.variables());
716 static_cast<Derived&>(*this).apply(x.body());
717 static_cast<Derived&>(*this).leave(x);
718 }
719
720 void apply(const action_formulas::exists& x)
721 {
722 static_cast<Derived&>(*this).enter(x);
723 static_cast<Derived&>(*this).apply(x.variables());
724 static_cast<Derived&>(*this).apply(x.body());
725 static_cast<Derived&>(*this).leave(x);
726 }
727
728 void apply(const action_formulas::at& x)
729 {
730 static_cast<Derived&>(*this).enter(x);
731 static_cast<Derived&>(*this).apply(x.operand());
732 static_cast<Derived&>(*this).apply(x.time_stamp());
733 static_cast<Derived&>(*this).leave(x);
734 }
735
736 void apply(const action_formulas::multi_action& x)
737 {
738 static_cast<Derived&>(*this).enter(x);
739 static_cast<Derived&>(*this).apply(x.actions());
740 static_cast<Derived&>(*this).leave(x);
741 }
742
743 void apply(const action_formulas::action_formula& x)
744 {
745 static_cast<Derived&>(*this).enter(x);
746 if (data::is_data_expression(x))
747 {
748 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
749 }
750 else if (data::is_untyped_data_parameter(x))
751 {
752 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
753 }
754 else if (action_formulas::is_true(x))
755 {
756 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
757 }
758 else if (action_formulas::is_false(x))
759 {
760 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
761 }
762 else if (action_formulas::is_not(x))
763 {
764 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
765 }
766 else if (action_formulas::is_and(x))
767 {
768 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
769 }
770 else if (action_formulas::is_or(x))
771 {
772 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
773 }
774 else if (action_formulas::is_imp(x))
775 {
776 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
777 }
778 else if (action_formulas::is_forall(x))
779 {
780 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
781 }
782 else if (action_formulas::is_exists(x))
783 {
784 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
785 }
786 else if (action_formulas::is_at(x))
787 {
788 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
789 }
790 else if (action_formulas::is_multi_action(x))
791 {
792 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
793 }
794 else if (process::is_untyped_multi_action(x))
795 {
796 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
797 }
798 static_cast<Derived&>(*this).leave(x);
799 }
800
801};
802
803/// \\brief Traverser class
804template <typename Derived>
805struct identifier_string_traverser: public add_traverser_identifier_strings<lps::identifier_string_traverser, Derived>
806{
807};
808//--- end generated action_formulas::add_traverser_identifier_strings code ---//
809
810//--- start generated action_formulas::add_traverser_action_labels code ---//
811template <template <class> class Traverser, class Derived>
812struct add_traverser_action_labels: public Traverser<Derived>
813{
814 using super = Traverser<Derived>;
815 using super::enter;
816 using super::leave;
817 using super::apply;
818
819 void apply(const action_formulas::true_& x)
820 {
821 static_cast<Derived&>(*this).enter(x);
822 // skip
823 static_cast<Derived&>(*this).leave(x);
824 }
825
826 void apply(const action_formulas::false_& x)
827 {
828 static_cast<Derived&>(*this).enter(x);
829 // skip
830 static_cast<Derived&>(*this).leave(x);
831 }
832
833 void apply(const action_formulas::not_& x)
834 {
835 static_cast<Derived&>(*this).enter(x);
836 static_cast<Derived&>(*this).apply(x.operand());
837 static_cast<Derived&>(*this).leave(x);
838 }
839
840 void apply(const action_formulas::and_& x)
841 {
842 static_cast<Derived&>(*this).enter(x);
843 static_cast<Derived&>(*this).apply(x.left());
844 static_cast<Derived&>(*this).apply(x.right());
845 static_cast<Derived&>(*this).leave(x);
846 }
847
848 void apply(const action_formulas::or_& x)
849 {
850 static_cast<Derived&>(*this).enter(x);
851 static_cast<Derived&>(*this).apply(x.left());
852 static_cast<Derived&>(*this).apply(x.right());
853 static_cast<Derived&>(*this).leave(x);
854 }
855
856 void apply(const action_formulas::imp& x)
857 {
858 static_cast<Derived&>(*this).enter(x);
859 static_cast<Derived&>(*this).apply(x.left());
860 static_cast<Derived&>(*this).apply(x.right());
861 static_cast<Derived&>(*this).leave(x);
862 }
863
864 void apply(const action_formulas::forall& x)
865 {
866 static_cast<Derived&>(*this).enter(x);
867 static_cast<Derived&>(*this).apply(x.body());
868 static_cast<Derived&>(*this).leave(x);
869 }
870
871 void apply(const action_formulas::exists& x)
872 {
873 static_cast<Derived&>(*this).enter(x);
874 static_cast<Derived&>(*this).apply(x.body());
875 static_cast<Derived&>(*this).leave(x);
876 }
877
878 void apply(const action_formulas::at& x)
879 {
880 static_cast<Derived&>(*this).enter(x);
881 static_cast<Derived&>(*this).apply(x.operand());
882 static_cast<Derived&>(*this).leave(x);
883 }
884
885 void apply(const action_formulas::multi_action& x)
886 {
887 static_cast<Derived&>(*this).enter(x);
888 static_cast<Derived&>(*this).apply(x.actions());
889 static_cast<Derived&>(*this).leave(x);
890 }
891
892 void apply(const action_formulas::action_formula& x)
893 {
894 static_cast<Derived&>(*this).enter(x);
895 if (data::is_data_expression(x))
896 {
897 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
898 }
899 else if (data::is_untyped_data_parameter(x))
900 {
901 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
902 }
903 else if (action_formulas::is_true(x))
904 {
905 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::true_>(x));
906 }
907 else if (action_formulas::is_false(x))
908 {
909 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::false_>(x));
910 }
911 else if (action_formulas::is_not(x))
912 {
913 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::not_>(x));
914 }
915 else if (action_formulas::is_and(x))
916 {
917 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::and_>(x));
918 }
919 else if (action_formulas::is_or(x))
920 {
921 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::or_>(x));
922 }
923 else if (action_formulas::is_imp(x))
924 {
925 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::imp>(x));
926 }
927 else if (action_formulas::is_forall(x))
928 {
929 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::forall>(x));
930 }
931 else if (action_formulas::is_exists(x))
932 {
933 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::exists>(x));
934 }
935 else if (action_formulas::is_at(x))
936 {
937 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::at>(x));
938 }
939 else if (action_formulas::is_multi_action(x))
940 {
941 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::multi_action>(x));
942 }
943 else if (process::is_untyped_multi_action(x))
944 {
945 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_multi_action>(x));
946 }
947 static_cast<Derived&>(*this).leave(x);
948 }
949
950};
951
952/// \\brief Traverser class
953template <typename Derived>
954struct action_label_traverser: public add_traverser_action_labels<lps::action_label_traverser, Derived>
955{
956};
957//--- end generated action_formulas::add_traverser_action_labels code ---//
958
959} // namespace action_formulas
960
961namespace regular_formulas
962{
963
964/// \brief Traversal class for regular_formula_traverser. Used as a base class for pbes_expression_traverser.
965template <typename Derived>
966struct regular_formula_traverser_base: public core::traverser<Derived>
967{
968 using super = core::traverser<Derived>;
969 using super::apply;
970 using super::enter;
971 using super::leave;
972
973 void apply(const data::data_expression& x)
974 {
975 static_cast<Derived&>(*this).enter(x);
976 // skip
977 static_cast<Derived&>(*this).leave(x);
978 }
979
980 void apply(const action_formulas::action_formula& x)
981 {
982 static_cast<Derived&>(*this).enter(x);
983 // skip
984 static_cast<Derived&>(*this).leave(x);
985 }
986};
987
988//--- start generated regular_formulas::add_traverser_sort_expressions code ---//
989template <template <class> class Traverser, class Derived>
990struct add_traverser_sort_expressions: public Traverser<Derived>
991{
992 using super = Traverser<Derived>;
993 using super::enter;
994 using super::leave;
995 using super::apply;
996
997 void apply(const regular_formulas::seq& x)
998 {
999 static_cast<Derived&>(*this).enter(x);
1000 static_cast<Derived&>(*this).apply(x.left());
1001 static_cast<Derived&>(*this).apply(x.right());
1002 static_cast<Derived&>(*this).leave(x);
1003 }
1004
1005 void apply(const regular_formulas::alt& x)
1006 {
1007 static_cast<Derived&>(*this).enter(x);
1008 static_cast<Derived&>(*this).apply(x.left());
1009 static_cast<Derived&>(*this).apply(x.right());
1010 static_cast<Derived&>(*this).leave(x);
1011 }
1012
1013 void apply(const regular_formulas::trans& x)
1014 {
1015 static_cast<Derived&>(*this).enter(x);
1016 static_cast<Derived&>(*this).apply(x.operand());
1017 static_cast<Derived&>(*this).leave(x);
1018 }
1019
1020 void apply(const regular_formulas::trans_or_nil& x)
1021 {
1022 static_cast<Derived&>(*this).enter(x);
1023 static_cast<Derived&>(*this).apply(x.operand());
1024 static_cast<Derived&>(*this).leave(x);
1025 }
1026
1027 void apply(const regular_formulas::untyped_regular_formula& x)
1028 {
1029 static_cast<Derived&>(*this).enter(x);
1030 static_cast<Derived&>(*this).apply(x.left());
1031 static_cast<Derived&>(*this).apply(x.right());
1032 static_cast<Derived&>(*this).leave(x);
1033 }
1034
1035 void apply(const regular_formulas::regular_formula& x)
1036 {
1037 static_cast<Derived&>(*this).enter(x);
1038 if (data::is_data_expression(x))
1039 {
1040 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1041 }
1042 else if (action_formulas::is_action_formula(x))
1043 {
1044 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1045 }
1046 else if (regular_formulas::is_seq(x))
1047 {
1048 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1049 }
1050 else if (regular_formulas::is_alt(x))
1051 {
1052 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1053 }
1054 else if (regular_formulas::is_trans(x))
1055 {
1056 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1057 }
1058 else if (regular_formulas::is_trans_or_nil(x))
1059 {
1060 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1061 }
1062 else if (regular_formulas::is_untyped_regular_formula(x))
1063 {
1064 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1065 }
1066 static_cast<Derived&>(*this).leave(x);
1067 }
1068
1069};
1070
1071/// \\brief Traverser class
1072template <typename Derived>
1073struct sort_expression_traverser: public add_traverser_sort_expressions<action_formulas::sort_expression_traverser, Derived>
1074{
1075};
1076//--- end generated regular_formulas::add_traverser_sort_expressions code ---//
1077
1078//--- start generated regular_formulas::add_traverser_data_expressions code ---//
1079template <template <class> class Traverser, class Derived>
1080struct add_traverser_data_expressions: public Traverser<Derived>
1081{
1082 using super = Traverser<Derived>;
1083 using super::enter;
1084 using super::leave;
1085 using super::apply;
1086
1087 void apply(const regular_formulas::seq& x)
1088 {
1089 static_cast<Derived&>(*this).enter(x);
1090 static_cast<Derived&>(*this).apply(x.left());
1091 static_cast<Derived&>(*this).apply(x.right());
1092 static_cast<Derived&>(*this).leave(x);
1093 }
1094
1095 void apply(const regular_formulas::alt& x)
1096 {
1097 static_cast<Derived&>(*this).enter(x);
1098 static_cast<Derived&>(*this).apply(x.left());
1099 static_cast<Derived&>(*this).apply(x.right());
1100 static_cast<Derived&>(*this).leave(x);
1101 }
1102
1103 void apply(const regular_formulas::trans& x)
1104 {
1105 static_cast<Derived&>(*this).enter(x);
1106 static_cast<Derived&>(*this).apply(x.operand());
1107 static_cast<Derived&>(*this).leave(x);
1108 }
1109
1110 void apply(const regular_formulas::trans_or_nil& x)
1111 {
1112 static_cast<Derived&>(*this).enter(x);
1113 static_cast<Derived&>(*this).apply(x.operand());
1114 static_cast<Derived&>(*this).leave(x);
1115 }
1116
1117 void apply(const regular_formulas::untyped_regular_formula& x)
1118 {
1119 static_cast<Derived&>(*this).enter(x);
1120 static_cast<Derived&>(*this).apply(x.left());
1121 static_cast<Derived&>(*this).apply(x.right());
1122 static_cast<Derived&>(*this).leave(x);
1123 }
1124
1125 void apply(const regular_formulas::regular_formula& x)
1126 {
1127 static_cast<Derived&>(*this).enter(x);
1128 if (data::is_data_expression(x))
1129 {
1130 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1131 }
1132 else if (action_formulas::is_action_formula(x))
1133 {
1134 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1135 }
1136 else if (regular_formulas::is_seq(x))
1137 {
1138 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1139 }
1140 else if (regular_formulas::is_alt(x))
1141 {
1142 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1143 }
1144 else if (regular_formulas::is_trans(x))
1145 {
1146 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1147 }
1148 else if (regular_formulas::is_trans_or_nil(x))
1149 {
1150 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1151 }
1152 else if (regular_formulas::is_untyped_regular_formula(x))
1153 {
1154 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1155 }
1156 static_cast<Derived&>(*this).leave(x);
1157 }
1158
1159};
1160
1161/// \\brief Traverser class
1162template <typename Derived>
1163struct data_expression_traverser: public add_traverser_data_expressions<action_formulas::data_expression_traverser, Derived>
1164{
1165};
1166//--- end generated regular_formulas::add_traverser_data_expressions code ---//
1167
1168//--- start generated regular_formulas::add_traverser_regular_formula_expressions code ---//
1169template <template <class> class Traverser, class Derived>
1170struct add_traverser_regular_formula_expressions: public Traverser<Derived>
1171{
1172 using super = Traverser<Derived>;
1173 using super::enter;
1174 using super::leave;
1175 using super::apply;
1176
1177 void apply(const regular_formulas::seq& x)
1178 {
1179 static_cast<Derived&>(*this).enter(x);
1180 static_cast<Derived&>(*this).apply(x.left());
1181 static_cast<Derived&>(*this).apply(x.right());
1182 static_cast<Derived&>(*this).leave(x);
1183 }
1184
1185 void apply(const regular_formulas::alt& x)
1186 {
1187 static_cast<Derived&>(*this).enter(x);
1188 static_cast<Derived&>(*this).apply(x.left());
1189 static_cast<Derived&>(*this).apply(x.right());
1190 static_cast<Derived&>(*this).leave(x);
1191 }
1192
1193 void apply(const regular_formulas::trans& x)
1194 {
1195 static_cast<Derived&>(*this).enter(x);
1196 static_cast<Derived&>(*this).apply(x.operand());
1197 static_cast<Derived&>(*this).leave(x);
1198 }
1199
1200 void apply(const regular_formulas::trans_or_nil& x)
1201 {
1202 static_cast<Derived&>(*this).enter(x);
1203 static_cast<Derived&>(*this).apply(x.operand());
1204 static_cast<Derived&>(*this).leave(x);
1205 }
1206
1207 void apply(const regular_formulas::untyped_regular_formula& x)
1208 {
1209 static_cast<Derived&>(*this).enter(x);
1210 static_cast<Derived&>(*this).apply(x.left());
1211 static_cast<Derived&>(*this).apply(x.right());
1212 static_cast<Derived&>(*this).leave(x);
1213 }
1214
1215 void apply(const regular_formulas::regular_formula& x)
1216 {
1217 static_cast<Derived&>(*this).enter(x);
1218 if (data::is_data_expression(x))
1219 {
1220 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1221 }
1222 else if (action_formulas::is_action_formula(x))
1223 {
1224 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1225 }
1226 else if (regular_formulas::is_seq(x))
1227 {
1228 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1229 }
1230 else if (regular_formulas::is_alt(x))
1231 {
1232 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1233 }
1234 else if (regular_formulas::is_trans(x))
1235 {
1236 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1237 }
1238 else if (regular_formulas::is_trans_or_nil(x))
1239 {
1240 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1241 }
1242 else if (regular_formulas::is_untyped_regular_formula(x))
1243 {
1244 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1245 }
1246 static_cast<Derived&>(*this).leave(x);
1247 }
1248
1249};
1250
1251/// \\brief Traverser class
1252template <typename Derived>
1253struct regular_formula_traverser: public add_traverser_regular_formula_expressions<regular_formulas::regular_formula_traverser_base, Derived>
1254{
1255};
1256//--- end generated regular_formulas::add_traverser_regular_formula_expressions code ---//
1257
1258//--- start generated regular_formulas::add_traverser_variables code ---//
1259template <template <class> class Traverser, class Derived>
1260struct add_traverser_variables: public Traverser<Derived>
1261{
1262 using super = Traverser<Derived>;
1263 using super::enter;
1264 using super::leave;
1265 using super::apply;
1266
1267 void apply(const regular_formulas::seq& x)
1268 {
1269 static_cast<Derived&>(*this).enter(x);
1270 static_cast<Derived&>(*this).apply(x.left());
1271 static_cast<Derived&>(*this).apply(x.right());
1272 static_cast<Derived&>(*this).leave(x);
1273 }
1274
1275 void apply(const regular_formulas::alt& x)
1276 {
1277 static_cast<Derived&>(*this).enter(x);
1278 static_cast<Derived&>(*this).apply(x.left());
1279 static_cast<Derived&>(*this).apply(x.right());
1280 static_cast<Derived&>(*this).leave(x);
1281 }
1282
1283 void apply(const regular_formulas::trans& x)
1284 {
1285 static_cast<Derived&>(*this).enter(x);
1286 static_cast<Derived&>(*this).apply(x.operand());
1287 static_cast<Derived&>(*this).leave(x);
1288 }
1289
1290 void apply(const regular_formulas::trans_or_nil& x)
1291 {
1292 static_cast<Derived&>(*this).enter(x);
1293 static_cast<Derived&>(*this).apply(x.operand());
1294 static_cast<Derived&>(*this).leave(x);
1295 }
1296
1297 void apply(const regular_formulas::untyped_regular_formula& x)
1298 {
1299 static_cast<Derived&>(*this).enter(x);
1300 static_cast<Derived&>(*this).apply(x.left());
1301 static_cast<Derived&>(*this).apply(x.right());
1302 static_cast<Derived&>(*this).leave(x);
1303 }
1304
1305 void apply(const regular_formulas::regular_formula& x)
1306 {
1307 static_cast<Derived&>(*this).enter(x);
1308 if (data::is_data_expression(x))
1309 {
1310 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1311 }
1312 else if (action_formulas::is_action_formula(x))
1313 {
1314 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1315 }
1316 else if (regular_formulas::is_seq(x))
1317 {
1318 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1319 }
1320 else if (regular_formulas::is_alt(x))
1321 {
1322 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1323 }
1324 else if (regular_formulas::is_trans(x))
1325 {
1326 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1327 }
1328 else if (regular_formulas::is_trans_or_nil(x))
1329 {
1330 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1331 }
1332 else if (regular_formulas::is_untyped_regular_formula(x))
1333 {
1334 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1335 }
1336 static_cast<Derived&>(*this).leave(x);
1337 }
1338
1339};
1340
1341/// \\brief Traverser class
1342template <typename Derived>
1343struct variable_traverser: public add_traverser_variables<action_formulas::variable_traverser, Derived>
1344{
1345};
1346//--- end generated regular_formulas::add_traverser_variables code ---//
1347
1348//--- start generated regular_formulas::add_traverser_identifier_strings code ---//
1349template <template <class> class Traverser, class Derived>
1350struct add_traverser_identifier_strings: public Traverser<Derived>
1351{
1352 using super = Traverser<Derived>;
1353 using super::enter;
1354 using super::leave;
1355 using super::apply;
1356
1357 void apply(const regular_formulas::seq& x)
1358 {
1359 static_cast<Derived&>(*this).enter(x);
1360 static_cast<Derived&>(*this).apply(x.left());
1361 static_cast<Derived&>(*this).apply(x.right());
1362 static_cast<Derived&>(*this).leave(x);
1363 }
1364
1365 void apply(const regular_formulas::alt& x)
1366 {
1367 static_cast<Derived&>(*this).enter(x);
1368 static_cast<Derived&>(*this).apply(x.left());
1369 static_cast<Derived&>(*this).apply(x.right());
1370 static_cast<Derived&>(*this).leave(x);
1371 }
1372
1373 void apply(const regular_formulas::trans& x)
1374 {
1375 static_cast<Derived&>(*this).enter(x);
1376 static_cast<Derived&>(*this).apply(x.operand());
1377 static_cast<Derived&>(*this).leave(x);
1378 }
1379
1380 void apply(const regular_formulas::trans_or_nil& x)
1381 {
1382 static_cast<Derived&>(*this).enter(x);
1383 static_cast<Derived&>(*this).apply(x.operand());
1384 static_cast<Derived&>(*this).leave(x);
1385 }
1386
1387 void apply(const regular_formulas::untyped_regular_formula& x)
1388 {
1389 static_cast<Derived&>(*this).enter(x);
1390 static_cast<Derived&>(*this).apply(x.name());
1391 static_cast<Derived&>(*this).apply(x.left());
1392 static_cast<Derived&>(*this).apply(x.right());
1393 static_cast<Derived&>(*this).leave(x);
1394 }
1395
1396 void apply(const regular_formulas::regular_formula& x)
1397 {
1398 static_cast<Derived&>(*this).enter(x);
1399 if (data::is_data_expression(x))
1400 {
1401 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1402 }
1403 else if (action_formulas::is_action_formula(x))
1404 {
1405 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1406 }
1407 else if (regular_formulas::is_seq(x))
1408 {
1409 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1410 }
1411 else if (regular_formulas::is_alt(x))
1412 {
1413 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1414 }
1415 else if (regular_formulas::is_trans(x))
1416 {
1417 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1418 }
1419 else if (regular_formulas::is_trans_or_nil(x))
1420 {
1421 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1422 }
1423 else if (regular_formulas::is_untyped_regular_formula(x))
1424 {
1425 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1426 }
1427 static_cast<Derived&>(*this).leave(x);
1428 }
1429
1430};
1431
1432/// \\brief Traverser class
1433template <typename Derived>
1434struct identifier_string_traverser: public add_traverser_identifier_strings<action_formulas::identifier_string_traverser, Derived>
1435{
1436};
1437//--- end generated regular_formulas::add_traverser_identifier_strings code ---//
1438
1439//--- start generated regular_formulas::add_traverser_action_labels code ---//
1440template <template <class> class Traverser, class Derived>
1441struct add_traverser_action_labels: public Traverser<Derived>
1442{
1443 using super = Traverser<Derived>;
1444 using super::enter;
1445 using super::leave;
1446 using super::apply;
1447
1448 void apply(const regular_formulas::seq& x)
1449 {
1450 static_cast<Derived&>(*this).enter(x);
1451 static_cast<Derived&>(*this).apply(x.left());
1452 static_cast<Derived&>(*this).apply(x.right());
1453 static_cast<Derived&>(*this).leave(x);
1454 }
1455
1456 void apply(const regular_formulas::alt& x)
1457 {
1458 static_cast<Derived&>(*this).enter(x);
1459 static_cast<Derived&>(*this).apply(x.left());
1460 static_cast<Derived&>(*this).apply(x.right());
1461 static_cast<Derived&>(*this).leave(x);
1462 }
1463
1464 void apply(const regular_formulas::trans& x)
1465 {
1466 static_cast<Derived&>(*this).enter(x);
1467 static_cast<Derived&>(*this).apply(x.operand());
1468 static_cast<Derived&>(*this).leave(x);
1469 }
1470
1471 void apply(const regular_formulas::trans_or_nil& x)
1472 {
1473 static_cast<Derived&>(*this).enter(x);
1474 static_cast<Derived&>(*this).apply(x.operand());
1475 static_cast<Derived&>(*this).leave(x);
1476 }
1477
1478 void apply(const regular_formulas::untyped_regular_formula& x)
1479 {
1480 static_cast<Derived&>(*this).enter(x);
1481 static_cast<Derived&>(*this).apply(x.left());
1482 static_cast<Derived&>(*this).apply(x.right());
1483 static_cast<Derived&>(*this).leave(x);
1484 }
1485
1486 void apply(const regular_formulas::regular_formula& x)
1487 {
1488 static_cast<Derived&>(*this).enter(x);
1489 if (data::is_data_expression(x))
1490 {
1491 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1492 }
1493 else if (action_formulas::is_action_formula(x))
1494 {
1495 static_cast<Derived&>(*this).apply(atermpp::down_cast<action_formulas::action_formula>(x));
1496 }
1497 else if (regular_formulas::is_seq(x))
1498 {
1499 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::seq>(x));
1500 }
1501 else if (regular_formulas::is_alt(x))
1502 {
1503 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::alt>(x));
1504 }
1505 else if (regular_formulas::is_trans(x))
1506 {
1507 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans>(x));
1508 }
1509 else if (regular_formulas::is_trans_or_nil(x))
1510 {
1511 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1512 }
1513 else if (regular_formulas::is_untyped_regular_formula(x))
1514 {
1515 static_cast<Derived&>(*this).apply(atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1516 }
1517 static_cast<Derived&>(*this).leave(x);
1518 }
1519
1520};
1521
1522/// \\brief Traverser class
1523template <typename Derived>
1524struct action_label_traverser: public add_traverser_action_labels<action_formulas::action_label_traverser, Derived>
1525{
1526};
1527//--- end generated regular_formulas::add_traverser_action_labels code ---//
1528
1529} // namespace regular_formulas
1530
1531namespace state_formulas
1532{
1533
1534/// \brief Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
1535template <typename Derived>
1536struct state_formula_traverser_base: public core::traverser<Derived>
1537{
1538 using super = core::traverser<Derived>;
1539 using super::apply;
1540 using super::enter;
1541 using super::leave;
1542
1543 void apply(const data::data_expression& x)
1544 {
1545 static_cast<Derived&>(*this).enter(x);
1546 // skip
1547 static_cast<Derived&>(*this).leave(x);
1548 }
1549
1550 void apply(const data::untyped_data_parameter& x)
1551 {
1552 static_cast<Derived&>(*this).enter(x);
1553 // skip
1554 static_cast<Derived&>(*this).leave(x);
1555 }
1556};
1557
1558//--- start generated state_formulas::add_traverser_sort_expressions code ---//
1559template <template <class> class Traverser, class Derived>
1560struct add_traverser_sort_expressions: public Traverser<Derived>
1561{
1562 using super = Traverser<Derived>;
1563 using super::enter;
1564 using super::leave;
1565 using super::apply;
1566
1567 void apply(const state_formulas::true_& x)
1568 {
1569 static_cast<Derived&>(*this).enter(x);
1570 // skip
1571 static_cast<Derived&>(*this).leave(x);
1572 }
1573
1574 void apply(const state_formulas::false_& x)
1575 {
1576 static_cast<Derived&>(*this).enter(x);
1577 // skip
1578 static_cast<Derived&>(*this).leave(x);
1579 }
1580
1581 void apply(const state_formulas::not_& x)
1582 {
1583 static_cast<Derived&>(*this).enter(x);
1584 static_cast<Derived&>(*this).apply(x.operand());
1585 static_cast<Derived&>(*this).leave(x);
1586 }
1587
1588 void apply(const state_formulas::minus& x)
1589 {
1590 static_cast<Derived&>(*this).enter(x);
1591 static_cast<Derived&>(*this).apply(x.operand());
1592 static_cast<Derived&>(*this).leave(x);
1593 }
1594
1595 void apply(const state_formulas::and_& x)
1596 {
1597 static_cast<Derived&>(*this).enter(x);
1598 static_cast<Derived&>(*this).apply(x.left());
1599 static_cast<Derived&>(*this).apply(x.right());
1600 static_cast<Derived&>(*this).leave(x);
1601 }
1602
1603 void apply(const state_formulas::or_& x)
1604 {
1605 static_cast<Derived&>(*this).enter(x);
1606 static_cast<Derived&>(*this).apply(x.left());
1607 static_cast<Derived&>(*this).apply(x.right());
1608 static_cast<Derived&>(*this).leave(x);
1609 }
1610
1611 void apply(const state_formulas::imp& x)
1612 {
1613 static_cast<Derived&>(*this).enter(x);
1614 static_cast<Derived&>(*this).apply(x.left());
1615 static_cast<Derived&>(*this).apply(x.right());
1616 static_cast<Derived&>(*this).leave(x);
1617 }
1618
1619 void apply(const state_formulas::plus& x)
1620 {
1621 static_cast<Derived&>(*this).enter(x);
1622 static_cast<Derived&>(*this).apply(x.left());
1623 static_cast<Derived&>(*this).apply(x.right());
1624 static_cast<Derived&>(*this).leave(x);
1625 }
1626
1627 void apply(const state_formulas::const_multiply& x)
1628 {
1629 static_cast<Derived&>(*this).enter(x);
1630 static_cast<Derived&>(*this).apply(x.left());
1631 static_cast<Derived&>(*this).apply(x.right());
1632 static_cast<Derived&>(*this).leave(x);
1633 }
1634
1635 void apply(const state_formulas::const_multiply_alt& x)
1636 {
1637 static_cast<Derived&>(*this).enter(x);
1638 static_cast<Derived&>(*this).apply(x.left());
1639 static_cast<Derived&>(*this).apply(x.right());
1640 static_cast<Derived&>(*this).leave(x);
1641 }
1642
1643 void apply(const state_formulas::forall& x)
1644 {
1645 static_cast<Derived&>(*this).enter(x);
1646 static_cast<Derived&>(*this).apply(x.variables());
1647 static_cast<Derived&>(*this).apply(x.body());
1648 static_cast<Derived&>(*this).leave(x);
1649 }
1650
1651 void apply(const state_formulas::exists& x)
1652 {
1653 static_cast<Derived&>(*this).enter(x);
1654 static_cast<Derived&>(*this).apply(x.variables());
1655 static_cast<Derived&>(*this).apply(x.body());
1656 static_cast<Derived&>(*this).leave(x);
1657 }
1658
1659 void apply(const state_formulas::infimum& x)
1660 {
1661 static_cast<Derived&>(*this).enter(x);
1662 static_cast<Derived&>(*this).apply(x.variables());
1663 static_cast<Derived&>(*this).apply(x.body());
1664 static_cast<Derived&>(*this).leave(x);
1665 }
1666
1667 void apply(const state_formulas::supremum& x)
1668 {
1669 static_cast<Derived&>(*this).enter(x);
1670 static_cast<Derived&>(*this).apply(x.variables());
1671 static_cast<Derived&>(*this).apply(x.body());
1672 static_cast<Derived&>(*this).leave(x);
1673 }
1674
1675 void apply(const state_formulas::sum& x)
1676 {
1677 static_cast<Derived&>(*this).enter(x);
1678 static_cast<Derived&>(*this).apply(x.variables());
1679 static_cast<Derived&>(*this).apply(x.body());
1680 static_cast<Derived&>(*this).leave(x);
1681 }
1682
1683 void apply(const state_formulas::must& x)
1684 {
1685 static_cast<Derived&>(*this).enter(x);
1686 static_cast<Derived&>(*this).apply(x.formula());
1687 static_cast<Derived&>(*this).apply(x.operand());
1688 static_cast<Derived&>(*this).leave(x);
1689 }
1690
1691 void apply(const state_formulas::may& x)
1692 {
1693 static_cast<Derived&>(*this).enter(x);
1694 static_cast<Derived&>(*this).apply(x.formula());
1695 static_cast<Derived&>(*this).apply(x.operand());
1696 static_cast<Derived&>(*this).leave(x);
1697 }
1698
1699 void apply(const state_formulas::yaled& x)
1700 {
1701 static_cast<Derived&>(*this).enter(x);
1702 // skip
1703 static_cast<Derived&>(*this).leave(x);
1704 }
1705
1706 void apply(const state_formulas::yaled_timed& x)
1707 {
1708 static_cast<Derived&>(*this).enter(x);
1709 static_cast<Derived&>(*this).apply(x.time_stamp());
1710 static_cast<Derived&>(*this).leave(x);
1711 }
1712
1713 void apply(const state_formulas::delay& x)
1714 {
1715 static_cast<Derived&>(*this).enter(x);
1716 // skip
1717 static_cast<Derived&>(*this).leave(x);
1718 }
1719
1720 void apply(const state_formulas::delay_timed& x)
1721 {
1722 static_cast<Derived&>(*this).enter(x);
1723 static_cast<Derived&>(*this).apply(x.time_stamp());
1724 static_cast<Derived&>(*this).leave(x);
1725 }
1726
1727 void apply(const state_formulas::variable& x)
1728 {
1729 static_cast<Derived&>(*this).enter(x);
1730 static_cast<Derived&>(*this).apply(x.arguments());
1731 static_cast<Derived&>(*this).leave(x);
1732 }
1733
1734 void apply(const state_formulas::nu& x)
1735 {
1736 static_cast<Derived&>(*this).enter(x);
1737 static_cast<Derived&>(*this).apply(x.assignments());
1738 static_cast<Derived&>(*this).apply(x.operand());
1739 static_cast<Derived&>(*this).leave(x);
1740 }
1741
1742 void apply(const state_formulas::mu& x)
1743 {
1744 static_cast<Derived&>(*this).enter(x);
1745 static_cast<Derived&>(*this).apply(x.assignments());
1746 static_cast<Derived&>(*this).apply(x.operand());
1747 static_cast<Derived&>(*this).leave(x);
1748 }
1749
1750 void apply(const state_formulas::state_formula_specification& x)
1751 {
1752 static_cast<Derived&>(*this).enter(x);
1753 static_cast<Derived&>(*this).apply(x.action_labels());
1754 static_cast<Derived&>(*this).apply(x.formula());
1755 static_cast<Derived&>(*this).leave(x);
1756 }
1757
1758 void apply(const state_formulas::state_formula& x)
1759 {
1760 static_cast<Derived&>(*this).enter(x);
1761 if (data::is_data_expression(x))
1762 {
1763 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
1764 }
1765 else if (data::is_untyped_data_parameter(x))
1766 {
1767 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
1768 }
1769 else if (state_formulas::is_true(x))
1770 {
1771 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
1772 }
1773 else if (state_formulas::is_false(x))
1774 {
1775 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
1776 }
1777 else if (state_formulas::is_not(x))
1778 {
1779 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
1780 }
1781 else if (state_formulas::is_minus(x))
1782 {
1783 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
1784 }
1785 else if (state_formulas::is_and(x))
1786 {
1787 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
1788 }
1789 else if (state_formulas::is_or(x))
1790 {
1791 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
1792 }
1793 else if (state_formulas::is_imp(x))
1794 {
1795 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
1796 }
1797 else if (state_formulas::is_plus(x))
1798 {
1799 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
1800 }
1801 else if (state_formulas::is_const_multiply(x))
1802 {
1803 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
1804 }
1805 else if (state_formulas::is_const_multiply_alt(x))
1806 {
1807 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
1808 }
1809 else if (state_formulas::is_forall(x))
1810 {
1811 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
1812 }
1813 else if (state_formulas::is_exists(x))
1814 {
1815 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
1816 }
1817 else if (state_formulas::is_infimum(x))
1818 {
1819 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
1820 }
1821 else if (state_formulas::is_supremum(x))
1822 {
1823 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
1824 }
1825 else if (state_formulas::is_sum(x))
1826 {
1827 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
1828 }
1829 else if (state_formulas::is_must(x))
1830 {
1831 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
1832 }
1833 else if (state_formulas::is_may(x))
1834 {
1835 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
1836 }
1837 else if (state_formulas::is_yaled(x))
1838 {
1839 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
1840 }
1841 else if (state_formulas::is_yaled_timed(x))
1842 {
1843 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
1844 }
1845 else if (state_formulas::is_delay(x))
1846 {
1847 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
1848 }
1849 else if (state_formulas::is_delay_timed(x))
1850 {
1851 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
1852 }
1853 else if (state_formulas::is_variable(x))
1854 {
1855 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
1856 }
1857 else if (state_formulas::is_nu(x))
1858 {
1859 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
1860 }
1861 else if (state_formulas::is_mu(x))
1862 {
1863 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
1864 }
1865 static_cast<Derived&>(*this).leave(x);
1866 }
1867
1868};
1869
1870/// \\brief Traverser class
1871template <typename Derived>
1872struct sort_expression_traverser: public add_traverser_sort_expressions<regular_formulas::sort_expression_traverser, Derived>
1873{
1874};
1875//--- end generated state_formulas::add_traverser_sort_expressions code ---//
1876
1877//--- start generated state_formulas::add_traverser_data_expressions code ---//
1878template <template <class> class Traverser, class Derived>
1879struct add_traverser_data_expressions: public Traverser<Derived>
1880{
1881 using super = Traverser<Derived>;
1882 using super::enter;
1883 using super::leave;
1884 using super::apply;
1885
1886 void apply(const state_formulas::true_& x)
1887 {
1888 static_cast<Derived&>(*this).enter(x);
1889 // skip
1890 static_cast<Derived&>(*this).leave(x);
1891 }
1892
1893 void apply(const state_formulas::false_& x)
1894 {
1895 static_cast<Derived&>(*this).enter(x);
1896 // skip
1897 static_cast<Derived&>(*this).leave(x);
1898 }
1899
1900 void apply(const state_formulas::not_& x)
1901 {
1902 static_cast<Derived&>(*this).enter(x);
1903 static_cast<Derived&>(*this).apply(x.operand());
1904 static_cast<Derived&>(*this).leave(x);
1905 }
1906
1907 void apply(const state_formulas::minus& x)
1908 {
1909 static_cast<Derived&>(*this).enter(x);
1910 static_cast<Derived&>(*this).apply(x.operand());
1911 static_cast<Derived&>(*this).leave(x);
1912 }
1913
1914 void apply(const state_formulas::and_& x)
1915 {
1916 static_cast<Derived&>(*this).enter(x);
1917 static_cast<Derived&>(*this).apply(x.left());
1918 static_cast<Derived&>(*this).apply(x.right());
1919 static_cast<Derived&>(*this).leave(x);
1920 }
1921
1922 void apply(const state_formulas::or_& x)
1923 {
1924 static_cast<Derived&>(*this).enter(x);
1925 static_cast<Derived&>(*this).apply(x.left());
1926 static_cast<Derived&>(*this).apply(x.right());
1927 static_cast<Derived&>(*this).leave(x);
1928 }
1929
1930 void apply(const state_formulas::imp& x)
1931 {
1932 static_cast<Derived&>(*this).enter(x);
1933 static_cast<Derived&>(*this).apply(x.left());
1934 static_cast<Derived&>(*this).apply(x.right());
1935 static_cast<Derived&>(*this).leave(x);
1936 }
1937
1938 void apply(const state_formulas::plus& x)
1939 {
1940 static_cast<Derived&>(*this).enter(x);
1941 static_cast<Derived&>(*this).apply(x.left());
1942 static_cast<Derived&>(*this).apply(x.right());
1943 static_cast<Derived&>(*this).leave(x);
1944 }
1945
1946 void apply(const state_formulas::const_multiply& x)
1947 {
1948 static_cast<Derived&>(*this).enter(x);
1949 static_cast<Derived&>(*this).apply(x.left());
1950 static_cast<Derived&>(*this).apply(x.right());
1951 static_cast<Derived&>(*this).leave(x);
1952 }
1953
1954 void apply(const state_formulas::const_multiply_alt& x)
1955 {
1956 static_cast<Derived&>(*this).enter(x);
1957 static_cast<Derived&>(*this).apply(x.left());
1958 static_cast<Derived&>(*this).apply(x.right());
1959 static_cast<Derived&>(*this).leave(x);
1960 }
1961
1962 void apply(const state_formulas::forall& x)
1963 {
1964 static_cast<Derived&>(*this).enter(x);
1965 static_cast<Derived&>(*this).apply(x.body());
1966 static_cast<Derived&>(*this).leave(x);
1967 }
1968
1969 void apply(const state_formulas::exists& x)
1970 {
1971 static_cast<Derived&>(*this).enter(x);
1972 static_cast<Derived&>(*this).apply(x.body());
1973 static_cast<Derived&>(*this).leave(x);
1974 }
1975
1976 void apply(const state_formulas::infimum& x)
1977 {
1978 static_cast<Derived&>(*this).enter(x);
1979 static_cast<Derived&>(*this).apply(x.body());
1980 static_cast<Derived&>(*this).leave(x);
1981 }
1982
1983 void apply(const state_formulas::supremum& x)
1984 {
1985 static_cast<Derived&>(*this).enter(x);
1986 static_cast<Derived&>(*this).apply(x.body());
1987 static_cast<Derived&>(*this).leave(x);
1988 }
1989
1990 void apply(const state_formulas::sum& x)
1991 {
1992 static_cast<Derived&>(*this).enter(x);
1993 static_cast<Derived&>(*this).apply(x.body());
1994 static_cast<Derived&>(*this).leave(x);
1995 }
1996
1997 void apply(const state_formulas::must& x)
1998 {
1999 static_cast<Derived&>(*this).enter(x);
2000 static_cast<Derived&>(*this).apply(x.formula());
2001 static_cast<Derived&>(*this).apply(x.operand());
2002 static_cast<Derived&>(*this).leave(x);
2003 }
2004
2005 void apply(const state_formulas::may& x)
2006 {
2007 static_cast<Derived&>(*this).enter(x);
2008 static_cast<Derived&>(*this).apply(x.formula());
2009 static_cast<Derived&>(*this).apply(x.operand());
2010 static_cast<Derived&>(*this).leave(x);
2011 }
2012
2013 void apply(const state_formulas::yaled& x)
2014 {
2015 static_cast<Derived&>(*this).enter(x);
2016 // skip
2017 static_cast<Derived&>(*this).leave(x);
2018 }
2019
2020 void apply(const state_formulas::yaled_timed& x)
2021 {
2022 static_cast<Derived&>(*this).enter(x);
2023 static_cast<Derived&>(*this).apply(x.time_stamp());
2024 static_cast<Derived&>(*this).leave(x);
2025 }
2026
2027 void apply(const state_formulas::delay& x)
2028 {
2029 static_cast<Derived&>(*this).enter(x);
2030 // skip
2031 static_cast<Derived&>(*this).leave(x);
2032 }
2033
2034 void apply(const state_formulas::delay_timed& x)
2035 {
2036 static_cast<Derived&>(*this).enter(x);
2037 static_cast<Derived&>(*this).apply(x.time_stamp());
2038 static_cast<Derived&>(*this).leave(x);
2039 }
2040
2041 void apply(const state_formulas::variable& x)
2042 {
2043 static_cast<Derived&>(*this).enter(x);
2044 static_cast<Derived&>(*this).apply(x.arguments());
2045 static_cast<Derived&>(*this).leave(x);
2046 }
2047
2048 void apply(const state_formulas::nu& x)
2049 {
2050 static_cast<Derived&>(*this).enter(x);
2051 static_cast<Derived&>(*this).apply(x.assignments());
2052 static_cast<Derived&>(*this).apply(x.operand());
2053 static_cast<Derived&>(*this).leave(x);
2054 }
2055
2056 void apply(const state_formulas::mu& x)
2057 {
2058 static_cast<Derived&>(*this).enter(x);
2059 static_cast<Derived&>(*this).apply(x.assignments());
2060 static_cast<Derived&>(*this).apply(x.operand());
2061 static_cast<Derived&>(*this).leave(x);
2062 }
2063
2064 void apply(const state_formulas::state_formula_specification& x)
2065 {
2066 static_cast<Derived&>(*this).enter(x);
2067 static_cast<Derived&>(*this).apply(x.formula());
2068 static_cast<Derived&>(*this).leave(x);
2069 }
2070
2071 void apply(const state_formulas::state_formula& x)
2072 {
2073 static_cast<Derived&>(*this).enter(x);
2074 if (data::is_data_expression(x))
2075 {
2076 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
2077 }
2078 else if (data::is_untyped_data_parameter(x))
2079 {
2080 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
2081 }
2082 else if (state_formulas::is_true(x))
2083 {
2084 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
2085 }
2086 else if (state_formulas::is_false(x))
2087 {
2088 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
2089 }
2090 else if (state_formulas::is_not(x))
2091 {
2092 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
2093 }
2094 else if (state_formulas::is_minus(x))
2095 {
2096 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
2097 }
2098 else if (state_formulas::is_and(x))
2099 {
2100 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
2101 }
2102 else if (state_formulas::is_or(x))
2103 {
2104 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
2105 }
2106 else if (state_formulas::is_imp(x))
2107 {
2108 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
2109 }
2110 else if (state_formulas::is_plus(x))
2111 {
2112 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
2113 }
2114 else if (state_formulas::is_const_multiply(x))
2115 {
2116 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
2117 }
2118 else if (state_formulas::is_const_multiply_alt(x))
2119 {
2120 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2121 }
2122 else if (state_formulas::is_forall(x))
2123 {
2124 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
2125 }
2126 else if (state_formulas::is_exists(x))
2127 {
2128 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
2129 }
2130 else if (state_formulas::is_infimum(x))
2131 {
2132 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
2133 }
2134 else if (state_formulas::is_supremum(x))
2135 {
2136 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
2137 }
2138 else if (state_formulas::is_sum(x))
2139 {
2140 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
2141 }
2142 else if (state_formulas::is_must(x))
2143 {
2144 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
2145 }
2146 else if (state_formulas::is_may(x))
2147 {
2148 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
2149 }
2150 else if (state_formulas::is_yaled(x))
2151 {
2152 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
2153 }
2154 else if (state_formulas::is_yaled_timed(x))
2155 {
2156 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
2157 }
2158 else if (state_formulas::is_delay(x))
2159 {
2160 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
2161 }
2162 else if (state_formulas::is_delay_timed(x))
2163 {
2164 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
2165 }
2166 else if (state_formulas::is_variable(x))
2167 {
2168 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
2169 }
2170 else if (state_formulas::is_nu(x))
2171 {
2172 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
2173 }
2174 else if (state_formulas::is_mu(x))
2175 {
2176 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
2177 }
2178 static_cast<Derived&>(*this).leave(x);
2179 }
2180
2181};
2182
2183/// \\brief Traverser class
2184template <typename Derived>
2185struct data_expression_traverser: public add_traverser_data_expressions<regular_formulas::data_expression_traverser, Derived>
2186{
2187};
2188//--- end generated state_formulas::add_traverser_data_expressions code ---//
2189
2190//--- start generated state_formulas::add_traverser_state_formula_expressions code ---//
2191template <template <class> class Traverser, class Derived>
2192struct add_traverser_state_formula_expressions: public Traverser<Derived>
2193{
2194 using super = Traverser<Derived>;
2195 using super::enter;
2196 using super::leave;
2197 using super::apply;
2198
2199 void apply(const state_formulas::true_& x)
2200 {
2201 static_cast<Derived&>(*this).enter(x);
2202 // skip
2203 static_cast<Derived&>(*this).leave(x);
2204 }
2205
2206 void apply(const state_formulas::false_& x)
2207 {
2208 static_cast<Derived&>(*this).enter(x);
2209 // skip
2210 static_cast<Derived&>(*this).leave(x);
2211 }
2212
2213 void apply(const state_formulas::not_& x)
2214 {
2215 static_cast<Derived&>(*this).enter(x);
2216 static_cast<Derived&>(*this).apply(x.operand());
2217 static_cast<Derived&>(*this).leave(x);
2218 }
2219
2220 void apply(const state_formulas::minus& x)
2221 {
2222 static_cast<Derived&>(*this).enter(x);
2223 static_cast<Derived&>(*this).apply(x.operand());
2224 static_cast<Derived&>(*this).leave(x);
2225 }
2226
2227 void apply(const state_formulas::and_& x)
2228 {
2229 static_cast<Derived&>(*this).enter(x);
2230 static_cast<Derived&>(*this).apply(x.left());
2231 static_cast<Derived&>(*this).apply(x.right());
2232 static_cast<Derived&>(*this).leave(x);
2233 }
2234
2235 void apply(const state_formulas::or_& x)
2236 {
2237 static_cast<Derived&>(*this).enter(x);
2238 static_cast<Derived&>(*this).apply(x.left());
2239 static_cast<Derived&>(*this).apply(x.right());
2240 static_cast<Derived&>(*this).leave(x);
2241 }
2242
2243 void apply(const state_formulas::imp& x)
2244 {
2245 static_cast<Derived&>(*this).enter(x);
2246 static_cast<Derived&>(*this).apply(x.left());
2247 static_cast<Derived&>(*this).apply(x.right());
2248 static_cast<Derived&>(*this).leave(x);
2249 }
2250
2251 void apply(const state_formulas::plus& x)
2252 {
2253 static_cast<Derived&>(*this).enter(x);
2254 static_cast<Derived&>(*this).apply(x.left());
2255 static_cast<Derived&>(*this).apply(x.right());
2256 static_cast<Derived&>(*this).leave(x);
2257 }
2258
2259 void apply(const state_formulas::const_multiply& x)
2260 {
2261 static_cast<Derived&>(*this).enter(x);
2262 static_cast<Derived&>(*this).apply(x.right());
2263 static_cast<Derived&>(*this).leave(x);
2264 }
2265
2266 void apply(const state_formulas::const_multiply_alt& x)
2267 {
2268 static_cast<Derived&>(*this).enter(x);
2269 static_cast<Derived&>(*this).apply(x.left());
2270 static_cast<Derived&>(*this).leave(x);
2271 }
2272
2273 void apply(const state_formulas::forall& x)
2274 {
2275 static_cast<Derived&>(*this).enter(x);
2276 static_cast<Derived&>(*this).apply(x.body());
2277 static_cast<Derived&>(*this).leave(x);
2278 }
2279
2280 void apply(const state_formulas::exists& x)
2281 {
2282 static_cast<Derived&>(*this).enter(x);
2283 static_cast<Derived&>(*this).apply(x.body());
2284 static_cast<Derived&>(*this).leave(x);
2285 }
2286
2287 void apply(const state_formulas::infimum& x)
2288 {
2289 static_cast<Derived&>(*this).enter(x);
2290 static_cast<Derived&>(*this).apply(x.body());
2291 static_cast<Derived&>(*this).leave(x);
2292 }
2293
2294 void apply(const state_formulas::supremum& x)
2295 {
2296 static_cast<Derived&>(*this).enter(x);
2297 static_cast<Derived&>(*this).apply(x.body());
2298 static_cast<Derived&>(*this).leave(x);
2299 }
2300
2301 void apply(const state_formulas::sum& x)
2302 {
2303 static_cast<Derived&>(*this).enter(x);
2304 static_cast<Derived&>(*this).apply(x.body());
2305 static_cast<Derived&>(*this).leave(x);
2306 }
2307
2308 void apply(const state_formulas::must& x)
2309 {
2310 static_cast<Derived&>(*this).enter(x);
2311 static_cast<Derived&>(*this).apply(x.operand());
2312 static_cast<Derived&>(*this).leave(x);
2313 }
2314
2315 void apply(const state_formulas::may& x)
2316 {
2317 static_cast<Derived&>(*this).enter(x);
2318 static_cast<Derived&>(*this).apply(x.operand());
2319 static_cast<Derived&>(*this).leave(x);
2320 }
2321
2322 void apply(const state_formulas::yaled& x)
2323 {
2324 static_cast<Derived&>(*this).enter(x);
2325 // skip
2326 static_cast<Derived&>(*this).leave(x);
2327 }
2328
2329 void apply(const state_formulas::yaled_timed& x)
2330 {
2331 static_cast<Derived&>(*this).enter(x);
2332 // skip
2333 static_cast<Derived&>(*this).leave(x);
2334 }
2335
2336 void apply(const state_formulas::delay& x)
2337 {
2338 static_cast<Derived&>(*this).enter(x);
2339 // skip
2340 static_cast<Derived&>(*this).leave(x);
2341 }
2342
2343 void apply(const state_formulas::delay_timed& x)
2344 {
2345 static_cast<Derived&>(*this).enter(x);
2346 // skip
2347 static_cast<Derived&>(*this).leave(x);
2348 }
2349
2350 void apply(const state_formulas::variable& x)
2351 {
2352 static_cast<Derived&>(*this).enter(x);
2353 // skip
2354 static_cast<Derived&>(*this).leave(x);
2355 }
2356
2357 void apply(const state_formulas::nu& x)
2358 {
2359 static_cast<Derived&>(*this).enter(x);
2360 static_cast<Derived&>(*this).apply(x.operand());
2361 static_cast<Derived&>(*this).leave(x);
2362 }
2363
2364 void apply(const state_formulas::mu& x)
2365 {
2366 static_cast<Derived&>(*this).enter(x);
2367 static_cast<Derived&>(*this).apply(x.operand());
2368 static_cast<Derived&>(*this).leave(x);
2369 }
2370
2371 void apply(const state_formulas::state_formula_specification& x)
2372 {
2373 static_cast<Derived&>(*this).enter(x);
2374 static_cast<Derived&>(*this).apply(x.formula());
2375 static_cast<Derived&>(*this).leave(x);
2376 }
2377
2378 void apply(const state_formulas::state_formula& x)
2379 {
2380 static_cast<Derived&>(*this).enter(x);
2381 if (data::is_data_expression(x))
2382 {
2383 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
2384 }
2385 else if (data::is_untyped_data_parameter(x))
2386 {
2387 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
2388 }
2389 else if (state_formulas::is_true(x))
2390 {
2391 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
2392 }
2393 else if (state_formulas::is_false(x))
2394 {
2395 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
2396 }
2397 else if (state_formulas::is_not(x))
2398 {
2399 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
2400 }
2401 else if (state_formulas::is_minus(x))
2402 {
2403 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
2404 }
2405 else if (state_formulas::is_and(x))
2406 {
2407 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
2408 }
2409 else if (state_formulas::is_or(x))
2410 {
2411 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
2412 }
2413 else if (state_formulas::is_imp(x))
2414 {
2415 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
2416 }
2417 else if (state_formulas::is_plus(x))
2418 {
2419 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
2420 }
2421 else if (state_formulas::is_const_multiply(x))
2422 {
2423 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
2424 }
2425 else if (state_formulas::is_const_multiply_alt(x))
2426 {
2427 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2428 }
2429 else if (state_formulas::is_forall(x))
2430 {
2431 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
2432 }
2433 else if (state_formulas::is_exists(x))
2434 {
2435 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
2436 }
2437 else if (state_formulas::is_infimum(x))
2438 {
2439 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
2440 }
2441 else if (state_formulas::is_supremum(x))
2442 {
2443 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
2444 }
2445 else if (state_formulas::is_sum(x))
2446 {
2447 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
2448 }
2449 else if (state_formulas::is_must(x))
2450 {
2451 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
2452 }
2453 else if (state_formulas::is_may(x))
2454 {
2455 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
2456 }
2457 else if (state_formulas::is_yaled(x))
2458 {
2459 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
2460 }
2461 else if (state_formulas::is_yaled_timed(x))
2462 {
2463 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
2464 }
2465 else if (state_formulas::is_delay(x))
2466 {
2467 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
2468 }
2469 else if (state_formulas::is_delay_timed(x))
2470 {
2471 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
2472 }
2473 else if (state_formulas::is_variable(x))
2474 {
2475 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
2476 }
2477 else if (state_formulas::is_nu(x))
2478 {
2479 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
2480 }
2481 else if (state_formulas::is_mu(x))
2482 {
2483 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
2484 }
2485 static_cast<Derived&>(*this).leave(x);
2486 }
2487
2488};
2489
2490/// \\brief Traverser class
2491template <typename Derived>
2492struct state_formula_traverser: public add_traverser_state_formula_expressions<state_formulas::state_formula_traverser_base, Derived>
2493{
2494};
2495//--- end generated state_formulas::add_traverser_state_formula_expressions code ---//
2496
2497//--- start generated state_formulas::add_traverser_variables code ---//
2498template <template <class> class Traverser, class Derived>
2499struct add_traverser_variables: public Traverser<Derived>
2500{
2501 using super = Traverser<Derived>;
2502 using super::enter;
2503 using super::leave;
2504 using super::apply;
2505
2506 void apply(const state_formulas::true_& x)
2507 {
2508 static_cast<Derived&>(*this).enter(x);
2509 // skip
2510 static_cast<Derived&>(*this).leave(x);
2511 }
2512
2513 void apply(const state_formulas::false_& x)
2514 {
2515 static_cast<Derived&>(*this).enter(x);
2516 // skip
2517 static_cast<Derived&>(*this).leave(x);
2518 }
2519
2520 void apply(const state_formulas::not_& x)
2521 {
2522 static_cast<Derived&>(*this).enter(x);
2523 static_cast<Derived&>(*this).apply(x.operand());
2524 static_cast<Derived&>(*this).leave(x);
2525 }
2526
2527 void apply(const state_formulas::minus& x)
2528 {
2529 static_cast<Derived&>(*this).enter(x);
2530 static_cast<Derived&>(*this).apply(x.operand());
2531 static_cast<Derived&>(*this).leave(x);
2532 }
2533
2534 void apply(const state_formulas::and_& x)
2535 {
2536 static_cast<Derived&>(*this).enter(x);
2537 static_cast<Derived&>(*this).apply(x.left());
2538 static_cast<Derived&>(*this).apply(x.right());
2539 static_cast<Derived&>(*this).leave(x);
2540 }
2541
2542 void apply(const state_formulas::or_& x)
2543 {
2544 static_cast<Derived&>(*this).enter(x);
2545 static_cast<Derived&>(*this).apply(x.left());
2546 static_cast<Derived&>(*this).apply(x.right());
2547 static_cast<Derived&>(*this).leave(x);
2548 }
2549
2550 void apply(const state_formulas::imp& x)
2551 {
2552 static_cast<Derived&>(*this).enter(x);
2553 static_cast<Derived&>(*this).apply(x.left());
2554 static_cast<Derived&>(*this).apply(x.right());
2555 static_cast<Derived&>(*this).leave(x);
2556 }
2557
2558 void apply(const state_formulas::plus& x)
2559 {
2560 static_cast<Derived&>(*this).enter(x);
2561 static_cast<Derived&>(*this).apply(x.left());
2562 static_cast<Derived&>(*this).apply(x.right());
2563 static_cast<Derived&>(*this).leave(x);
2564 }
2565
2566 void apply(const state_formulas::const_multiply& x)
2567 {
2568 static_cast<Derived&>(*this).enter(x);
2569 static_cast<Derived&>(*this).apply(x.left());
2570 static_cast<Derived&>(*this).apply(x.right());
2571 static_cast<Derived&>(*this).leave(x);
2572 }
2573
2574 void apply(const state_formulas::const_multiply_alt& x)
2575 {
2576 static_cast<Derived&>(*this).enter(x);
2577 static_cast<Derived&>(*this).apply(x.left());
2578 static_cast<Derived&>(*this).apply(x.right());
2579 static_cast<Derived&>(*this).leave(x);
2580 }
2581
2582 void apply(const state_formulas::forall& x)
2583 {
2584 static_cast<Derived&>(*this).enter(x);
2585 static_cast<Derived&>(*this).apply(x.variables());
2586 static_cast<Derived&>(*this).apply(x.body());
2587 static_cast<Derived&>(*this).leave(x);
2588 }
2589
2590 void apply(const state_formulas::exists& x)
2591 {
2592 static_cast<Derived&>(*this).enter(x);
2593 static_cast<Derived&>(*this).apply(x.variables());
2594 static_cast<Derived&>(*this).apply(x.body());
2595 static_cast<Derived&>(*this).leave(x);
2596 }
2597
2598 void apply(const state_formulas::infimum& x)
2599 {
2600 static_cast<Derived&>(*this).enter(x);
2601 static_cast<Derived&>(*this).apply(x.variables());
2602 static_cast<Derived&>(*this).apply(x.body());
2603 static_cast<Derived&>(*this).leave(x);
2604 }
2605
2606 void apply(const state_formulas::supremum& x)
2607 {
2608 static_cast<Derived&>(*this).enter(x);
2609 static_cast<Derived&>(*this).apply(x.variables());
2610 static_cast<Derived&>(*this).apply(x.body());
2611 static_cast<Derived&>(*this).leave(x);
2612 }
2613
2614 void apply(const state_formulas::sum& x)
2615 {
2616 static_cast<Derived&>(*this).enter(x);
2617 static_cast<Derived&>(*this).apply(x.variables());
2618 static_cast<Derived&>(*this).apply(x.body());
2619 static_cast<Derived&>(*this).leave(x);
2620 }
2621
2622 void apply(const state_formulas::must& x)
2623 {
2624 static_cast<Derived&>(*this).enter(x);
2625 static_cast<Derived&>(*this).apply(x.formula());
2626 static_cast<Derived&>(*this).apply(x.operand());
2627 static_cast<Derived&>(*this).leave(x);
2628 }
2629
2630 void apply(const state_formulas::may& x)
2631 {
2632 static_cast<Derived&>(*this).enter(x);
2633 static_cast<Derived&>(*this).apply(x.formula());
2634 static_cast<Derived&>(*this).apply(x.operand());
2635 static_cast<Derived&>(*this).leave(x);
2636 }
2637
2638 void apply(const state_formulas::yaled& x)
2639 {
2640 static_cast<Derived&>(*this).enter(x);
2641 // skip
2642 static_cast<Derived&>(*this).leave(x);
2643 }
2644
2645 void apply(const state_formulas::yaled_timed& x)
2646 {
2647 static_cast<Derived&>(*this).enter(x);
2648 static_cast<Derived&>(*this).apply(x.time_stamp());
2649 static_cast<Derived&>(*this).leave(x);
2650 }
2651
2652 void apply(const state_formulas::delay& x)
2653 {
2654 static_cast<Derived&>(*this).enter(x);
2655 // skip
2656 static_cast<Derived&>(*this).leave(x);
2657 }
2658
2659 void apply(const state_formulas::delay_timed& x)
2660 {
2661 static_cast<Derived&>(*this).enter(x);
2662 static_cast<Derived&>(*this).apply(x.time_stamp());
2663 static_cast<Derived&>(*this).leave(x);
2664 }
2665
2666 void apply(const state_formulas::variable& x)
2667 {
2668 static_cast<Derived&>(*this).enter(x);
2669 static_cast<Derived&>(*this).apply(x.arguments());
2670 static_cast<Derived&>(*this).leave(x);
2671 }
2672
2673 void apply(const state_formulas::nu& x)
2674 {
2675 static_cast<Derived&>(*this).enter(x);
2676 static_cast<Derived&>(*this).apply(x.assignments());
2677 static_cast<Derived&>(*this).apply(x.operand());
2678 static_cast<Derived&>(*this).leave(x);
2679 }
2680
2681 void apply(const state_formulas::mu& x)
2682 {
2683 static_cast<Derived&>(*this).enter(x);
2684 static_cast<Derived&>(*this).apply(x.assignments());
2685 static_cast<Derived&>(*this).apply(x.operand());
2686 static_cast<Derived&>(*this).leave(x);
2687 }
2688
2689 void apply(const state_formulas::state_formula_specification& x)
2690 {
2691 static_cast<Derived&>(*this).enter(x);
2692 static_cast<Derived&>(*this).apply(x.formula());
2693 static_cast<Derived&>(*this).leave(x);
2694 }
2695
2696 void apply(const state_formulas::state_formula& x)
2697 {
2698 static_cast<Derived&>(*this).enter(x);
2699 if (data::is_data_expression(x))
2700 {
2701 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
2702 }
2703 else if (data::is_untyped_data_parameter(x))
2704 {
2705 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
2706 }
2707 else if (state_formulas::is_true(x))
2708 {
2709 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
2710 }
2711 else if (state_formulas::is_false(x))
2712 {
2713 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
2714 }
2715 else if (state_formulas::is_not(x))
2716 {
2717 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
2718 }
2719 else if (state_formulas::is_minus(x))
2720 {
2721 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
2722 }
2723 else if (state_formulas::is_and(x))
2724 {
2725 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
2726 }
2727 else if (state_formulas::is_or(x))
2728 {
2729 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
2730 }
2731 else if (state_formulas::is_imp(x))
2732 {
2733 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
2734 }
2735 else if (state_formulas::is_plus(x))
2736 {
2737 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
2738 }
2739 else if (state_formulas::is_const_multiply(x))
2740 {
2741 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
2742 }
2743 else if (state_formulas::is_const_multiply_alt(x))
2744 {
2745 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2746 }
2747 else if (state_formulas::is_forall(x))
2748 {
2749 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
2750 }
2751 else if (state_formulas::is_exists(x))
2752 {
2753 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
2754 }
2755 else if (state_formulas::is_infimum(x))
2756 {
2757 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
2758 }
2759 else if (state_formulas::is_supremum(x))
2760 {
2761 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
2762 }
2763 else if (state_formulas::is_sum(x))
2764 {
2765 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
2766 }
2767 else if (state_formulas::is_must(x))
2768 {
2769 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
2770 }
2771 else if (state_formulas::is_may(x))
2772 {
2773 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
2774 }
2775 else if (state_formulas::is_yaled(x))
2776 {
2777 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
2778 }
2779 else if (state_formulas::is_yaled_timed(x))
2780 {
2781 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
2782 }
2783 else if (state_formulas::is_delay(x))
2784 {
2785 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
2786 }
2787 else if (state_formulas::is_delay_timed(x))
2788 {
2789 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
2790 }
2791 else if (state_formulas::is_variable(x))
2792 {
2793 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
2794 }
2795 else if (state_formulas::is_nu(x))
2796 {
2797 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
2798 }
2799 else if (state_formulas::is_mu(x))
2800 {
2801 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
2802 }
2803 static_cast<Derived&>(*this).leave(x);
2804 }
2805
2806};
2807
2808/// \\brief Traverser class
2809template <typename Derived>
2810struct variable_traverser: public add_traverser_variables<regular_formulas::variable_traverser, Derived>
2811{
2812};
2813//--- end generated state_formulas::add_traverser_variables code ---//
2814
2815//--- start generated state_formulas::add_traverser_state_variables code ---//
2816template <template <class> class Traverser, class Derived>
2817struct add_traverser_state_variables: public Traverser<Derived>
2818{
2819 using super = Traverser<Derived>;
2820 using super::enter;
2821 using super::leave;
2822 using super::apply;
2823
2824 void apply(const state_formulas::true_& x)
2825 {
2826 static_cast<Derived&>(*this).enter(x);
2827 // skip
2828 static_cast<Derived&>(*this).leave(x);
2829 }
2830
2831 void apply(const state_formulas::false_& x)
2832 {
2833 static_cast<Derived&>(*this).enter(x);
2834 // skip
2835 static_cast<Derived&>(*this).leave(x);
2836 }
2837
2838 void apply(const state_formulas::not_& x)
2839 {
2840 static_cast<Derived&>(*this).enter(x);
2841 static_cast<Derived&>(*this).apply(x.operand());
2842 static_cast<Derived&>(*this).leave(x);
2843 }
2844
2845 void apply(const state_formulas::minus& x)
2846 {
2847 static_cast<Derived&>(*this).enter(x);
2848 static_cast<Derived&>(*this).apply(x.operand());
2849 static_cast<Derived&>(*this).leave(x);
2850 }
2851
2852 void apply(const state_formulas::and_& x)
2853 {
2854 static_cast<Derived&>(*this).enter(x);
2855 static_cast<Derived&>(*this).apply(x.left());
2856 static_cast<Derived&>(*this).apply(x.right());
2857 static_cast<Derived&>(*this).leave(x);
2858 }
2859
2860 void apply(const state_formulas::or_& x)
2861 {
2862 static_cast<Derived&>(*this).enter(x);
2863 static_cast<Derived&>(*this).apply(x.left());
2864 static_cast<Derived&>(*this).apply(x.right());
2865 static_cast<Derived&>(*this).leave(x);
2866 }
2867
2868 void apply(const state_formulas::imp& x)
2869 {
2870 static_cast<Derived&>(*this).enter(x);
2871 static_cast<Derived&>(*this).apply(x.left());
2872 static_cast<Derived&>(*this).apply(x.right());
2873 static_cast<Derived&>(*this).leave(x);
2874 }
2875
2876 void apply(const state_formulas::plus& x)
2877 {
2878 static_cast<Derived&>(*this).enter(x);
2879 static_cast<Derived&>(*this).apply(x.left());
2880 static_cast<Derived&>(*this).apply(x.right());
2881 static_cast<Derived&>(*this).leave(x);
2882 }
2883
2884 void apply(const state_formulas::const_multiply& x)
2885 {
2886 static_cast<Derived&>(*this).enter(x);
2887 static_cast<Derived&>(*this).apply(x.right());
2888 static_cast<Derived&>(*this).leave(x);
2889 }
2890
2891 void apply(const state_formulas::const_multiply_alt& x)
2892 {
2893 static_cast<Derived&>(*this).enter(x);
2894 static_cast<Derived&>(*this).apply(x.left());
2895 static_cast<Derived&>(*this).leave(x);
2896 }
2897
2898 void apply(const state_formulas::forall& x)
2899 {
2900 static_cast<Derived&>(*this).enter(x);
2901 static_cast<Derived&>(*this).apply(x.body());
2902 static_cast<Derived&>(*this).leave(x);
2903 }
2904
2905 void apply(const state_formulas::exists& x)
2906 {
2907 static_cast<Derived&>(*this).enter(x);
2908 static_cast<Derived&>(*this).apply(x.body());
2909 static_cast<Derived&>(*this).leave(x);
2910 }
2911
2912 void apply(const state_formulas::infimum& x)
2913 {
2914 static_cast<Derived&>(*this).enter(x);
2915 static_cast<Derived&>(*this).apply(x.body());
2916 static_cast<Derived&>(*this).leave(x);
2917 }
2918
2919 void apply(const state_formulas::supremum& x)
2920 {
2921 static_cast<Derived&>(*this).enter(x);
2922 static_cast<Derived&>(*this).apply(x.body());
2923 static_cast<Derived&>(*this).leave(x);
2924 }
2925
2926 void apply(const state_formulas::sum& x)
2927 {
2928 static_cast<Derived&>(*this).enter(x);
2929 static_cast<Derived&>(*this).apply(x.body());
2930 static_cast<Derived&>(*this).leave(x);
2931 }
2932
2933 void apply(const state_formulas::must& x)
2934 {
2935 static_cast<Derived&>(*this).enter(x);
2936 static_cast<Derived&>(*this).apply(x.operand());
2937 static_cast<Derived&>(*this).leave(x);
2938 }
2939
2940 void apply(const state_formulas::may& x)
2941 {
2942 static_cast<Derived&>(*this).enter(x);
2943 static_cast<Derived&>(*this).apply(x.operand());
2944 static_cast<Derived&>(*this).leave(x);
2945 }
2946
2947 void apply(const state_formulas::yaled& x)
2948 {
2949 static_cast<Derived&>(*this).enter(x);
2950 // skip
2951 static_cast<Derived&>(*this).leave(x);
2952 }
2953
2954 void apply(const state_formulas::yaled_timed& x)
2955 {
2956 static_cast<Derived&>(*this).enter(x);
2957 // skip
2958 static_cast<Derived&>(*this).leave(x);
2959 }
2960
2961 void apply(const state_formulas::delay& x)
2962 {
2963 static_cast<Derived&>(*this).enter(x);
2964 // skip
2965 static_cast<Derived&>(*this).leave(x);
2966 }
2967
2968 void apply(const state_formulas::delay_timed& x)
2969 {
2970 static_cast<Derived&>(*this).enter(x);
2971 // skip
2972 static_cast<Derived&>(*this).leave(x);
2973 }
2974
2975 void apply(const state_formulas::variable& x)
2976 {
2977 static_cast<Derived&>(*this).enter(x);
2978 // skip
2979 static_cast<Derived&>(*this).leave(x);
2980 }
2981
2982 void apply(const state_formulas::nu& x)
2983 {
2984 static_cast<Derived&>(*this).enter(x);
2985 static_cast<Derived&>(*this).apply(x.operand());
2986 static_cast<Derived&>(*this).leave(x);
2987 }
2988
2989 void apply(const state_formulas::mu& x)
2990 {
2991 static_cast<Derived&>(*this).enter(x);
2992 static_cast<Derived&>(*this).apply(x.operand());
2993 static_cast<Derived&>(*this).leave(x);
2994 }
2995
2996 void apply(const state_formulas::state_formula_specification& x)
2997 {
2998 static_cast<Derived&>(*this).enter(x);
2999 static_cast<Derived&>(*this).apply(x.formula());
3000 static_cast<Derived&>(*this).leave(x);
3001 }
3002
3003 void apply(const state_formulas::state_formula& x)
3004 {
3005 static_cast<Derived&>(*this).enter(x);
3006 if (data::is_data_expression(x))
3007 {
3008 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
3009 }
3010 else if (data::is_untyped_data_parameter(x))
3011 {
3012 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
3013 }
3014 else if (state_formulas::is_true(x))
3015 {
3016 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
3017 }
3018 else if (state_formulas::is_false(x))
3019 {
3020 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
3021 }
3022 else if (state_formulas::is_not(x))
3023 {
3024 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
3025 }
3026 else if (state_formulas::is_minus(x))
3027 {
3028 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
3029 }
3030 else if (state_formulas::is_and(x))
3031 {
3032 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
3033 }
3034 else if (state_formulas::is_or(x))
3035 {
3036 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
3037 }
3038 else if (state_formulas::is_imp(x))
3039 {
3040 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
3041 }
3042 else if (state_formulas::is_plus(x))
3043 {
3044 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
3045 }
3046 else if (state_formulas::is_const_multiply(x))
3047 {
3048 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
3049 }
3050 else if (state_formulas::is_const_multiply_alt(x))
3051 {
3052 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
3053 }
3054 else if (state_formulas::is_forall(x))
3055 {
3056 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
3057 }
3058 else if (state_formulas::is_exists(x))
3059 {
3060 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
3061 }
3062 else if (state_formulas::is_infimum(x))
3063 {
3064 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
3065 }
3066 else if (state_formulas::is_supremum(x))
3067 {
3068 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
3069 }
3070 else if (state_formulas::is_sum(x))
3071 {
3072 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
3073 }
3074 else if (state_formulas::is_must(x))
3075 {
3076 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
3077 }
3078 else if (state_formulas::is_may(x))
3079 {
3080 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
3081 }
3082 else if (state_formulas::is_yaled(x))
3083 {
3084 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
3085 }
3086 else if (state_formulas::is_yaled_timed(x))
3087 {
3088 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
3089 }
3090 else if (state_formulas::is_delay(x))
3091 {
3092 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
3093 }
3094 else if (state_formulas::is_delay_timed(x))
3095 {
3096 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
3097 }
3098 else if (state_formulas::is_variable(x))
3099 {
3100 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
3101 }
3102 else if (state_formulas::is_nu(x))
3103 {
3104 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
3105 }
3106 else if (state_formulas::is_mu(x))
3107 {
3108 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
3109 }
3110 static_cast<Derived&>(*this).leave(x);
3111 }
3112
3113};
3114
3115/// \\brief Traverser class
3116template <typename Derived>
3117struct state_variable_traverser: public add_traverser_state_variables<state_formulas::state_formula_traverser_base, Derived>
3118{
3119};
3120//--- end generated state_formulas::add_traverser_state_variables code ---//
3121
3122//--- start generated state_formulas::add_traverser_identifier_strings code ---//
3123template <template <class> class Traverser, class Derived>
3124struct add_traverser_identifier_strings: public Traverser<Derived>
3125{
3126 using super = Traverser<Derived>;
3127 using super::enter;
3128 using super::leave;
3129 using super::apply;
3130
3131 void apply(const state_formulas::true_& x)
3132 {
3133 static_cast<Derived&>(*this).enter(x);
3134 // skip
3135 static_cast<Derived&>(*this).leave(x);
3136 }
3137
3138 void apply(const state_formulas::false_& x)
3139 {
3140 static_cast<Derived&>(*this).enter(x);
3141 // skip
3142 static_cast<Derived&>(*this).leave(x);
3143 }
3144
3145 void apply(const state_formulas::not_& x)
3146 {
3147 static_cast<Derived&>(*this).enter(x);
3148 static_cast<Derived&>(*this).apply(x.operand());
3149 static_cast<Derived&>(*this).leave(x);
3150 }
3151
3152 void apply(const state_formulas::minus& x)
3153 {
3154 static_cast<Derived&>(*this).enter(x);
3155 static_cast<Derived&>(*this).apply(x.operand());
3156 static_cast<Derived&>(*this).leave(x);
3157 }
3158
3159 void apply(const state_formulas::and_& x)
3160 {
3161 static_cast<Derived&>(*this).enter(x);
3162 static_cast<Derived&>(*this).apply(x.left());
3163 static_cast<Derived&>(*this).apply(x.right());
3164 static_cast<Derived&>(*this).leave(x);
3165 }
3166
3167 void apply(const state_formulas::or_& x)
3168 {
3169 static_cast<Derived&>(*this).enter(x);
3170 static_cast<Derived&>(*this).apply(x.left());
3171 static_cast<Derived&>(*this).apply(x.right());
3172 static_cast<Derived&>(*this).leave(x);
3173 }
3174
3175 void apply(const state_formulas::imp& x)
3176 {
3177 static_cast<Derived&>(*this).enter(x);
3178 static_cast<Derived&>(*this).apply(x.left());
3179 static_cast<Derived&>(*this).apply(x.right());
3180 static_cast<Derived&>(*this).leave(x);
3181 }
3182
3183 void apply(const state_formulas::plus& x)
3184 {
3185 static_cast<Derived&>(*this).enter(x);
3186 static_cast<Derived&>(*this).apply(x.left());
3187 static_cast<Derived&>(*this).apply(x.right());
3188 static_cast<Derived&>(*this).leave(x);
3189 }
3190
3191 void apply(const state_formulas::const_multiply& x)
3192 {
3193 static_cast<Derived&>(*this).enter(x);
3194 static_cast<Derived&>(*this).apply(x.left());
3195 static_cast<Derived&>(*this).apply(x.right());
3196 static_cast<Derived&>(*this).leave(x);
3197 }
3198
3199 void apply(const state_formulas::const_multiply_alt& x)
3200 {
3201 static_cast<Derived&>(*this).enter(x);
3202 static_cast<Derived&>(*this).apply(x.left());
3203 static_cast<Derived&>(*this).apply(x.right());
3204 static_cast<Derived&>(*this).leave(x);
3205 }
3206
3207 void apply(const state_formulas::forall& x)
3208 {
3209 static_cast<Derived&>(*this).enter(x);
3210 static_cast<Derived&>(*this).apply(x.variables());
3211 static_cast<Derived&>(*this).apply(x.body());
3212 static_cast<Derived&>(*this).leave(x);
3213 }
3214
3215 void apply(const state_formulas::exists& x)
3216 {
3217 static_cast<Derived&>(*this).enter(x);
3218 static_cast<Derived&>(*this).apply(x.variables());
3219 static_cast<Derived&>(*this).apply(x.body());
3220 static_cast<Derived&>(*this).leave(x);
3221 }
3222
3223 void apply(const state_formulas::infimum& x)
3224 {
3225 static_cast<Derived&>(*this).enter(x);
3226 static_cast<Derived&>(*this).apply(x.variables());
3227 static_cast<Derived&>(*this).apply(x.body());
3228 static_cast<Derived&>(*this).leave(x);
3229 }
3230
3231 void apply(const state_formulas::supremum& x)
3232 {
3233 static_cast<Derived&>(*this).enter(x);
3234 static_cast<Derived&>(*this).apply(x.variables());
3235 static_cast<Derived&>(*this).apply(x.body());
3236 static_cast<Derived&>(*this).leave(x);
3237 }
3238
3239 void apply(const state_formulas::sum& x)
3240 {
3241 static_cast<Derived&>(*this).enter(x);
3242 static_cast<Derived&>(*this).apply(x.variables());
3243 static_cast<Derived&>(*this).apply(x.body());
3244 static_cast<Derived&>(*this).leave(x);
3245 }
3246
3247 void apply(const state_formulas::must& x)
3248 {
3249 static_cast<Derived&>(*this).enter(x);
3250 static_cast<Derived&>(*this).apply(x.formula());
3251 static_cast<Derived&>(*this).apply(x.operand());
3252 static_cast<Derived&>(*this).leave(x);
3253 }
3254
3255 void apply(const state_formulas::may& x)
3256 {
3257 static_cast<Derived&>(*this).enter(x);
3258 static_cast<Derived&>(*this).apply(x.formula());
3259 static_cast<Derived&>(*this).apply(x.operand());
3260 static_cast<Derived&>(*this).leave(x);
3261 }
3262
3263 void apply(const state_formulas::yaled& x)
3264 {
3265 static_cast<Derived&>(*this).enter(x);
3266 // skip
3267 static_cast<Derived&>(*this).leave(x);
3268 }
3269
3270 void apply(const state_formulas::yaled_timed& x)
3271 {
3272 static_cast<Derived&>(*this).enter(x);
3273 static_cast<Derived&>(*this).apply(x.time_stamp());
3274 static_cast<Derived&>(*this).leave(x);
3275 }
3276
3277 void apply(const state_formulas::delay& x)
3278 {
3279 static_cast<Derived&>(*this).enter(x);
3280 // skip
3281 static_cast<Derived&>(*this).leave(x);
3282 }
3283
3284 void apply(const state_formulas::delay_timed& x)
3285 {
3286 static_cast<Derived&>(*this).enter(x);
3287 static_cast<Derived&>(*this).apply(x.time_stamp());
3288 static_cast<Derived&>(*this).leave(x);
3289 }
3290
3291 void apply(const state_formulas::variable& x)
3292 {
3293 static_cast<Derived&>(*this).enter(x);
3294 static_cast<Derived&>(*this).apply(x.name());
3295 static_cast<Derived&>(*this).apply(x.arguments());
3296 static_cast<Derived&>(*this).leave(x);
3297 }
3298
3299 void apply(const state_formulas::nu& x)
3300 {
3301 static_cast<Derived&>(*this).enter(x);
3302 static_cast<Derived&>(*this).apply(x.name());
3303 static_cast<Derived&>(*this).apply(x.assignments());
3304 static_cast<Derived&>(*this).apply(x.operand());
3305 static_cast<Derived&>(*this).leave(x);
3306 }
3307
3308 void apply(const state_formulas::mu& x)
3309 {
3310 static_cast<Derived&>(*this).enter(x);
3311 static_cast<Derived&>(*this).apply(x.name());
3312 static_cast<Derived&>(*this).apply(x.assignments());
3313 static_cast<Derived&>(*this).apply(x.operand());
3314 static_cast<Derived&>(*this).leave(x);
3315 }
3316
3317 void apply(const state_formulas::state_formula_specification& x)
3318 {
3319 static_cast<Derived&>(*this).enter(x);
3320 static_cast<Derived&>(*this).apply(x.action_labels());
3321 static_cast<Derived&>(*this).apply(x.formula());
3322 static_cast<Derived&>(*this).leave(x);
3323 }
3324
3325 void apply(const state_formulas::state_formula& x)
3326 {
3327 static_cast<Derived&>(*this).enter(x);
3328 if (data::is_data_expression(x))
3329 {
3330 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
3331 }
3332 else if (data::is_untyped_data_parameter(x))
3333 {
3334 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
3335 }
3336 else if (state_formulas::is_true(x))
3337 {
3338 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
3339 }
3340 else if (state_formulas::is_false(x))
3341 {
3342 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
3343 }
3344 else if (state_formulas::is_not(x))
3345 {
3346 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
3347 }
3348 else if (state_formulas::is_minus(x))
3349 {
3350 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
3351 }
3352 else if (state_formulas::is_and(x))
3353 {
3354 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
3355 }
3356 else if (state_formulas::is_or(x))
3357 {
3358 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
3359 }
3360 else if (state_formulas::is_imp(x))
3361 {
3362 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
3363 }
3364 else if (state_formulas::is_plus(x))
3365 {
3366 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
3367 }
3368 else if (state_formulas::is_const_multiply(x))
3369 {
3370 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
3371 }
3372 else if (state_formulas::is_const_multiply_alt(x))
3373 {
3374 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
3375 }
3376 else if (state_formulas::is_forall(x))
3377 {
3378 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
3379 }
3380 else if (state_formulas::is_exists(x))
3381 {
3382 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
3383 }
3384 else if (state_formulas::is_infimum(x))
3385 {
3386 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
3387 }
3388 else if (state_formulas::is_supremum(x))
3389 {
3390 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
3391 }
3392 else if (state_formulas::is_sum(x))
3393 {
3394 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
3395 }
3396 else if (state_formulas::is_must(x))
3397 {
3398 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
3399 }
3400 else if (state_formulas::is_may(x))
3401 {
3402 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
3403 }
3404 else if (state_formulas::is_yaled(x))
3405 {
3406 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
3407 }
3408 else if (state_formulas::is_yaled_timed(x))
3409 {
3410 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
3411 }
3412 else if (state_formulas::is_delay(x))
3413 {
3414 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
3415 }
3416 else if (state_formulas::is_delay_timed(x))
3417 {
3418 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
3419 }
3420 else if (state_formulas::is_variable(x))
3421 {
3422 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
3423 }
3424 else if (state_formulas::is_nu(x))
3425 {
3426 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
3427 }
3428 else if (state_formulas::is_mu(x))
3429 {
3430 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
3431 }
3432 static_cast<Derived&>(*this).leave(x);
3433 }
3434
3435};
3436
3437/// \\brief Traverser class
3438template <typename Derived>
3439struct identifier_string_traverser: public add_traverser_identifier_strings<regular_formulas::identifier_string_traverser, Derived>
3440{
3441};
3442//--- end generated state_formulas::add_traverser_identifier_strings code ---//
3443
3444//--- start generated state_formulas::add_traverser_regular_formula_expressions code ---//
3445template <template <class> class Traverser, class Derived>
3446struct add_traverser_regular_formula_expressions: public Traverser<Derived>
3447{
3448 using super = Traverser<Derived>;
3449 using super::enter;
3450 using super::leave;
3451 using super::apply;
3452
3453 void apply(const state_formulas::true_& x)
3454 {
3455 static_cast<Derived&>(*this).enter(x);
3456 // skip
3457 static_cast<Derived&>(*this).leave(x);
3458 }
3459
3460 void apply(const state_formulas::false_& x)
3461 {
3462 static_cast<Derived&>(*this).enter(x);
3463 // skip
3464 static_cast<Derived&>(*this).leave(x);
3465 }
3466
3467 void apply(const state_formulas::not_& x)
3468 {
3469 static_cast<Derived&>(*this).enter(x);
3470 static_cast<Derived&>(*this).apply(x.operand());
3471 static_cast<Derived&>(*this).leave(x);
3472 }
3473
3474 void apply(const state_formulas::minus& x)
3475 {
3476 static_cast<Derived&>(*this).enter(x);
3477 static_cast<Derived&>(*this).apply(x.operand());
3478 static_cast<Derived&>(*this).leave(x);
3479 }
3480
3481 void apply(const state_formulas::and_& x)
3482 {
3483 static_cast<Derived&>(*this).enter(x);
3484 static_cast<Derived&>(*this).apply(x.left());
3485 static_cast<Derived&>(*this).apply(x.right());
3486 static_cast<Derived&>(*this).leave(x);
3487 }
3488
3489 void apply(const state_formulas::or_& x)
3490 {
3491 static_cast<Derived&>(*this).enter(x);
3492 static_cast<Derived&>(*this).apply(x.left());
3493 static_cast<Derived&>(*this).apply(x.right());
3494 static_cast<Derived&>(*this).leave(x);
3495 }
3496
3497 void apply(const state_formulas::imp& x)
3498 {
3499 static_cast<Derived&>(*this).enter(x);
3500 static_cast<Derived&>(*this).apply(x.left());
3501 static_cast<Derived&>(*this).apply(x.right());
3502 static_cast<Derived&>(*this).leave(x);
3503 }
3504
3505 void apply(const state_formulas::plus& x)
3506 {
3507 static_cast<Derived&>(*this).enter(x);
3508 static_cast<Derived&>(*this).apply(x.left());
3509 static_cast<Derived&>(*this).apply(x.right());
3510 static_cast<Derived&>(*this).leave(x);
3511 }
3512
3513 void apply(const state_formulas::const_multiply& x)
3514 {
3515 static_cast<Derived&>(*this).enter(x);
3516 static_cast<Derived&>(*this).apply(x.right());
3517 static_cast<Derived&>(*this).leave(x);
3518 }
3519
3520 void apply(const state_formulas::const_multiply_alt& x)
3521 {
3522 static_cast<Derived&>(*this).enter(x);
3523 static_cast<Derived&>(*this).apply(x.left());
3524 static_cast<Derived&>(*this).leave(x);
3525 }
3526
3527 void apply(const state_formulas::forall& x)
3528 {
3529 static_cast<Derived&>(*this).enter(x);
3530 static_cast<Derived&>(*this).apply(x.body());
3531 static_cast<Derived&>(*this).leave(x);
3532 }
3533
3534 void apply(const state_formulas::exists& x)
3535 {
3536 static_cast<Derived&>(*this).enter(x);
3537 static_cast<Derived&>(*this).apply(x.body());
3538 static_cast<Derived&>(*this).leave(x);
3539 }
3540
3541 void apply(const state_formulas::infimum& x)
3542 {
3543 static_cast<Derived&>(*this).enter(x);
3544 static_cast<Derived&>(*this).apply(x.body());
3545 static_cast<Derived&>(*this).leave(x);
3546 }
3547
3548 void apply(const state_formulas::supremum& x)
3549 {
3550 static_cast<Derived&>(*this).enter(x);
3551 static_cast<Derived&>(*this).apply(x.body());
3552 static_cast<Derived&>(*this).leave(x);
3553 }
3554
3555 void apply(const state_formulas::sum& x)
3556 {
3557 static_cast<Derived&>(*this).enter(x);
3558 static_cast<Derived&>(*this).apply(x.body());
3559 static_cast<Derived&>(*this).leave(x);
3560 }
3561
3562 void apply(const state_formulas::must& x)
3563 {
3564 static_cast<Derived&>(*this).enter(x);
3565 static_cast<Derived&>(*this).apply(x.formula());
3566 static_cast<Derived&>(*this).apply(x.operand());
3567 static_cast<Derived&>(*this).leave(x);
3568 }
3569
3570 void apply(const state_formulas::may& x)
3571 {
3572 static_cast<Derived&>(*this).enter(x);
3573 static_cast<Derived&>(*this).apply(x.formula());
3574 static_cast<Derived&>(*this).apply(x.operand());
3575 static_cast<Derived&>(*this).leave(x);
3576 }
3577
3578 void apply(const state_formulas::yaled& x)
3579 {
3580 static_cast<Derived&>(*this).enter(x);
3581 // skip
3582 static_cast<Derived&>(*this).leave(x);
3583 }
3584
3585 void apply(const state_formulas::yaled_timed& x)
3586 {
3587 static_cast<Derived&>(*this).enter(x);
3588 // skip
3589 static_cast<Derived&>(*this).leave(x);
3590 }
3591
3592 void apply(const state_formulas::delay& x)
3593 {
3594 static_cast<Derived&>(*this).enter(x);
3595 // skip
3596 static_cast<Derived&>(*this).leave(x);
3597 }
3598
3599 void apply(const state_formulas::delay_timed& x)
3600 {
3601 static_cast<Derived&>(*this).enter(x);
3602 // skip
3603 static_cast<Derived&>(*this).leave(x);
3604 }
3605
3606 void apply(const state_formulas::variable& x)
3607 {
3608 static_cast<Derived&>(*this).enter(x);
3609 // skip
3610 static_cast<Derived&>(*this).leave(x);
3611 }
3612
3613 void apply(const state_formulas::nu& x)
3614 {
3615 static_cast<Derived&>(*this).enter(x);
3616 static_cast<Derived&>(*this).apply(x.operand());
3617 static_cast<Derived&>(*this).leave(x);
3618 }
3619
3620 void apply(const state_formulas::mu& x)
3621 {
3622 static_cast<Derived&>(*this).enter(x);
3623 static_cast<Derived&>(*this).apply(x.operand());
3624 static_cast<Derived&>(*this).leave(x);
3625 }
3626
3627 void apply(const state_formulas::state_formula_specification& x)
3628 {
3629 static_cast<Derived&>(*this).enter(x);
3630 static_cast<Derived&>(*this).apply(x.formula());
3631 static_cast<Derived&>(*this).leave(x);
3632 }
3633
3634 void apply(const state_formulas::state_formula& x)
3635 {
3636 static_cast<Derived&>(*this).enter(x);
3637 if (data::is_data_expression(x))
3638 {
3639 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
3640 }
3641 else if (data::is_untyped_data_parameter(x))
3642 {
3643 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
3644 }
3645 else if (state_formulas::is_true(x))
3646 {
3647 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
3648 }
3649 else if (state_formulas::is_false(x))
3650 {
3651 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
3652 }
3653 else if (state_formulas::is_not(x))
3654 {
3655 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
3656 }
3657 else if (state_formulas::is_minus(x))
3658 {
3659 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
3660 }
3661 else if (state_formulas::is_and(x))
3662 {
3663 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
3664 }
3665 else if (state_formulas::is_or(x))
3666 {
3667 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
3668 }
3669 else if (state_formulas::is_imp(x))
3670 {
3671 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
3672 }
3673 else if (state_formulas::is_plus(x))
3674 {
3675 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
3676 }
3677 else if (state_formulas::is_const_multiply(x))
3678 {
3679 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
3680 }
3681 else if (state_formulas::is_const_multiply_alt(x))
3682 {
3683 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
3684 }
3685 else if (state_formulas::is_forall(x))
3686 {
3687 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
3688 }
3689 else if (state_formulas::is_exists(x))
3690 {
3691 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
3692 }
3693 else if (state_formulas::is_infimum(x))
3694 {
3695 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
3696 }
3697 else if (state_formulas::is_supremum(x))
3698 {
3699 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
3700 }
3701 else if (state_formulas::is_sum(x))
3702 {
3703 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
3704 }
3705 else if (state_formulas::is_must(x))
3706 {
3707 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
3708 }
3709 else if (state_formulas::is_may(x))
3710 {
3711 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
3712 }
3713 else if (state_formulas::is_yaled(x))
3714 {
3715 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
3716 }
3717 else if (state_formulas::is_yaled_timed(x))
3718 {
3719 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
3720 }
3721 else if (state_formulas::is_delay(x))
3722 {
3723 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
3724 }
3725 else if (state_formulas::is_delay_timed(x))
3726 {
3727 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
3728 }
3729 else if (state_formulas::is_variable(x))
3730 {
3731 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
3732 }
3733 else if (state_formulas::is_nu(x))
3734 {
3735 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
3736 }
3737 else if (state_formulas::is_mu(x))
3738 {
3739 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
3740 }
3741 static_cast<Derived&>(*this).leave(x);
3742 }
3743
3744};
3745
3746/// \\brief Traverser class
3747template <typename Derived>
3748struct regular_formula_traverser: public add_traverser_regular_formula_expressions<regular_formulas::regular_formula_traverser, Derived>
3749{
3750};
3751//--- end generated state_formulas::add_traverser_regular_formula_expressions code ---//
3752
3753//--- start generated state_formulas::add_traverser_action_labels code ---//
3754template <template <class> class Traverser, class Derived>
3755struct add_traverser_action_labels: public Traverser<Derived>
3756{
3757 using super = Traverser<Derived>;
3758 using super::enter;
3759 using super::leave;
3760 using super::apply;
3761
3762 void apply(const state_formulas::true_& x)
3763 {
3764 static_cast<Derived&>(*this).enter(x);
3765 // skip
3766 static_cast<Derived&>(*this).leave(x);
3767 }
3768
3769 void apply(const state_formulas::false_& x)
3770 {
3771 static_cast<Derived&>(*this).enter(x);
3772 // skip
3773 static_cast<Derived&>(*this).leave(x);
3774 }
3775
3776 void apply(const state_formulas::not_& x)
3777 {
3778 static_cast<Derived&>(*this).enter(x);
3779 static_cast<Derived&>(*this).apply(x.operand());
3780 static_cast<Derived&>(*this).leave(x);
3781 }
3782
3783 void apply(const state_formulas::minus& x)
3784 {
3785 static_cast<Derived&>(*this).enter(x);
3786 static_cast<Derived&>(*this).apply(x.operand());
3787 static_cast<Derived&>(*this).leave(x);
3788 }
3789
3790 void apply(const state_formulas::and_& x)
3791 {
3792 static_cast<Derived&>(*this).enter(x);
3793 static_cast<Derived&>(*this).apply(x.left());
3794 static_cast<Derived&>(*this).apply(x.right());
3795 static_cast<Derived&>(*this).leave(x);
3796 }
3797
3798 void apply(const state_formulas::or_& x)
3799 {
3800 static_cast<Derived&>(*this).enter(x);
3801 static_cast<Derived&>(*this).apply(x.left());
3802 static_cast<Derived&>(*this).apply(x.right());
3803 static_cast<Derived&>(*this).leave(x);
3804 }
3805
3806 void apply(const state_formulas::imp& x)
3807 {
3808 static_cast<Derived&>(*this).enter(x);
3809 static_cast<Derived&>(*this).apply(x.left());
3810 static_cast<Derived&>(*this).apply(x.right());
3811 static_cast<Derived&>(*this).leave(x);
3812 }
3813
3814 void apply(const state_formulas::plus& x)
3815 {
3816 static_cast<Derived&>(*this).enter(x);
3817 static_cast<Derived&>(*this).apply(x.left());
3818 static_cast<Derived&>(*this).apply(x.right());
3819 static_cast<Derived&>(*this).leave(x);
3820 }
3821
3822 void apply(const state_formulas::const_multiply& x)
3823 {
3824 static_cast<Derived&>(*this).enter(x);
3825 static_cast<Derived&>(*this).apply(x.right());
3826 static_cast<Derived&>(*this).leave(x);
3827 }
3828
3829 void apply(const state_formulas::const_multiply_alt& x)
3830 {
3831 static_cast<Derived&>(*this).enter(x);
3832 static_cast<Derived&>(*this).apply(x.left());
3833 static_cast<Derived&>(*this).leave(x);
3834 }
3835
3836 void apply(const state_formulas::forall& x)
3837 {
3838 static_cast<Derived&>(*this).enter(x);
3839 static_cast<Derived&>(*this).apply(x.body());
3840 static_cast<Derived&>(*this).leave(x);
3841 }
3842
3843 void apply(const state_formulas::exists& x)
3844 {
3845 static_cast<Derived&>(*this).enter(x);
3846 static_cast<Derived&>(*this).apply(x.body());
3847 static_cast<Derived&>(*this).leave(x);
3848 }
3849
3850 void apply(const state_formulas::infimum& x)
3851 {
3852 static_cast<Derived&>(*this).enter(x);
3853 static_cast<Derived&>(*this).apply(x.body());
3854 static_cast<Derived&>(*this).leave(x);
3855 }
3856
3857 void apply(const state_formulas::supremum& x)
3858 {
3859 static_cast<Derived&>(*this).enter(x);
3860 static_cast<Derived&>(*this).apply(x.body());
3861 static_cast<Derived&>(*this).leave(x);
3862 }
3863
3864 void apply(const state_formulas::sum& x)
3865 {
3866 static_cast<Derived&>(*this).enter(x);
3867 static_cast<Derived&>(*this).apply(x.body());
3868 static_cast<Derived&>(*this).leave(x);
3869 }
3870
3871 void apply(const state_formulas::must& x)
3872 {
3873 static_cast<Derived&>(*this).enter(x);
3874 static_cast<Derived&>(*this).apply(x.formula());
3875 static_cast<Derived&>(*this).apply(x.operand());
3876 static_cast<Derived&>(*this).leave(x);
3877 }
3878
3879 void apply(const state_formulas::may& x)
3880 {
3881 static_cast<Derived&>(*this).enter(x);
3882 static_cast<Derived&>(*this).apply(x.formula());
3883 static_cast<Derived&>(*this).apply(x.operand());
3884 static_cast<Derived&>(*this).leave(x);
3885 }
3886
3887 void apply(const state_formulas::yaled& x)
3888 {
3889 static_cast<Derived&>(*this).enter(x);
3890 // skip
3891 static_cast<Derived&>(*this).leave(x);
3892 }
3893
3894 void apply(const state_formulas::yaled_timed& x)
3895 {
3896 static_cast<Derived&>(*this).enter(x);
3897 // skip
3898 static_cast<Derived&>(*this).leave(x);
3899 }
3900
3901 void apply(const state_formulas::delay& x)
3902 {
3903 static_cast<Derived&>(*this).enter(x);
3904 // skip
3905 static_cast<Derived&>(*this).leave(x);
3906 }
3907
3908 void apply(const state_formulas::delay_timed& x)
3909 {
3910 static_cast<Derived&>(*this).enter(x);
3911 // skip
3912 static_cast<Derived&>(*this).leave(x);
3913 }
3914
3915 void apply(const state_formulas::variable& x)
3916 {
3917 static_cast<Derived&>(*this).enter(x);
3918 // skip
3919 static_cast<Derived&>(*this).leave(x);
3920 }
3921
3922 void apply(const state_formulas::nu& x)
3923 {
3924 static_cast<Derived&>(*this).enter(x);
3925 static_cast<Derived&>(*this).apply(x.operand());
3926 static_cast<Derived&>(*this).leave(x);
3927 }
3928
3929 void apply(const state_formulas::mu& x)
3930 {
3931 static_cast<Derived&>(*this).enter(x);
3932 static_cast<Derived&>(*this).apply(x.operand());
3933 static_cast<Derived&>(*this).leave(x);
3934 }
3935
3936 void apply(const state_formulas::state_formula_specification& x)
3937 {
3938 static_cast<Derived&>(*this).enter(x);
3939 static_cast<Derived&>(*this).apply(x.action_labels());
3940 static_cast<Derived&>(*this).apply(x.formula());
3941 static_cast<Derived&>(*this).leave(x);
3942 }
3943
3944 void apply(const state_formulas::state_formula& x)
3945 {
3946 static_cast<Derived&>(*this).enter(x);
3947 if (data::is_data_expression(x))
3948 {
3949 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
3950 }
3951 else if (data::is_untyped_data_parameter(x))
3952 {
3953 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
3954 }
3955 else if (state_formulas::is_true(x))
3956 {
3957 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::true_>(x));
3958 }
3959 else if (state_formulas::is_false(x))
3960 {
3961 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::false_>(x));
3962 }
3963 else if (state_formulas::is_not(x))
3964 {
3965 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::not_>(x));
3966 }
3967 else if (state_formulas::is_minus(x))
3968 {
3969 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::minus>(x));
3970 }
3971 else if (state_formulas::is_and(x))
3972 {
3973 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::and_>(x));
3974 }
3975 else if (state_formulas::is_or(x))
3976 {
3977 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::or_>(x));
3978 }
3979 else if (state_formulas::is_imp(x))
3980 {
3981 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::imp>(x));
3982 }
3983 else if (state_formulas::is_plus(x))
3984 {
3985 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::plus>(x));
3986 }
3987 else if (state_formulas::is_const_multiply(x))
3988 {
3989 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply>(x));
3990 }
3991 else if (state_formulas::is_const_multiply_alt(x))
3992 {
3993 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::const_multiply_alt>(x));
3994 }
3995 else if (state_formulas::is_forall(x))
3996 {
3997 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::forall>(x));
3998 }
3999 else if (state_formulas::is_exists(x))
4000 {
4001 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::exists>(x));
4002 }
4003 else if (state_formulas::is_infimum(x))
4004 {
4005 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::infimum>(x));
4006 }
4007 else if (state_formulas::is_supremum(x))
4008 {
4009 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::supremum>(x));
4010 }
4011 else if (state_formulas::is_sum(x))
4012 {
4013 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::sum>(x));
4014 }
4015 else if (state_formulas::is_must(x))
4016 {
4017 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::must>(x));
4018 }
4019 else if (state_formulas::is_may(x))
4020 {
4021 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::may>(x));
4022 }
4023 else if (state_formulas::is_yaled(x))
4024 {
4025 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled>(x));
4026 }
4027 else if (state_formulas::is_yaled_timed(x))
4028 {
4029 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::yaled_timed>(x));
4030 }
4031 else if (state_formulas::is_delay(x))
4032 {
4033 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay>(x));
4034 }
4035 else if (state_formulas::is_delay_timed(x))
4036 {
4037 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::delay_timed>(x));
4038 }
4039 else if (state_formulas::is_variable(x))
4040 {
4041 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::variable>(x));
4042 }
4043 else if (state_formulas::is_nu(x))
4044 {
4045 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::nu>(x));
4046 }
4047 else if (state_formulas::is_mu(x))
4048 {
4049 static_cast<Derived&>(*this).apply(atermpp::down_cast<state_formulas::mu>(x));
4050 }
4051 static_cast<Derived&>(*this).leave(x);
4052 }
4053
4054};
4055
4056/// \\brief Traverser class
4057template <typename Derived>
4058struct action_label_traverser: public add_traverser_action_labels<regular_formulas::action_label_traverser, Derived>
4059{
4060};
4061//--- end generated state_formulas::add_traverser_action_labels code ---//
4062
4063} // namespace state_formulas
4064
4065} // namespace mcrl2
4066
4067#endif // MCRL2_MODAL_FORMULA_TRAVERSER_H
mcrl2::action_formulas::action_formula
\brief An action formula
Definition action_formula.h:24
mcrl2::action_formulas::and_
\brief The and operator for action formulas
Definition action_formula.h:299
mcrl2::action_formulas::and_::left
const action_formula & left() const
Definition action_formula.h:325
mcrl2::action_formulas::and_::right
const action_formula & right() const
Definition action_formula.h:330
mcrl2::action_formulas::at
\brief The at operator for action formulas
Definition action_formula.h:679
mcrl2::action_formulas::at::time_stamp
const data::data_expression & time_stamp() const
Definition action_formula.h:710
mcrl2::action_formulas::at::operand
const action_formula & operand() const
Definition action_formula.h:705
mcrl2::action_formulas::exists
\brief The existential quantification operator for action formulas
Definition action_formula.h:603
mcrl2::action_formulas::exists::variables
const data::variable_list & variables() const
Definition action_formula.h:629
mcrl2::action_formulas::exists::body
const action_formula & body() const
Definition action_formula.h:634
mcrl2::action_formulas::false_
\brief The value false for action formulas
Definition action_formula.h:175
mcrl2::action_formulas::forall
\brief The universal quantification operator for action formulas
Definition action_formula.h:527
mcrl2::action_formulas::forall::body
const action_formula & body() const
Definition action_formula.h:558
mcrl2::action_formulas::forall::variables
const data::variable_list & variables() const
Definition action_formula.h:553
mcrl2::action_formulas::imp
\brief The implication operator for action formulas
Definition action_formula.h:451
mcrl2::action_formulas::imp::left
const action_formula & left() const
Definition action_formula.h:477
mcrl2::action_formulas::imp::right
const action_formula & right() const
Definition action_formula.h:482
mcrl2::action_formulas::multi_action
\brief The multi action for action formulas
Definition action_formula.h:755
mcrl2::action_formulas::multi_action::actions
const process::action_list & actions() const
Definition action_formula.h:781
mcrl2::action_formulas::not_
\brief The not operator for action formulas
Definition action_formula.h:228
mcrl2::action_formulas::not_::operand
const action_formula & operand() const
Definition action_formula.h:254
mcrl2::action_formulas::or_
\brief The or operator for action formulas
Definition action_formula.h:375
mcrl2::action_formulas::or_::right
const action_formula & right() const
Definition action_formula.h:406
mcrl2::action_formulas::or_::left
const action_formula & left() const
Definition action_formula.h:401
mcrl2::action_formulas::true_
\brief The value true for action formulas
Definition action_formula.h:122
mcrl2::data::data_expression
data expression.
Definition data_expression.h:130
mcrl2::data::data_specification
data specification.
Definition data_specification.h:50
mcrl2::data::data_specification::data_specification
data_specification()=default
Default constructor. Generate a data specification that contains only booleans and positive numbers.
mcrl2::data::sort_specification
Definition sort_specification.h:44
mcrl2::data::untyped_data_parameter
\brief An untyped parameter
Definition untyped_data_parameter.h:24
mcrl2::lps::stochastic_specification
Linear process specification.
Definition stochastic_specification.h:34
mcrl2::process::untyped_multi_action
\brief An untyped multi action or data application
Definition untyped_multi_action.h:23
mcrl2::regular_formulas::alt
\brief The alt operator for regular formulas
Definition regular_formula.h:181
mcrl2::regular_formulas::alt::right
const regular_formula & right() const
Definition regular_formula.h:212
mcrl2::regular_formulas::alt::left
const regular_formula & left() const
Definition regular_formula.h:207
mcrl2::regular_formulas::regular_formula
\brief A regular formula
Definition regular_formula.h:23
mcrl2::regular_formulas::seq
\brief The seq operator for regular formulas
Definition regular_formula.h:105
mcrl2::regular_formulas::seq::right
const regular_formula & right() const
Definition regular_formula.h:136
mcrl2::regular_formulas::seq::left
const regular_formula & left() const
Definition regular_formula.h:131
mcrl2::regular_formulas::trans_or_nil
\brief The 'trans or nil' operator for regular formulas
Definition regular_formula.h:328
mcrl2::regular_formulas::trans_or_nil::operand
const regular_formula & operand() const
Definition regular_formula.h:354
mcrl2::regular_formulas::trans
\brief The trans operator for regular formulas
Definition regular_formula.h:257
mcrl2::regular_formulas::trans::operand
const regular_formula & operand() const
Definition regular_formula.h:283
mcrl2::regular_formulas::untyped_regular_formula
\brief An untyped regular formula or action formula
Definition regular_formula.h:399
mcrl2::regular_formulas::untyped_regular_formula::right
const regular_formula & right() const
Definition regular_formula.h:440
mcrl2::regular_formulas::untyped_regular_formula::left
const regular_formula & left() const
Definition regular_formula.h:435
mcrl2::regular_formulas::untyped_regular_formula::name
const core::identifier_string & name() const
Definition regular_formula.h:430
mcrl2::state_formulas::and_
\brief The and operator for state formulas
Definition state_formula.h:396
mcrl2::state_formulas::and_::right
const state_formula & right() const
Definition state_formula.h:427
mcrl2::state_formulas::and_::left
const state_formula & left() const
Definition state_formula.h:422
mcrl2::state_formulas::const_multiply_alt
\brief The multiply operator for state formulas with values
Definition state_formula.h:776
mcrl2::state_formulas::const_multiply_alt::left
const state_formula & left() const
Definition state_formula.h:802
mcrl2::state_formulas::const_multiply_alt::right
const data::data_expression & right() const
Definition state_formula.h:807
mcrl2::state_formulas::const_multiply
\brief The multiply operator for state formulas with values
Definition state_formula.h:700
mcrl2::state_formulas::const_multiply::left
const data::data_expression & left() const
Definition state_formula.h:726
mcrl2::state_formulas::const_multiply::right
const state_formula & right() const
Definition state_formula.h:731
mcrl2::state_formulas::delay_timed
\brief The timed delay operator for state formulas
Definition state_formula.h:1561
mcrl2::state_formulas::delay_timed::time_stamp
const data::data_expression & time_stamp() const
Definition state_formula.h:1587
mcrl2::state_formulas::delay
\brief The delay operator for state formulas
Definition state_formula.h:1508
mcrl2::state_formulas::exists
\brief The existential quantification operator for state formulas
Definition state_formula.h:928
mcrl2::state_formulas::exists::body
const state_formula & body() const
Definition state_formula.h:959
mcrl2::state_formulas::exists::variables
const data::variable_list & variables() const
Definition state_formula.h:954
mcrl2::state_formulas::false_
\brief The value false for state formulas
Definition state_formula.h:201
mcrl2::state_formulas::forall
\brief The universal quantification operator for state formulas
Definition state_formula.h:852
mcrl2::state_formulas::forall::body
const state_formula & body() const
Definition state_formula.h:883
mcrl2::state_formulas::forall::variables
const data::variable_list & variables() const
Definition state_formula.h:878
mcrl2::state_formulas::imp
\brief The implication operator for state formulas
Definition state_formula.h:548
mcrl2::state_formulas::imp::left
const state_formula & left() const
Definition state_formula.h:574
mcrl2::state_formulas::imp::right
const state_formula & right() const
Definition state_formula.h:579
mcrl2::state_formulas::infimum
\brief The infimum over a data type for state formulas
Definition state_formula.h:1004
mcrl2::state_formulas::infimum::variables
const data::variable_list & variables() const
Definition state_formula.h:1030
mcrl2::state_formulas::infimum::body
const state_formula & body() const
Definition state_formula.h:1035
mcrl2::state_formulas::may
\brief The may operator for state formulas
Definition state_formula.h:1308
mcrl2::state_formulas::may::operand
const state_formula & operand() const
Definition state_formula.h:1339
mcrl2::state_formulas::may::formula
const regular_formulas::regular_formula & formula() const
Definition state_formula.h:1334
mcrl2::state_formulas::minus
\brief The minus operator for state formulas
Definition state_formula.h:325
mcrl2::state_formulas::minus::operand
const state_formula & operand() const
Definition state_formula.h:351
mcrl2::state_formulas::mu
\brief The mu operator for state formulas
Definition state_formula.h:1799
mcrl2::state_formulas::mu::name
const core::identifier_string & name() const
Definition state_formula.h:1830
mcrl2::state_formulas::mu::assignments
const data::assignment_list & assignments() const
Definition state_formula.h:1835
mcrl2::state_formulas::mu::operand
const state_formula & operand() const
Definition state_formula.h:1840
mcrl2::state_formulas::must
\brief The must operator for state formulas
Definition state_formula.h:1232
mcrl2::state_formulas::must::formula
const regular_formulas::regular_formula & formula() const
Definition state_formula.h:1258
mcrl2::state_formulas::must::operand
const state_formula & operand() const
Definition state_formula.h:1263
mcrl2::state_formulas::not_
\brief The not operator for state formulas
Definition state_formula.h:254
mcrl2::state_formulas::not_::operand
const state_formula & operand() const
Definition state_formula.h:280
mcrl2::state_formulas::nu
\brief The nu operator for state formulas
Definition state_formula.h:1713
mcrl2::state_formulas::nu::name
const core::identifier_string & name() const
Definition state_formula.h:1744
mcrl2::state_formulas::nu::operand
const state_formula & operand() const
Definition state_formula.h:1754
mcrl2::state_formulas::nu::assignments
const data::assignment_list & assignments() const
Definition state_formula.h:1749
mcrl2::state_formulas::or_
\brief The or operator for state formulas
Definition state_formula.h:472
mcrl2::state_formulas::or_::right
const state_formula & right() const
Definition state_formula.h:503
mcrl2::state_formulas::or_::left
const state_formula & left() const
Definition state_formula.h:498
mcrl2::state_formulas::plus
\brief The plus operator for state formulas with values
Definition state_formula.h:624
mcrl2::state_formulas::plus::left
const state_formula & left() const
Definition state_formula.h:650
mcrl2::state_formulas::plus::right
const state_formula & right() const
Definition state_formula.h:655
mcrl2::state_formulas::state_formula_specification
Definition state_formula_specification.h:20
mcrl2::state_formulas::state_formula_specification::m_action_labels
process::action_label_list m_action_labels
The action specification of the specification.
Definition state_formula_specification.h:26
mcrl2::state_formulas::state_formula_specification::formula
const state_formula & formula() const
Returns the formula of the state formula specification.
Definition state_formula_specification.h:72
mcrl2::state_formulas::state_formula_specification::state_formula_specification
state_formula_specification(const state_formula &formula, const data::data_specification &data=data::data_specification(), const process::action_label_list &action_labels={})
Constructor of a state formula specification.
Definition state_formula_specification.h:36
mcrl2::state_formulas::state_formula_specification::m_formula
state_formula m_formula
The formula of the specification.
Definition state_formula_specification.h:29
mcrl2::state_formulas::state_formula_specification::m_data
data::data_specification m_data
The data specification of the specification.
Definition state_formula_specification.h:23
mcrl2::state_formulas::state_formula_specification::state_formula_specification
state_formula_specification()=default
Constructor.
mcrl2::state_formulas::state_formula_specification::formula
state_formula & formula()
Returns the formula of the state formula specification.
Definition state_formula_specification.h:79
mcrl2::state_formulas::state_formula_specification::action_labels
const process::action_label_list & action_labels() const
Returns the action label specification.
Definition state_formula_specification.h:58
mcrl2::state_formulas::state_formula_specification::action_labels
process::action_label_list & action_labels()
Returns the action label specification.
Definition state_formula_specification.h:65
mcrl2::state_formulas::state_formula
\brief A state formula
Definition state_formula.h:23
mcrl2::state_formulas::state_formula::state_formula
state_formula(const state_formula &) noexcept=default
Move semantics.
mcrl2::state_formulas::sum
\brief The sum over a data type for state formulas
Definition state_formula.h:1156
mcrl2::state_formulas::sum::variables
const data::variable_list & variables() const
Definition state_formula.h:1182
mcrl2::state_formulas::sum::body
const state_formula & body() const
Definition state_formula.h:1187
mcrl2::state_formulas::supremum
\brief The supremum over a data type for state formulas
Definition state_formula.h:1080
mcrl2::state_formulas::supremum::body
const state_formula & body() const
Definition state_formula.h:1111
mcrl2::state_formulas::supremum::variables
const data::variable_list & variables() const
Definition state_formula.h:1106
mcrl2::state_formulas::true_
\brief The value true for state formulas
Definition state_formula.h:148
mcrl2::state_formulas::variable
\brief The state formula variable
Definition state_formula.h:1632
mcrl2::state_formulas::variable::name
const core::identifier_string & name() const
Definition state_formula.h:1663
mcrl2::state_formulas::variable::arguments
const data::data_expression_list & arguments() const
Definition state_formula.h:1668
mcrl2::state_formulas::yaled_timed
\brief The timed yaled operator for state formulas
Definition state_formula.h:1437
mcrl2::state_formulas::yaled_timed::time_stamp
const data::data_expression & time_stamp() const
Definition state_formula.h:1463
mcrl2::state_formulas::yaled
\brief The yaled operator for state formulas
Definition state_formula.h:1384
parser_tables_mcrl2
D_ParserTables parser_tables_mcrl2
mcrl2::action_formulas::detail
Definition modal_formula.cpp:41
mcrl2::action_formulas::detail::parse_action_formula
action_formula parse_action_formula(const std::string &text)
Definition modal_formula.cpp:43
mcrl2::action_formulas
Definition modal_formula.cpp:24
mcrl2::action_formulas::pp
std::string pp(const action_formulas::exists &x, bool arg0)
Definition modal_formula.cpp:30
mcrl2::action_formulas::is_at
bool is_at(const atermpp::aterm &x)
Definition action_formula.h:728
mcrl2::action_formulas::pp
std::string pp(const action_formulas::imp &x, bool arg0)
Definition modal_formula.cpp:33
mcrl2::action_formulas::pp
std::string pp(const action_formulas::at &x, bool arg0)
Definition modal_formula.cpp:29
mcrl2::action_formulas::pp
std::string pp(const action_formulas::forall &x, bool arg0)
Definition modal_formula.cpp:32
mcrl2::action_formulas::pp
std::string pp(const action_formulas::or_ &x, bool arg0)
Definition modal_formula.cpp:36
mcrl2::action_formulas::pp
std::string pp(const action_formulas::action_formula &x, bool arg0)
Definition modal_formula.cpp:27
mcrl2::action_formulas::pp
std::string pp(const action_formulas::true_ &x, bool arg0)
Definition modal_formula.cpp:37
mcrl2::action_formulas::find_all_variables
std::set< data::variable > find_all_variables(const action_formulas::action_formula &x)
Definition modal_formula.cpp:38
mcrl2::action_formulas::is_or
bool is_or(const atermpp::aterm &x)
Definition action_formula.h:424
mcrl2::action_formulas::is_true
bool is_true(const atermpp::aterm &x)
Definition action_formula.h:148
mcrl2::action_formulas::is_forall
bool is_forall(const atermpp::aterm &x)
Definition action_formula.h:576
mcrl2::action_formulas::pp
std::string pp(const action_formulas::not_ &x, bool arg0)
Definition modal_formula.cpp:35
mcrl2::action_formulas::is_false
bool is_false(const atermpp::aterm &x)
Definition action_formula.h:201
mcrl2::action_formulas::is_not
bool is_not(const atermpp::aterm &x)
Definition action_formula.h:272
mcrl2::action_formulas::is_imp
bool is_imp(const atermpp::aterm &x)
Definition action_formula.h:500
mcrl2::action_formulas::is_and
bool is_and(const atermpp::aterm &x)
Definition action_formula.h:348
mcrl2::action_formulas::is_multi_action
bool is_multi_action(const atermpp::aterm &x)
Definition action_formula.h:799
mcrl2::action_formulas::pp
std::string pp(const action_formulas::multi_action &x, bool arg0)
Definition modal_formula.cpp:34
mcrl2::action_formulas::pp
std::string pp(const action_formulas::false_ &x, bool arg0)
Definition modal_formula.cpp:31
mcrl2::action_formulas::is_exists
bool is_exists(const atermpp::aterm &x)
Definition action_formula.h:652
mcrl2::action_formulas::pp
std::string pp(const action_formulas::and_ &x, bool arg0)
Definition modal_formula.cpp:28
mcrl2::action_formulas::is_action_formula
bool is_action_formula(const atermpp::aterm &x)
Definition action_formula.h:83
mcrl2::core::warn_left_merge_merge
void warn_left_merge_merge(const parse_node &)
Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.
Definition parser_utility.h:221
mcrl2::core::warn_and_or
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
Definition parser_utility.h:215
mcrl2::data::is_data_expression
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
Definition data_expression.h:232
mcrl2::data::is_untyped_data_parameter
bool is_untyped_data_parameter(const atermpp::aterm &x)
Definition untyped_data_parameter.h:84
mcrl2::lps
The main namespace for the LPS library.
Definition constelm.h:18
mcrl2::process
The main namespace for the Process library.
Definition alphabet_reduce.h:18
mcrl2::process::is_untyped_multi_action
bool is_untyped_multi_action(const atermpp::aterm &x)
Definition untyped_multi_action.h:73
mcrl2::regular_formulas::detail
Definition modal_formula.cpp:71
mcrl2::regular_formulas::detail::parse_regular_formula
regular_formula parse_regular_formula(const std::string &text)
Definition modal_formula.cpp:73
mcrl2::regular_formulas
Definition modal_formula.cpp:59
mcrl2::regular_formulas::is_alt
bool is_alt(const atermpp::aterm &x)
Definition regular_formula.h:230
mcrl2::regular_formulas::is_untyped_regular_formula
bool is_untyped_regular_formula(const atermpp::aterm &x)
Definition regular_formula.h:458
mcrl2::regular_formulas::is_trans
bool is_trans(const atermpp::aterm &x)
Definition regular_formula.h:301
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::trans &x, bool arg0)
Definition modal_formula.cpp:65
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::alt &x, bool arg0)
Definition modal_formula.cpp:62
mcrl2::regular_formulas::is_trans_or_nil
bool is_trans_or_nil(const atermpp::aterm &x)
Definition regular_formula.h:372
mcrl2::regular_formulas::is_seq
bool is_seq(const atermpp::aterm &x)
Definition regular_formula.h:154
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::untyped_regular_formula &x, bool arg0)
Definition modal_formula.cpp:67
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::seq &x, bool arg0)
Definition modal_formula.cpp:64
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::trans_or_nil &x, bool arg0)
Definition modal_formula.cpp:66
mcrl2::regular_formulas::pp
std::string pp(const regular_formulas::regular_formula &x, bool arg0)
Definition modal_formula.cpp:63
mcrl2::state_formulas::algorithms
Definition modal_formula.cpp:155
mcrl2::state_formulas::algorithms::parse_state_formula_specification
state_formula_specification parse_state_formula_specification(const std::string &text, const bool formula_is_quantitative)
Parses a state formula specification from text.
Definition modal_formula.cpp:172
mcrl2::state_formulas::algorithms::normalize
state_formula normalize(const state_formula &x)
Normalizes a state formula, i.e. removes any occurrences of ! or =>.
mcrl2::state_formulas::algorithms::is_normalized
bool is_normalized(const state_formula &x)
Checks if a state formula is normalized.
Definition modal_formula.cpp:197
mcrl2::state_formulas::algorithms::parse_state_formula
state_formula parse_state_formula(std::istream &in, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
Parses a state formula from an input stream.
Definition modal_formula.cpp:157
mcrl2::state_formulas::algorithms::normalize
state_formula normalize(const state_formula &x, bool quantitative=false, bool negated=false)
Definition modal_formula.cpp:192
mcrl2::state_formulas::algorithms::is_monotonous
bool is_monotonous(const state_formula &f)
Returns true if the state formula is monotonous.
Definition modal_formula.cpp:187
mcrl2::state_formulas::algorithms::parse_state_formula
state_formula parse_state_formula(const std::string &text, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
Parses a state formula from text.
Definition modal_formula.cpp:162
mcrl2::state_formulas::algorithms::parse_state_formula_specification
state_formula_specification parse_state_formula_specification(std::istream &in, const bool formula_is_quantitative)
Parses a state formula specification from an input stream.
Definition modal_formula.cpp:167
mcrl2::state_formulas::algorithms::parse_state_formula_specification
state_formula_specification parse_state_formula_specification(const std::string &text, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
Parses a state formula specification from text.
Definition modal_formula.cpp:182
mcrl2::state_formulas::algorithms::is_timed
bool is_timed(const state_formula &x)
Definition modal_formula.cpp:202
mcrl2::state_formulas::algorithms::find_state_variable_names
std::set< core::identifier_string > find_state_variable_names(const state_formula &x)
Returns the names of the state variables that occur in x.
Definition modal_formula.cpp:207
mcrl2::state_formulas::algorithms::parse_state_formula_specification
state_formula_specification parse_state_formula_specification(std::istream &in, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
Parses a state formula specification from an input stream.
Definition modal_formula.cpp:177
mcrl2::state_formulas::detail
Definition modal_formula.cpp:126
mcrl2::state_formulas::detail::parse_state_formula_specification
state_formula_specification parse_state_formula_specification(const std::string &text)
Definition modal_formula.cpp:139
mcrl2::state_formulas::detail::parse_state_formula
state_formula parse_state_formula(const std::string &text)
Definition modal_formula.cpp:128
mcrl2::state_formulas
Definition modal_formula.cpp:88
mcrl2::state_formulas::is_infimum
bool is_infimum(const atermpp::aterm &x)
Definition state_formula.h:1053
mcrl2::state_formulas::pp
std::string pp(const state_formulas::nu &x, bool arg0)
Definition modal_formula.cpp:106
mcrl2::state_formulas::pp
std::string pp(const state_formulas::exists &x, bool arg0)
Definition modal_formula.cpp:96
mcrl2::state_formulas::pp
std::string pp(const state_formulas::not_ &x, bool arg0)
Definition modal_formula.cpp:105
mcrl2::state_formulas::is_and
bool is_and(const atermpp::aterm &x)
Definition state_formula.h:445
mcrl2::state_formulas::pp
std::string pp(const state_formulas::supremum &x, bool arg0)
Definition modal_formula.cpp:112
mcrl2::state_formulas::is_delay_timed
bool is_delay_timed(const atermpp::aterm &x)
Definition state_formula.h:1605
mcrl2::state_formulas::is_const_multiply
bool is_const_multiply(const atermpp::aterm &x)
Definition state_formula.h:749
mcrl2::state_formulas::operator<<
std::ostream & operator<<(std::ostream &out, const state_formula_specification &x)
Definition state_formula_specification.h:94
mcrl2::state_formulas::pp
std::string pp(const state_formulas::must &x, bool arg0)
Definition modal_formula.cpp:104
mcrl2::state_formulas::is_minus
bool is_minus(const atermpp::aterm &x)
Definition state_formula.h:369
mcrl2::state_formulas::is_exists
bool is_exists(const atermpp::aterm &x)
Definition state_formula.h:977
mcrl2::state_formulas::is_not
bool is_not(const atermpp::aterm &x)
Definition state_formula.h:298
mcrl2::state_formulas::pp
std::string pp(const state_formulas::minus &x, bool arg0)
Definition modal_formula.cpp:102
mcrl2::state_formulas::is_supremum
bool is_supremum(const atermpp::aterm &x)
Definition state_formula.h:1129
mcrl2::state_formulas::is_must
bool is_must(const atermpp::aterm &x)
Definition state_formula.h:1281
mcrl2::state_formulas::find_all_variables
std::set< data::variable > find_all_variables(const state_formulas::state_formula &x)
Definition modal_formula.cpp:120
mcrl2::state_formulas::is_yaled
bool is_yaled(const atermpp::aterm &x)
Definition state_formula.h:1410
mcrl2::state_formulas::find_free_variables
std::set< data::variable > find_free_variables(const state_formulas::state_formula &x)
Definition modal_formula.cpp:121
mcrl2::state_formulas::is_true
bool is_true(const atermpp::aterm &x)
Definition state_formula.h:174
mcrl2::state_formulas::pp
std::string pp(const state_formulas::true_ &x, bool arg0)
Definition modal_formula.cpp:113
mcrl2::state_formulas::pp
std::string pp(const state_formulas::state_formula &x, bool arg0)
Definition modal_formula.cpp:109
mcrl2::state_formulas::pp
std::string pp(const state_formulas::const_multiply &x, bool arg0)
Definition modal_formula.cpp:92
mcrl2::state_formulas::pp
std::string pp(const state_formulas::delay_timed &x, bool arg0)
Definition modal_formula.cpp:95
mcrl2::state_formulas::is_variable
bool is_variable(const atermpp::aterm &x)
Definition state_formula.h:1686
mcrl2::state_formulas::is_may
bool is_may(const atermpp::aterm &x)
Definition state_formula.h:1357
mcrl2::state_formulas::is_yaled_timed
bool is_yaled_timed(const atermpp::aterm &x)
Definition state_formula.h:1481
mcrl2::state_formulas::is_imp
bool is_imp(const atermpp::aterm &x)
Definition state_formula.h:597
mcrl2::state_formulas::is_timed
bool is_timed(const state_formula &x)
Checks if a state formula is timed.
Definition is_timed.h:71
mcrl2::state_formulas::pp
std::string pp(const state_formulas::imp &x, bool arg0)
Definition modal_formula.cpp:99
mcrl2::state_formulas::pp
std::string pp(const state_formulas::mu &x, bool arg0)
Definition modal_formula.cpp:103
mcrl2::state_formulas::is_monotonous
bool is_monotonous(const state_formula &f)
Returns true if the state formula is monotonous.
Definition is_monotonous.h:166
mcrl2::state_formulas::is_sum
bool is_sum(const atermpp::aterm &x)
Definition state_formula.h:1205
mcrl2::state_formulas::translate_user_notation
state_formulas::state_formula translate_user_notation(const state_formulas::state_formula &x)
Definition modal_formula.cpp:118
mcrl2::state_formulas::normalize_sorts
state_formulas::state_formula normalize_sorts(const state_formulas::state_formula &x, const data::sort_specification &sortspec)
Definition modal_formula.cpp:117
mcrl2::state_formulas::is_nu
bool is_nu(const atermpp::aterm &x)
Definition state_formula.h:1772
mcrl2::state_formulas::pp
std::string pp(const state_formulas::delay &x, bool arg0)
Definition modal_formula.cpp:94
mcrl2::state_formulas::pp
std::string pp(const state_formulas::forall &x, bool arg0)
Definition modal_formula.cpp:98
mcrl2::state_formulas::pp
std::string pp(const state_formulas::sum &x, bool arg0)
Definition modal_formula.cpp:111
mcrl2::state_formulas::pp
std::string pp(const state_formulas::yaled &x, bool arg0)
Definition modal_formula.cpp:115
mcrl2::state_formulas::is_delay
bool is_delay(const atermpp::aterm &x)
Definition state_formula.h:1534
mcrl2::state_formulas::pp
std::string pp(const state_formulas::infimum &x, bool arg0)
Definition modal_formula.cpp:100
mcrl2::state_formulas::pp
std::string pp(const state_formulas::or_ &x, bool arg0)
Definition modal_formula.cpp:107
mcrl2::state_formulas::pp
std::string pp(const state_formulas::may &x, bool arg0)
Definition modal_formula.cpp:101
mcrl2::state_formulas::is_false
bool is_false(const atermpp::aterm &x)
Definition state_formula.h:227
mcrl2::state_formulas::is_plus
bool is_plus(const atermpp::aterm &x)
Definition state_formula.h:673
mcrl2::state_formulas::pp
std::string pp(const state_formulas::and_ &x, bool arg0)
Definition modal_formula.cpp:91
mcrl2::state_formulas::pp
std::string pp(const state_formulas::false_ &x, bool arg0)
Definition modal_formula.cpp:97
mcrl2::state_formulas::pp
std::string pp(const state_formulas::const_multiply_alt &x, bool arg0)
Definition modal_formula.cpp:93
mcrl2::state_formulas::is_mu
bool is_mu(const atermpp::aterm &x)
Definition state_formula.h:1858
mcrl2::state_formulas::is_forall
bool is_forall(const atermpp::aterm &x)
Definition state_formula.h:901
mcrl2::state_formulas::pp
std::string pp(const state_formulas::state_formula_specification &x, bool arg0)
Definition modal_formula.cpp:110
mcrl2::state_formulas::is_const_multiply_alt
bool is_const_multiply_alt(const atermpp::aterm &x)
Definition state_formula.h:825
mcrl2::state_formulas::pp
std::string pp(const state_formulas::yaled_timed &x, bool arg0)
Definition modal_formula.cpp:116
mcrl2::state_formulas::pp
std::string pp(const state_formulas::plus &x, bool arg0)
Definition modal_formula.cpp:108
mcrl2::state_formulas::is_or
bool is_or(const atermpp::aterm &x)
Definition state_formula.h:521
mcrl2::state_formulas::pp
std::string pp(const state_formulas::variable &x, bool arg0)
Definition modal_formula.cpp:114
mcrl2::state_formulas::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const state_formulas::state_formula &x)
Definition modal_formula.cpp:119
mcrl2::state_formulas::find_action_labels
std::set< process::action_label > find_action_labels(const state_formulas::state_formula &x)
Definition modal_formula.cpp:123
mcrl2::state_formulas::find_identifiers
std::set< core::identifier_string > find_identifiers(const state_formulas::state_formula &x)
Definition modal_formula.cpp:122
mcrl2::action_formulas::action_formula_traverser_base
Base class for action_formula_traverser.
Definition traverser.h:27
mcrl2::action_formulas::action_formula_traverser_base::apply
void apply(const data::data_expression &x)
Definition traverser.h:33
mcrl2::action_formulas::action_formula_traverser_base::apply
void apply(const process::untyped_multi_action &x)
Definition traverser.h:47
mcrl2::action_formulas::action_formula_traverser_base::apply
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:40
mcrl2::action_formulas::action_formula_traverser
\brief Traverser class
Definition traverser.h:502
mcrl2::action_formulas::action_label_traverser
\brief Traverser class
Definition traverser.h:955
mcrl2::action_formulas::add_traverser_action_formula_expressions
Definition traverser.h:360
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:395
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:373
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:439
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:403
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:432
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:366
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:387
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::at &x)
Definition traverser.h:425
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:418
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:411
mcrl2::action_formulas::add_traverser_action_formula_expressions::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:380
mcrl2::action_formulas::add_traverser_action_labels
Definition traverser.h:813
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:864
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:826
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:819
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:833
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::at &x)
Definition traverser.h:878
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:892
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:885
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:871
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:856
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:840
mcrl2::action_formulas::add_traverser_action_labels::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:848
mcrl2::action_formulas::add_traverser_data_expressions
Definition traverser.h:210
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:283
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::at &x)
Definition traverser.h:275
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:268
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:290
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:261
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:230
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:223
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:245
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:216
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:237
mcrl2::action_formulas::add_traverser_data_expressions::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:253
mcrl2::action_formulas::add_traverser_identifier_strings
Definition traverser.h:661
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:712
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:696
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:674
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:688
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:743
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:736
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::at &x)
Definition traverser.h:728
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:667
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:704
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:681
mcrl2::action_formulas::add_traverser_identifier_strings::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:720
mcrl2::action_formulas::add_traverser_sort_expressions
Definition traverser.h:58
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:140
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:64
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:93
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:133
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:109
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:85
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:71
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::at &x)
Definition traverser.h:125
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:78
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:101
mcrl2::action_formulas::add_traverser_sort_expressions::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:117
mcrl2::action_formulas::add_traverser_variables
Definition traverser.h:509
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::imp &x)
Definition traverser.h:552
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::and_ &x)
Definition traverser.h:536
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::or_ &x)
Definition traverser.h:544
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::forall &x)
Definition traverser.h:560
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::at &x)
Definition traverser.h:576
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::multi_action &x)
Definition traverser.h:584
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::true_ &x)
Definition traverser.h:515
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:591
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::exists &x)
Definition traverser.h:568
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::not_ &x)
Definition traverser.h:529
mcrl2::action_formulas::add_traverser_variables::apply
void apply(const action_formulas::false_ &x)
Definition traverser.h:522
mcrl2::action_formulas::data_expression_traverser
\brief Traverser class
Definition traverser.h:353
mcrl2::action_formulas::detail::action_formula_actions
Definition parse_impl.h:26
mcrl2::action_formulas::detail::action_formula_actions::action_formula_actions
action_formula_actions(const core::parser &parser_)
Definition parse_impl.h:27
mcrl2::action_formulas::detail::action_formula_actions::parse_ActFrm
action_formulas::action_formula parse_ActFrm(const core::parse_node &node) const
Definition parse_impl.h:31
mcrl2::action_formulas::identifier_string_traverser
\brief Traverser class
Definition traverser.h:806
mcrl2::action_formulas::sort_expression_traverser
\brief Traverser class
Definition traverser.h:203
mcrl2::action_formulas::variable_traverser
\brief Traverser class
Definition traverser.h:654
mcrl2::core::traverser
expression traverser that visits all sub expressions
Definition traverser.h:29
mcrl2::regular_formulas::action_label_traverser
\brief Traverser class
Definition traverser.h:1525
mcrl2::regular_formulas::add_traverser_action_labels
Definition traverser.h:1442
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1456
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1471
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1478
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1464
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:1448
mcrl2::regular_formulas::add_traverser_action_labels::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1486
mcrl2::regular_formulas::add_traverser_data_expressions
Definition traverser.h:1081
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1110
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1125
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:1087
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1095
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1117
mcrl2::regular_formulas::add_traverser_data_expressions::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1103
mcrl2::regular_formulas::add_traverser_identifier_strings
Definition traverser.h:1351
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1387
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1365
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1396
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1373
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:1357
mcrl2::regular_formulas::add_traverser_identifier_strings::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1380
mcrl2::regular_formulas::add_traverser_regular_formula_expressions
Definition traverser.h:1171
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1185
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1207
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:1177
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1215
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1200
mcrl2::regular_formulas::add_traverser_regular_formula_expressions::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1193
mcrl2::regular_formulas::add_traverser_sort_expressions
Definition traverser.h:991
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1013
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1005
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1027
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1020
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1035
mcrl2::regular_formulas::add_traverser_sort_expressions::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:997
mcrl2::regular_formulas::add_traverser_variables
Definition traverser.h:1261
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::trans_or_nil &x)
Definition traverser.h:1290
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::regular_formula &x)
Definition traverser.h:1305
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::alt &x)
Definition traverser.h:1275
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::untyped_regular_formula &x)
Definition traverser.h:1297
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::seq &x)
Definition traverser.h:1267
mcrl2::regular_formulas::add_traverser_variables::apply
void apply(const regular_formulas::trans &x)
Definition traverser.h:1283
mcrl2::regular_formulas::data_expression_traverser
\brief Traverser class
Definition traverser.h:1164
mcrl2::regular_formulas::detail::regular_formula_actions
Definition parse_impl.h:56
mcrl2::regular_formulas::detail::regular_formula_actions::parse_RegFrm
regular_formulas::regular_formula parse_RegFrm(const core::parse_node &node) const
Definition parse_impl.h:61
mcrl2::regular_formulas::detail::regular_formula_actions::regular_formula_actions
regular_formula_actions(const core::parser &parser_)
Definition parse_impl.h:57
mcrl2::regular_formulas::identifier_string_traverser
\brief Traverser class
Definition traverser.h:1435
mcrl2::regular_formulas::regular_formula_traverser_base
Traversal class for regular_formula_traverser. Used as a base class for pbes_expression_traverser.
Definition traverser.h:967
mcrl2::regular_formulas::regular_formula_traverser_base::apply
void apply(const action_formulas::action_formula &x)
Definition traverser.h:980
mcrl2::regular_formulas::regular_formula_traverser_base::apply
void apply(const data::data_expression &x)
Definition traverser.h:973
mcrl2::regular_formulas::regular_formula_traverser
\brief Traverser class
Definition traverser.h:1254
mcrl2::regular_formulas::sort_expression_traverser
\brief Traverser class
Definition traverser.h:1074
mcrl2::regular_formulas::variable_traverser
\brief Traverser class
Definition traverser.h:1344
mcrl2::state_formulas::action_label_traverser
\brief Traverser class
Definition traverser.h:4059
mcrl2::state_formulas::add_traverser_action_labels
Definition traverser.h:3756
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:3929
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:3944
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:3901
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:3915
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:3850
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:3783
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:3769
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:3864
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:3822
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:3908
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::must &x)
Definition traverser.h:3871
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:3814
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:3806
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:3894
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:3922
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:3843
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:3857
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:3762
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:3776
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:3829
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:3936
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:3790
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:3798
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::may &x)
Definition traverser.h:3879
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:3887
mcrl2::state_formulas::add_traverser_action_labels::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:3836
mcrl2::state_formulas::add_traverser_data_expressions
Definition traverser.h:1880
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:1938
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:1983
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:1914
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:2056
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:1990
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:2041
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:1900
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:2064
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::may &x)
Definition traverser.h:2005
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:1962
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:1922
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:1969
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:1893
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:2020
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:1886
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:2034
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::must &x)
Definition traverser.h:1997
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:2048
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:2013
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:2071
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:1930
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:2027
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:1954
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:1907
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:1946
mcrl2::state_formulas::add_traverser_data_expressions::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:1976
mcrl2::state_formulas::add_traverser_identifier_strings
Definition traverser.h:3125
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:3183
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:3291
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:3231
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:3191
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:3277
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:3167
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:3299
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:3215
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:3239
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:3263
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:3308
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:3270
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:3138
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:3325
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:3159
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:3199
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:3317
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:3175
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:3152
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::must &x)
Definition traverser.h:3247
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:3284
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:3207
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::may &x)
Definition traverser.h:3255
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:3223
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:3145
mcrl2::state_formulas::add_traverser_identifier_strings::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:3131
mcrl2::state_formulas::add_traverser_regular_formula_expressions
Definition traverser.h:3447
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::may &x)
Definition traverser.h:3570
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:3460
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:3541
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:3453
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:3505
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:3497
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:3467
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:3592
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:3613
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:3527
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:3627
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:3585
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:3606
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:3513
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:3599
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:3474
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:3620
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:3555
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:3634
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:3520
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:3578
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::must &x)
Definition traverser.h:3562
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:3548
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:3489
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:3534
mcrl2::state_formulas::add_traverser_regular_formula_expressions::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:3481
mcrl2::state_formulas::add_traverser_sort_expressions
Definition traverser.h:1561
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:1699
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:1627
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:1727
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:1758
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:1720
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:1619
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:1667
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:1595
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::must &x)
Definition traverser.h:1683
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:1651
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:1574
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:1713
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:1734
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:1581
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:1635
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::may &x)
Definition traverser.h:1691
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:1643
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:1706
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:1659
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:1603
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:1567
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:1750
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:1611
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:1588
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:1675
mcrl2::state_formulas::add_traverser_sort_expressions::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:1742
mcrl2::state_formulas::add_traverser_state_formula_expressions
Definition traverser.h:2193
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:2259
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:2243
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:2364
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:2329
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:2266
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:2287
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:2378
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:2273
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:2322
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:2294
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:2206
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:2350
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:2336
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:2251
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:2227
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:2280
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:2235
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::may &x)
Definition traverser.h:2315
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::must &x)
Definition traverser.h:2308
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:2343
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:2301
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:2199
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:2220
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:2213
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:2357
mcrl2::state_formulas::add_traverser_state_formula_expressions::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:2371
mcrl2::state_formulas::add_traverser_state_variables
Definition traverser.h:2818
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:2961
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:2975
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::may &x)
Definition traverser.h:2940
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:2912
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:2852
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:3003
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:2905
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:2989
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:2831
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:2860
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:2884
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:2954
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:2838
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:2824
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:2868
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:2926
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:2876
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:2996
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::must &x)
Definition traverser.h:2933
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:2947
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:2898
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:2891
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:2845
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:2968
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:2982
mcrl2::state_formulas::add_traverser_state_variables::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:2919
mcrl2::state_formulas::add_traverser_variables
Definition traverser.h:2500
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::false_ &x)
Definition traverser.h:2513
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::const_multiply_alt &x)
Definition traverser.h:2574
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::true_ &x)
Definition traverser.h:2506
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::and_ &x)
Definition traverser.h:2534
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::exists &x)
Definition traverser.h:2590
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::or_ &x)
Definition traverser.h:2542
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::infimum &x)
Definition traverser.h:2598
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::yaled &x)
Definition traverser.h:2638
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::yaled_timed &x)
Definition traverser.h:2645
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::plus &x)
Definition traverser.h:2558
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::sum &x)
Definition traverser.h:2614
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::delay_timed &x)
Definition traverser.h:2659
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::must &x)
Definition traverser.h:2622
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::forall &x)
Definition traverser.h:2582
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::mu &x)
Definition traverser.h:2681
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::delay &x)
Definition traverser.h:2652
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::state_formula_specification &x)
Definition traverser.h:2689
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::const_multiply &x)
Definition traverser.h:2566
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::variable &x)
Definition traverser.h:2666
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::supremum &x)
Definition traverser.h:2606
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::may &x)
Definition traverser.h:2630
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::state_formula &x)
Definition traverser.h:2696
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::nu &x)
Definition traverser.h:2673
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::imp &x)
Definition traverser.h:2550
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::minus &x)
Definition traverser.h:2527
mcrl2::state_formulas::add_traverser_variables::apply
void apply(const state_formulas::not_ &x)
Definition traverser.h:2520
mcrl2::state_formulas::data_expression_traverser
\brief Traverser class
Definition traverser.h:2186
mcrl2::state_formulas::detail::is_timed_traverser
Function that determines if a state formula is time dependent.
Definition is_timed.h:25
mcrl2::state_formulas::detail::is_timed_traverser::apply
void apply(const process::untyped_multi_action &)
Definition is_timed.h:43
mcrl2::state_formulas::detail::is_timed_traverser::enter
void enter(const action_formulas::at &)
Definition is_timed.h:58
mcrl2::state_formulas::detail::is_timed_traverser::apply
void apply(const data::data_expression &)
Definition is_timed.h:33
mcrl2::state_formulas::detail::is_timed_traverser::result
bool result
Definition is_timed.h:31
mcrl2::state_formulas::detail::is_timed_traverser::enter
void enter(const delay_timed &)
Definition is_timed.h:48
mcrl2::state_formulas::detail::is_timed_traverser::enter
void enter(const yaled_timed &)
Definition is_timed.h:53
mcrl2::state_formulas::detail::is_timed_traverser::apply
void apply(const data::untyped_data_parameter &)
Definition is_timed.h:38
mcrl2::state_formulas::detail::state_formula_actions
Definition parse_impl.h:94
mcrl2::state_formulas::detail::state_formula_actions::parse_StateFrmSpec
untyped_state_formula_specification parse_StateFrmSpec(const core::parse_node &node) const
Definition parse_impl.h:204
mcrl2::state_formulas::detail::state_formula_actions::state_formula_actions
state_formula_actions(const core::parser &parser_)
Definition parse_impl.h:95
mcrl2::state_formulas::detail::state_formula_actions::parse_StateFrm
state_formulas::state_formula parse_StateFrm(const core::parse_node &node) const
Definition parse_impl.h:133
mcrl2::state_formulas::detail::untyped_state_formula_specification
Definition parse_impl.h:79
mcrl2::state_formulas::detail::untyped_state_formula_specification::construct_state_formula_specification
state_formula_specification construct_state_formula_specification()
Definition parse_impl.h:83
mcrl2::state_formulas::identifier_string_traverser
\brief Traverser class
Definition traverser.h:3440
mcrl2::state_formulas::regular_formula_traverser
\brief Traverser class
Definition traverser.h:3749
mcrl2::state_formulas::sort_expression_traverser
\brief Traverser class
Definition traverser.h:1873
mcrl2::state_formulas::state_formula_traverser_base
Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
Definition traverser.h:1537
mcrl2::state_formulas::state_formula_traverser_base::apply
void apply(const data::data_expression &x)
Definition traverser.h:1543
mcrl2::state_formulas::state_formula_traverser_base::apply
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:1550
mcrl2::state_formulas::state_formula_traverser
\brief Traverser class
Definition traverser.h:2493
mcrl2::state_formulas::state_variable_traverser
\brief Traverser class
Definition traverser.h:3118
mcrl2::state_formulas::variable_traverser
\brief Traverser class
Definition traverser.h:2811