mCRL2
Loading...
Searching...
No Matches
builder.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_BUILDER_H
13#define MCRL2_MODAL_FORMULA_BUILDER_H
14
15#include "mcrl2/lps/builder.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_builder_base: public core::builder<Derived>
27{
28 typedef core::builder<Derived> super;
29 using super::apply;
30
31 template <class T>
32 void apply(T& result, const data::data_expression& x)
33 {
34 static_cast<Derived&>(*this).enter(x);
35 // skip
36 static_cast<Derived&>(*this).leave(x);
37 result = x;
38 }
39};
40
41//--- start generated action_formulas::add_sort_expressions code ---//
42template <template <class> class Builder, class Derived>
43struct add_sort_expressions: public Builder<Derived>
44{
45 typedef Builder<Derived> super;
46 using super::enter;
47 using super::leave;
48 using super::update;
49 using super::apply;
50
51 template <class T>
52 void apply(T& result, const action_formulas::true_& x)
53 {
54
55 result = x;
56 static_cast<Derived&>(*this).enter(x);
57 // skip
58 static_cast<Derived&>(*this).leave(x);
59 result = x;
60 }
61
62 template <class T>
63 void apply(T& result, const action_formulas::false_& x)
64 {
65
66 result = x;
67 static_cast<Derived&>(*this).enter(x);
68 // skip
69 static_cast<Derived&>(*this).leave(x);
70 result = x;
71 }
72
73 template <class T>
74 void apply(T& result, const action_formulas::not_& x)
75 {
76
77 static_cast<Derived&>(*this).enter(x);
78 action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
79 static_cast<Derived&>(*this).leave(x);
80 }
81
82 template <class T>
83 void apply(T& result, const action_formulas::and_& x)
84 {
85
86 static_cast<Derived&>(*this).enter(x);
87 action_formulas::make_and_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
88 static_cast<Derived&>(*this).leave(x);
89 }
90
91 template <class T>
92 void apply(T& result, const action_formulas::or_& x)
93 {
94
95 static_cast<Derived&>(*this).enter(x);
96 action_formulas::make_or_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
97 static_cast<Derived&>(*this).leave(x);
98 }
99
100 template <class T>
101 void apply(T& result, const action_formulas::imp& x)
102 {
103
104 static_cast<Derived&>(*this).enter(x);
105 action_formulas::make_imp(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
106 static_cast<Derived&>(*this).leave(x);
107 }
108
109 template <class T>
110 void apply(T& result, const action_formulas::forall& x)
111 {
112
113 static_cast<Derived&>(*this).enter(x);
114 action_formulas::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
115 static_cast<Derived&>(*this).leave(x);
116 }
117
118 template <class T>
119 void apply(T& result, const action_formulas::exists& x)
120 {
121
122 static_cast<Derived&>(*this).enter(x);
123 action_formulas::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
124 static_cast<Derived&>(*this).leave(x);
125 }
126
127 template <class T>
128 void apply(T& result, const action_formulas::at& x)
129 {
130
131 static_cast<Derived&>(*this).enter(x);
132 action_formulas::make_at(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
133 static_cast<Derived&>(*this).leave(x);
134 }
135
136 template <class T>
137 void apply(T& result, const action_formulas::multi_action& x)
138 {
139
140 static_cast<Derived&>(*this).enter(x);
141 action_formulas::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
142 static_cast<Derived&>(*this).leave(x);
143 }
144
145 template <class T>
146 void apply(T& result, const action_formulas::action_formula& x)
147 {
148
149 static_cast<Derived&>(*this).enter(x);
150 if (data::is_data_expression(x))
151 {
152 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
153 }
154 else if (data::is_untyped_data_parameter(x))
155 {
156 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
157 }
158 else if (action_formulas::is_true(x))
159 {
160 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
161 }
162 else if (action_formulas::is_false(x))
163 {
164 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
165 }
166 else if (action_formulas::is_not(x))
167 {
168 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
169 }
170 else if (action_formulas::is_and(x))
171 {
172 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
173 }
174 else if (action_formulas::is_or(x))
175 {
176 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
177 }
178 else if (action_formulas::is_imp(x))
179 {
180 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
181 }
182 else if (action_formulas::is_forall(x))
183 {
184 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
185 }
186 else if (action_formulas::is_exists(x))
187 {
188 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
189 }
190 else if (action_formulas::is_at(x))
191 {
192 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
193 }
194 else if (action_formulas::is_multi_action(x))
195 {
196 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
197 }
198 else if (process::is_untyped_multi_action(x))
199 {
200 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
201 }
202 static_cast<Derived&>(*this).leave(x);
203 }
204
205};
206
208template <typename Derived>
209struct sort_expression_builder: public add_sort_expressions<lps::sort_expression_builder, Derived>
210{
211};
212//--- end generated action_formulas::add_sort_expressions code ---//
213
214//--- start generated action_formulas::add_data_expressions code ---//
215template <template <class> class Builder, class Derived>
216struct add_data_expressions: public Builder<Derived>
217{
218 typedef Builder<Derived> super;
219 using super::enter;
220 using super::leave;
221 using super::update;
222 using super::apply;
223
224 template <class T>
225 void apply(T& result, const action_formulas::true_& x)
226 {
227
228 result = x;
229 static_cast<Derived&>(*this).enter(x);
230 // skip
231 static_cast<Derived&>(*this).leave(x);
232 result = x;
233 }
234
235 template <class T>
236 void apply(T& result, const action_formulas::false_& x)
237 {
238
239 result = x;
240 static_cast<Derived&>(*this).enter(x);
241 // skip
242 static_cast<Derived&>(*this).leave(x);
243 result = x;
244 }
245
246 template <class T>
247 void apply(T& result, const action_formulas::not_& x)
248 {
249
250 static_cast<Derived&>(*this).enter(x);
251 action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
252 static_cast<Derived&>(*this).leave(x);
253 }
254
255 template <class T>
256 void apply(T& result, const action_formulas::and_& x)
257 {
258
259 static_cast<Derived&>(*this).enter(x);
260 action_formulas::make_and_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
261 static_cast<Derived&>(*this).leave(x);
262 }
263
264 template <class T>
265 void apply(T& result, const action_formulas::or_& x)
266 {
267
268 static_cast<Derived&>(*this).enter(x);
269 action_formulas::make_or_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
270 static_cast<Derived&>(*this).leave(x);
271 }
272
273 template <class T>
274 void apply(T& result, const action_formulas::imp& x)
275 {
276
277 static_cast<Derived&>(*this).enter(x);
278 action_formulas::make_imp(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
279 static_cast<Derived&>(*this).leave(x);
280 }
281
282 template <class T>
283 void apply(T& result, const action_formulas::forall& x)
284 {
285
286 static_cast<Derived&>(*this).enter(x);
287 action_formulas::make_forall(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
288 static_cast<Derived&>(*this).leave(x);
289 }
290
291 template <class T>
292 void apply(T& result, const action_formulas::exists& x)
293 {
294
295 static_cast<Derived&>(*this).enter(x);
296 action_formulas::make_exists(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
297 static_cast<Derived&>(*this).leave(x);
298 }
299
300 template <class T>
301 void apply(T& result, const action_formulas::at& x)
302 {
303
304 static_cast<Derived&>(*this).enter(x);
305 action_formulas::make_at(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
306 static_cast<Derived&>(*this).leave(x);
307 }
308
309 template <class T>
310 void apply(T& result, const action_formulas::multi_action& x)
311 {
312
313 static_cast<Derived&>(*this).enter(x);
314 action_formulas::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
315 static_cast<Derived&>(*this).leave(x);
316 }
317
318 template <class T>
319 void apply(T& result, const action_formulas::action_formula& x)
320 {
321
322 static_cast<Derived&>(*this).enter(x);
323 if (data::is_data_expression(x))
324 {
325 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
326 }
327 else if (data::is_untyped_data_parameter(x))
328 {
329 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
330 }
331 else if (action_formulas::is_true(x))
332 {
333 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
334 }
335 else if (action_formulas::is_false(x))
336 {
337 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
338 }
339 else if (action_formulas::is_not(x))
340 {
341 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
342 }
343 else if (action_formulas::is_and(x))
344 {
345 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
346 }
347 else if (action_formulas::is_or(x))
348 {
349 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
350 }
351 else if (action_formulas::is_imp(x))
352 {
353 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
354 }
355 else if (action_formulas::is_forall(x))
356 {
357 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
358 }
359 else if (action_formulas::is_exists(x))
360 {
361 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
362 }
363 else if (action_formulas::is_at(x))
364 {
365 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
366 }
367 else if (action_formulas::is_multi_action(x))
368 {
369 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
370 }
371 else if (process::is_untyped_multi_action(x))
372 {
373 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
374 }
375 static_cast<Derived&>(*this).leave(x);
376 }
377
378};
379
381template <typename Derived>
382struct data_expression_builder: public add_data_expressions<lps::data_expression_builder, Derived>
383{
384};
385//--- end generated action_formulas::add_data_expressions code ---//
386
387//--- start generated action_formulas::add_variables code ---//
388template <template <class> class Builder, class Derived>
389struct add_variables: public Builder<Derived>
390{
391 typedef Builder<Derived> super;
392 using super::enter;
393 using super::leave;
394 using super::update;
395 using super::apply;
396
397 template <class T>
398 void apply(T& result, const action_formulas::true_& x)
399 {
400
401 result = x;
402 static_cast<Derived&>(*this).enter(x);
403 // skip
404 static_cast<Derived&>(*this).leave(x);
405 result = x;
406 }
407
408 template <class T>
409 void apply(T& result, const action_formulas::false_& x)
410 {
411
412 result = x;
413 static_cast<Derived&>(*this).enter(x);
414 // skip
415 static_cast<Derived&>(*this).leave(x);
416 result = x;
417 }
418
419 template <class T>
420 void apply(T& result, const action_formulas::not_& x)
421 {
422
423 static_cast<Derived&>(*this).enter(x);
424 action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
425 static_cast<Derived&>(*this).leave(x);
426 }
427
428 template <class T>
429 void apply(T& result, const action_formulas::and_& x)
430 {
431
432 static_cast<Derived&>(*this).enter(x);
433 action_formulas::make_and_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
434 static_cast<Derived&>(*this).leave(x);
435 }
436
437 template <class T>
438 void apply(T& result, const action_formulas::or_& x)
439 {
440
441 static_cast<Derived&>(*this).enter(x);
442 action_formulas::make_or_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
443 static_cast<Derived&>(*this).leave(x);
444 }
445
446 template <class T>
447 void apply(T& result, const action_formulas::imp& x)
448 {
449
450 static_cast<Derived&>(*this).enter(x);
451 action_formulas::make_imp(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
452 static_cast<Derived&>(*this).leave(x);
453 }
454
455 template <class T>
456 void apply(T& result, const action_formulas::forall& x)
457 {
458
459 static_cast<Derived&>(*this).enter(x);
460 action_formulas::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
461 static_cast<Derived&>(*this).leave(x);
462 }
463
464 template <class T>
465 void apply(T& result, const action_formulas::exists& x)
466 {
467
468 static_cast<Derived&>(*this).enter(x);
469 action_formulas::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
470 static_cast<Derived&>(*this).leave(x);
471 }
472
473 template <class T>
474 void apply(T& result, const action_formulas::at& x)
475 {
476
477 static_cast<Derived&>(*this).enter(x);
478 action_formulas::make_at(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
479 static_cast<Derived&>(*this).leave(x);
480 }
481
482 template <class T>
483 void apply(T& result, const action_formulas::multi_action& x)
484 {
485
486 static_cast<Derived&>(*this).enter(x);
487 action_formulas::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
488 static_cast<Derived&>(*this).leave(x);
489 }
490
491 template <class T>
492 void apply(T& result, const action_formulas::action_formula& x)
493 {
494
495 static_cast<Derived&>(*this).enter(x);
496 if (data::is_data_expression(x))
497 {
498 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
499 }
500 else if (data::is_untyped_data_parameter(x))
501 {
502 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
503 }
504 else if (action_formulas::is_true(x))
505 {
506 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
507 }
508 else if (action_formulas::is_false(x))
509 {
510 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
511 }
512 else if (action_formulas::is_not(x))
513 {
514 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
515 }
516 else if (action_formulas::is_and(x))
517 {
518 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
519 }
520 else if (action_formulas::is_or(x))
521 {
522 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
523 }
524 else if (action_formulas::is_imp(x))
525 {
526 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
527 }
528 else if (action_formulas::is_forall(x))
529 {
530 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
531 }
532 else if (action_formulas::is_exists(x))
533 {
534 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
535 }
536 else if (action_formulas::is_at(x))
537 {
538 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
539 }
540 else if (action_formulas::is_multi_action(x))
541 {
542 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
543 }
544 else if (process::is_untyped_multi_action(x))
545 {
546 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
547 }
548 static_cast<Derived&>(*this).leave(x);
549 }
550
551};
552
554template <typename Derived>
555struct variable_builder: public add_variables<lps::data_expression_builder, Derived>
556{
557};
558//--- end generated action_formulas::add_variables code ---//
559
560//--- start generated action_formulas::add_action_formula_expressions code ---//
561template <template <class> class Builder, class Derived>
562struct add_action_formula_expressions: public Builder<Derived>
563{
564 typedef Builder<Derived> super;
565 using super::enter;
566 using super::leave;
567 using super::update;
568 using super::apply;
569
570 template <class T>
571 void apply(T& result, const action_formulas::true_& x)
572 {
573
574 result = x;
575 static_cast<Derived&>(*this).enter(x);
576 // skip
577 static_cast<Derived&>(*this).leave(x);
578 result = x;
579 }
580
581 template <class T>
582 void apply(T& result, const action_formulas::false_& x)
583 {
584
585 result = x;
586 static_cast<Derived&>(*this).enter(x);
587 // skip
588 static_cast<Derived&>(*this).leave(x);
589 result = x;
590 }
591
592 template <class T>
593 void apply(T& result, const action_formulas::not_& x)
594 {
595
596 static_cast<Derived&>(*this).enter(x);
597 action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
598 static_cast<Derived&>(*this).leave(x);
599 }
600
601 template <class T>
602 void apply(T& result, const action_formulas::and_& x)
603 {
604
605 static_cast<Derived&>(*this).enter(x);
606 action_formulas::make_and_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
607 static_cast<Derived&>(*this).leave(x);
608 }
609
610 template <class T>
611 void apply(T& result, const action_formulas::or_& x)
612 {
613
614 static_cast<Derived&>(*this).enter(x);
615 action_formulas::make_or_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
616 static_cast<Derived&>(*this).leave(x);
617 }
618
619 template <class T>
620 void apply(T& result, const action_formulas::imp& x)
621 {
622
623 static_cast<Derived&>(*this).enter(x);
624 action_formulas::make_imp(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
625 static_cast<Derived&>(*this).leave(x);
626 }
627
628 template <class T>
629 void apply(T& result, const action_formulas::forall& x)
630 {
631
632 static_cast<Derived&>(*this).enter(x);
633 action_formulas::make_forall(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
634 static_cast<Derived&>(*this).leave(x);
635 }
636
637 template <class T>
638 void apply(T& result, const action_formulas::exists& x)
639 {
640
641 static_cast<Derived&>(*this).enter(x);
642 action_formulas::make_exists(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
643 static_cast<Derived&>(*this).leave(x);
644 }
645
646 template <class T>
647 void apply(T& result, const action_formulas::at& x)
648 {
649
650 static_cast<Derived&>(*this).enter(x);
651 action_formulas::make_at(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, x.time_stamp());
652 static_cast<Derived&>(*this).leave(x);
653 }
654
655 template <class T>
656 void apply(T& result, const action_formulas::multi_action& x)
657 {
658
659 result = x;
660 static_cast<Derived&>(*this).enter(x);
661 // skip
662 static_cast<Derived&>(*this).leave(x);
663 result = x;
664 }
665
666 template <class T>
667 void apply(T& result, const action_formulas::action_formula& x)
668 {
669
670 static_cast<Derived&>(*this).enter(x);
671 if (data::is_data_expression(x))
672 {
673 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
674 }
675 else if (data::is_untyped_data_parameter(x))
676 {
677 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
678 }
679 else if (action_formulas::is_true(x))
680 {
681 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
682 }
683 else if (action_formulas::is_false(x))
684 {
685 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
686 }
687 else if (action_formulas::is_not(x))
688 {
689 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
690 }
691 else if (action_formulas::is_and(x))
692 {
693 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
694 }
695 else if (action_formulas::is_or(x))
696 {
697 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
698 }
699 else if (action_formulas::is_imp(x))
700 {
701 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
702 }
703 else if (action_formulas::is_forall(x))
704 {
705 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
706 }
707 else if (action_formulas::is_exists(x))
708 {
709 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
710 }
711 else if (action_formulas::is_at(x))
712 {
713 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
714 }
715 else if (action_formulas::is_multi_action(x))
716 {
717 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
718 }
719 else if (process::is_untyped_multi_action(x))
720 {
721 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
722 }
723 static_cast<Derived&>(*this).leave(x);
724 }
725
726};
727
729template <typename Derived>
730struct action_formula_builder: public add_action_formula_expressions<action_formulas::action_formula_builder_base, Derived>
731{
732};
733//--- end generated action_formulas::add_action_formula_expressions code ---//
734
735} // namespace action_formulas
736
737namespace regular_formulas
738{
739
741template <typename Derived>
742struct regular_formula_builder_base: public core::builder<Derived>
743{
744 typedef core::builder<Derived> super;
745 using super::apply;
746
747 template <class T>
748 void apply(T& result, const data::data_expression& x)
749 // void apply(regular_formula& result, const data::data_expression& x)
750 {
751 static_cast<Derived&>(*this).enter(x);
752 // skip
753 static_cast<Derived&>(*this).leave(x);
754 result = x;
755 }
756
757 template <class T>
758 void apply(T& result, const action_formulas::action_formula& x)
759 // void apply(regular_formula& result, const action_formulas::action_formula& x)
760 {
761 static_cast<Derived&>(*this).enter(x);
762 // skip
763 static_cast<Derived&>(*this).leave(x);
764 result = x;
765 }
766};
767
768//--- start generated regular_formulas::add_sort_expressions code ---//
769template <template <class> class Builder, class Derived>
770struct add_sort_expressions: public Builder<Derived>
771{
772 typedef Builder<Derived> super;
773 using super::enter;
774 using super::leave;
775 using super::update;
776 using super::apply;
777
778 template <class T>
779 void apply(T& result, const regular_formulas::seq& x)
780 {
781
782 static_cast<Derived&>(*this).enter(x);
783 regular_formulas::make_seq(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
784 static_cast<Derived&>(*this).leave(x);
785 }
786
787 template <class T>
788 void apply(T& result, const regular_formulas::alt& x)
789 {
790
791 static_cast<Derived&>(*this).enter(x);
792 regular_formulas::make_alt(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
793 static_cast<Derived&>(*this).leave(x);
794 }
795
796 template <class T>
797 void apply(T& result, const regular_formulas::trans& x)
798 {
799
800 static_cast<Derived&>(*this).enter(x);
801 regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
802 static_cast<Derived&>(*this).leave(x);
803 }
804
805 template <class T>
806 void apply(T& result, const regular_formulas::trans_or_nil& x)
807 {
808
809 static_cast<Derived&>(*this).enter(x);
810 regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
811 static_cast<Derived&>(*this).leave(x);
812 }
813
814 template <class T>
815 void apply(T& result, const regular_formulas::untyped_regular_formula& x)
816 {
817
818 static_cast<Derived&>(*this).enter(x);
819 regular_formulas::make_untyped_regular_formula(result, x.name(), [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
820 static_cast<Derived&>(*this).leave(x);
821 }
822
823 template <class T>
824 void apply(T& result, const regular_formulas::regular_formula& x)
825 {
826
827 static_cast<Derived&>(*this).enter(x);
828 if (data::is_data_expression(x))
829 {
830 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
831 }
832 else if (action_formulas::is_action_formula(x))
833 {
834 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
835 }
836 else if (regular_formulas::is_seq(x))
837 {
838 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
839 }
840 else if (regular_formulas::is_alt(x))
841 {
842 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
843 }
844 else if (regular_formulas::is_trans(x))
845 {
846 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
847 }
848 else if (regular_formulas::is_trans_or_nil(x))
849 {
850 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
851 }
852 else if (regular_formulas::is_untyped_regular_formula(x))
853 {
854 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
855 }
856 static_cast<Derived&>(*this).leave(x);
857 }
858
859};
860
862template <typename Derived>
863struct sort_expression_builder: public add_sort_expressions<action_formulas::sort_expression_builder, Derived>
864{
865};
866//--- end generated regular_formulas::add_sort_expressions code ---//
867
868//--- start generated regular_formulas::add_data_expressions code ---//
869template <template <class> class Builder, class Derived>
870struct add_data_expressions: public Builder<Derived>
871{
872 typedef Builder<Derived> super;
873 using super::enter;
874 using super::leave;
875 using super::update;
876 using super::apply;
877
878 template <class T>
879 void apply(T& result, const regular_formulas::seq& x)
880 {
881
882 static_cast<Derived&>(*this).enter(x);
883 regular_formulas::make_seq(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
884 static_cast<Derived&>(*this).leave(x);
885 }
886
887 template <class T>
888 void apply(T& result, const regular_formulas::alt& x)
889 {
890
891 static_cast<Derived&>(*this).enter(x);
892 regular_formulas::make_alt(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
893 static_cast<Derived&>(*this).leave(x);
894 }
895
896 template <class T>
897 void apply(T& result, const regular_formulas::trans& x)
898 {
899
900 static_cast<Derived&>(*this).enter(x);
901 regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
902 static_cast<Derived&>(*this).leave(x);
903 }
904
905 template <class T>
906 void apply(T& result, const regular_formulas::trans_or_nil& x)
907 {
908
909 static_cast<Derived&>(*this).enter(x);
910 regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
911 static_cast<Derived&>(*this).leave(x);
912 }
913
914 template <class T>
915 void apply(T& result, const regular_formulas::untyped_regular_formula& x)
916 {
917
918 static_cast<Derived&>(*this).enter(x);
919 regular_formulas::make_untyped_regular_formula(result, x.name(), [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
920 static_cast<Derived&>(*this).leave(x);
921 }
922
923 template <class T>
924 void apply(T& result, const regular_formulas::regular_formula& x)
925 {
926
927 static_cast<Derived&>(*this).enter(x);
928 if (data::is_data_expression(x))
929 {
930 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
931 }
932 else if (action_formulas::is_action_formula(x))
933 {
934 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
935 }
936 else if (regular_formulas::is_seq(x))
937 {
938 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
939 }
940 else if (regular_formulas::is_alt(x))
941 {
942 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
943 }
944 else if (regular_formulas::is_trans(x))
945 {
946 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
947 }
948 else if (regular_formulas::is_trans_or_nil(x))
949 {
950 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
951 }
952 else if (regular_formulas::is_untyped_regular_formula(x))
953 {
954 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
955 }
956 static_cast<Derived&>(*this).leave(x);
957 }
958
959};
960
962template <typename Derived>
963struct data_expression_builder: public add_data_expressions<action_formulas::data_expression_builder, Derived>
964{
965};
966//--- end generated regular_formulas::add_data_expressions code ---//
967
968//--- start generated regular_formulas::add_variables code ---//
969template <template <class> class Builder, class Derived>
970struct add_variables: public Builder<Derived>
971{
972 typedef Builder<Derived> super;
973 using super::enter;
974 using super::leave;
975 using super::update;
976 using super::apply;
977
978 template <class T>
979 void apply(T& result, const regular_formulas::seq& x)
980 {
981
982 static_cast<Derived&>(*this).enter(x);
983 regular_formulas::make_seq(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
984 static_cast<Derived&>(*this).leave(x);
985 }
986
987 template <class T>
988 void apply(T& result, const regular_formulas::alt& x)
989 {
990
991 static_cast<Derived&>(*this).enter(x);
992 regular_formulas::make_alt(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
993 static_cast<Derived&>(*this).leave(x);
994 }
995
996 template <class T>
997 void apply(T& result, const regular_formulas::trans& x)
998 {
999
1000 static_cast<Derived&>(*this).enter(x);
1001 regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1002 static_cast<Derived&>(*this).leave(x);
1003 }
1004
1005 template <class T>
1006 void apply(T& result, const regular_formulas::trans_or_nil& x)
1007 {
1008
1009 static_cast<Derived&>(*this).enter(x);
1010 regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1011 static_cast<Derived&>(*this).leave(x);
1012 }
1013
1014 template <class T>
1015 void apply(T& result, const regular_formulas::untyped_regular_formula& x)
1016 {
1017
1018 static_cast<Derived&>(*this).enter(x);
1019 regular_formulas::make_untyped_regular_formula(result, x.name(), [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1020 static_cast<Derived&>(*this).leave(x);
1021 }
1022
1023 template <class T>
1024 void apply(T& result, const regular_formulas::regular_formula& x)
1025 {
1026
1027 static_cast<Derived&>(*this).enter(x);
1028 if (data::is_data_expression(x))
1029 {
1030 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1031 }
1032 else if (action_formulas::is_action_formula(x))
1033 {
1034 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
1035 }
1036 else if (regular_formulas::is_seq(x))
1037 {
1038 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
1039 }
1040 else if (regular_formulas::is_alt(x))
1041 {
1042 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
1043 }
1044 else if (regular_formulas::is_trans(x))
1045 {
1046 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
1047 }
1048 else if (regular_formulas::is_trans_or_nil(x))
1049 {
1050 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1051 }
1052 else if (regular_formulas::is_untyped_regular_formula(x))
1053 {
1054 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1055 }
1056 static_cast<Derived&>(*this).leave(x);
1057 }
1058
1059};
1060
1062template <typename Derived>
1063struct variable_builder: public add_variables<action_formulas::data_expression_builder, Derived>
1064{
1065};
1066//--- end generated regular_formulas::add_variables code ---//
1067
1068//--- start generated regular_formulas::add_regular_formula_expressions code ---//
1069template <template <class> class Builder, class Derived>
1070struct add_regular_formula_expressions: public Builder<Derived>
1071{
1072 typedef Builder<Derived> super;
1073 using super::enter;
1074 using super::leave;
1075 using super::update;
1076 using super::apply;
1077
1078 template <class T>
1079 void apply(T& result, const regular_formulas::seq& x)
1080 {
1081
1082 static_cast<Derived&>(*this).enter(x);
1083 regular_formulas::make_seq(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1084 static_cast<Derived&>(*this).leave(x);
1085 }
1086
1087 template <class T>
1088 void apply(T& result, const regular_formulas::alt& x)
1089 {
1090
1091 static_cast<Derived&>(*this).enter(x);
1092 regular_formulas::make_alt(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1093 static_cast<Derived&>(*this).leave(x);
1094 }
1095
1096 template <class T>
1097 void apply(T& result, const regular_formulas::trans& x)
1098 {
1099
1100 static_cast<Derived&>(*this).enter(x);
1101 regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1102 static_cast<Derived&>(*this).leave(x);
1103 }
1104
1105 template <class T>
1106 void apply(T& result, const regular_formulas::trans_or_nil& x)
1107 {
1108
1109 static_cast<Derived&>(*this).enter(x);
1110 regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1111 static_cast<Derived&>(*this).leave(x);
1112 }
1113
1114 template <class T>
1115 void apply(T& result, const regular_formulas::untyped_regular_formula& x)
1116 {
1117
1118 static_cast<Derived&>(*this).enter(x);
1119 regular_formulas::make_untyped_regular_formula(result, x.name(), [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1120 static_cast<Derived&>(*this).leave(x);
1121 }
1122
1123 template <class T>
1124 void apply(T& result, const regular_formulas::regular_formula& x)
1125 {
1126
1127 static_cast<Derived&>(*this).enter(x);
1128 if (data::is_data_expression(x))
1129 {
1130 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1131 }
1132 else if (action_formulas::is_action_formula(x))
1133 {
1134 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
1135 }
1136 else if (regular_formulas::is_seq(x))
1137 {
1138 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
1139 }
1140 else if (regular_formulas::is_alt(x))
1141 {
1142 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
1143 }
1144 else if (regular_formulas::is_trans(x))
1145 {
1146 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
1147 }
1148 else if (regular_formulas::is_trans_or_nil(x))
1149 {
1150 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1151 }
1152 else if (regular_formulas::is_untyped_regular_formula(x))
1153 {
1154 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1155 }
1156 static_cast<Derived&>(*this).leave(x);
1157 }
1158
1159};
1160
1162template <typename Derived>
1163struct regular_formula_builder: public add_regular_formula_expressions<regular_formulas::regular_formula_builder_base, Derived>
1164{
1165};
1166//--- end generated regular_formulas::add_regular_formula_expressions code ---//
1167
1168} // namespace regular_formulas
1169
1170namespace state_formulas
1171{
1172
1174template <typename Derived>
1175struct state_formula_builder_base: public core::builder<Derived>
1176{
1177 typedef core::builder<Derived> super;
1178 using super::apply;
1179
1180 template <class T>
1181 void apply(T& result, const data::data_expression& x)
1182 {
1183 static_cast<Derived&>(*this).enter(x);
1184 // skip
1185 static_cast<Derived&>(*this).leave(x);
1186 result = x;
1187 }
1188
1189};
1190
1191//--- start generated state_formulas::add_sort_expressions code ---//
1192template <template <class> class Builder, class Derived>
1193struct add_sort_expressions: public Builder<Derived>
1194{
1195 typedef Builder<Derived> super;
1196 using super::enter;
1197 using super::leave;
1198 using super::update;
1199 using super::apply;
1200
1201 template <class T>
1202 void apply(T& result, const state_formulas::true_& x)
1203 {
1204
1205 result = x;
1206 static_cast<Derived&>(*this).enter(x);
1207 // skip
1208 static_cast<Derived&>(*this).leave(x);
1209 result = x;
1210 }
1211
1212 template <class T>
1213 void apply(T& result, const state_formulas::false_& x)
1214 {
1215
1216 result = x;
1217 static_cast<Derived&>(*this).enter(x);
1218 // skip
1219 static_cast<Derived&>(*this).leave(x);
1220 result = x;
1221 }
1222
1223 template <class T>
1224 void apply(T& result, const state_formulas::not_& x)
1225 {
1226
1227 static_cast<Derived&>(*this).enter(x);
1228 state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1229 static_cast<Derived&>(*this).leave(x);
1230 }
1231
1232 template <class T>
1233 void apply(T& result, const state_formulas::minus& x)
1234 {
1235
1236 static_cast<Derived&>(*this).enter(x);
1237 state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1238 static_cast<Derived&>(*this).leave(x);
1239 }
1240
1241 template <class T>
1242 void apply(T& result, const state_formulas::and_& x)
1243 {
1244
1245 static_cast<Derived&>(*this).enter(x);
1246 state_formulas::make_and_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1247 static_cast<Derived&>(*this).leave(x);
1248 }
1249
1250 template <class T>
1251 void apply(T& result, const state_formulas::or_& x)
1252 {
1253
1254 static_cast<Derived&>(*this).enter(x);
1255 state_formulas::make_or_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1256 static_cast<Derived&>(*this).leave(x);
1257 }
1258
1259 template <class T>
1260 void apply(T& result, const state_formulas::imp& x)
1261 {
1262
1263 static_cast<Derived&>(*this).enter(x);
1264 state_formulas::make_imp(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1265 static_cast<Derived&>(*this).leave(x);
1266 }
1267
1268 template <class T>
1269 void apply(T& result, const state_formulas::plus& x)
1270 {
1271
1272 static_cast<Derived&>(*this).enter(x);
1273 state_formulas::make_plus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1274 static_cast<Derived&>(*this).leave(x);
1275 }
1276
1277 template <class T>
1278 void apply(T& result, const state_formulas::const_multiply& x)
1279 {
1280
1281 static_cast<Derived&>(*this).enter(x);
1282 state_formulas::make_const_multiply(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1283 static_cast<Derived&>(*this).leave(x);
1284 }
1285
1286 template <class T>
1287 void apply(T& result, const state_formulas::const_multiply_alt& x)
1288 {
1289
1290 static_cast<Derived&>(*this).enter(x);
1291 state_formulas::make_const_multiply_alt(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1292 static_cast<Derived&>(*this).leave(x);
1293 }
1294
1295 template <class T>
1296 void apply(T& result, const state_formulas::forall& x)
1297 {
1298
1299 static_cast<Derived&>(*this).enter(x);
1300 state_formulas::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1301 static_cast<Derived&>(*this).leave(x);
1302 }
1303
1304 template <class T>
1305 void apply(T& result, const state_formulas::exists& x)
1306 {
1307
1308 static_cast<Derived&>(*this).enter(x);
1309 state_formulas::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1310 static_cast<Derived&>(*this).leave(x);
1311 }
1312
1313 template <class T>
1314 void apply(T& result, const state_formulas::infimum& x)
1315 {
1316
1317 static_cast<Derived&>(*this).enter(x);
1318 state_formulas::make_infimum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1319 static_cast<Derived&>(*this).leave(x);
1320 }
1321
1322 template <class T>
1323 void apply(T& result, const state_formulas::supremum& x)
1324 {
1325
1326 static_cast<Derived&>(*this).enter(x);
1327 state_formulas::make_supremum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1328 static_cast<Derived&>(*this).leave(x);
1329 }
1330
1331 template <class T>
1332 void apply(T& result, const state_formulas::sum& x)
1333 {
1334
1335 static_cast<Derived&>(*this).enter(x);
1336 state_formulas::make_sum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1337 static_cast<Derived&>(*this).leave(x);
1338 }
1339
1340 template <class T>
1341 void apply(T& result, const state_formulas::must& x)
1342 {
1343
1344 static_cast<Derived&>(*this).enter(x);
1345 state_formulas::make_must(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1346 static_cast<Derived&>(*this).leave(x);
1347 }
1348
1349 template <class T>
1350 void apply(T& result, const state_formulas::may& x)
1351 {
1352
1353 static_cast<Derived&>(*this).enter(x);
1354 state_formulas::make_may(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1355 static_cast<Derived&>(*this).leave(x);
1356 }
1357
1358 template <class T>
1359 void apply(T& result, const state_formulas::yaled& x)
1360 {
1361
1362 result = x;
1363 static_cast<Derived&>(*this).enter(x);
1364 // skip
1365 static_cast<Derived&>(*this).leave(x);
1366 result = x;
1367 }
1368
1369 template <class T>
1370 void apply(T& result, const state_formulas::yaled_timed& x)
1371 {
1372
1373 static_cast<Derived&>(*this).enter(x);
1374 state_formulas::make_yaled_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1375 static_cast<Derived&>(*this).leave(x);
1376 }
1377
1378 template <class T>
1379 void apply(T& result, const state_formulas::delay& x)
1380 {
1381
1382 result = x;
1383 static_cast<Derived&>(*this).enter(x);
1384 // skip
1385 static_cast<Derived&>(*this).leave(x);
1386 result = x;
1387 }
1388
1389 template <class T>
1390 void apply(T& result, const state_formulas::delay_timed& x)
1391 {
1392
1393 static_cast<Derived&>(*this).enter(x);
1394 state_formulas::make_delay_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1395 static_cast<Derived&>(*this).leave(x);
1396 }
1397
1398 template <class T>
1399 void apply(T& result, const state_formulas::variable& x)
1400 {
1401
1402 static_cast<Derived&>(*this).enter(x);
1403 state_formulas::make_variable(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
1404 static_cast<Derived&>(*this).leave(x);
1405 }
1406
1407 template <class T>
1408 void apply(T& result, const state_formulas::nu& x)
1409 {
1410
1411 static_cast<Derived&>(*this).enter(x);
1412 state_formulas::make_nu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1413 static_cast<Derived&>(*this).leave(x);
1414 }
1415
1416 template <class T>
1417 void apply(T& result, const state_formulas::mu& x)
1418 {
1419
1420 static_cast<Derived&>(*this).enter(x);
1421 state_formulas::make_mu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1422 static_cast<Derived&>(*this).leave(x);
1423 }
1424
1425 void update(state_formulas::state_formula_specification& x)
1426 {
1427 static_cast<Derived&>(*this).enter(x);
1428 process::action_label_list result_action_labels;
1429 static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
1430 x.action_labels() = result_action_labels;
1431 state_formula result_formula;
1432 static_cast<Derived&>(*this).apply(result_formula, x.formula());
1433 x.formula() = result_formula;
1434 static_cast<Derived&>(*this).leave(x);
1435 }
1436
1437 template <class T>
1438 void apply(T& result, const state_formulas::state_formula& x)
1439 {
1440
1441 static_cast<Derived&>(*this).enter(x);
1442 if (data::is_data_expression(x))
1443 {
1444 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1445 }
1446 else if (data::is_untyped_data_parameter(x))
1447 {
1448 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1449 }
1450 else if (state_formulas::is_true(x))
1451 {
1452 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
1453 }
1454 else if (state_formulas::is_false(x))
1455 {
1456 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
1457 }
1458 else if (state_formulas::is_not(x))
1459 {
1460 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
1461 }
1462 else if (state_formulas::is_minus(x))
1463 {
1464 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
1465 }
1466 else if (state_formulas::is_and(x))
1467 {
1468 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
1469 }
1470 else if (state_formulas::is_or(x))
1471 {
1472 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
1473 }
1474 else if (state_formulas::is_imp(x))
1475 {
1476 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
1477 }
1478 else if (state_formulas::is_plus(x))
1479 {
1480 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
1481 }
1482 else if (state_formulas::is_const_multiply(x))
1483 {
1484 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
1485 }
1486 else if (state_formulas::is_const_multiply_alt(x))
1487 {
1488 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
1489 }
1490 else if (state_formulas::is_forall(x))
1491 {
1492 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
1493 }
1494 else if (state_formulas::is_exists(x))
1495 {
1496 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
1497 }
1498 else if (state_formulas::is_infimum(x))
1499 {
1500 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
1501 }
1502 else if (state_formulas::is_supremum(x))
1503 {
1504 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
1505 }
1506 else if (state_formulas::is_sum(x))
1507 {
1508 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
1509 }
1510 else if (state_formulas::is_must(x))
1511 {
1512 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
1513 }
1514 else if (state_formulas::is_may(x))
1515 {
1516 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
1517 }
1518 else if (state_formulas::is_yaled(x))
1519 {
1520 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
1521 }
1522 else if (state_formulas::is_yaled_timed(x))
1523 {
1524 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
1525 }
1526 else if (state_formulas::is_delay(x))
1527 {
1528 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
1529 }
1530 else if (state_formulas::is_delay_timed(x))
1531 {
1532 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
1533 }
1534 else if (state_formulas::is_variable(x))
1535 {
1536 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
1537 }
1538 else if (state_formulas::is_nu(x))
1539 {
1540 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
1541 }
1542 else if (state_formulas::is_mu(x))
1543 {
1544 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
1545 }
1546 static_cast<Derived&>(*this).leave(x);
1547 }
1548
1549};
1550
1552template <typename Derived>
1553struct sort_expression_builder: public add_sort_expressions<regular_formulas::sort_expression_builder, Derived>
1554{
1555};
1556//--- end generated state_formulas::add_sort_expressions code ---//
1557
1558//--- start generated state_formulas::add_data_expressions code ---//
1559template <template <class> class Builder, class Derived>
1560struct add_data_expressions: public Builder<Derived>
1561{
1562 typedef Builder<Derived> super;
1563 using super::enter;
1564 using super::leave;
1565 using super::update;
1566 using super::apply;
1567
1568 template <class T>
1569 void apply(T& result, const state_formulas::true_& x)
1570 {
1571
1572 result = x;
1573 static_cast<Derived&>(*this).enter(x);
1574 // skip
1575 static_cast<Derived&>(*this).leave(x);
1576 result = x;
1577 }
1578
1579 template <class T>
1580 void apply(T& result, const state_formulas::false_& x)
1581 {
1582
1583 result = x;
1584 static_cast<Derived&>(*this).enter(x);
1585 // skip
1586 static_cast<Derived&>(*this).leave(x);
1587 result = x;
1588 }
1589
1590 template <class T>
1591 void apply(T& result, const state_formulas::not_& x)
1592 {
1593
1594 static_cast<Derived&>(*this).enter(x);
1595 state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1596 static_cast<Derived&>(*this).leave(x);
1597 }
1598
1599 template <class T>
1600 void apply(T& result, const state_formulas::minus& x)
1601 {
1602
1603 static_cast<Derived&>(*this).enter(x);
1604 state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1605 static_cast<Derived&>(*this).leave(x);
1606 }
1607
1608 template <class T>
1609 void apply(T& result, const state_formulas::and_& x)
1610 {
1611
1612 static_cast<Derived&>(*this).enter(x);
1613 state_formulas::make_and_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1614 static_cast<Derived&>(*this).leave(x);
1615 }
1616
1617 template <class T>
1618 void apply(T& result, const state_formulas::or_& x)
1619 {
1620
1621 static_cast<Derived&>(*this).enter(x);
1622 state_formulas::make_or_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1623 static_cast<Derived&>(*this).leave(x);
1624 }
1625
1626 template <class T>
1627 void apply(T& result, const state_formulas::imp& x)
1628 {
1629
1630 static_cast<Derived&>(*this).enter(x);
1631 state_formulas::make_imp(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1632 static_cast<Derived&>(*this).leave(x);
1633 }
1634
1635 template <class T>
1636 void apply(T& result, const state_formulas::plus& x)
1637 {
1638
1639 static_cast<Derived&>(*this).enter(x);
1640 state_formulas::make_plus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1641 static_cast<Derived&>(*this).leave(x);
1642 }
1643
1644 template <class T>
1645 void apply(T& result, const state_formulas::const_multiply& x)
1646 {
1647
1648 static_cast<Derived&>(*this).enter(x);
1649 state_formulas::make_const_multiply(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1650 static_cast<Derived&>(*this).leave(x);
1651 }
1652
1653 template <class T>
1654 void apply(T& result, const state_formulas::const_multiply_alt& x)
1655 {
1656
1657 static_cast<Derived&>(*this).enter(x);
1658 state_formulas::make_const_multiply_alt(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1659 static_cast<Derived&>(*this).leave(x);
1660 }
1661
1662 template <class T>
1663 void apply(T& result, const state_formulas::forall& x)
1664 {
1665
1666 static_cast<Derived&>(*this).enter(x);
1667 state_formulas::make_forall(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1668 static_cast<Derived&>(*this).leave(x);
1669 }
1670
1671 template <class T>
1672 void apply(T& result, const state_formulas::exists& x)
1673 {
1674
1675 static_cast<Derived&>(*this).enter(x);
1676 state_formulas::make_exists(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1677 static_cast<Derived&>(*this).leave(x);
1678 }
1679
1680 template <class T>
1681 void apply(T& result, const state_formulas::infimum& x)
1682 {
1683
1684 static_cast<Derived&>(*this).enter(x);
1685 state_formulas::make_infimum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1686 static_cast<Derived&>(*this).leave(x);
1687 }
1688
1689 template <class T>
1690 void apply(T& result, const state_formulas::supremum& x)
1691 {
1692
1693 static_cast<Derived&>(*this).enter(x);
1694 state_formulas::make_supremum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1695 static_cast<Derived&>(*this).leave(x);
1696 }
1697
1698 template <class T>
1699 void apply(T& result, const state_formulas::sum& x)
1700 {
1701
1702 static_cast<Derived&>(*this).enter(x);
1703 state_formulas::make_sum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1704 static_cast<Derived&>(*this).leave(x);
1705 }
1706
1707 template <class T>
1708 void apply(T& result, const state_formulas::must& x)
1709 {
1710
1711 static_cast<Derived&>(*this).enter(x);
1712 state_formulas::make_must(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1713 static_cast<Derived&>(*this).leave(x);
1714 }
1715
1716 template <class T>
1717 void apply(T& result, const state_formulas::may& x)
1718 {
1719
1720 static_cast<Derived&>(*this).enter(x);
1721 state_formulas::make_may(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1722 static_cast<Derived&>(*this).leave(x);
1723 }
1724
1725 template <class T>
1726 void apply(T& result, const state_formulas::yaled& x)
1727 {
1728
1729 result = x;
1730 static_cast<Derived&>(*this).enter(x);
1731 // skip
1732 static_cast<Derived&>(*this).leave(x);
1733 result = x;
1734 }
1735
1736 template <class T>
1737 void apply(T& result, const state_formulas::yaled_timed& x)
1738 {
1739
1740 static_cast<Derived&>(*this).enter(x);
1741 state_formulas::make_yaled_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1742 static_cast<Derived&>(*this).leave(x);
1743 }
1744
1745 template <class T>
1746 void apply(T& result, const state_formulas::delay& x)
1747 {
1748
1749 result = x;
1750 static_cast<Derived&>(*this).enter(x);
1751 // skip
1752 static_cast<Derived&>(*this).leave(x);
1753 result = x;
1754 }
1755
1756 template <class T>
1757 void apply(T& result, const state_formulas::delay_timed& x)
1758 {
1759
1760 static_cast<Derived&>(*this).enter(x);
1761 state_formulas::make_delay_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1762 static_cast<Derived&>(*this).leave(x);
1763 }
1764
1765 template <class T>
1766 void apply(T& result, const state_formulas::variable& x)
1767 {
1768
1769 static_cast<Derived&>(*this).enter(x);
1770 state_formulas::make_variable(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
1771 static_cast<Derived&>(*this).leave(x);
1772 }
1773
1774 template <class T>
1775 void apply(T& result, const state_formulas::nu& x)
1776 {
1777
1778 static_cast<Derived&>(*this).enter(x);
1779 state_formulas::make_nu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1780 static_cast<Derived&>(*this).leave(x);
1781 }
1782
1783 template <class T>
1784 void apply(T& result, const state_formulas::mu& x)
1785 {
1786
1787 static_cast<Derived&>(*this).enter(x);
1788 state_formulas::make_mu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1789 static_cast<Derived&>(*this).leave(x);
1790 }
1791
1792 void update(state_formulas::state_formula_specification& x)
1793 {
1794 static_cast<Derived&>(*this).enter(x);
1795 state_formula result_formula;
1796 static_cast<Derived&>(*this).apply(result_formula, x.formula());
1797 x.formula() = result_formula;
1798 static_cast<Derived&>(*this).leave(x);
1799 }
1800
1801 template <class T>
1802 void apply(T& result, const state_formulas::state_formula& x)
1803 {
1804
1805 static_cast<Derived&>(*this).enter(x);
1806 if (data::is_data_expression(x))
1807 {
1808 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1809 }
1810 else if (data::is_untyped_data_parameter(x))
1811 {
1812 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1813 }
1814 else if (state_formulas::is_true(x))
1815 {
1816 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
1817 }
1818 else if (state_formulas::is_false(x))
1819 {
1820 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
1821 }
1822 else if (state_formulas::is_not(x))
1823 {
1824 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
1825 }
1826 else if (state_formulas::is_minus(x))
1827 {
1828 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
1829 }
1830 else if (state_formulas::is_and(x))
1831 {
1832 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
1833 }
1834 else if (state_formulas::is_or(x))
1835 {
1836 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
1837 }
1838 else if (state_formulas::is_imp(x))
1839 {
1840 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
1841 }
1842 else if (state_formulas::is_plus(x))
1843 {
1844 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
1845 }
1846 else if (state_formulas::is_const_multiply(x))
1847 {
1848 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
1849 }
1850 else if (state_formulas::is_const_multiply_alt(x))
1851 {
1852 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
1853 }
1854 else if (state_formulas::is_forall(x))
1855 {
1856 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
1857 }
1858 else if (state_formulas::is_exists(x))
1859 {
1860 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
1861 }
1862 else if (state_formulas::is_infimum(x))
1863 {
1864 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
1865 }
1866 else if (state_formulas::is_supremum(x))
1867 {
1868 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
1869 }
1870 else if (state_formulas::is_sum(x))
1871 {
1872 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
1873 }
1874 else if (state_formulas::is_must(x))
1875 {
1876 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
1877 }
1878 else if (state_formulas::is_may(x))
1879 {
1880 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
1881 }
1882 else if (state_formulas::is_yaled(x))
1883 {
1884 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
1885 }
1886 else if (state_formulas::is_yaled_timed(x))
1887 {
1888 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
1889 }
1890 else if (state_formulas::is_delay(x))
1891 {
1892 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
1893 }
1894 else if (state_formulas::is_delay_timed(x))
1895 {
1896 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
1897 }
1898 else if (state_formulas::is_variable(x))
1899 {
1900 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
1901 }
1902 else if (state_formulas::is_nu(x))
1903 {
1904 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
1905 }
1906 else if (state_formulas::is_mu(x))
1907 {
1908 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
1909 }
1910 static_cast<Derived&>(*this).leave(x);
1911 }
1912
1913};
1914
1916template <typename Derived>
1917struct data_expression_builder: public add_data_expressions<regular_formulas::data_expression_builder, Derived>
1918{
1919};
1920//--- end generated state_formulas::add_data_expressions code ---//
1921
1922//--- start generated state_formulas::add_variables code ---//
1923template <template <class> class Builder, class Derived>
1924struct add_variables: public Builder<Derived>
1925{
1926 typedef Builder<Derived> super;
1927 using super::enter;
1928 using super::leave;
1929 using super::update;
1930 using super::apply;
1931
1932 template <class T>
1933 void apply(T& result, const state_formulas::true_& x)
1934 {
1935
1936 result = x;
1937 static_cast<Derived&>(*this).enter(x);
1938 // skip
1939 static_cast<Derived&>(*this).leave(x);
1940 result = x;
1941 }
1942
1943 template <class T>
1944 void apply(T& result, const state_formulas::false_& x)
1945 {
1946
1947 result = x;
1948 static_cast<Derived&>(*this).enter(x);
1949 // skip
1950 static_cast<Derived&>(*this).leave(x);
1951 result = x;
1952 }
1953
1954 template <class T>
1955 void apply(T& result, const state_formulas::not_& x)
1956 {
1957
1958 static_cast<Derived&>(*this).enter(x);
1959 state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1960 static_cast<Derived&>(*this).leave(x);
1961 }
1962
1963 template <class T>
1964 void apply(T& result, const state_formulas::minus& x)
1965 {
1966
1967 static_cast<Derived&>(*this).enter(x);
1968 state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1969 static_cast<Derived&>(*this).leave(x);
1970 }
1971
1972 template <class T>
1973 void apply(T& result, const state_formulas::and_& x)
1974 {
1975
1976 static_cast<Derived&>(*this).enter(x);
1977 state_formulas::make_and_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1978 static_cast<Derived&>(*this).leave(x);
1979 }
1980
1981 template <class T>
1982 void apply(T& result, const state_formulas::or_& x)
1983 {
1984
1985 static_cast<Derived&>(*this).enter(x);
1986 state_formulas::make_or_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1987 static_cast<Derived&>(*this).leave(x);
1988 }
1989
1990 template <class T>
1991 void apply(T& result, const state_formulas::imp& x)
1992 {
1993
1994 static_cast<Derived&>(*this).enter(x);
1995 state_formulas::make_imp(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1996 static_cast<Derived&>(*this).leave(x);
1997 }
1998
1999 template <class T>
2000 void apply(T& result, const state_formulas::plus& x)
2001 {
2002
2003 static_cast<Derived&>(*this).enter(x);
2004 state_formulas::make_plus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2005 static_cast<Derived&>(*this).leave(x);
2006 }
2007
2008 template <class T>
2009 void apply(T& result, const state_formulas::const_multiply& x)
2010 {
2011
2012 static_cast<Derived&>(*this).enter(x);
2013 state_formulas::make_const_multiply(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2014 static_cast<Derived&>(*this).leave(x);
2015 }
2016
2017 template <class T>
2018 void apply(T& result, const state_formulas::const_multiply_alt& x)
2019 {
2020
2021 static_cast<Derived&>(*this).enter(x);
2022 state_formulas::make_const_multiply_alt(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2023 static_cast<Derived&>(*this).leave(x);
2024 }
2025
2026 template <class T>
2027 void apply(T& result, const state_formulas::forall& x)
2028 {
2029
2030 static_cast<Derived&>(*this).enter(x);
2031 state_formulas::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2032 static_cast<Derived&>(*this).leave(x);
2033 }
2034
2035 template <class T>
2036 void apply(T& result, const state_formulas::exists& x)
2037 {
2038
2039 static_cast<Derived&>(*this).enter(x);
2040 state_formulas::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2041 static_cast<Derived&>(*this).leave(x);
2042 }
2043
2044 template <class T>
2045 void apply(T& result, const state_formulas::infimum& x)
2046 {
2047
2048 static_cast<Derived&>(*this).enter(x);
2049 state_formulas::make_infimum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2050 static_cast<Derived&>(*this).leave(x);
2051 }
2052
2053 template <class T>
2054 void apply(T& result, const state_formulas::supremum& x)
2055 {
2056
2057 static_cast<Derived&>(*this).enter(x);
2058 state_formulas::make_supremum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2059 static_cast<Derived&>(*this).leave(x);
2060 }
2061
2062 template <class T>
2063 void apply(T& result, const state_formulas::sum& x)
2064 {
2065
2066 static_cast<Derived&>(*this).enter(x);
2067 state_formulas::make_sum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2068 static_cast<Derived&>(*this).leave(x);
2069 }
2070
2071 template <class T>
2072 void apply(T& result, const state_formulas::must& x)
2073 {
2074
2075 static_cast<Derived&>(*this).enter(x);
2076 state_formulas::make_must(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2077 static_cast<Derived&>(*this).leave(x);
2078 }
2079
2080 template <class T>
2081 void apply(T& result, const state_formulas::may& x)
2082 {
2083
2084 static_cast<Derived&>(*this).enter(x);
2085 state_formulas::make_may(result, [&](regular_formulas::regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.formula()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2086 static_cast<Derived&>(*this).leave(x);
2087 }
2088
2089 template <class T>
2090 void apply(T& result, const state_formulas::yaled& x)
2091 {
2092
2093 result = x;
2094 static_cast<Derived&>(*this).enter(x);
2095 // skip
2096 static_cast<Derived&>(*this).leave(x);
2097 result = x;
2098 }
2099
2100 template <class T>
2101 void apply(T& result, const state_formulas::yaled_timed& x)
2102 {
2103
2104 static_cast<Derived&>(*this).enter(x);
2105 state_formulas::make_yaled_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
2106 static_cast<Derived&>(*this).leave(x);
2107 }
2108
2109 template <class T>
2110 void apply(T& result, const state_formulas::delay& x)
2111 {
2112
2113 result = x;
2114 static_cast<Derived&>(*this).enter(x);
2115 // skip
2116 static_cast<Derived&>(*this).leave(x);
2117 result = x;
2118 }
2119
2120 template <class T>
2121 void apply(T& result, const state_formulas::delay_timed& x)
2122 {
2123
2124 static_cast<Derived&>(*this).enter(x);
2125 state_formulas::make_delay_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
2126 static_cast<Derived&>(*this).leave(x);
2127 }
2128
2129 template <class T>
2130 void apply(T& result, const state_formulas::variable& x)
2131 {
2132
2133 static_cast<Derived&>(*this).enter(x);
2134 state_formulas::make_variable(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
2135 static_cast<Derived&>(*this).leave(x);
2136 }
2137
2138 template <class T>
2139 void apply(T& result, const state_formulas::nu& x)
2140 {
2141
2142 static_cast<Derived&>(*this).enter(x);
2143 state_formulas::make_nu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2144 static_cast<Derived&>(*this).leave(x);
2145 }
2146
2147 template <class T>
2148 void apply(T& result, const state_formulas::mu& x)
2149 {
2150
2151 static_cast<Derived&>(*this).enter(x);
2152 state_formulas::make_mu(result, x.name(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2153 static_cast<Derived&>(*this).leave(x);
2154 }
2155
2156 void update(state_formulas::state_formula_specification& x)
2157 {
2158 static_cast<Derived&>(*this).enter(x);
2159 state_formula result_formula;
2160 static_cast<Derived&>(*this).apply(result_formula, x.formula());
2161 x.formula() = result_formula;
2162 static_cast<Derived&>(*this).leave(x);
2163 }
2164
2165 template <class T>
2166 void apply(T& result, const state_formulas::state_formula& x)
2167 {
2168
2169 static_cast<Derived&>(*this).enter(x);
2170 if (data::is_data_expression(x))
2171 {
2172 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
2173 }
2174 else if (data::is_untyped_data_parameter(x))
2175 {
2176 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
2177 }
2178 else if (state_formulas::is_true(x))
2179 {
2180 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
2181 }
2182 else if (state_formulas::is_false(x))
2183 {
2184 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
2185 }
2186 else if (state_formulas::is_not(x))
2187 {
2188 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
2189 }
2190 else if (state_formulas::is_minus(x))
2191 {
2192 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
2193 }
2194 else if (state_formulas::is_and(x))
2195 {
2196 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
2197 }
2198 else if (state_formulas::is_or(x))
2199 {
2200 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
2201 }
2202 else if (state_formulas::is_imp(x))
2203 {
2204 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
2205 }
2206 else if (state_formulas::is_plus(x))
2207 {
2208 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
2209 }
2210 else if (state_formulas::is_const_multiply(x))
2211 {
2212 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
2213 }
2214 else if (state_formulas::is_const_multiply_alt(x))
2215 {
2216 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2217 }
2218 else if (state_formulas::is_forall(x))
2219 {
2220 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
2221 }
2222 else if (state_formulas::is_exists(x))
2223 {
2224 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
2225 }
2226 else if (state_formulas::is_infimum(x))
2227 {
2228 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
2229 }
2230 else if (state_formulas::is_supremum(x))
2231 {
2232 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
2233 }
2234 else if (state_formulas::is_sum(x))
2235 {
2236 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
2237 }
2238 else if (state_formulas::is_must(x))
2239 {
2240 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
2241 }
2242 else if (state_formulas::is_may(x))
2243 {
2244 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
2245 }
2246 else if (state_formulas::is_yaled(x))
2247 {
2248 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
2249 }
2250 else if (state_formulas::is_yaled_timed(x))
2251 {
2252 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
2253 }
2254 else if (state_formulas::is_delay(x))
2255 {
2256 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
2257 }
2258 else if (state_formulas::is_delay_timed(x))
2259 {
2260 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
2261 }
2262 else if (state_formulas::is_variable(x))
2263 {
2264 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
2265 }
2266 else if (state_formulas::is_nu(x))
2267 {
2268 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
2269 }
2270 else if (state_formulas::is_mu(x))
2271 {
2272 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
2273 }
2274 static_cast<Derived&>(*this).leave(x);
2275 }
2276
2277};
2278
2280template <typename Derived>
2281struct variable_builder: public add_variables<regular_formulas::data_expression_builder, Derived>
2282{
2283};
2284//--- end generated state_formulas::add_variables code ---//
2285
2286//--- start generated state_formulas::add_state_formula_expressions code ---//
2287template <template <class> class Builder, class Derived>
2288struct add_state_formula_expressions: public Builder<Derived>
2289{
2290 typedef Builder<Derived> super;
2291 using super::enter;
2292 using super::leave;
2293 using super::update;
2294 using super::apply;
2295
2296 template <class T>
2297 void apply(T& result, const state_formulas::true_& x)
2298 {
2299
2300 result = x;
2301 static_cast<Derived&>(*this).enter(x);
2302 // skip
2303 static_cast<Derived&>(*this).leave(x);
2304 result = x;
2305 }
2306
2307 template <class T>
2308 void apply(T& result, const state_formulas::false_& x)
2309 {
2310
2311 result = x;
2312 static_cast<Derived&>(*this).enter(x);
2313 // skip
2314 static_cast<Derived&>(*this).leave(x);
2315 result = x;
2316 }
2317
2318 template <class T>
2319 void apply(T& result, const state_formulas::not_& x)
2320 {
2321
2322 static_cast<Derived&>(*this).enter(x);
2323 state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2324 static_cast<Derived&>(*this).leave(x);
2325 }
2326
2327 template <class T>
2328 void apply(T& result, const state_formulas::minus& x)
2329 {
2330
2331 static_cast<Derived&>(*this).enter(x);
2332 state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2333 static_cast<Derived&>(*this).leave(x);
2334 }
2335
2336 template <class T>
2337 void apply(T& result, const state_formulas::and_& x)
2338 {
2339
2340 static_cast<Derived&>(*this).enter(x);
2341 state_formulas::make_and_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2342 static_cast<Derived&>(*this).leave(x);
2343 }
2344
2345 template <class T>
2346 void apply(T& result, const state_formulas::or_& x)
2347 {
2348
2349 static_cast<Derived&>(*this).enter(x);
2350 state_formulas::make_or_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2351 static_cast<Derived&>(*this).leave(x);
2352 }
2353
2354 template <class T>
2355 void apply(T& result, const state_formulas::imp& x)
2356 {
2357
2358 static_cast<Derived&>(*this).enter(x);
2359 state_formulas::make_imp(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2360 static_cast<Derived&>(*this).leave(x);
2361 }
2362
2363 template <class T>
2364 void apply(T& result, const state_formulas::plus& x)
2365 {
2366
2367 static_cast<Derived&>(*this).enter(x);
2368 state_formulas::make_plus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2369 static_cast<Derived&>(*this).leave(x);
2370 }
2371
2372 template <class T>
2373 void apply(T& result, const state_formulas::const_multiply& x)
2374 {
2375
2376 static_cast<Derived&>(*this).enter(x);
2377 state_formulas::make_const_multiply(result, x.left(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2378 static_cast<Derived&>(*this).leave(x);
2379 }
2380
2381 template <class T>
2382 void apply(T& result, const state_formulas::const_multiply_alt& x)
2383 {
2384
2385 static_cast<Derived&>(*this).enter(x);
2386 state_formulas::make_const_multiply_alt(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, x.right());
2387 static_cast<Derived&>(*this).leave(x);
2388 }
2389
2390 template <class T>
2391 void apply(T& result, const state_formulas::forall& x)
2392 {
2393
2394 static_cast<Derived&>(*this).enter(x);
2395 state_formulas::make_forall(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2396 static_cast<Derived&>(*this).leave(x);
2397 }
2398
2399 template <class T>
2400 void apply(T& result, const state_formulas::exists& x)
2401 {
2402
2403 static_cast<Derived&>(*this).enter(x);
2404 state_formulas::make_exists(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2405 static_cast<Derived&>(*this).leave(x);
2406 }
2407
2408 template <class T>
2409 void apply(T& result, const state_formulas::infimum& x)
2410 {
2411
2412 static_cast<Derived&>(*this).enter(x);
2413 state_formulas::make_infimum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2414 static_cast<Derived&>(*this).leave(x);
2415 }
2416
2417 template <class T>
2418 void apply(T& result, const state_formulas::supremum& x)
2419 {
2420
2421 static_cast<Derived&>(*this).enter(x);
2422 state_formulas::make_supremum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2423 static_cast<Derived&>(*this).leave(x);
2424 }
2425
2426 template <class T>
2427 void apply(T& result, const state_formulas::sum& x)
2428 {
2429
2430 static_cast<Derived&>(*this).enter(x);
2431 state_formulas::make_sum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2432 static_cast<Derived&>(*this).leave(x);
2433 }
2434
2435 template <class T>
2436 void apply(T& result, const state_formulas::must& x)
2437 {
2438
2439 static_cast<Derived&>(*this).enter(x);
2440 state_formulas::make_must(result, x.formula(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2441 static_cast<Derived&>(*this).leave(x);
2442 }
2443
2444 template <class T>
2445 void apply(T& result, const state_formulas::may& x)
2446 {
2447
2448 static_cast<Derived&>(*this).enter(x);
2449 state_formulas::make_may(result, x.formula(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2450 static_cast<Derived&>(*this).leave(x);
2451 }
2452
2453 template <class T>
2454 void apply(T& result, const state_formulas::yaled& x)
2455 {
2456
2457 result = x;
2458 static_cast<Derived&>(*this).enter(x);
2459 // skip
2460 static_cast<Derived&>(*this).leave(x);
2461 result = x;
2462 }
2463
2464 template <class T>
2465 void apply(T& result, const state_formulas::yaled_timed& x)
2466 {
2467
2468 result = x;
2469 static_cast<Derived&>(*this).enter(x);
2470 // skip
2471 static_cast<Derived&>(*this).leave(x);
2472 result = x;
2473 }
2474
2475 template <class T>
2476 void apply(T& result, const state_formulas::delay& x)
2477 {
2478
2479 result = x;
2480 static_cast<Derived&>(*this).enter(x);
2481 // skip
2482 static_cast<Derived&>(*this).leave(x);
2483 result = x;
2484 }
2485
2486 template <class T>
2487 void apply(T& result, const state_formulas::delay_timed& x)
2488 {
2489
2490 result = x;
2491 static_cast<Derived&>(*this).enter(x);
2492 // skip
2493 static_cast<Derived&>(*this).leave(x);
2494 result = x;
2495 }
2496
2497 template <class T>
2498 void apply(T& result, const state_formulas::variable& x)
2499 {
2500
2501 result = x;
2502 static_cast<Derived&>(*this).enter(x);
2503 // skip
2504 static_cast<Derived&>(*this).leave(x);
2505 result = x;
2506 }
2507
2508 template <class T>
2509 void apply(T& result, const state_formulas::nu& x)
2510 {
2511
2512 static_cast<Derived&>(*this).enter(x);
2513 state_formulas::make_nu(result, x.name(), x.assignments(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2514 static_cast<Derived&>(*this).leave(x);
2515 }
2516
2517 template <class T>
2518 void apply(T& result, const state_formulas::mu& x)
2519 {
2520
2521 static_cast<Derived&>(*this).enter(x);
2522 state_formulas::make_mu(result, x.name(), x.assignments(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2523 static_cast<Derived&>(*this).leave(x);
2524 }
2525
2526 void update(state_formulas::state_formula_specification& x)
2527 {
2528 static_cast<Derived&>(*this).enter(x);
2529 state_formula result_formula;
2530 static_cast<Derived&>(*this).apply(result_formula, x.formula());
2531 x.formula() = result_formula;
2532 static_cast<Derived&>(*this).leave(x);
2533 }
2534
2535 template <class T>
2536 void apply(T& result, const state_formulas::state_formula& x)
2537 {
2538
2539 static_cast<Derived&>(*this).enter(x);
2540 if (data::is_data_expression(x))
2541 {
2542 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
2543 }
2544 else if (data::is_untyped_data_parameter(x))
2545 {
2546 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
2547 }
2548 else if (state_formulas::is_true(x))
2549 {
2550 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
2551 }
2552 else if (state_formulas::is_false(x))
2553 {
2554 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
2555 }
2556 else if (state_formulas::is_not(x))
2557 {
2558 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
2559 }
2560 else if (state_formulas::is_minus(x))
2561 {
2562 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
2563 }
2564 else if (state_formulas::is_and(x))
2565 {
2566 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
2567 }
2568 else if (state_formulas::is_or(x))
2569 {
2570 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
2571 }
2572 else if (state_formulas::is_imp(x))
2573 {
2574 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
2575 }
2576 else if (state_formulas::is_plus(x))
2577 {
2578 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
2579 }
2580 else if (state_formulas::is_const_multiply(x))
2581 {
2582 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
2583 }
2584 else if (state_formulas::is_const_multiply_alt(x))
2585 {
2586 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2587 }
2588 else if (state_formulas::is_forall(x))
2589 {
2590 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
2591 }
2592 else if (state_formulas::is_exists(x))
2593 {
2594 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
2595 }
2596 else if (state_formulas::is_infimum(x))
2597 {
2598 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
2599 }
2600 else if (state_formulas::is_supremum(x))
2601 {
2602 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
2603 }
2604 else if (state_formulas::is_sum(x))
2605 {
2606 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
2607 }
2608 else if (state_formulas::is_must(x))
2609 {
2610 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
2611 }
2612 else if (state_formulas::is_may(x))
2613 {
2614 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
2615 }
2616 else if (state_formulas::is_yaled(x))
2617 {
2618 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
2619 }
2620 else if (state_formulas::is_yaled_timed(x))
2621 {
2622 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
2623 }
2624 else if (state_formulas::is_delay(x))
2625 {
2626 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
2627 }
2628 else if (state_formulas::is_delay_timed(x))
2629 {
2630 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
2631 }
2632 else if (state_formulas::is_variable(x))
2633 {
2634 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
2635 }
2636 else if (state_formulas::is_nu(x))
2637 {
2638 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
2639 }
2640 else if (state_formulas::is_mu(x))
2641 {
2642 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
2643 }
2644 static_cast<Derived&>(*this).leave(x);
2645 }
2646
2647};
2648
2650template <typename Derived>
2651struct state_formula_builder: public add_state_formula_expressions<state_formulas::state_formula_builder_base, Derived>
2652{
2653};
2654//--- end generated state_formulas::add_state_formula_expressions code ---//
2655
2656} // namespace state_formulas
2657
2658} // namespace mcrl2
2659
2660#endif // MCRL2_MODAL_FORMULA_BUILDER_H
atermpp::term_list< variable >
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::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::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::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::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
builder.h
add your file description here.
mcrl2::action_formulas::make_exists
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:646
mcrl2::action_formulas::is_at
bool is_at(const atermpp::aterm &x)
Definition action_formula.h:731
mcrl2::action_formulas::make_not_
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:266
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::make_and_
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:342
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::make_imp
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:494
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::make_forall
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:570
mcrl2::action_formulas::make_or_
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:418
mcrl2::action_formulas::make_multi_action
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:793
mcrl2::action_formulas::is_multi_action
bool is_multi_action(const atermpp::aterm &x)
Definition action_formula.h:802
mcrl2::action_formulas::make_at
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_formula.h:722
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::make_trans
void make_trans(atermpp::aterm &t, const ARGUMENTS &... args)
Definition regular_formula.h:295
mcrl2::regular_formulas::make_seq
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
Definition regular_formula.h:148
mcrl2::regular_formulas::make_trans_or_nil
void make_trans_or_nil(atermpp::aterm &t, const ARGUMENTS &... args)
Definition regular_formula.h:366
mcrl2::regular_formulas::is_trans
bool is_trans(const atermpp::aterm &x)
Definition regular_formula.h:304
mcrl2::regular_formulas::make_alt
void make_alt(atermpp::aterm &t, const ARGUMENTS &... args)
Definition regular_formula.h:224
mcrl2::regular_formulas::make_untyped_regular_formula
void make_untyped_regular_formula(atermpp::aterm &t, const ARGUMENTS &... args)
Definition regular_formula.h:452
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::make_imp
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:591
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::make_const_multiply
void make_const_multiply(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:743
mcrl2::state_formulas::make_exists
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:971
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::make_and_
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:439
mcrl2::state_formulas::is_true
bool is_true(const atermpp::aterm &x)
Definition state_formula.h:177
mcrl2::state_formulas::make_plus
void make_plus(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:667
mcrl2::state_formulas::is_variable
bool is_variable(const atermpp::aterm &x)
Definition state_formula.h:1689
mcrl2::state_formulas::make_not_
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:292
mcrl2::state_formulas::make_infimum
void make_infimum(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1047
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::make_delay_timed
void make_delay_timed(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1599
mcrl2::state_formulas::make_const_multiply_alt
void make_const_multiply_alt(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:819
mcrl2::state_formulas::make_may
void make_may(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1351
mcrl2::state_formulas::is_sum
bool is_sum(const atermpp::aterm &x)
Definition state_formula.h:1208
mcrl2::state_formulas::make_must
void make_must(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1275
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::make_variable
void make_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1680
mcrl2::state_formulas::make_nu
void make_nu(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1766
mcrl2::state_formulas::make_supremum
void make_supremum(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1123
mcrl2::state_formulas::make_sum
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1199
mcrl2::state_formulas::is_plus
bool is_plus(const atermpp::aterm &x)
Definition state_formula.h:676
mcrl2::state_formulas::make_forall
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:895
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::make_minus
void make_minus(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:363
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::state_formulas::make_or_
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:515
mcrl2::state_formulas::make_yaled_timed
void make_yaled_timed(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1475
mcrl2::state_formulas::make_mu
void make_mu(atermpp::aterm &t, const ARGUMENTS &... args)
Definition state_formula.h:1852
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_builder_base
Base class for action_formula_builder.
Definition builder.h:27
mcrl2::action_formulas::action_formula_builder_base::super
core::builder< Derived > super
Definition builder.h:28
mcrl2::action_formulas::action_formula_builder_base::apply
void apply(T &result, const data::data_expression &x)
Definition builder.h:32
mcrl2::action_formulas::action_formula_builder
\brief Builder class
Definition builder.h:731
mcrl2::action_formulas::add_action_formula_expressions
Definition builder.h:563
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::forall &x)
Definition builder.h:629
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::not_ &x)
Definition builder.h:593
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::at &x)
Definition builder.h:647
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::multi_action &x)
Definition builder.h:656
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::and_ &x)
Definition builder.h:602
mcrl2::action_formulas::add_action_formula_expressions::super
Builder< Derived > super
Definition builder.h:564
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::exists &x)
Definition builder.h:638
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::imp &x)
Definition builder.h:620
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::action_formula &x)
Definition builder.h:667
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::true_ &x)
Definition builder.h:571
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::or_ &x)
Definition builder.h:611
mcrl2::action_formulas::add_action_formula_expressions::apply
void apply(T &result, const action_formulas::false_ &x)
Definition builder.h:582
mcrl2::action_formulas::add_data_expressions
Definition builder.h:217
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::action_formula &x)
Definition builder.h:319
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::and_ &x)
Definition builder.h:256
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::exists &x)
Definition builder.h:292
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::false_ &x)
Definition builder.h:236
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::at &x)
Definition builder.h:301
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::or_ &x)
Definition builder.h:265
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::multi_action &x)
Definition builder.h:310
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::true_ &x)
Definition builder.h:225
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::not_ &x)
Definition builder.h:247
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::imp &x)
Definition builder.h:274
mcrl2::action_formulas::add_data_expressions::super
Builder< Derived > super
Definition builder.h:218
mcrl2::action_formulas::add_data_expressions::apply
void apply(T &result, const action_formulas::forall &x)
Definition builder.h:283
mcrl2::action_formulas::add_sort_expressions
Definition builder.h:44
mcrl2::action_formulas::add_sort_expressions::super
Builder< Derived > super
Definition builder.h:45
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::exists &x)
Definition builder.h:119
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::forall &x)
Definition builder.h:110
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::true_ &x)
Definition builder.h:52
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::or_ &x)
Definition builder.h:92
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::false_ &x)
Definition builder.h:63
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::at &x)
Definition builder.h:128
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::and_ &x)
Definition builder.h:83
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::imp &x)
Definition builder.h:101
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::not_ &x)
Definition builder.h:74
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::action_formula &x)
Definition builder.h:146
mcrl2::action_formulas::add_sort_expressions::apply
void apply(T &result, const action_formulas::multi_action &x)
Definition builder.h:137
mcrl2::action_formulas::add_variables
Definition builder.h:390
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::action_formula &x)
Definition builder.h:492
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::not_ &x)
Definition builder.h:420
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::true_ &x)
Definition builder.h:398
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::or_ &x)
Definition builder.h:438
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::exists &x)
Definition builder.h:465
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::and_ &x)
Definition builder.h:429
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::imp &x)
Definition builder.h:447
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::at &x)
Definition builder.h:474
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::false_ &x)
Definition builder.h:409
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::forall &x)
Definition builder.h:456
mcrl2::action_formulas::add_variables::super
Builder< Derived > super
Definition builder.h:391
mcrl2::action_formulas::add_variables::apply
void apply(T &result, const action_formulas::multi_action &x)
Definition builder.h:483
mcrl2::action_formulas::data_expression_builder
\brief Builder class
Definition builder.h:383
mcrl2::action_formulas::sort_expression_builder
\brief Builder class
Definition builder.h:210
mcrl2::action_formulas::variable_builder
\brief Builder class
Definition builder.h:556
mcrl2::core::builder
expression builder that visits all sub expressions
Definition builder.h:42
mcrl2::core::builder::apply
void apply(atermpp::term_list< T > &result, const atermpp::term_list< U > &x)
Definition builder.h:89
mcrl2::regular_formulas::add_data_expressions
Definition builder.h:871
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::trans &x)
Definition builder.h:897
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::trans_or_nil &x)
Definition builder.h:906
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::seq &x)
Definition builder.h:879
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::regular_formula &x)
Definition builder.h:924
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::alt &x)
Definition builder.h:888
mcrl2::regular_formulas::add_data_expressions::apply
void apply(T &result, const regular_formulas::untyped_regular_formula &x)
Definition builder.h:915
mcrl2::regular_formulas::add_data_expressions::super
Builder< Derived > super
Definition builder.h:872
mcrl2::regular_formulas::add_regular_formula_expressions
Definition builder.h:1071
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::trans_or_nil &x)
Definition builder.h:1106
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::seq &x)
Definition builder.h:1079
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::regular_formula &x)
Definition builder.h:1124
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::untyped_regular_formula &x)
Definition builder.h:1115
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::trans &x)
Definition builder.h:1097
mcrl2::regular_formulas::add_regular_formula_expressions::super
Builder< Derived > super
Definition builder.h:1072
mcrl2::regular_formulas::add_regular_formula_expressions::apply
void apply(T &result, const regular_formulas::alt &x)
Definition builder.h:1088
mcrl2::regular_formulas::add_sort_expressions
Definition builder.h:771
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::trans &x)
Definition builder.h:797
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::seq &x)
Definition builder.h:779
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::regular_formula &x)
Definition builder.h:824
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::untyped_regular_formula &x)
Definition builder.h:815
mcrl2::regular_formulas::add_sort_expressions::super
Builder< Derived > super
Definition builder.h:772
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::alt &x)
Definition builder.h:788
mcrl2::regular_formulas::add_sort_expressions::apply
void apply(T &result, const regular_formulas::trans_or_nil &x)
Definition builder.h:806
mcrl2::regular_formulas::add_variables
Definition builder.h:971
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::untyped_regular_formula &x)
Definition builder.h:1015
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::trans_or_nil &x)
Definition builder.h:1006
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::seq &x)
Definition builder.h:979
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::trans &x)
Definition builder.h:997
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::alt &x)
Definition builder.h:988
mcrl2::regular_formulas::add_variables::super
Builder< Derived > super
Definition builder.h:972
mcrl2::regular_formulas::add_variables::apply
void apply(T &result, const regular_formulas::regular_formula &x)
Definition builder.h:1024
mcrl2::regular_formulas::data_expression_builder
\brief Builder class
Definition builder.h:964
mcrl2::regular_formulas::regular_formula_builder_base
Builder class for regular_formula_builder. Used as a base class for pbes_expression_builder.
Definition builder.h:743
mcrl2::regular_formulas::regular_formula_builder_base::super
core::builder< Derived > super
Definition builder.h:744
mcrl2::regular_formulas::regular_formula_builder_base::apply
void apply(T &result, const data::data_expression &x)
Definition builder.h:748
mcrl2::regular_formulas::regular_formula_builder_base::apply
void apply(T &result, const action_formulas::action_formula &x)
Definition builder.h:758
mcrl2::regular_formulas::regular_formula_builder
\brief Builder class
Definition builder.h:1164
mcrl2::regular_formulas::sort_expression_builder
\brief Builder class
Definition builder.h:864
mcrl2::regular_formulas::variable_builder
\brief Builder class
Definition builder.h:1064
mcrl2::state_formulas::add_data_expressions
Definition builder.h:1561
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::nu &x)
Definition builder.h:1775
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::supremum &x)
Definition builder.h:1690
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::imp &x)
Definition builder.h:1627
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::state_formula &x)
Definition builder.h:1802
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::plus &x)
Definition builder.h:1636
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::yaled &x)
Definition builder.h:1726
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::false_ &x)
Definition builder.h:1580
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::yaled_timed &x)
Definition builder.h:1737
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::const_multiply &x)
Definition builder.h:1645
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::and_ &x)
Definition builder.h:1609
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::exists &x)
Definition builder.h:1672
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::may &x)
Definition builder.h:1717
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::minus &x)
Definition builder.h:1600
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::infimum &x)
Definition builder.h:1681
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::or_ &x)
Definition builder.h:1618
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::sum &x)
Definition builder.h:1699
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::mu &x)
Definition builder.h:1784
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::must &x)
Definition builder.h:1708
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::variable &x)
Definition builder.h:1766
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::not_ &x)
Definition builder.h:1591
mcrl2::state_formulas::add_data_expressions::super
Builder< Derived > super
Definition builder.h:1562
mcrl2::state_formulas::add_data_expressions::update
void update(state_formulas::state_formula_specification &x)
Definition builder.h:1792
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::delay &x)
Definition builder.h:1746
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::true_ &x)
Definition builder.h:1569
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::const_multiply_alt &x)
Definition builder.h:1654
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::forall &x)
Definition builder.h:1663
mcrl2::state_formulas::add_data_expressions::apply
void apply(T &result, const state_formulas::delay_timed &x)
Definition builder.h:1757
mcrl2::state_formulas::add_sort_expressions
Definition builder.h:1194
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::supremum &x)
Definition builder.h:1323
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::yaled &x)
Definition builder.h:1359
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::true_ &x)
Definition builder.h:1202
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::const_multiply &x)
Definition builder.h:1278
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::false_ &x)
Definition builder.h:1213
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::const_multiply_alt &x)
Definition builder.h:1287
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::sum &x)
Definition builder.h:1332
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::not_ &x)
Definition builder.h:1224
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::may &x)
Definition builder.h:1350
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::forall &x)
Definition builder.h:1296
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::exists &x)
Definition builder.h:1305
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::delay_timed &x)
Definition builder.h:1390
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::yaled_timed &x)
Definition builder.h:1370
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::mu &x)
Definition builder.h:1417
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::delay &x)
Definition builder.h:1379
mcrl2::state_formulas::add_sort_expressions::super
Builder< Derived > super
Definition builder.h:1195
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::must &x)
Definition builder.h:1341
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::infimum &x)
Definition builder.h:1314
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::imp &x)
Definition builder.h:1260
mcrl2::state_formulas::add_sort_expressions::update
void update(state_formulas::state_formula_specification &x)
Definition builder.h:1425
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::state_formula &x)
Definition builder.h:1438
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::nu &x)
Definition builder.h:1408
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::and_ &x)
Definition builder.h:1242
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::minus &x)
Definition builder.h:1233
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::variable &x)
Definition builder.h:1399
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::plus &x)
Definition builder.h:1269
mcrl2::state_formulas::add_sort_expressions::apply
void apply(T &result, const state_formulas::or_ &x)
Definition builder.h:1251
mcrl2::state_formulas::add_state_formula_expressions
Definition builder.h:2289
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::exists &x)
Definition builder.h:2400
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::yaled &x)
Definition builder.h:2454
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::plus &x)
Definition builder.h:2364
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::delay_timed &x)
Definition builder.h:2487
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::must &x)
Definition builder.h:2436
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::sum &x)
Definition builder.h:2427
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::infimum &x)
Definition builder.h:2409
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::const_multiply &x)
Definition builder.h:2373
mcrl2::state_formulas::add_state_formula_expressions::update
void update(state_formulas::state_formula_specification &x)
Definition builder.h:2526
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::may &x)
Definition builder.h:2445
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::false_ &x)
Definition builder.h:2308
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::or_ &x)
Definition builder.h:2346
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::imp &x)
Definition builder.h:2355
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::not_ &x)
Definition builder.h:2319
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::variable &x)
Definition builder.h:2498
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::forall &x)
Definition builder.h:2391
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::delay &x)
Definition builder.h:2476
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::yaled_timed &x)
Definition builder.h:2465
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::supremum &x)
Definition builder.h:2418
mcrl2::state_formulas::add_state_formula_expressions::super
Builder< Derived > super
Definition builder.h:2290
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::const_multiply_alt &x)
Definition builder.h:2382
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::nu &x)
Definition builder.h:2509
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::and_ &x)
Definition builder.h:2337
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::minus &x)
Definition builder.h:2328
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::mu &x)
Definition builder.h:2518
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::true_ &x)
Definition builder.h:2297
mcrl2::state_formulas::add_state_formula_expressions::apply
void apply(T &result, const state_formulas::state_formula &x)
Definition builder.h:2536
mcrl2::state_formulas::add_variables
Definition builder.h:1925
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::true_ &x)
Definition builder.h:1933
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::may &x)
Definition builder.h:2081
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::not_ &x)
Definition builder.h:1955
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::and_ &x)
Definition builder.h:1973
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::minus &x)
Definition builder.h:1964
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::delay &x)
Definition builder.h:2110
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::plus &x)
Definition builder.h:2000
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::yaled &x)
Definition builder.h:2090
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::exists &x)
Definition builder.h:2036
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::variable &x)
Definition builder.h:2130
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::sum &x)
Definition builder.h:2063
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::forall &x)
Definition builder.h:2027
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::infimum &x)
Definition builder.h:2045
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::mu &x)
Definition builder.h:2148
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::yaled_timed &x)
Definition builder.h:2101
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::supremum &x)
Definition builder.h:2054
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::false_ &x)
Definition builder.h:1944
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::or_ &x)
Definition builder.h:1982
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::delay_timed &x)
Definition builder.h:2121
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::const_multiply &x)
Definition builder.h:2009
mcrl2::state_formulas::add_variables::super
Builder< Derived > super
Definition builder.h:1926
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::state_formula &x)
Definition builder.h:2166
mcrl2::state_formulas::add_variables::update
void update(state_formulas::state_formula_specification &x)
Definition builder.h:2156
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::must &x)
Definition builder.h:2072
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::imp &x)
Definition builder.h:1991
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::const_multiply_alt &x)
Definition builder.h:2018
mcrl2::state_formulas::add_variables::apply
void apply(T &result, const state_formulas::nu &x)
Definition builder.h:2139
mcrl2::state_formulas::data_expression_builder
\brief Builder class
Definition builder.h:1918
mcrl2::state_formulas::sort_expression_builder
\brief Builder class
Definition builder.h:1554
mcrl2::state_formulas::state_formula_builder_base
Builder class for pbes_expressions. Used as a base class for pbes_expression_builder.
Definition builder.h:1176
mcrl2::state_formulas::state_formula_builder_base::super
core::builder< Derived > super
Definition builder.h:1177
mcrl2::state_formulas::state_formula_builder_base::apply
void apply(T &result, const data::data_expression &x)
Definition builder.h:1181
mcrl2::state_formulas::state_formula_builder
\brief Builder class
Definition builder.h:2652
mcrl2::state_formulas::variable_builder
\brief Builder class
Definition builder.h:2282