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