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/pbes/builder.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_BUILDER_H
13 : #define MCRL2_PBES_BUILDER_H
14 :
15 : #include "mcrl2/data/builder.h"
16 : #include "mcrl2/pbes/pbes.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace pbes_system
22 : {
23 :
24 : /// \brief Builder class
25 : template <typename Derived>
26 : struct pbes_expression_builder_base: public core::builder<Derived>
27 : {
28 : typedef core::builder<Derived> super;
29 : using super::enter;
30 : using super::leave;
31 : using super::update;
32 : using super::apply;
33 :
34 : template <class T>
35 1232 : void apply(T& result, const data::data_expression& x)
36 : {
37 1232 : result = x;
38 1232 : }
39 : };
40 :
41 : // Adds sort expression traversal to a builder
42 : //--- start generated add_sort_expressions code ---//
43 : template <template <class> class Builder, class Derived>
44 : struct add_sort_expressions: public Builder<Derived>
45 : {
46 : typedef Builder<Derived> super;
47 : using super::enter;
48 : using super::leave;
49 : using super::update;
50 : using super::apply;
51 :
52 : template <class T>
53 2864 : void apply(T& result, const pbes_system::propositional_variable& x)
54 : {
55 :
56 2864 : static_cast<Derived&>(*this).enter(x);
57 5728 : pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
58 2864 : static_cast<Derived&>(*this).leave(x);
59 2864 : }
60 :
61 2863 : void update(pbes_system::pbes_equation& x)
62 : {
63 2863 : static_cast<Derived&>(*this).enter(x);
64 2863 : propositional_variable result_variable;
65 2863 : static_cast<Derived&>(*this).apply(result_variable, x.variable());
66 2863 : x.variable() = result_variable;
67 2863 : pbes_expression result_formula;
68 2863 : static_cast<Derived&>(*this).apply(result_formula, x.formula());
69 2863 : x.formula() = result_formula;
70 2863 : static_cast<Derived&>(*this).leave(x);
71 2863 : }
72 :
73 467 : void update(pbes_system::pbes& x)
74 : {
75 467 : static_cast<Derived&>(*this).enter(x);
76 467 : static_cast<Derived&>(*this).update(x.global_variables());
77 467 : static_cast<Derived&>(*this).update(x.equations());
78 467 : propositional_variable_instantiation result_initial_state;
79 467 : static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
80 467 : x.initial_state() = result_initial_state;
81 467 : static_cast<Derived&>(*this).leave(x);
82 467 : }
83 :
84 : template <class T>
85 469 : void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
86 : {
87 :
88 469 : static_cast<Derived&>(*this).enter(x);
89 938 : pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
90 469 : static_cast<Derived&>(*this).leave(x);
91 469 : }
92 :
93 : template <class T>
94 143 : void apply(T& result, const pbes_system::not_& x)
95 : {
96 :
97 143 : static_cast<Derived&>(*this).enter(x);
98 286 : pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
99 143 : static_cast<Derived&>(*this).leave(x);
100 143 : }
101 :
102 : template <class T>
103 422 : void apply(T& result, const pbes_system::and_& x)
104 : {
105 :
106 422 : static_cast<Derived&>(*this).enter(x);
107 1266 : pbes_system::make_and_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
108 422 : static_cast<Derived&>(*this).leave(x);
109 422 : }
110 :
111 : template <class T>
112 380 : void apply(T& result, const pbes_system::or_& x)
113 : {
114 :
115 380 : static_cast<Derived&>(*this).enter(x);
116 1140 : pbes_system::make_or_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
117 380 : static_cast<Derived&>(*this).leave(x);
118 380 : }
119 :
120 : template <class T>
121 176 : void apply(T& result, const pbes_system::imp& x)
122 : {
123 :
124 176 : static_cast<Derived&>(*this).enter(x);
125 528 : pbes_system::make_imp(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
126 176 : static_cast<Derived&>(*this).leave(x);
127 176 : }
128 :
129 : template <class T>
130 219 : void apply(T& result, const pbes_system::forall& x)
131 : {
132 :
133 219 : static_cast<Derived&>(*this).enter(x);
134 657 : pbes_system::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
135 219 : static_cast<Derived&>(*this).leave(x);
136 219 : }
137 :
138 : template <class T>
139 119 : void apply(T& result, const pbes_system::exists& x)
140 : {
141 :
142 119 : static_cast<Derived&>(*this).enter(x);
143 357 : pbes_system::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
144 119 : static_cast<Derived&>(*this).leave(x);
145 119 : }
146 :
147 : template <class T>
148 5302 : void apply(T& result, const pbes_system::pbes_expression& x)
149 : {
150 :
151 5302 : static_cast<Derived&>(*this).enter(x);
152 5302 : if (data::is_data_expression(x))
153 : {
154 3054 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
155 : }
156 2248 : else if (data::is_variable(x))
157 : {
158 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
159 : }
160 2248 : else if (data::is_untyped_data_parameter(x))
161 : {
162 787 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
163 : }
164 1461 : else if (pbes_system::is_propositional_variable_instantiation(x))
165 : {
166 2 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
167 : }
168 1459 : else if (pbes_system::is_not(x))
169 : {
170 143 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
171 : }
172 1316 : else if (pbes_system::is_and(x))
173 : {
174 422 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
175 : }
176 894 : else if (pbes_system::is_or(x))
177 : {
178 380 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
179 : }
180 514 : else if (pbes_system::is_imp(x))
181 : {
182 176 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
183 : }
184 338 : else if (pbes_system::is_forall(x))
185 : {
186 219 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
187 : }
188 119 : else if (pbes_system::is_exists(x))
189 : {
190 119 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
191 : }
192 5302 : static_cast<Derived&>(*this).leave(x);
193 5302 : }
194 :
195 : };
196 :
197 : /// \\brief Builder class
198 : template <typename Derived>
199 : struct sort_expression_builder: public add_sort_expressions<data::sort_expression_builder, Derived>
200 : {
201 : };
202 : //--- end generated add_sort_expressions code ---//
203 :
204 : // Adds data expression traversal to a builder
205 : //--- start generated add_data_expressions code ---//
206 : template <template <class> class Builder, class Derived>
207 : struct add_data_expressions: public Builder<Derived>
208 : {
209 : typedef Builder<Derived> super;
210 : using super::enter;
211 : using super::leave;
212 : using super::update;
213 : using super::apply;
214 :
215 2868 : void update(pbes_system::pbes_equation& x)
216 : {
217 2868 : static_cast<Derived&>(*this).enter(x);
218 2868 : pbes_expression result_formula;
219 2868 : static_cast<Derived&>(*this).apply(result_formula, x.formula());
220 2868 : x.formula() = result_formula;
221 2868 : static_cast<Derived&>(*this).leave(x);
222 2868 : }
223 :
224 466 : void update(pbes_system::pbes& x)
225 : {
226 466 : static_cast<Derived&>(*this).enter(x);
227 466 : static_cast<Derived&>(*this).update(x.equations());
228 466 : propositional_variable_instantiation result_initial_state;
229 466 : static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
230 466 : x.initial_state() = result_initial_state;
231 466 : static_cast<Derived&>(*this).leave(x);
232 466 : }
233 :
234 : template <class T>
235 1789 : void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
236 : {
237 :
238 1789 : static_cast<Derived&>(*this).enter(x);
239 3578 : pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
240 1789 : static_cast<Derived&>(*this).leave(x);
241 1789 : }
242 :
243 : template <class T>
244 193 : void apply(T& result, const pbes_system::not_& x)
245 : {
246 :
247 193 : static_cast<Derived&>(*this).enter(x);
248 386 : pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
249 193 : static_cast<Derived&>(*this).leave(x);
250 193 : }
251 :
252 : template <class T>
253 594 : void apply(T& result, const pbes_system::and_& x)
254 : {
255 :
256 594 : static_cast<Derived&>(*this).enter(x);
257 1782 : pbes_system::make_and_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
258 594 : static_cast<Derived&>(*this).leave(x);
259 594 : }
260 :
261 : template <class T>
262 497 : void apply(T& result, const pbes_system::or_& x)
263 : {
264 :
265 497 : static_cast<Derived&>(*this).enter(x);
266 1491 : pbes_system::make_or_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
267 497 : static_cast<Derived&>(*this).leave(x);
268 497 : }
269 :
270 : template <class T>
271 179 : void apply(T& result, const pbes_system::imp& x)
272 : {
273 :
274 179 : static_cast<Derived&>(*this).enter(x);
275 537 : pbes_system::make_imp(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
276 179 : static_cast<Derived&>(*this).leave(x);
277 179 : }
278 :
279 : template <class T>
280 238 : void apply(T& result, const pbes_system::forall& x)
281 : {
282 :
283 238 : static_cast<Derived&>(*this).enter(x);
284 476 : pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
285 238 : static_cast<Derived&>(*this).leave(x);
286 238 : }
287 :
288 : template <class T>
289 136 : void apply(T& result, const pbes_system::exists& x)
290 : {
291 :
292 136 : static_cast<Derived&>(*this).enter(x);
293 272 : pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
294 136 : static_cast<Derived&>(*this).leave(x);
295 136 : }
296 :
297 : template <class T>
298 6979 : void apply(T& result, const pbes_system::pbes_expression& x)
299 : {
300 :
301 6979 : static_cast<Derived&>(*this).enter(x);
302 6979 : if (data::is_data_expression(x))
303 : {
304 3765 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
305 : }
306 3214 : else if (data::is_variable(x))
307 : {
308 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
309 : }
310 3214 : else if (data::is_untyped_data_parameter(x))
311 : {
312 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
313 : }
314 3214 : else if (pbes_system::is_propositional_variable_instantiation(x))
315 : {
316 1319 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
317 : }
318 1895 : else if (pbes_system::is_not(x))
319 : {
320 193 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
321 : }
322 1702 : else if (pbes_system::is_and(x))
323 : {
324 594 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
325 : }
326 1108 : else if (pbes_system::is_or(x))
327 : {
328 497 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
329 : }
330 611 : else if (pbes_system::is_imp(x))
331 : {
332 179 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
333 : }
334 432 : else if (pbes_system::is_forall(x))
335 : {
336 268 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
337 : }
338 164 : else if (pbes_system::is_exists(x))
339 : {
340 164 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
341 : }
342 6979 : static_cast<Derived&>(*this).leave(x);
343 6979 : }
344 :
345 : };
346 :
347 : /// \\brief Builder class
348 : template <typename Derived>
349 : struct data_expression_builder: public add_data_expressions<data::data_expression_builder, Derived>
350 : {
351 : };
352 : //--- end generated add_data_expressions code ---//
353 :
354 : //--- start generated add_variables code ---//
355 : template <template <class> class Builder, class Derived>
356 : struct add_variables: public Builder<Derived>
357 : {
358 : typedef Builder<Derived> super;
359 : using super::enter;
360 : using super::leave;
361 : using super::update;
362 : using super::apply;
363 :
364 : template <class T>
365 : void apply(T& result, const pbes_system::propositional_variable& x)
366 : {
367 :
368 : static_cast<Derived&>(*this).enter(x);
369 : pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
370 : static_cast<Derived&>(*this).leave(x);
371 : }
372 :
373 : void update(pbes_system::pbes_equation& x)
374 : {
375 : static_cast<Derived&>(*this).enter(x);
376 : propositional_variable result_variable;
377 : static_cast<Derived&>(*this).apply(result_variable, x.variable());
378 : x.variable() = result_variable;
379 : pbes_expression result_formula;
380 : static_cast<Derived&>(*this).apply(result_formula, x.formula());
381 : x.formula() = result_formula;
382 : static_cast<Derived&>(*this).leave(x);
383 : }
384 :
385 : void update(pbes_system::pbes& x)
386 : {
387 : static_cast<Derived&>(*this).enter(x);
388 : static_cast<Derived&>(*this).update(x.global_variables());
389 : static_cast<Derived&>(*this).update(x.equations());
390 : propositional_variable_instantiation result_initial_state;
391 : static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
392 : x.initial_state() = result_initial_state;
393 : static_cast<Derived&>(*this).leave(x);
394 : }
395 :
396 : template <class T>
397 : void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
398 : {
399 :
400 : static_cast<Derived&>(*this).enter(x);
401 : pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
402 : static_cast<Derived&>(*this).leave(x);
403 : }
404 :
405 : template <class T>
406 : void apply(T& result, const pbes_system::not_& x)
407 : {
408 :
409 : static_cast<Derived&>(*this).enter(x);
410 : pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
411 : static_cast<Derived&>(*this).leave(x);
412 : }
413 :
414 : template <class T>
415 : void apply(T& result, const pbes_system::and_& x)
416 : {
417 :
418 : static_cast<Derived&>(*this).enter(x);
419 : pbes_system::make_and_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
420 : static_cast<Derived&>(*this).leave(x);
421 : }
422 :
423 : template <class T>
424 : void apply(T& result, const pbes_system::or_& x)
425 : {
426 :
427 : static_cast<Derived&>(*this).enter(x);
428 : pbes_system::make_or_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
429 : static_cast<Derived&>(*this).leave(x);
430 : }
431 :
432 : template <class T>
433 : void apply(T& result, const pbes_system::imp& x)
434 : {
435 :
436 : static_cast<Derived&>(*this).enter(x);
437 : pbes_system::make_imp(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
438 : static_cast<Derived&>(*this).leave(x);
439 : }
440 :
441 : template <class T>
442 : void apply(T& result, const pbes_system::forall& x)
443 : {
444 :
445 : static_cast<Derived&>(*this).enter(x);
446 : pbes_system::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
447 : static_cast<Derived&>(*this).leave(x);
448 : }
449 :
450 : template <class T>
451 : void apply(T& result, const pbes_system::exists& x)
452 : {
453 :
454 : static_cast<Derived&>(*this).enter(x);
455 : pbes_system::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
456 : static_cast<Derived&>(*this).leave(x);
457 : }
458 :
459 : template <class T>
460 : void apply(T& result, const pbes_system::pbes_expression& x)
461 : {
462 :
463 : static_cast<Derived&>(*this).enter(x);
464 : if (data::is_data_expression(x))
465 : {
466 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
467 : }
468 : else if (data::is_variable(x))
469 : {
470 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
471 : }
472 : else if (data::is_untyped_data_parameter(x))
473 : {
474 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
475 : }
476 : else if (pbes_system::is_propositional_variable_instantiation(x))
477 : {
478 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
479 : }
480 : else if (pbes_system::is_not(x))
481 : {
482 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
483 : }
484 : else if (pbes_system::is_and(x))
485 : {
486 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
487 : }
488 : else if (pbes_system::is_or(x))
489 : {
490 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
491 : }
492 : else if (pbes_system::is_imp(x))
493 : {
494 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
495 : }
496 : else if (pbes_system::is_forall(x))
497 : {
498 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
499 : }
500 : else if (pbes_system::is_exists(x))
501 : {
502 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
503 : }
504 : static_cast<Derived&>(*this).leave(x);
505 : }
506 :
507 : };
508 :
509 : /// \\brief Builder class
510 : template <typename Derived>
511 : struct variable_builder: public add_variables<data::data_expression_builder, Derived>
512 : {
513 : };
514 : //--- end generated add_variables code ---//
515 :
516 : // Adds pbes expression traversal to a builder
517 : //--- start generated add_pbes_expressions code ---//
518 : template <template <class> class Builder, class Derived>
519 : struct add_pbes_expressions: public Builder<Derived>
520 : {
521 : typedef Builder<Derived> super;
522 : using super::enter;
523 : using super::leave;
524 : using super::update;
525 : using super::apply;
526 :
527 1176 : void update(pbes_system::pbes_equation& x)
528 : {
529 1176 : static_cast<Derived&>(*this).enter(x);
530 1176 : pbes_expression result_formula;
531 1176 : static_cast<Derived&>(*this).apply(result_formula, x.formula());
532 1176 : x.formula() = result_formula;
533 1176 : static_cast<Derived&>(*this).leave(x);
534 1176 : }
535 :
536 610 : void update(pbes_system::pbes& x)
537 : {
538 610 : static_cast<Derived&>(*this).enter(x);
539 610 : static_cast<Derived&>(*this).update(x.equations());
540 610 : static_cast<Derived&>(*this).leave(x);
541 610 : }
542 :
543 : template <class T>
544 2653 : void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
545 : {
546 :
547 2653 : result = x;
548 2653 : static_cast<Derived&>(*this).enter(x);
549 : // skip
550 2653 : static_cast<Derived&>(*this).leave(x);
551 2653 : result = x;
552 2653 : }
553 :
554 : template <class T>
555 143 : void apply(T& result, const pbes_system::not_& x)
556 : {
557 :
558 143 : static_cast<Derived&>(*this).enter(x);
559 286 : pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
560 143 : static_cast<Derived&>(*this).leave(x);
561 143 : }
562 :
563 : template <class T>
564 3046 : void apply(T& result, const pbes_system::and_& x)
565 : {
566 :
567 3046 : static_cast<Derived&>(*this).enter(x);
568 9138 : pbes_system::make_and_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
569 3046 : static_cast<Derived&>(*this).leave(x);
570 3046 : }
571 :
572 : template <class T>
573 1882 : void apply(T& result, const pbes_system::or_& x)
574 : {
575 :
576 1882 : static_cast<Derived&>(*this).enter(x);
577 5646 : pbes_system::make_or_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
578 1882 : static_cast<Derived&>(*this).leave(x);
579 1882 : }
580 :
581 : template <class T>
582 178 : void apply(T& result, const pbes_system::imp& x)
583 : {
584 :
585 178 : static_cast<Derived&>(*this).enter(x);
586 534 : pbes_system::make_imp(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
587 178 : static_cast<Derived&>(*this).leave(x);
588 178 : }
589 :
590 : template <class T>
591 64 : void apply(T& result, const pbes_system::forall& x)
592 : {
593 :
594 64 : static_cast<Derived&>(*this).enter(x);
595 128 : pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
596 64 : static_cast<Derived&>(*this).leave(x);
597 64 : }
598 :
599 : template <class T>
600 19 : void apply(T& result, const pbes_system::exists& x)
601 : {
602 :
603 19 : static_cast<Derived&>(*this).enter(x);
604 38 : pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
605 19 : static_cast<Derived&>(*this).leave(x);
606 19 : }
607 :
608 : template <class T>
609 128411 : void apply(T& result, const pbes_system::pbes_expression& x)
610 : {
611 :
612 128411 : static_cast<Derived&>(*this).enter(x);
613 128411 : if (data::is_data_expression(x))
614 : {
615 39956 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
616 : }
617 88455 : else if (data::is_variable(x))
618 : {
619 0 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
620 : }
621 88455 : else if (data::is_untyped_data_parameter(x))
622 : {
623 787 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
624 : }
625 87668 : else if (pbes_system::is_propositional_variable_instantiation(x))
626 : {
627 18618 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
628 : }
629 69050 : else if (pbes_system::is_not(x))
630 : {
631 294 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
632 : }
633 68756 : else if (pbes_system::is_and(x))
634 : {
635 32768 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
636 : }
637 35988 : else if (pbes_system::is_or(x))
638 : {
639 30603 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
640 : }
641 5385 : else if (pbes_system::is_imp(x))
642 : {
643 778 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
644 : }
645 4607 : else if (pbes_system::is_forall(x))
646 : {
647 3039 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
648 : }
649 1568 : else if (pbes_system::is_exists(x))
650 : {
651 1568 : static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
652 : }
653 128411 : static_cast<Derived&>(*this).leave(x);
654 128411 : }
655 :
656 : };
657 :
658 : /// \\brief Builder class
659 : template <typename Derived>
660 : struct pbes_expression_builder: public add_pbes_expressions<pbes_system::pbes_expression_builder_base, Derived>
661 : {
662 : };
663 : //--- end generated add_pbes_expressions code ---//
664 :
665 : } // namespace pbes_system
666 :
667 : } // namespace mcrl2
668 :
669 : #endif // MCRL2_PBES_BUILDER_H
|
