mCRL2
Loading...
Searching...
No Matches
traverser.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/pbes/traverser.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_PBES_TRAVERSER_H
13#define MCRL2_PBES_TRAVERSER_H
14
15#include "mcrl2/pbes/pbes.h"
16
17namespace mcrl2::pbes_system
18{
19
20/// \brief Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
21template <typename Derived>
22struct pbes_expression_traverser_base: public core::traverser<Derived>
23{
24 using super = core::traverser<Derived>;
25 using super::apply;
26 using super::enter;
27 using super::leave;
28
29 void apply(const data::data_expression& x)
30 {
31 static_cast<Derived&>(*this).enter(x);
32 // skip
33 static_cast<Derived&>(*this).leave(x);
34 }
35
36 void apply(const data::untyped_data_parameter& x)
37 {
38 static_cast<Derived&>(*this).enter(x);
39 // skip
40 static_cast<Derived&>(*this).leave(x);
41 }
42};
43
44//--- start generated add_traverser_sort_expressions code ---//
45template <template <class> class Traverser, class Derived>
46struct add_traverser_sort_expressions: public Traverser<Derived>
47{
48 using super = Traverser<Derived>;
49 using super::enter;
50 using super::leave;
51 using super::apply;
52
53 void apply(const pbes_system::propositional_variable& x)
54 {
55 static_cast<Derived&>(*this).enter(x);
56 static_cast<Derived&>(*this).apply(x.parameters());
57 static_cast<Derived&>(*this).leave(x);
58 }
59
60 void apply(const pbes_system::pbes_equation& x)
61 {
62 static_cast<Derived&>(*this).enter(x);
63 static_cast<Derived&>(*this).apply(x.variable());
64 static_cast<Derived&>(*this).apply(x.formula());
65 static_cast<Derived&>(*this).leave(x);
66 }
67
68 void apply(const pbes_system::pbes& x)
69 {
70 static_cast<Derived&>(*this).enter(x);
71 static_cast<Derived&>(*this).apply(x.global_variables());
72 static_cast<Derived&>(*this).apply(x.equations());
73 static_cast<Derived&>(*this).apply(x.initial_state());
74 static_cast<Derived&>(*this).leave(x);
75 }
76
77 void apply(const pbes_system::propositional_variable_instantiation& x)
78 {
79 static_cast<Derived&>(*this).enter(x);
80 static_cast<Derived&>(*this).apply(x.parameters());
81 static_cast<Derived&>(*this).leave(x);
82 }
83
84 void apply(const pbes_system::not_& x)
85 {
86 static_cast<Derived&>(*this).enter(x);
87 static_cast<Derived&>(*this).apply(x.operand());
88 static_cast<Derived&>(*this).leave(x);
89 }
90
91 void apply(const pbes_system::and_& x)
92 {
93 static_cast<Derived&>(*this).enter(x);
94 static_cast<Derived&>(*this).apply(x.left());
95 static_cast<Derived&>(*this).apply(x.right());
96 static_cast<Derived&>(*this).leave(x);
97 }
98
99 void apply(const pbes_system::or_& x)
100 {
101 static_cast<Derived&>(*this).enter(x);
102 static_cast<Derived&>(*this).apply(x.left());
103 static_cast<Derived&>(*this).apply(x.right());
104 static_cast<Derived&>(*this).leave(x);
105 }
106
107 void apply(const pbes_system::imp& x)
108 {
109 static_cast<Derived&>(*this).enter(x);
110 static_cast<Derived&>(*this).apply(x.left());
111 static_cast<Derived&>(*this).apply(x.right());
112 static_cast<Derived&>(*this).leave(x);
113 }
114
115 void apply(const pbes_system::forall& x)
116 {
117 static_cast<Derived&>(*this).enter(x);
118 static_cast<Derived&>(*this).apply(x.variables());
119 static_cast<Derived&>(*this).apply(x.body());
120 static_cast<Derived&>(*this).leave(x);
121 }
122
123 void apply(const pbes_system::exists& x)
124 {
125 static_cast<Derived&>(*this).enter(x);
126 static_cast<Derived&>(*this).apply(x.variables());
127 static_cast<Derived&>(*this).apply(x.body());
128 static_cast<Derived&>(*this).leave(x);
129 }
130
131 void apply(const pbes_system::pbes_expression& x)
132 {
133 static_cast<Derived&>(*this).enter(x);
134 if (data::is_data_expression(x))
135 {
136 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
137 }
138 else if (data::is_untyped_data_parameter(x))
139 {
140 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
141 }
142 else if (pbes_system::is_propositional_variable_instantiation(x))
143 {
144 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
145 }
146 else if (pbes_system::is_not(x))
147 {
148 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
149 }
150 else if (pbes_system::is_and(x))
151 {
152 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
153 }
154 else if (pbes_system::is_or(x))
155 {
156 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
157 }
158 else if (pbes_system::is_imp(x))
159 {
160 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
161 }
162 else if (pbes_system::is_forall(x))
163 {
164 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
165 }
166 else if (pbes_system::is_exists(x))
167 {
168 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
169 }
170 static_cast<Derived&>(*this).leave(x);
171 }
172
173};
174
175/// \\brief Traverser class
176template <typename Derived>
177struct sort_expression_traverser: public add_traverser_sort_expressions<data::sort_expression_traverser, Derived>
178{
179};
180//--- end generated add_traverser_sort_expressions code ---//
181
182//--- start generated add_traverser_data_expressions code ---//
183template <template <class> class Traverser, class Derived>
184struct add_traverser_data_expressions: public Traverser<Derived>
185{
186 using super = Traverser<Derived>;
187 using super::enter;
188 using super::leave;
189 using super::apply;
190
191 void apply(const pbes_system::pbes_equation& x)
192 {
193 static_cast<Derived&>(*this).enter(x);
194 static_cast<Derived&>(*this).apply(x.formula());
195 static_cast<Derived&>(*this).leave(x);
196 }
197
198 void apply(const pbes_system::pbes& x)
199 {
200 static_cast<Derived&>(*this).enter(x);
201 static_cast<Derived&>(*this).apply(x.equations());
202 static_cast<Derived&>(*this).apply(x.initial_state());
203 static_cast<Derived&>(*this).leave(x);
204 }
205
206 void apply(const pbes_system::propositional_variable_instantiation& x)
207 {
208 static_cast<Derived&>(*this).enter(x);
209 static_cast<Derived&>(*this).apply(x.parameters());
210 static_cast<Derived&>(*this).leave(x);
211 }
212
213 void apply(const pbes_system::not_& x)
214 {
215 static_cast<Derived&>(*this).enter(x);
216 static_cast<Derived&>(*this).apply(x.operand());
217 static_cast<Derived&>(*this).leave(x);
218 }
219
220 void apply(const pbes_system::and_& x)
221 {
222 static_cast<Derived&>(*this).enter(x);
223 static_cast<Derived&>(*this).apply(x.left());
224 static_cast<Derived&>(*this).apply(x.right());
225 static_cast<Derived&>(*this).leave(x);
226 }
227
228 void apply(const pbes_system::or_& x)
229 {
230 static_cast<Derived&>(*this).enter(x);
231 static_cast<Derived&>(*this).apply(x.left());
232 static_cast<Derived&>(*this).apply(x.right());
233 static_cast<Derived&>(*this).leave(x);
234 }
235
236 void apply(const pbes_system::imp& x)
237 {
238 static_cast<Derived&>(*this).enter(x);
239 static_cast<Derived&>(*this).apply(x.left());
240 static_cast<Derived&>(*this).apply(x.right());
241 static_cast<Derived&>(*this).leave(x);
242 }
243
244 void apply(const pbes_system::forall& x)
245 {
246 static_cast<Derived&>(*this).enter(x);
247 static_cast<Derived&>(*this).apply(x.body());
248 static_cast<Derived&>(*this).leave(x);
249 }
250
251 void apply(const pbes_system::exists& x)
252 {
253 static_cast<Derived&>(*this).enter(x);
254 static_cast<Derived&>(*this).apply(x.body());
255 static_cast<Derived&>(*this).leave(x);
256 }
257
258 void apply(const pbes_system::pbes_expression& x)
259 {
260 static_cast<Derived&>(*this).enter(x);
261 if (data::is_data_expression(x))
262 {
263 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
264 }
265 else if (data::is_untyped_data_parameter(x))
266 {
267 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
268 }
269 else if (pbes_system::is_propositional_variable_instantiation(x))
270 {
271 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
272 }
273 else if (pbes_system::is_not(x))
274 {
275 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
276 }
277 else if (pbes_system::is_and(x))
278 {
279 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
280 }
281 else if (pbes_system::is_or(x))
282 {
283 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
284 }
285 else if (pbes_system::is_imp(x))
286 {
287 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
288 }
289 else if (pbes_system::is_forall(x))
290 {
291 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
292 }
293 else if (pbes_system::is_exists(x))
294 {
295 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
296 }
297 static_cast<Derived&>(*this).leave(x);
298 }
299
300};
301
302/// \\brief Traverser class
303template <typename Derived>
304struct data_expression_traverser: public add_traverser_data_expressions<data::data_expression_traverser, Derived>
305{
306};
307//--- end generated add_traverser_data_expressions code ---//
308
309//--- start generated add_traverser_pbes_expressions code ---//
310template <template <class> class Traverser, class Derived>
311struct add_traverser_pbes_expressions: public Traverser<Derived>
312{
313 using super = Traverser<Derived>;
314 using super::enter;
315 using super::leave;
316 using super::apply;
317
318 void apply(const pbes_system::pbes_equation& x)
319 {
320 static_cast<Derived&>(*this).enter(x);
321 static_cast<Derived&>(*this).apply(x.formula());
322 static_cast<Derived&>(*this).leave(x);
323 }
324
325 void apply(const pbes_system::pbes& x)
326 {
327 static_cast<Derived&>(*this).enter(x);
328 static_cast<Derived&>(*this).apply(x.equations());
329 static_cast<Derived&>(*this).leave(x);
330 }
331
332 void apply(const pbes_system::propositional_variable_instantiation& x)
333 {
334 static_cast<Derived&>(*this).enter(x);
335 // skip
336 static_cast<Derived&>(*this).leave(x);
337 }
338
339 void apply(const pbes_system::not_& x)
340 {
341 static_cast<Derived&>(*this).enter(x);
342 static_cast<Derived&>(*this).apply(x.operand());
343 static_cast<Derived&>(*this).leave(x);
344 }
345
346 void apply(const pbes_system::and_& x)
347 {
348 static_cast<Derived&>(*this).enter(x);
349 static_cast<Derived&>(*this).apply(x.left());
350 static_cast<Derived&>(*this).apply(x.right());
351 static_cast<Derived&>(*this).leave(x);
352 }
353
354 void apply(const pbes_system::or_& x)
355 {
356 static_cast<Derived&>(*this).enter(x);
357 static_cast<Derived&>(*this).apply(x.left());
358 static_cast<Derived&>(*this).apply(x.right());
359 static_cast<Derived&>(*this).leave(x);
360 }
361
362 void apply(const pbes_system::imp& x)
363 {
364 static_cast<Derived&>(*this).enter(x);
365 static_cast<Derived&>(*this).apply(x.left());
366 static_cast<Derived&>(*this).apply(x.right());
367 static_cast<Derived&>(*this).leave(x);
368 }
369
370 void apply(const pbes_system::forall& x)
371 {
372 static_cast<Derived&>(*this).enter(x);
373 static_cast<Derived&>(*this).apply(x.body());
374 static_cast<Derived&>(*this).leave(x);
375 }
376
377 void apply(const pbes_system::exists& x)
378 {
379 static_cast<Derived&>(*this).enter(x);
380 static_cast<Derived&>(*this).apply(x.body());
381 static_cast<Derived&>(*this).leave(x);
382 }
383
384 void apply(const pbes_system::pbes_expression& x)
385 {
386 static_cast<Derived&>(*this).enter(x);
387 if (data::is_data_expression(x))
388 {
389 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
390 }
391 else if (data::is_untyped_data_parameter(x))
392 {
393 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
394 }
395 else if (pbes_system::is_propositional_variable_instantiation(x))
396 {
397 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
398 }
399 else if (pbes_system::is_not(x))
400 {
401 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
402 }
403 else if (pbes_system::is_and(x))
404 {
405 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
406 }
407 else if (pbes_system::is_or(x))
408 {
409 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
410 }
411 else if (pbes_system::is_imp(x))
412 {
413 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
414 }
415 else if (pbes_system::is_forall(x))
416 {
417 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
418 }
419 else if (pbes_system::is_exists(x))
420 {
421 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
422 }
423 static_cast<Derived&>(*this).leave(x);
424 }
425
426};
427
428/// \\brief Traverser class
429template <typename Derived>
430struct pbes_expression_traverser: public add_traverser_pbes_expressions<pbes_system::pbes_expression_traverser_base, Derived>
431{
432};
433//--- end generated add_traverser_pbes_expressions code ---//
434
435//--- start generated add_traverser_variables code ---//
436template <template <class> class Traverser, class Derived>
437struct add_traverser_variables: public Traverser<Derived>
438{
439 using super = Traverser<Derived>;
440 using super::enter;
441 using super::leave;
442 using super::apply;
443
444 void apply(const pbes_system::propositional_variable& x)
445 {
446 static_cast<Derived&>(*this).enter(x);
447 static_cast<Derived&>(*this).apply(x.parameters());
448 static_cast<Derived&>(*this).leave(x);
449 }
450
451 void apply(const pbes_system::pbes_equation& x)
452 {
453 static_cast<Derived&>(*this).enter(x);
454 static_cast<Derived&>(*this).apply(x.variable());
455 static_cast<Derived&>(*this).apply(x.formula());
456 static_cast<Derived&>(*this).leave(x);
457 }
458
459 void apply(const pbes_system::pbes& x)
460 {
461 static_cast<Derived&>(*this).enter(x);
462 static_cast<Derived&>(*this).apply(x.global_variables());
463 static_cast<Derived&>(*this).apply(x.equations());
464 static_cast<Derived&>(*this).apply(x.initial_state());
465 static_cast<Derived&>(*this).leave(x);
466 }
467
468 void apply(const pbes_system::propositional_variable_instantiation& x)
469 {
470 static_cast<Derived&>(*this).enter(x);
471 static_cast<Derived&>(*this).apply(x.parameters());
472 static_cast<Derived&>(*this).leave(x);
473 }
474
475 void apply(const pbes_system::not_& x)
476 {
477 static_cast<Derived&>(*this).enter(x);
478 static_cast<Derived&>(*this).apply(x.operand());
479 static_cast<Derived&>(*this).leave(x);
480 }
481
482 void apply(const pbes_system::and_& x)
483 {
484 static_cast<Derived&>(*this).enter(x);
485 static_cast<Derived&>(*this).apply(x.left());
486 static_cast<Derived&>(*this).apply(x.right());
487 static_cast<Derived&>(*this).leave(x);
488 }
489
490 void apply(const pbes_system::or_& x)
491 {
492 static_cast<Derived&>(*this).enter(x);
493 static_cast<Derived&>(*this).apply(x.left());
494 static_cast<Derived&>(*this).apply(x.right());
495 static_cast<Derived&>(*this).leave(x);
496 }
497
498 void apply(const pbes_system::imp& x)
499 {
500 static_cast<Derived&>(*this).enter(x);
501 static_cast<Derived&>(*this).apply(x.left());
502 static_cast<Derived&>(*this).apply(x.right());
503 static_cast<Derived&>(*this).leave(x);
504 }
505
506 void apply(const pbes_system::forall& x)
507 {
508 static_cast<Derived&>(*this).enter(x);
509 static_cast<Derived&>(*this).apply(x.variables());
510 static_cast<Derived&>(*this).apply(x.body());
511 static_cast<Derived&>(*this).leave(x);
512 }
513
514 void apply(const pbes_system::exists& x)
515 {
516 static_cast<Derived&>(*this).enter(x);
517 static_cast<Derived&>(*this).apply(x.variables());
518 static_cast<Derived&>(*this).apply(x.body());
519 static_cast<Derived&>(*this).leave(x);
520 }
521
522 void apply(const pbes_system::pbes_expression& x)
523 {
524 static_cast<Derived&>(*this).enter(x);
525 if (data::is_data_expression(x))
526 {
527 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
528 }
529 else if (data::is_untyped_data_parameter(x))
530 {
531 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
532 }
533 else if (pbes_system::is_propositional_variable_instantiation(x))
534 {
535 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
536 }
537 else if (pbes_system::is_not(x))
538 {
539 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
540 }
541 else if (pbes_system::is_and(x))
542 {
543 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
544 }
545 else if (pbes_system::is_or(x))
546 {
547 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
548 }
549 else if (pbes_system::is_imp(x))
550 {
551 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
552 }
553 else if (pbes_system::is_forall(x))
554 {
555 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
556 }
557 else if (pbes_system::is_exists(x))
558 {
559 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
560 }
561 static_cast<Derived&>(*this).leave(x);
562 }
563
564};
565
566/// \\brief Traverser class
567template <typename Derived>
568struct variable_traverser: public add_traverser_variables<data::variable_traverser, Derived>
569{
570};
571//--- end generated add_traverser_variables code ---//
572
573//--- start generated add_traverser_identifier_strings code ---//
574template <template <class> class Traverser, class Derived>
575struct add_traverser_identifier_strings: public Traverser<Derived>
576{
577 using super = Traverser<Derived>;
578 using super::enter;
579 using super::leave;
580 using super::apply;
581
582 void apply(const pbes_system::propositional_variable& x)
583 {
584 static_cast<Derived&>(*this).enter(x);
585 static_cast<Derived&>(*this).apply(x.name());
586 static_cast<Derived&>(*this).apply(x.parameters());
587 static_cast<Derived&>(*this).leave(x);
588 }
589
590 void apply(const pbes_system::pbes_equation& x)
591 {
592 static_cast<Derived&>(*this).enter(x);
593 static_cast<Derived&>(*this).apply(x.variable());
594 static_cast<Derived&>(*this).apply(x.formula());
595 static_cast<Derived&>(*this).leave(x);
596 }
597
598 void apply(const pbes_system::pbes& x)
599 {
600 static_cast<Derived&>(*this).enter(x);
601 static_cast<Derived&>(*this).apply(x.global_variables());
602 static_cast<Derived&>(*this).apply(x.equations());
603 static_cast<Derived&>(*this).apply(x.initial_state());
604 static_cast<Derived&>(*this).leave(x);
605 }
606
607 void apply(const pbes_system::propositional_variable_instantiation& x)
608 {
609 static_cast<Derived&>(*this).enter(x);
610 static_cast<Derived&>(*this).apply(x.name());
611 static_cast<Derived&>(*this).apply(x.parameters());
612 static_cast<Derived&>(*this).leave(x);
613 }
614
615 void apply(const pbes_system::not_& x)
616 {
617 static_cast<Derived&>(*this).enter(x);
618 static_cast<Derived&>(*this).apply(x.operand());
619 static_cast<Derived&>(*this).leave(x);
620 }
621
622 void apply(const pbes_system::and_& x)
623 {
624 static_cast<Derived&>(*this).enter(x);
625 static_cast<Derived&>(*this).apply(x.left());
626 static_cast<Derived&>(*this).apply(x.right());
627 static_cast<Derived&>(*this).leave(x);
628 }
629
630 void apply(const pbes_system::or_& x)
631 {
632 static_cast<Derived&>(*this).enter(x);
633 static_cast<Derived&>(*this).apply(x.left());
634 static_cast<Derived&>(*this).apply(x.right());
635 static_cast<Derived&>(*this).leave(x);
636 }
637
638 void apply(const pbes_system::imp& x)
639 {
640 static_cast<Derived&>(*this).enter(x);
641 static_cast<Derived&>(*this).apply(x.left());
642 static_cast<Derived&>(*this).apply(x.right());
643 static_cast<Derived&>(*this).leave(x);
644 }
645
646 void apply(const pbes_system::forall& x)
647 {
648 static_cast<Derived&>(*this).enter(x);
649 static_cast<Derived&>(*this).apply(x.variables());
650 static_cast<Derived&>(*this).apply(x.body());
651 static_cast<Derived&>(*this).leave(x);
652 }
653
654 void apply(const pbes_system::exists& x)
655 {
656 static_cast<Derived&>(*this).enter(x);
657 static_cast<Derived&>(*this).apply(x.variables());
658 static_cast<Derived&>(*this).apply(x.body());
659 static_cast<Derived&>(*this).leave(x);
660 }
661
662 void apply(const pbes_system::pbes_expression& x)
663 {
664 static_cast<Derived&>(*this).enter(x);
665 if (data::is_data_expression(x))
666 {
667 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::data_expression>(x));
668 }
669 else if (data::is_untyped_data_parameter(x))
670 {
671 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
672 }
673 else if (pbes_system::is_propositional_variable_instantiation(x))
674 {
675 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
676 }
677 else if (pbes_system::is_not(x))
678 {
679 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::not_>(x));
680 }
681 else if (pbes_system::is_and(x))
682 {
683 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::and_>(x));
684 }
685 else if (pbes_system::is_or(x))
686 {
687 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::or_>(x));
688 }
689 else if (pbes_system::is_imp(x))
690 {
691 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::imp>(x));
692 }
693 else if (pbes_system::is_forall(x))
694 {
695 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::forall>(x));
696 }
697 else if (pbes_system::is_exists(x))
698 {
699 static_cast<Derived&>(*this).apply(atermpp::down_cast<pbes_system::exists>(x));
700 }
701 static_cast<Derived&>(*this).leave(x);
702 }
703
704};
705
706/// \\brief Traverser class
707template <typename Derived>
708struct identifier_string_traverser: public add_traverser_identifier_strings<data::identifier_string_traverser, Derived>
709{
710};
711//--- end generated add_traverser_identifier_strings code ---//
712
713} // namespace mcrl2::pbes_system
714
715#endif // MCRL2_PBES_TRAVERSER_H
mcrl2::data::data_expression
data expression.
Definition data_expression.h:130
mcrl2::data::data_specification
data specification.
Definition data_specification.h:50
mcrl2::data::sort_specification
Definition sort_specification.h:44
mcrl2::data::untyped_data_parameter
\brief An untyped parameter
Definition untyped_data_parameter.h:24
mcrl2::data::variable
\brief A data variable
Definition variable.h:25
mcrl2::pbes_system::and_
\brief The and operator for pbes expressions
Definition pbes_expression.h:287
mcrl2::pbes_system::and_::left
const pbes_expression & left() const
Definition pbes_expression.h:313
mcrl2::pbes_system::and_::right
const pbes_expression & right() const
Definition pbes_expression.h:318
mcrl2::pbes_system::exists
\brief The existential quantification operator for pbes expressions
Definition pbes_expression.h:591
mcrl2::pbes_system::exists::variables
const data::variable_list & variables() const
Definition pbes_expression.h:617
mcrl2::pbes_system::exists::body
const pbes_expression & body() const
Definition pbes_expression.h:622
mcrl2::pbes_system::forall
\brief The universal quantification operator for pbes expressions
Definition pbes_expression.h:515
mcrl2::pbes_system::forall::body
const pbes_expression & body() const
Definition pbes_expression.h:546
mcrl2::pbes_system::forall::variables
const data::variable_list & variables() const
Definition pbes_expression.h:541
mcrl2::pbes_system::imp
\brief The implication operator for pbes expressions
Definition pbes_expression.h:439
mcrl2::pbes_system::imp::left
const pbes_expression & left() const
Definition pbes_expression.h:465
mcrl2::pbes_system::imp::right
const pbes_expression & right() const
Definition pbes_expression.h:470
mcrl2::pbes_system::not_
\brief The not operator for pbes expressions
Definition pbes_expression.h:216
mcrl2::pbes_system::not_::operand
const pbes_expression & operand() const
Definition pbes_expression.h:242
mcrl2::pbes_system::or_
\brief The or operator for pbes expressions
Definition pbes_expression.h:363
mcrl2::pbes_system::or_::left
const pbes_expression & left() const
Definition pbes_expression.h:389
mcrl2::pbes_system::or_::right
const pbes_expression & right() const
Definition pbes_expression.h:394
mcrl2::pbes_system::pbes_equation
pbes equation.
Definition pbes_equation.h:29
mcrl2::pbes_system::pbes_equation::formula
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
Definition pbes_equation.h:95
mcrl2::pbes_system::pbes_equation::is_solved
bool is_solved() const
Returns true if the predicate formula on the right hand side contains no predicate variables.
Definition pbes.cpp:102
mcrl2::pbes_system::pbes_equation::variable
const propositional_variable & variable() const
Returns the pbes variable of the equation.
Definition pbes_equation.h:81
mcrl2::pbes_system::pbes_expression
\brief A pbes expression
Definition pbes_expression.h:25
mcrl2::pbes_system::pbes
parameterized boolean equation system
Definition pbes.h:54
mcrl2::pbes_system::pbes::initial_state
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:187
mcrl2::pbes_system::pbes::occurring_variable_instantiations
std::set< propositional_variable_instantiation > occurring_variable_instantiations() const
Returns the set of occurring propositional variable instantiations of the pbes. This is the set of va...
Definition pbes.cpp:107
mcrl2::pbes_system::propositional_variable_instantiation
\brief A propositional variable instantiation
Definition pbes_expression.h:111
mcrl2::pbes_system::propositional_variable_instantiation::parameters
const data::data_expression_list & parameters() const
Definition pbes_expression.h:126
mcrl2::pbes_system::propositional_variable_instantiation::name
const core::identifier_string & name() const
Definition pbes_expression.h:121
mcrl2::pbes_system::propositional_variable
\brief A propositional variable declaration
Definition propositional_variable.h:24
mcrl2::pbes_system::propositional_variable::parameters
const data::variable_list & parameters() const
Definition propositional_variable.h:60
mcrl2::pbes_system::propositional_variable::name
const core::identifier_string & name() const
Definition propositional_variable.h:55
parser_tables_mcrl2
D_ParserTables parser_tables_mcrl2
mcrl2::core::warn_and_or
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
Definition parser_utility.h:215
mcrl2::data::is_data_expression
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
Definition data_expression.h:232
mcrl2::data::is_untyped_data_parameter
bool is_untyped_data_parameter(const atermpp::aterm &x)
Definition untyped_data_parameter.h:84
mcrl2::pbes_system::algorithms::instantiate_global_variables
void instantiate_global_variables(pbes &p)
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them....
Definition pbes.cpp:64
mcrl2::pbes_system::algorithms::is_bes
bool is_bes(const pbes &x)
Returns true if a PBES is in BES form.
Definition pbes.cpp:69
mcrl2::pbes_system::detail
Definition pbesinst_finite_algorithm.h:88
mcrl2::pbes_system::detail::parse_pbes_new
untyped_pbes parse_pbes_new(const std::string &text)
Definition pbes.cpp:132
mcrl2::pbes_system::detail::complete_pbes
void complete_pbes(pbes &x)
Definition pbes.cpp:143
mcrl2::pbes_system::detail::has_propositional_variables
bool has_propositional_variables(const pbes_expression &x)
Definition has_propositional_variables.h:36
mcrl2::pbes_system::detail::parse_propositional_variable
propositional_variable parse_propositional_variable(const std::string &text)
Definition pbes.cpp:150
mcrl2::pbes_system::detail::parse_pbes_expression
pbes_expression parse_pbes_expression(const std::string &text)
Definition pbes.cpp:159
mcrl2::pbes_system::detail::is_well_typed
bool is_well_typed(const pbes_equation &eqn)
Checks if the equation is well typed.
Definition is_well_typed.h:154
mcrl2::pbes_system::detail::parse_pbes_expression_new
pbes_expression parse_pbes_expression_new(const std::string &text)
Definition pbes.cpp:121
mcrl2::pbes_system
The main namespace for the PBES library.
Definition algorithms.cpp:22
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_equation &x)
Definition pbes.cpp:55
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_list &x, bool arg0)
Definition pbes.cpp:30
mcrl2::pbes_system::pp
std::string pp(const pbes_system::or_ &x, bool arg0)
Definition pbes.cpp:40
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
Definition pbes.cpp:53
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
Definition pbes.cpp:46
mcrl2::pbes_system::pp
std::string pp(const pbes_system::imp &x, bool arg0)
Definition pbes.cpp:38
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
Definition pbes.cpp:32
mcrl2::pbes_system::normalize_sorts
pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
Definition pbes.cpp:48
mcrl2::pbes_system::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
Definition pbes.cpp:51
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation_vector &x, bool arg0)
Definition pbes.cpp:27
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression_list &x, bool arg0)
Definition pbes.cpp:28
mcrl2::pbes_system::is_not
bool is_not(const atermpp::aterm &x)
Definition pbes_expression.h:260
mcrl2::pbes_system::find_propositional_variable_instantiations
std::set< pbes_system::propositional_variable_instantiation > find_propositional_variable_instantiations(const pbes_system::pbes_expression &x)
Definition pbes.cpp:57
mcrl2::pbes_system::is_exists
bool is_exists(const atermpp::aterm &x)
Definition pbes_expression.h:640
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
Definition pbes.cpp:47
mcrl2::pbes_system::is_or
bool is_or(const atermpp::aterm &x)
Definition pbes_expression.h:412
mcrl2::pbes_system::is_well_typed_pbes
bool is_well_typed_pbes(const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
Definition pbes.cpp:90
mcrl2::pbes_system::find_function_symbols
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
Definition pbes.cpp:56
mcrl2::pbes_system::is_forall
bool is_forall(const atermpp::aterm &x)
Definition pbes_expression.h:564
mcrl2::pbes_system::typecheck_pbes
void typecheck_pbes(pbes &pbesspec)
Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.
Definition typecheck.h:272
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable &x, bool arg0)
Definition pbes.cpp:44
mcrl2::pbes_system::pp
std::string pp(const pbes_system::exists &x, bool arg0)
Definition pbes.cpp:35
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression &x, bool arg0)
Definition pbes.cpp:43
mcrl2::pbes_system::is_well_typed
bool is_well_typed(const pbes_equation &eqn)
Definition pbes.cpp:76
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_expression &x)
Definition pbes.cpp:54
mcrl2::pbes_system::translate_user_notation
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
Definition pbes.cpp:50
mcrl2::pbes_system::search_variable
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
Definition pbes.cpp:59
mcrl2::pbes_system::find_all_variables
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
Definition pbes.cpp:52
mcrl2::pbes_system::pp
std::string pp(const pbes_system::not_ &x, bool arg0)
Definition pbes.cpp:39
mcrl2::pbes_system::complete_data_specification
void complete_data_specification(pbes &)
Adds all sorts that appear in the PBES p to the data specification of p.
Definition pbes.h:307
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation &x, bool arg0)
Definition pbes.cpp:42
mcrl2::pbes_system::find_identifiers
std::set< core::identifier_string > find_identifiers(const pbes_system::pbes_expression &x)
Definition pbes.cpp:58
mcrl2::pbes_system::is_propositional_variable_instantiation
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
Definition pbes_expression.h:189
mcrl2::pbes_system::is_well_typed_equation
bool is_well_typed_equation(const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
Definition pbes.cpp:81
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation &x, bool arg0)
Definition pbes.cpp:45
mcrl2::pbes_system::is_and
bool is_and(const atermpp::aterm &x)
Definition pbes_expression.h:336
mcrl2::pbes_system::translate_user_notation
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:49
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes &x, bool arg0)
Definition pbes.cpp:41
mcrl2::pbes_system::is_imp
bool is_imp(const atermpp::aterm &x)
Definition pbes_expression.h:488
mcrl2::pbes_system::pp
std::string pp(const pbes_system::and_ &x, bool arg0)
Definition pbes.cpp:34
mcrl2::pbes_system::pp
std::string pp(const pbes_system::fixpoint_symbol &x, bool arg0)
Definition pbes.cpp:36
mcrl2::pbes_system::pp
std::string pp(const pbes_system::forall &x, bool arg0)
Definition pbes.cpp:37
mcrl2::core::traverser
expression traverser that visits all sub expressions
Definition traverser.h:29
mcrl2::pbes_system::add_traverser_data_expressions
Definition traverser.h:185
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:236
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:213
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:206
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:251
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:198
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:191
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:258
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:228
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:220
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:244
mcrl2::pbes_system::add_traverser_identifier_strings
Definition traverser.h:576
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:598
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:662
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:654
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:622
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:615
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:582
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:638
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:646
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:630
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:590
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:607
mcrl2::pbes_system::add_traverser_pbes_expressions
Definition traverser.h:312
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:332
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:346
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:370
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:318
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:354
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:362
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:384
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:377
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:339
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:325
mcrl2::pbes_system::add_traverser_sort_expressions
Definition traverser.h:47
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:123
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:99
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:77
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:53
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:107
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:91
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:68
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:115
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:60
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:131
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:84
mcrl2::pbes_system::add_traverser_variables
Definition traverser.h:438
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:459
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:444
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:490
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:468
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:475
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:514
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:482
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:498
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:522
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:451
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:506
mcrl2::pbes_system::data_expression_traverser
\brief Traverser class
Definition traverser.h:305
mcrl2::pbes_system::detail::has_propositional_variables_traverser
Definition has_propositional_variables.h:21
mcrl2::pbes_system::detail::has_propositional_variables_traverser::result
bool result
Definition has_propositional_variables.h:27
mcrl2::pbes_system::detail::has_propositional_variables_traverser::enter
void enter(const propositional_variable_instantiation &)
Definition has_propositional_variables.h:29
mcrl2::pbes_system::detail::pbes_actions
Definition parse_impl.h:24
mcrl2::pbes_system::detail::pbes_actions::parse_PropVarDecl
pbes_system::propositional_variable parse_PropVarDecl(const core::parse_node &node) const
Definition parse_impl.h:47
mcrl2::pbes_system::detail::pbes_actions::pbes_actions
pbes_actions(const core::parser &parser_)
Definition parse_impl.h:25
mcrl2::pbes_system::detail::pbes_actions::parse_PbesSpec
untyped_pbes parse_PbesSpec(const core::parse_node &node) const
Definition parse_impl.h:84
mcrl2::pbes_system::detail::pbes_actions::parse_PbesExpr
pbes_system::pbes_expression parse_PbesExpr(const core::parse_node &node) const
Definition parse_impl.h:29
mcrl2::pbes_system::identifier_string_traverser
\brief Traverser class
Definition traverser.h:709
mcrl2::pbes_system::pbes_expression_traverser_base
Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
Definition traverser.h:23
mcrl2::pbes_system::pbes_expression_traverser_base::apply
void apply(const data::data_expression &x)
Definition traverser.h:29
mcrl2::pbes_system::pbes_expression_traverser_base::apply
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:36
mcrl2::pbes_system::pbes_expression_traverser
\brief Traverser class
Definition traverser.h:431
mcrl2::pbes_system::pg_actions
Definition pg_parse.h:75
mcrl2::pbes_system::sort_expression_traverser
\brief Traverser class
Definition traverser.h:178
mcrl2::pbes_system::untyped_pbes
Definition untyped_pbes.h:21
mcrl2::pbes_system::variable_traverser
\brief Traverser class
Definition traverser.h:569