Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/modal_formula/builder.h
10 : /// \brief add your file description here.
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 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace action_formulas
22 : {
23 :
24 : /// \brief Base class for action_formula_builder.
25 : template <typename Derived>
26 : struct 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 ---//
42 : template <template <class> class Builder, class Derived>
43 : struct 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 103 : void apply(T& result, const action_formulas::true_& x)
53 : {
54 :
55 103 : result = x;
56 103 : static_cast<Derived&>(*this).enter(x);
57 : // skip
58 103 : static_cast<Derived&>(*this).leave(x);
59 103 : result = x;
60 103 : }
61 :
62 : template <class T>
63 6 : void apply(T& result, const action_formulas::false_& x)
64 : {
65 :
66 6 : result = x;
67 6 : static_cast<Derived&>(*this).enter(x);
68 : // skip
69 6 : static_cast<Derived&>(*this).leave(x);
70 6 : result = x;
71 6 : }
72 :
73 : template <class T>
74 69 : void apply(T& result, const action_formulas::not_& x)
75 : {
76 :
77 69 : static_cast<Derived&>(*this).enter(x);
78 138 : action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
79 69 : static_cast<Derived&>(*this).leave(x);
80 69 : }
81 :
82 : template <class T>
83 22 : void apply(T& result, const action_formulas::and_& x)
84 : {
85 :
86 22 : static_cast<Derived&>(*this).enter(x);
87 66 : 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 22 : static_cast<Derived&>(*this).leave(x);
89 22 : }
90 :
91 : template <class T>
92 9 : void apply(T& result, const action_formulas::or_& x)
93 : {
94 :
95 9 : static_cast<Derived&>(*this).enter(x);
96 27 : 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 9 : static_cast<Derived&>(*this).leave(x);
98 9 : }
99 :
100 : template <class T>
101 0 : void apply(T& result, const action_formulas::imp& x)
102 : {
103 :
104 0 : static_cast<Derived&>(*this).enter(x);
105 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
107 0 : }
108 :
109 : template <class T>
110 9 : void apply(T& result, const action_formulas::forall& x)
111 : {
112 :
113 9 : static_cast<Derived&>(*this).enter(x);
114 27 : 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 9 : static_cast<Derived&>(*this).leave(x);
116 9 : }
117 :
118 : template <class T>
119 5 : void apply(T& result, const action_formulas::exists& x)
120 : {
121 :
122 5 : static_cast<Derived&>(*this).enter(x);
123 15 : 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 5 : static_cast<Derived&>(*this).leave(x);
125 5 : }
126 :
127 : template <class T>
128 0 : void apply(T& result, const action_formulas::at& x)
129 : {
130 :
131 0 : static_cast<Derived&>(*this).enter(x);
132 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
134 0 : }
135 :
136 : template <class T>
137 212 : void apply(T& result, const action_formulas::multi_action& x)
138 : {
139 :
140 212 : static_cast<Derived&>(*this).enter(x);
141 424 : action_formulas::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
142 212 : static_cast<Derived&>(*this).leave(x);
143 212 : }
144 :
145 : template <class T>
146 614 : void apply(T& result, const action_formulas::action_formula& x)
147 : {
148 :
149 614 : static_cast<Derived&>(*this).enter(x);
150 614 : if (data::is_data_expression(x))
151 : {
152 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
153 : }
154 614 : else if (data::is_untyped_data_parameter(x))
155 : {
156 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
157 : }
158 614 : else if (action_formulas::is_true(x))
159 : {
160 103 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
161 : }
162 511 : else if (action_formulas::is_false(x))
163 : {
164 6 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
165 : }
166 505 : else if (action_formulas::is_not(x))
167 : {
168 69 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
169 : }
170 436 : else if (action_formulas::is_and(x))
171 : {
172 22 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
173 : }
174 414 : else if (action_formulas::is_or(x))
175 : {
176 9 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
177 : }
178 405 : else if (action_formulas::is_imp(x))
179 : {
180 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
181 : }
182 405 : else if (action_formulas::is_forall(x))
183 : {
184 9 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
185 : }
186 396 : else if (action_formulas::is_exists(x))
187 : {
188 5 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
189 : }
190 391 : else if (action_formulas::is_at(x))
191 : {
192 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
193 : }
194 391 : else if (action_formulas::is_multi_action(x))
195 : {
196 212 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
197 : }
198 179 : else if (process::is_untyped_multi_action(x))
199 : {
200 179 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
201 : }
202 614 : static_cast<Derived&>(*this).leave(x);
203 614 : }
204 :
205 : };
206 :
207 : /// \\brief Builder class
208 : template <typename Derived>
209 : struct 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 ---//
215 : template <template <class> class Builder, class Derived>
216 : struct 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 60 : void apply(T& result, const action_formulas::true_& x)
226 : {
227 :
228 60 : result = x;
229 60 : static_cast<Derived&>(*this).enter(x);
230 : // skip
231 60 : static_cast<Derived&>(*this).leave(x);
232 60 : result = x;
233 60 : }
234 :
235 : template <class T>
236 2 : void apply(T& result, const action_formulas::false_& x)
237 : {
238 :
239 2 : result = x;
240 2 : static_cast<Derived&>(*this).enter(x);
241 : // skip
242 2 : static_cast<Derived&>(*this).leave(x);
243 2 : result = x;
244 2 : }
245 :
246 : template <class T>
247 35 : void apply(T& result, const action_formulas::not_& x)
248 : {
249 :
250 35 : static_cast<Derived&>(*this).enter(x);
251 70 : action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
252 35 : static_cast<Derived&>(*this).leave(x);
253 35 : }
254 :
255 : template <class T>
256 9 : void apply(T& result, const action_formulas::and_& x)
257 : {
258 :
259 9 : static_cast<Derived&>(*this).enter(x);
260 27 : 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 9 : static_cast<Derived&>(*this).leave(x);
262 9 : }
263 :
264 : template <class T>
265 3 : void apply(T& result, const action_formulas::or_& x)
266 : {
267 :
268 3 : static_cast<Derived&>(*this).enter(x);
269 9 : 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 3 : static_cast<Derived&>(*this).leave(x);
271 3 : }
272 :
273 : template <class T>
274 0 : void apply(T& result, const action_formulas::imp& x)
275 : {
276 :
277 0 : static_cast<Derived&>(*this).enter(x);
278 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
280 0 : }
281 :
282 : template <class T>
283 3 : void apply(T& result, const action_formulas::forall& x)
284 : {
285 :
286 3 : static_cast<Derived&>(*this).enter(x);
287 6 : action_formulas::make_forall(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
288 3 : static_cast<Derived&>(*this).leave(x);
289 3 : }
290 :
291 : template <class T>
292 2 : void apply(T& result, const action_formulas::exists& x)
293 : {
294 :
295 2 : static_cast<Derived&>(*this).enter(x);
296 4 : action_formulas::make_exists(result, x.variables(), [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
297 2 : static_cast<Derived&>(*this).leave(x);
298 2 : }
299 :
300 : template <class T>
301 0 : void apply(T& result, const action_formulas::at& x)
302 : {
303 :
304 0 : static_cast<Derived&>(*this).enter(x);
305 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
307 0 : }
308 :
309 : template <class T>
310 191 : void apply(T& result, const action_formulas::multi_action& x)
311 : {
312 :
313 191 : static_cast<Derived&>(*this).enter(x);
314 382 : action_formulas::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
315 191 : static_cast<Derived&>(*this).leave(x);
316 191 : }
317 :
318 : template <class T>
319 305 : void apply(T& result, const action_formulas::action_formula& x)
320 : {
321 :
322 305 : static_cast<Derived&>(*this).enter(x);
323 305 : if (data::is_data_expression(x))
324 : {
325 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
326 : }
327 305 : else if (data::is_untyped_data_parameter(x))
328 : {
329 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
330 : }
331 305 : else if (action_formulas::is_true(x))
332 : {
333 60 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
334 : }
335 245 : else if (action_formulas::is_false(x))
336 : {
337 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
338 : }
339 243 : else if (action_formulas::is_not(x))
340 : {
341 35 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
342 : }
343 208 : else if (action_formulas::is_and(x))
344 : {
345 9 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
346 : }
347 199 : else if (action_formulas::is_or(x))
348 : {
349 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
350 : }
351 196 : else if (action_formulas::is_imp(x))
352 : {
353 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
354 : }
355 196 : else if (action_formulas::is_forall(x))
356 : {
357 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
358 : }
359 193 : else if (action_formulas::is_exists(x))
360 : {
361 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
362 : }
363 191 : else if (action_formulas::is_at(x))
364 : {
365 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
366 : }
367 191 : else if (action_formulas::is_multi_action(x))
368 : {
369 191 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
370 : }
371 0 : else if (process::is_untyped_multi_action(x))
372 : {
373 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
374 : }
375 305 : static_cast<Derived&>(*this).leave(x);
376 305 : }
377 :
378 : };
379 :
380 : /// \\brief Builder class
381 : template <typename Derived>
382 : struct 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 ---//
388 : template <template <class> class Builder, class Derived>
389 : struct 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 :
553 : /// \\brief Builder class
554 : template <typename Derived>
555 : struct 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 ---//
561 : template <template <class> class Builder, class Derived>
562 : struct 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 61 : void apply(T& result, const action_formulas::true_& x)
572 : {
573 :
574 61 : result = x;
575 61 : static_cast<Derived&>(*this).enter(x);
576 : // skip
577 61 : static_cast<Derived&>(*this).leave(x);
578 61 : result = x;
579 61 : }
580 :
581 : template <class T>
582 2 : void apply(T& result, const action_formulas::false_& x)
583 : {
584 :
585 2 : result = x;
586 2 : static_cast<Derived&>(*this).enter(x);
587 : // skip
588 2 : static_cast<Derived&>(*this).leave(x);
589 2 : result = x;
590 2 : }
591 :
592 : template <class T>
593 37 : void apply(T& result, const action_formulas::not_& x)
594 : {
595 :
596 37 : static_cast<Derived&>(*this).enter(x);
597 74 : action_formulas::make_not_(result, [&](action_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
598 37 : static_cast<Derived&>(*this).leave(x);
599 37 : }
600 :
601 : template <class T>
602 9 : void apply(T& result, const action_formulas::and_& x)
603 : {
604 :
605 9 : static_cast<Derived&>(*this).enter(x);
606 27 : 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 9 : static_cast<Derived&>(*this).leave(x);
608 9 : }
609 :
610 : template <class T>
611 3 : void apply(T& result, const action_formulas::or_& x)
612 : {
613 :
614 3 : static_cast<Derived&>(*this).enter(x);
615 9 : 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 3 : static_cast<Derived&>(*this).leave(x);
617 3 : }
618 :
619 : template <class T>
620 0 : void apply(T& result, const action_formulas::imp& x)
621 : {
622 :
623 0 : static_cast<Derived&>(*this).enter(x);
624 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
626 0 : }
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 0 : void apply(T& result, const action_formulas::multi_action& x)
657 : {
658 :
659 0 : result = x;
660 0 : static_cast<Derived&>(*this).enter(x);
661 : // skip
662 0 : static_cast<Derived&>(*this).leave(x);
663 0 : result = x;
664 0 : }
665 :
666 : template <class T>
667 296 : void apply(T& result, const action_formulas::action_formula& x)
668 : {
669 :
670 296 : static_cast<Derived&>(*this).enter(x);
671 296 : if (data::is_data_expression(x))
672 : {
673 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
674 : }
675 296 : else if (data::is_untyped_data_parameter(x))
676 : {
677 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
678 : }
679 296 : else if (action_formulas::is_true(x))
680 : {
681 61 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::true_>(x));
682 : }
683 235 : else if (action_formulas::is_false(x))
684 : {
685 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::false_>(x));
686 : }
687 233 : else if (action_formulas::is_not(x))
688 : {
689 37 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::not_>(x));
690 : }
691 196 : else if (action_formulas::is_and(x))
692 : {
693 9 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::and_>(x));
694 : }
695 187 : else if (action_formulas::is_or(x))
696 : {
697 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::or_>(x));
698 : }
699 184 : else if (action_formulas::is_imp(x))
700 : {
701 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::imp>(x));
702 : }
703 184 : else if (action_formulas::is_forall(x))
704 : {
705 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::forall>(x));
706 : }
707 181 : else if (action_formulas::is_exists(x))
708 : {
709 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::exists>(x));
710 : }
711 179 : else if (action_formulas::is_at(x))
712 : {
713 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::at>(x));
714 : }
715 179 : else if (action_formulas::is_multi_action(x))
716 : {
717 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::multi_action>(x));
718 : }
719 179 : else if (process::is_untyped_multi_action(x))
720 : {
721 179 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_multi_action>(x));
722 : }
723 296 : static_cast<Derived&>(*this).leave(x);
724 296 : }
725 :
726 : };
727 :
728 : /// \\brief Builder class
729 : template <typename Derived>
730 : struct 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 :
737 : namespace regular_formulas
738 : {
739 :
740 : /// \brief Builder class for regular_formula_builder. Used as a base class for pbes_expression_builder.
741 : template <typename Derived>
742 : struct 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 0 : void apply(T& result, const data::data_expression& x)
749 : // void apply(regular_formula& result, const data::data_expression& x)
750 : {
751 0 : static_cast<Derived&>(*this).enter(x);
752 : // skip
753 0 : static_cast<Derived&>(*this).leave(x);
754 0 : result = x;
755 0 : }
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 ---//
769 : template <template <class> class Builder, class Derived>
770 : struct 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 0 : void apply(T& result, const regular_formulas::seq& x)
780 : {
781 :
782 0 : static_cast<Derived&>(*this).enter(x);
783 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
785 0 : }
786 :
787 : template <class T>
788 0 : void apply(T& result, const regular_formulas::alt& x)
789 : {
790 :
791 0 : static_cast<Derived&>(*this).enter(x);
792 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
794 0 : }
795 :
796 : template <class T>
797 0 : void apply(T& result, const regular_formulas::trans& x)
798 : {
799 :
800 0 : static_cast<Derived&>(*this).enter(x);
801 0 : regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
802 0 : static_cast<Derived&>(*this).leave(x);
803 0 : }
804 :
805 : template <class T>
806 33 : void apply(T& result, const regular_formulas::trans_or_nil& x)
807 : {
808 :
809 33 : static_cast<Derived&>(*this).enter(x);
810 66 : regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
811 33 : static_cast<Derived&>(*this).leave(x);
812 33 : }
813 :
814 : template <class T>
815 5 : void apply(T& result, const regular_formulas::untyped_regular_formula& x)
816 : {
817 :
818 5 : static_cast<Derived&>(*this).enter(x);
819 15 : 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 5 : static_cast<Derived&>(*this).leave(x);
821 5 : }
822 :
823 : template <class T>
824 507 : void apply(T& result, const regular_formulas::regular_formula& x)
825 : {
826 :
827 507 : static_cast<Derived&>(*this).enter(x);
828 507 : if (data::is_data_expression(x))
829 : {
830 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
831 : }
832 507 : else if (action_formulas::is_action_formula(x))
833 : {
834 469 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
835 : }
836 38 : else if (regular_formulas::is_seq(x))
837 : {
838 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
839 : }
840 38 : else if (regular_formulas::is_alt(x))
841 : {
842 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
843 : }
844 38 : else if (regular_formulas::is_trans(x))
845 : {
846 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
847 : }
848 38 : else if (regular_formulas::is_trans_or_nil(x))
849 : {
850 33 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
851 : }
852 5 : else if (regular_formulas::is_untyped_regular_formula(x))
853 : {
854 5 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
855 : }
856 507 : static_cast<Derived&>(*this).leave(x);
857 507 : }
858 :
859 : };
860 :
861 : /// \\brief Builder class
862 : template <typename Derived>
863 : struct 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 ---//
869 : template <template <class> class Builder, class Derived>
870 : struct 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 0 : void apply(T& result, const regular_formulas::seq& x)
880 : {
881 :
882 0 : static_cast<Derived&>(*this).enter(x);
883 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
885 0 : }
886 :
887 : template <class T>
888 0 : void apply(T& result, const regular_formulas::alt& x)
889 : {
890 :
891 0 : static_cast<Derived&>(*this).enter(x);
892 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
894 0 : }
895 :
896 : template <class T>
897 0 : void apply(T& result, const regular_formulas::trans& x)
898 : {
899 :
900 0 : static_cast<Derived&>(*this).enter(x);
901 0 : regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
902 0 : static_cast<Derived&>(*this).leave(x);
903 0 : }
904 :
905 : template <class T>
906 2 : void apply(T& result, const regular_formulas::trans_or_nil& x)
907 : {
908 :
909 2 : static_cast<Derived&>(*this).enter(x);
910 4 : regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
911 2 : static_cast<Derived&>(*this).leave(x);
912 2 : }
913 :
914 : template <class T>
915 0 : void apply(T& result, const regular_formulas::untyped_regular_formula& x)
916 : {
917 :
918 0 : static_cast<Derived&>(*this).enter(x);
919 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
921 0 : }
922 :
923 : template <class T>
924 234 : void apply(T& result, const regular_formulas::regular_formula& x)
925 : {
926 :
927 234 : static_cast<Derived&>(*this).enter(x);
928 234 : if (data::is_data_expression(x))
929 : {
930 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
931 : }
932 234 : else if (action_formulas::is_action_formula(x))
933 : {
934 232 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
935 : }
936 2 : else if (regular_formulas::is_seq(x))
937 : {
938 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
939 : }
940 2 : else if (regular_formulas::is_alt(x))
941 : {
942 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
943 : }
944 2 : else if (regular_formulas::is_trans(x))
945 : {
946 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
947 : }
948 2 : else if (regular_formulas::is_trans_or_nil(x))
949 : {
950 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
951 : }
952 0 : else if (regular_formulas::is_untyped_regular_formula(x))
953 : {
954 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
955 : }
956 234 : static_cast<Derived&>(*this).leave(x);
957 234 : }
958 :
959 : };
960 :
961 : /// \\brief Builder class
962 : template <typename Derived>
963 : struct 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 ---//
969 : template <template <class> class Builder, class Derived>
970 : struct 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 :
1061 : /// \\brief Builder class
1062 : template <typename Derived>
1063 : struct 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 ---//
1069 : template <template <class> class Builder, class Derived>
1070 : struct 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 0 : void apply(T& result, const regular_formulas::seq& x)
1080 : {
1081 :
1082 0 : static_cast<Derived&>(*this).enter(x);
1083 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
1085 0 : }
1086 :
1087 : template <class T>
1088 0 : void apply(T& result, const regular_formulas::alt& x)
1089 : {
1090 :
1091 0 : static_cast<Derived&>(*this).enter(x);
1092 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
1094 0 : }
1095 :
1096 : template <class T>
1097 0 : void apply(T& result, const regular_formulas::trans& x)
1098 : {
1099 :
1100 0 : static_cast<Derived&>(*this).enter(x);
1101 0 : regular_formulas::make_trans(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1102 0 : static_cast<Derived&>(*this).leave(x);
1103 0 : }
1104 :
1105 : template <class T>
1106 33 : void apply(T& result, const regular_formulas::trans_or_nil& x)
1107 : {
1108 :
1109 33 : static_cast<Derived&>(*this).enter(x);
1110 66 : regular_formulas::make_trans_or_nil(result, [&](regular_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1111 33 : static_cast<Derived&>(*this).leave(x);
1112 33 : }
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 268 : void apply(T& result, const regular_formulas::regular_formula& x)
1125 : {
1126 :
1127 268 : static_cast<Derived&>(*this).enter(x);
1128 268 : if (data::is_data_expression(x))
1129 : {
1130 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1131 : }
1132 268 : else if (action_formulas::is_action_formula(x))
1133 : {
1134 230 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<action_formulas::action_formula>(x));
1135 : }
1136 38 : else if (regular_formulas::is_seq(x))
1137 : {
1138 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::seq>(x));
1139 : }
1140 38 : else if (regular_formulas::is_alt(x))
1141 : {
1142 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::alt>(x));
1143 : }
1144 38 : else if (regular_formulas::is_trans(x))
1145 : {
1146 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans>(x));
1147 : }
1148 38 : else if (regular_formulas::is_trans_or_nil(x))
1149 : {
1150 33 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::trans_or_nil>(x));
1151 : }
1152 5 : else if (regular_formulas::is_untyped_regular_formula(x))
1153 : {
1154 5 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<regular_formulas::untyped_regular_formula>(x));
1155 : }
1156 268 : static_cast<Derived&>(*this).leave(x);
1157 268 : }
1158 :
1159 : };
1160 :
1161 : /// \\brief Builder class
1162 : template <typename Derived>
1163 : struct 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 :
1170 : namespace state_formulas
1171 : {
1172 :
1173 : /// \brief Builder class for pbes_expressions. Used as a base class for pbes_expression_builder.
1174 : template <typename Derived>
1175 : struct 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 18 : void apply(T& result, const data::data_expression& x)
1182 : {
1183 18 : static_cast<Derived&>(*this).enter(x);
1184 : // skip
1185 18 : static_cast<Derived&>(*this).leave(x);
1186 18 : result = x;
1187 18 : }
1188 :
1189 : };
1190 :
1191 : //--- start generated state_formulas::add_sort_expressions code ---//
1192 : template <template <class> class Builder, class Derived>
1193 : struct 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 184 : void apply(T& result, const state_formulas::true_& x)
1203 : {
1204 :
1205 184 : result = x;
1206 184 : static_cast<Derived&>(*this).enter(x);
1207 : // skip
1208 184 : static_cast<Derived&>(*this).leave(x);
1209 184 : result = x;
1210 184 : }
1211 :
1212 : template <class T>
1213 84 : void apply(T& result, const state_formulas::false_& x)
1214 : {
1215 :
1216 84 : result = x;
1217 84 : static_cast<Derived&>(*this).enter(x);
1218 : // skip
1219 84 : static_cast<Derived&>(*this).leave(x);
1220 84 : result = x;
1221 84 : }
1222 :
1223 : template <class T>
1224 109 : void apply(T& result, const state_formulas::not_& x)
1225 : {
1226 :
1227 109 : static_cast<Derived&>(*this).enter(x);
1228 218 : state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1229 109 : static_cast<Derived&>(*this).leave(x);
1230 109 : }
1231 :
1232 : template <class T>
1233 0 : void apply(T& result, const state_formulas::minus& x)
1234 : {
1235 :
1236 0 : static_cast<Derived&>(*this).enter(x);
1237 0 : state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1238 0 : static_cast<Derived&>(*this).leave(x);
1239 0 : }
1240 :
1241 : template <class T>
1242 143 : void apply(T& result, const state_formulas::and_& x)
1243 : {
1244 :
1245 143 : static_cast<Derived&>(*this).enter(x);
1246 429 : 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 143 : static_cast<Derived&>(*this).leave(x);
1248 143 : }
1249 :
1250 : template <class T>
1251 67 : void apply(T& result, const state_formulas::or_& x)
1252 : {
1253 :
1254 67 : static_cast<Derived&>(*this).enter(x);
1255 201 : 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 67 : static_cast<Derived&>(*this).leave(x);
1257 67 : }
1258 :
1259 : template <class T>
1260 38 : void apply(T& result, const state_formulas::imp& x)
1261 : {
1262 :
1263 38 : static_cast<Derived&>(*this).enter(x);
1264 114 : 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 38 : static_cast<Derived&>(*this).leave(x);
1266 38 : }
1267 :
1268 : template <class T>
1269 0 : void apply(T& result, const state_formulas::plus& x)
1270 : {
1271 :
1272 0 : static_cast<Derived&>(*this).enter(x);
1273 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
1275 0 : }
1276 :
1277 : template <class T>
1278 1 : void apply(T& result, const state_formulas::const_multiply& x)
1279 : {
1280 :
1281 1 : static_cast<Derived&>(*this).enter(x);
1282 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1284 1 : }
1285 :
1286 : template <class T>
1287 1 : void apply(T& result, const state_formulas::const_multiply_alt& x)
1288 : {
1289 :
1290 1 : static_cast<Derived&>(*this).enter(x);
1291 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1293 1 : }
1294 :
1295 : template <class T>
1296 28 : void apply(T& result, const state_formulas::forall& x)
1297 : {
1298 :
1299 28 : static_cast<Derived&>(*this).enter(x);
1300 84 : 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 28 : static_cast<Derived&>(*this).leave(x);
1302 28 : }
1303 :
1304 : template <class T>
1305 14 : void apply(T& result, const state_formulas::exists& x)
1306 : {
1307 :
1308 14 : static_cast<Derived&>(*this).enter(x);
1309 42 : 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 14 : static_cast<Derived&>(*this).leave(x);
1311 14 : }
1312 :
1313 : template <class T>
1314 2 : void apply(T& result, const state_formulas::infimum& x)
1315 : {
1316 :
1317 2 : static_cast<Derived&>(*this).enter(x);
1318 6 : 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 2 : static_cast<Derived&>(*this).leave(x);
1320 2 : }
1321 :
1322 : template <class T>
1323 1 : void apply(T& result, const state_formulas::supremum& x)
1324 : {
1325 :
1326 1 : static_cast<Derived&>(*this).enter(x);
1327 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1329 1 : }
1330 :
1331 : template <class T>
1332 1 : void apply(T& result, const state_formulas::sum& x)
1333 : {
1334 :
1335 1 : static_cast<Derived&>(*this).enter(x);
1336 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1338 1 : }
1339 :
1340 : template <class T>
1341 250 : void apply(T& result, const state_formulas::must& x)
1342 : {
1343 :
1344 250 : static_cast<Derived&>(*this).enter(x);
1345 750 : 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 250 : static_cast<Derived&>(*this).leave(x);
1347 250 : }
1348 :
1349 : template <class T>
1350 214 : void apply(T& result, const state_formulas::may& x)
1351 : {
1352 :
1353 214 : static_cast<Derived&>(*this).enter(x);
1354 642 : 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 214 : static_cast<Derived&>(*this).leave(x);
1356 214 : }
1357 :
1358 : template <class T>
1359 0 : void apply(T& result, const state_formulas::yaled& x)
1360 : {
1361 :
1362 0 : result = x;
1363 0 : static_cast<Derived&>(*this).enter(x);
1364 : // skip
1365 0 : static_cast<Derived&>(*this).leave(x);
1366 0 : result = x;
1367 0 : }
1368 :
1369 : template <class T>
1370 3 : void apply(T& result, const state_formulas::yaled_timed& x)
1371 : {
1372 :
1373 3 : static_cast<Derived&>(*this).enter(x);
1374 6 : state_formulas::make_yaled_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1375 3 : static_cast<Derived&>(*this).leave(x);
1376 3 : }
1377 :
1378 : template <class T>
1379 0 : void apply(T& result, const state_formulas::delay& x)
1380 : {
1381 :
1382 0 : result = x;
1383 0 : static_cast<Derived&>(*this).enter(x);
1384 : // skip
1385 0 : static_cast<Derived&>(*this).leave(x);
1386 0 : result = x;
1387 0 : }
1388 :
1389 : template <class T>
1390 5 : void apply(T& result, const state_formulas::delay_timed& x)
1391 : {
1392 :
1393 5 : static_cast<Derived&>(*this).enter(x);
1394 10 : state_formulas::make_delay_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1395 5 : static_cast<Derived&>(*this).leave(x);
1396 5 : }
1397 :
1398 : template <class T>
1399 108 : void apply(T& result, const state_formulas::variable& x)
1400 : {
1401 :
1402 108 : static_cast<Derived&>(*this).enter(x);
1403 216 : state_formulas::make_variable(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
1404 108 : static_cast<Derived&>(*this).leave(x);
1405 108 : }
1406 :
1407 : template <class T>
1408 119 : void apply(T& result, const state_formulas::nu& x)
1409 : {
1410 :
1411 119 : static_cast<Derived&>(*this).enter(x);
1412 357 : 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 119 : static_cast<Derived&>(*this).leave(x);
1414 119 : }
1415 :
1416 : template <class T>
1417 165 : void apply(T& result, const state_formulas::mu& x)
1418 : {
1419 :
1420 165 : static_cast<Derived&>(*this).enter(x);
1421 495 : 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 165 : static_cast<Derived&>(*this).leave(x);
1423 165 : }
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 1722 : void apply(T& result, const state_formulas::state_formula& x)
1439 : {
1440 :
1441 1722 : static_cast<Derived&>(*this).enter(x);
1442 1722 : if (data::is_data_expression(x))
1443 : {
1444 42 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1445 : }
1446 1680 : else if (data::is_untyped_data_parameter(x))
1447 : {
1448 143 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1449 : }
1450 1537 : else if (state_formulas::is_true(x))
1451 : {
1452 184 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
1453 : }
1454 1353 : else if (state_formulas::is_false(x))
1455 : {
1456 84 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
1457 : }
1458 1269 : else if (state_formulas::is_not(x))
1459 : {
1460 109 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
1461 : }
1462 1160 : else if (state_formulas::is_minus(x))
1463 : {
1464 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
1465 : }
1466 1160 : else if (state_formulas::is_and(x))
1467 : {
1468 143 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
1469 : }
1470 1017 : else if (state_formulas::is_or(x))
1471 : {
1472 67 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
1473 : }
1474 950 : else if (state_formulas::is_imp(x))
1475 : {
1476 38 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
1477 : }
1478 912 : else if (state_formulas::is_plus(x))
1479 : {
1480 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
1481 : }
1482 912 : else if (state_formulas::is_const_multiply(x))
1483 : {
1484 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
1485 : }
1486 911 : else if (state_formulas::is_const_multiply_alt(x))
1487 : {
1488 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
1489 : }
1490 910 : else if (state_formulas::is_forall(x))
1491 : {
1492 28 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
1493 : }
1494 882 : else if (state_formulas::is_exists(x))
1495 : {
1496 14 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
1497 : }
1498 868 : else if (state_formulas::is_infimum(x))
1499 : {
1500 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
1501 : }
1502 866 : else if (state_formulas::is_supremum(x))
1503 : {
1504 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
1505 : }
1506 865 : else if (state_formulas::is_sum(x))
1507 : {
1508 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
1509 : }
1510 864 : else if (state_formulas::is_must(x))
1511 : {
1512 250 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
1513 : }
1514 614 : else if (state_formulas::is_may(x))
1515 : {
1516 214 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
1517 : }
1518 400 : else if (state_formulas::is_yaled(x))
1519 : {
1520 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
1521 : }
1522 400 : else if (state_formulas::is_yaled_timed(x))
1523 : {
1524 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
1525 : }
1526 397 : else if (state_formulas::is_delay(x))
1527 : {
1528 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
1529 : }
1530 397 : else if (state_formulas::is_delay_timed(x))
1531 : {
1532 5 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
1533 : }
1534 392 : else if (state_formulas::is_variable(x))
1535 : {
1536 108 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
1537 : }
1538 284 : else if (state_formulas::is_nu(x))
1539 : {
1540 119 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
1541 : }
1542 165 : else if (state_formulas::is_mu(x))
1543 : {
1544 165 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
1545 : }
1546 1722 : static_cast<Derived&>(*this).leave(x);
1547 1722 : }
1548 :
1549 : };
1550 :
1551 : /// \\brief Builder class
1552 : template <typename Derived>
1553 : struct 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 ---//
1559 : template <template <class> class Builder, class Derived>
1560 : struct 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 97 : void apply(T& result, const state_formulas::true_& x)
1570 : {
1571 :
1572 97 : result = x;
1573 97 : static_cast<Derived&>(*this).enter(x);
1574 : // skip
1575 97 : static_cast<Derived&>(*this).leave(x);
1576 97 : result = x;
1577 97 : }
1578 :
1579 : template <class T>
1580 38 : void apply(T& result, const state_formulas::false_& x)
1581 : {
1582 :
1583 38 : result = x;
1584 38 : static_cast<Derived&>(*this).enter(x);
1585 : // skip
1586 38 : static_cast<Derived&>(*this).leave(x);
1587 38 : result = x;
1588 38 : }
1589 :
1590 : template <class T>
1591 39 : void apply(T& result, const state_formulas::not_& x)
1592 : {
1593 :
1594 39 : static_cast<Derived&>(*this).enter(x);
1595 78 : state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1596 39 : static_cast<Derived&>(*this).leave(x);
1597 39 : }
1598 :
1599 : template <class T>
1600 0 : void apply(T& result, const state_formulas::minus& x)
1601 : {
1602 :
1603 0 : static_cast<Derived&>(*this).enter(x);
1604 0 : state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1605 0 : static_cast<Derived&>(*this).leave(x);
1606 0 : }
1607 :
1608 : template <class T>
1609 91 : void apply(T& result, const state_formulas::and_& x)
1610 : {
1611 :
1612 91 : static_cast<Derived&>(*this).enter(x);
1613 273 : 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 91 : static_cast<Derived&>(*this).leave(x);
1615 91 : }
1616 :
1617 : template <class T>
1618 46 : void apply(T& result, const state_formulas::or_& x)
1619 : {
1620 :
1621 46 : static_cast<Derived&>(*this).enter(x);
1622 138 : 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 46 : static_cast<Derived&>(*this).leave(x);
1624 46 : }
1625 :
1626 : template <class T>
1627 24 : void apply(T& result, const state_formulas::imp& x)
1628 : {
1629 :
1630 24 : static_cast<Derived&>(*this).enter(x);
1631 72 : 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 24 : static_cast<Derived&>(*this).leave(x);
1633 24 : }
1634 :
1635 : template <class T>
1636 0 : void apply(T& result, const state_formulas::plus& x)
1637 : {
1638 :
1639 0 : static_cast<Derived&>(*this).enter(x);
1640 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
1642 0 : }
1643 :
1644 : template <class T>
1645 1 : void apply(T& result, const state_formulas::const_multiply& x)
1646 : {
1647 :
1648 1 : static_cast<Derived&>(*this).enter(x);
1649 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1651 1 : }
1652 :
1653 : template <class T>
1654 1 : void apply(T& result, const state_formulas::const_multiply_alt& x)
1655 : {
1656 :
1657 1 : static_cast<Derived&>(*this).enter(x);
1658 3 : 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 1 : static_cast<Derived&>(*this).leave(x);
1660 1 : }
1661 :
1662 : template <class T>
1663 19 : void apply(T& result, const state_formulas::forall& x)
1664 : {
1665 :
1666 19 : static_cast<Derived&>(*this).enter(x);
1667 38 : state_formulas::make_forall(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1668 19 : static_cast<Derived&>(*this).leave(x);
1669 19 : }
1670 :
1671 : template <class T>
1672 8 : void apply(T& result, const state_formulas::exists& x)
1673 : {
1674 :
1675 8 : static_cast<Derived&>(*this).enter(x);
1676 16 : state_formulas::make_exists(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1677 8 : static_cast<Derived&>(*this).leave(x);
1678 8 : }
1679 :
1680 : template <class T>
1681 2 : void apply(T& result, const state_formulas::infimum& x)
1682 : {
1683 :
1684 2 : static_cast<Derived&>(*this).enter(x);
1685 4 : state_formulas::make_infimum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1686 2 : static_cast<Derived&>(*this).leave(x);
1687 2 : }
1688 :
1689 : template <class T>
1690 1 : void apply(T& result, const state_formulas::supremum& x)
1691 : {
1692 :
1693 1 : static_cast<Derived&>(*this).enter(x);
1694 2 : state_formulas::make_supremum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1695 1 : static_cast<Derived&>(*this).leave(x);
1696 1 : }
1697 :
1698 : template <class T>
1699 1 : void apply(T& result, const state_formulas::sum& x)
1700 : {
1701 :
1702 1 : static_cast<Derived&>(*this).enter(x);
1703 2 : state_formulas::make_sum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
1704 1 : static_cast<Derived&>(*this).leave(x);
1705 1 : }
1706 :
1707 : template <class T>
1708 136 : void apply(T& result, const state_formulas::must& x)
1709 : {
1710 :
1711 136 : static_cast<Derived&>(*this).enter(x);
1712 408 : 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 136 : static_cast<Derived&>(*this).leave(x);
1714 136 : }
1715 :
1716 : template <class T>
1717 96 : void apply(T& result, const state_formulas::may& x)
1718 : {
1719 :
1720 96 : static_cast<Derived&>(*this).enter(x);
1721 288 : 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 96 : static_cast<Derived&>(*this).leave(x);
1723 96 : }
1724 :
1725 : template <class T>
1726 0 : void apply(T& result, const state_formulas::yaled& x)
1727 : {
1728 :
1729 0 : result = x;
1730 0 : static_cast<Derived&>(*this).enter(x);
1731 : // skip
1732 0 : static_cast<Derived&>(*this).leave(x);
1733 0 : result = x;
1734 0 : }
1735 :
1736 : template <class T>
1737 1 : void apply(T& result, const state_formulas::yaled_timed& x)
1738 : {
1739 :
1740 1 : static_cast<Derived&>(*this).enter(x);
1741 2 : state_formulas::make_yaled_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1742 1 : static_cast<Derived&>(*this).leave(x);
1743 1 : }
1744 :
1745 : template <class T>
1746 0 : void apply(T& result, const state_formulas::delay& x)
1747 : {
1748 :
1749 0 : result = x;
1750 0 : static_cast<Derived&>(*this).enter(x);
1751 : // skip
1752 0 : static_cast<Derived&>(*this).leave(x);
1753 0 : result = x;
1754 0 : }
1755 :
1756 : template <class T>
1757 3 : void apply(T& result, const state_formulas::delay_timed& x)
1758 : {
1759 :
1760 3 : static_cast<Derived&>(*this).enter(x);
1761 6 : state_formulas::make_delay_timed(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
1762 3 : static_cast<Derived&>(*this).leave(x);
1763 3 : }
1764 :
1765 : template <class T>
1766 174 : void apply(T& result, const state_formulas::variable& x)
1767 : {
1768 :
1769 174 : static_cast<Derived&>(*this).enter(x);
1770 348 : state_formulas::make_variable(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
1771 174 : static_cast<Derived&>(*this).leave(x);
1772 174 : }
1773 :
1774 : template <class T>
1775 82 : void apply(T& result, const state_formulas::nu& x)
1776 : {
1777 :
1778 82 : static_cast<Derived&>(*this).enter(x);
1779 246 : 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 82 : static_cast<Derived&>(*this).leave(x);
1781 82 : }
1782 :
1783 : template <class T>
1784 117 : void apply(T& result, const state_formulas::mu& x)
1785 : {
1786 :
1787 117 : static_cast<Derived&>(*this).enter(x);
1788 351 : 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 117 : static_cast<Derived&>(*this).leave(x);
1790 117 : }
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 1003 : void apply(T& result, const state_formulas::state_formula& x)
1803 : {
1804 :
1805 1003 : static_cast<Derived&>(*this).enter(x);
1806 1003 : if (data::is_data_expression(x))
1807 : {
1808 26 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
1809 : }
1810 977 : else if (data::is_untyped_data_parameter(x))
1811 : {
1812 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1813 : }
1814 977 : else if (state_formulas::is_true(x))
1815 : {
1816 97 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
1817 : }
1818 880 : else if (state_formulas::is_false(x))
1819 : {
1820 38 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
1821 : }
1822 842 : else if (state_formulas::is_not(x))
1823 : {
1824 39 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
1825 : }
1826 803 : else if (state_formulas::is_minus(x))
1827 : {
1828 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
1829 : }
1830 803 : else if (state_formulas::is_and(x))
1831 : {
1832 91 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
1833 : }
1834 712 : else if (state_formulas::is_or(x))
1835 : {
1836 46 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
1837 : }
1838 666 : else if (state_formulas::is_imp(x))
1839 : {
1840 24 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
1841 : }
1842 642 : else if (state_formulas::is_plus(x))
1843 : {
1844 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
1845 : }
1846 642 : else if (state_formulas::is_const_multiply(x))
1847 : {
1848 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
1849 : }
1850 641 : else if (state_formulas::is_const_multiply_alt(x))
1851 : {
1852 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
1853 : }
1854 640 : else if (state_formulas::is_forall(x))
1855 : {
1856 19 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
1857 : }
1858 621 : else if (state_formulas::is_exists(x))
1859 : {
1860 8 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
1861 : }
1862 613 : else if (state_formulas::is_infimum(x))
1863 : {
1864 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
1865 : }
1866 611 : else if (state_formulas::is_supremum(x))
1867 : {
1868 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
1869 : }
1870 610 : else if (state_formulas::is_sum(x))
1871 : {
1872 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
1873 : }
1874 609 : else if (state_formulas::is_must(x))
1875 : {
1876 136 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
1877 : }
1878 473 : else if (state_formulas::is_may(x))
1879 : {
1880 96 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
1881 : }
1882 377 : else if (state_formulas::is_yaled(x))
1883 : {
1884 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
1885 : }
1886 377 : else if (state_formulas::is_yaled_timed(x))
1887 : {
1888 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
1889 : }
1890 376 : else if (state_formulas::is_delay(x))
1891 : {
1892 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
1893 : }
1894 376 : else if (state_formulas::is_delay_timed(x))
1895 : {
1896 3 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
1897 : }
1898 373 : else if (state_formulas::is_variable(x))
1899 : {
1900 174 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
1901 : }
1902 199 : else if (state_formulas::is_nu(x))
1903 : {
1904 82 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
1905 : }
1906 117 : else if (state_formulas::is_mu(x))
1907 : {
1908 117 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
1909 : }
1910 1003 : static_cast<Derived&>(*this).leave(x);
1911 1003 : }
1912 :
1913 : };
1914 :
1915 : /// \\brief Builder class
1916 : template <typename Derived>
1917 : struct 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 ---//
1923 : template <template <class> class Builder, class Derived>
1924 : struct 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 :
2279 : /// \\brief Builder class
2280 : template <typename Derived>
2281 : struct 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 ---//
2287 : template <template <class> class Builder, class Derived>
2288 : struct 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 205 : void apply(T& result, const state_formulas::true_& x)
2298 : {
2299 :
2300 205 : result = x;
2301 205 : static_cast<Derived&>(*this).enter(x);
2302 : // skip
2303 205 : static_cast<Derived&>(*this).leave(x);
2304 205 : result = x;
2305 205 : }
2306 :
2307 : template <class T>
2308 84 : void apply(T& result, const state_formulas::false_& x)
2309 : {
2310 :
2311 84 : result = x;
2312 84 : static_cast<Derived&>(*this).enter(x);
2313 : // skip
2314 84 : static_cast<Derived&>(*this).leave(x);
2315 84 : result = x;
2316 84 : }
2317 :
2318 : template <class T>
2319 83 : void apply(T& result, const state_formulas::not_& x)
2320 : {
2321 :
2322 83 : static_cast<Derived&>(*this).enter(x);
2323 166 : state_formulas::make_not_(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2324 83 : static_cast<Derived&>(*this).leave(x);
2325 83 : }
2326 :
2327 : template <class T>
2328 0 : void apply(T& result, const state_formulas::minus& x)
2329 : {
2330 :
2331 0 : static_cast<Derived&>(*this).enter(x);
2332 0 : state_formulas::make_minus(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2333 0 : static_cast<Derived&>(*this).leave(x);
2334 0 : }
2335 :
2336 : template <class T>
2337 160 : void apply(T& result, const state_formulas::and_& x)
2338 : {
2339 :
2340 160 : static_cast<Derived&>(*this).enter(x);
2341 480 : 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 159 : static_cast<Derived&>(*this).leave(x);
2343 159 : }
2344 :
2345 : template <class T>
2346 83 : void apply(T& result, const state_formulas::or_& x)
2347 : {
2348 :
2349 83 : static_cast<Derived&>(*this).enter(x);
2350 249 : 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 83 : static_cast<Derived&>(*this).leave(x);
2352 83 : }
2353 :
2354 : template <class T>
2355 39 : void apply(T& result, const state_formulas::imp& x)
2356 : {
2357 :
2358 39 : static_cast<Derived&>(*this).enter(x);
2359 117 : 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 39 : static_cast<Derived&>(*this).leave(x);
2361 39 : }
2362 :
2363 : template <class T>
2364 0 : void apply(T& result, const state_formulas::plus& x)
2365 : {
2366 :
2367 0 : static_cast<Derived&>(*this).enter(x);
2368 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
2370 0 : }
2371 :
2372 : template <class T>
2373 0 : void apply(T& result, const state_formulas::const_multiply& x)
2374 : {
2375 :
2376 0 : static_cast<Derived&>(*this).enter(x);
2377 0 : state_formulas::make_const_multiply(result, x.left(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
2378 0 : static_cast<Derived&>(*this).leave(x);
2379 0 : }
2380 :
2381 : template <class T>
2382 0 : void apply(T& result, const state_formulas::const_multiply_alt& x)
2383 : {
2384 :
2385 0 : static_cast<Derived&>(*this).enter(x);
2386 0 : state_formulas::make_const_multiply_alt(result, [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, x.right());
2387 0 : static_cast<Derived&>(*this).leave(x);
2388 0 : }
2389 :
2390 : template <class T>
2391 9 : void apply(T& result, const state_formulas::forall& x)
2392 : {
2393 :
2394 9 : static_cast<Derived&>(*this).enter(x);
2395 18 : state_formulas::make_forall(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2396 9 : static_cast<Derived&>(*this).leave(x);
2397 9 : }
2398 :
2399 : template <class T>
2400 6 : void apply(T& result, const state_formulas::exists& x)
2401 : {
2402 :
2403 6 : static_cast<Derived&>(*this).enter(x);
2404 12 : state_formulas::make_exists(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2405 6 : static_cast<Derived&>(*this).leave(x);
2406 6 : }
2407 :
2408 : template <class T>
2409 0 : void apply(T& result, const state_formulas::infimum& x)
2410 : {
2411 :
2412 0 : static_cast<Derived&>(*this).enter(x);
2413 0 : state_formulas::make_infimum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2414 0 : static_cast<Derived&>(*this).leave(x);
2415 0 : }
2416 :
2417 : template <class T>
2418 0 : void apply(T& result, const state_formulas::supremum& x)
2419 : {
2420 :
2421 0 : static_cast<Derived&>(*this).enter(x);
2422 0 : state_formulas::make_supremum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2423 0 : static_cast<Derived&>(*this).leave(x);
2424 0 : }
2425 :
2426 : template <class T>
2427 0 : void apply(T& result, const state_formulas::sum& x)
2428 : {
2429 :
2430 0 : static_cast<Derived&>(*this).enter(x);
2431 0 : state_formulas::make_sum(result, x.variables(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
2432 0 : static_cast<Derived&>(*this).leave(x);
2433 0 : }
2434 :
2435 : template <class T>
2436 136 : void apply(T& result, const state_formulas::must& x)
2437 : {
2438 :
2439 136 : static_cast<Derived&>(*this).enter(x);
2440 272 : state_formulas::make_must(result, x.formula(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2441 136 : static_cast<Derived&>(*this).leave(x);
2442 136 : }
2443 :
2444 : template <class T>
2445 155 : void apply(T& result, const state_formulas::may& x)
2446 : {
2447 :
2448 155 : static_cast<Derived&>(*this).enter(x);
2449 310 : state_formulas::make_may(result, x.formula(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2450 155 : static_cast<Derived&>(*this).leave(x);
2451 155 : }
2452 :
2453 : template <class T>
2454 0 : void apply(T& result, const state_formulas::yaled& x)
2455 : {
2456 :
2457 0 : result = x;
2458 0 : static_cast<Derived&>(*this).enter(x);
2459 : // skip
2460 0 : static_cast<Derived&>(*this).leave(x);
2461 0 : result = x;
2462 0 : }
2463 :
2464 : template <class T>
2465 2 : void apply(T& result, const state_formulas::yaled_timed& x)
2466 : {
2467 :
2468 2 : result = x;
2469 2 : static_cast<Derived&>(*this).enter(x);
2470 : // skip
2471 2 : static_cast<Derived&>(*this).leave(x);
2472 2 : result = x;
2473 2 : }
2474 :
2475 : template <class T>
2476 0 : void apply(T& result, const state_formulas::delay& x)
2477 : {
2478 :
2479 0 : result = x;
2480 0 : static_cast<Derived&>(*this).enter(x);
2481 : // skip
2482 0 : static_cast<Derived&>(*this).leave(x);
2483 0 : result = x;
2484 0 : }
2485 :
2486 : template <class T>
2487 2 : void apply(T& result, const state_formulas::delay_timed& x)
2488 : {
2489 :
2490 2 : result = x;
2491 2 : static_cast<Derived&>(*this).enter(x);
2492 : // skip
2493 2 : static_cast<Derived&>(*this).leave(x);
2494 2 : result = x;
2495 2 : }
2496 :
2497 : template <class T>
2498 2 : void apply(T& result, const state_formulas::variable& x)
2499 : {
2500 :
2501 2 : result = x;
2502 2 : static_cast<Derived&>(*this).enter(x);
2503 : // skip
2504 2 : static_cast<Derived&>(*this).leave(x);
2505 2 : result = x;
2506 2 : }
2507 :
2508 : template <class T>
2509 2 : void apply(T& result, const state_formulas::nu& x)
2510 : {
2511 :
2512 2 : static_cast<Derived&>(*this).enter(x);
2513 4 : state_formulas::make_nu(result, x.name(), x.assignments(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2514 2 : static_cast<Derived&>(*this).leave(x);
2515 2 : }
2516 :
2517 : template <class T>
2518 9 : void apply(T& result, const state_formulas::mu& x)
2519 : {
2520 :
2521 9 : static_cast<Derived&>(*this).enter(x);
2522 18 : state_formulas::make_mu(result, x.name(), x.assignments(), [&](state_formula& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
2523 9 : static_cast<Derived&>(*this).leave(x);
2524 9 : }
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 2512 : void apply(T& result, const state_formulas::state_formula& x)
2537 : {
2538 :
2539 2512 : static_cast<Derived&>(*this).enter(x);
2540 2512 : if (data::is_data_expression(x))
2541 : {
2542 58 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
2543 : }
2544 2454 : else if (data::is_untyped_data_parameter(x))
2545 : {
2546 143 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
2547 : }
2548 2311 : else if (state_formulas::is_true(x))
2549 : {
2550 256 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::true_>(x));
2551 : }
2552 2055 : else if (state_formulas::is_false(x))
2553 : {
2554 103 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::false_>(x));
2555 : }
2556 1952 : else if (state_formulas::is_not(x))
2557 : {
2558 246 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::not_>(x));
2559 : }
2560 1706 : else if (state_formulas::is_minus(x))
2561 : {
2562 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::minus>(x));
2563 : }
2564 1706 : else if (state_formulas::is_and(x))
2565 : {
2566 196 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::and_>(x));
2567 : }
2568 1510 : else if (state_formulas::is_or(x))
2569 : {
2570 129 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::or_>(x));
2571 : }
2572 1381 : else if (state_formulas::is_imp(x))
2573 : {
2574 54 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::imp>(x));
2575 : }
2576 1327 : else if (state_formulas::is_plus(x))
2577 : {
2578 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::plus>(x));
2579 : }
2580 1327 : else if (state_formulas::is_const_multiply(x))
2581 : {
2582 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply>(x));
2583 : }
2584 1326 : else if (state_formulas::is_const_multiply_alt(x))
2585 : {
2586 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::const_multiply_alt>(x));
2587 : }
2588 1325 : else if (state_formulas::is_forall(x))
2589 : {
2590 31 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::forall>(x));
2591 : }
2592 1294 : else if (state_formulas::is_exists(x))
2593 : {
2594 17 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::exists>(x));
2595 : }
2596 1277 : else if (state_formulas::is_infimum(x))
2597 : {
2598 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::infimum>(x));
2599 : }
2600 1275 : else if (state_formulas::is_supremum(x))
2601 : {
2602 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::supremum>(x));
2603 : }
2604 1274 : else if (state_formulas::is_sum(x))
2605 : {
2606 1 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::sum>(x));
2607 : }
2608 1273 : else if (state_formulas::is_must(x))
2609 : {
2610 322 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::must>(x));
2611 : }
2612 951 : else if (state_formulas::is_may(x))
2613 : {
2614 327 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::may>(x));
2615 : }
2616 624 : else if (state_formulas::is_yaled(x))
2617 : {
2618 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled>(x));
2619 : }
2620 624 : else if (state_formulas::is_yaled_timed(x))
2621 : {
2622 4 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::yaled_timed>(x));
2623 : }
2624 620 : else if (state_formulas::is_delay(x))
2625 : {
2626 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay>(x));
2627 : }
2628 620 : else if (state_formulas::is_delay_timed(x))
2629 : {
2630 6 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::delay_timed>(x));
2631 : }
2632 614 : else if (state_formulas::is_variable(x))
2633 : {
2634 236 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::variable>(x));
2635 : }
2636 378 : else if (state_formulas::is_nu(x))
2637 : {
2638 144 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::nu>(x));
2639 : }
2640 234 : else if (state_formulas::is_mu(x))
2641 : {
2642 234 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<state_formulas::mu>(x));
2643 : }
2644 2505 : static_cast<Derived&>(*this).leave(x);
2645 2505 : }
2646 :
2647 : };
2648 :
2649 : /// \\brief Builder class
2650 : template <typename Derived>
2651 : struct 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
|
