mCRL2
Loading...
Searching...
No Matches
builder.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_PBES_BUILDER_H
13#define MCRL2_PBES_BUILDER_H
14
15#include "mcrl2/data/builder.h"
16#include "mcrl2/pbes/pbes.h"
17
18namespace mcrl2
19{
20
21namespace pbes_system
22{
23
25template <typename Derived>
27{
29 using super::enter;
30 using super::leave;
31 using super::update;
32 using super::apply;
33
34 template <class T>
35 void apply(T& result, const data::data_expression& x)
36 {
37 result = x;
38 }
39};
40
41// Adds sort expression traversal to a builder
42//--- start generated add_sort_expressions code ---//
43template <template <class> class Builder, class Derived>
44struct 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>
54 {
55
56 static_cast<Derived&>(*this).enter(x);
57 pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
58 static_cast<Derived&>(*this).leave(x);
59 }
60
62 {
63 static_cast<Derived&>(*this).enter(x);
64 propositional_variable result_variable;
65 static_cast<Derived&>(*this).apply(result_variable, x.variable());
66 x.variable() = result_variable;
67 pbes_expression result_formula;
68 static_cast<Derived&>(*this).apply(result_formula, x.formula());
69 x.formula() = result_formula;
70 static_cast<Derived&>(*this).leave(x);
71 }
72
74 {
75 static_cast<Derived&>(*this).enter(x);
76 static_cast<Derived&>(*this).update(x.global_variables());
77 static_cast<Derived&>(*this).update(x.equations());
78 propositional_variable_instantiation result_initial_state;
79 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
80 x.initial_state() = result_initial_state;
81 static_cast<Derived&>(*this).leave(x);
82 }
83
84 template <class T>
86 {
87
88 static_cast<Derived&>(*this).enter(x);
89 pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
90 static_cast<Derived&>(*this).leave(x);
91 }
92
93 template <class T>
94 void apply(T& result, const pbes_system::not_& x)
95 {
96
97 static_cast<Derived&>(*this).enter(x);
98 pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
99 static_cast<Derived&>(*this).leave(x);
100 }
101
102 template <class T>
103 void apply(T& result, const pbes_system::and_& x)
104 {
105
106 static_cast<Derived&>(*this).enter(x);
107 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 static_cast<Derived&>(*this).leave(x);
109 }
110
111 template <class T>
112 void apply(T& result, const pbes_system::or_& x)
113 {
114
115 static_cast<Derived&>(*this).enter(x);
116 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 static_cast<Derived&>(*this).leave(x);
118 }
119
120 template <class T>
121 void apply(T& result, const pbes_system::imp& x)
122 {
123
124 static_cast<Derived&>(*this).enter(x);
125 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 static_cast<Derived&>(*this).leave(x);
127 }
128
129 template <class T>
130 void apply(T& result, const pbes_system::forall& x)
131 {
132
133 static_cast<Derived&>(*this).enter(x);
134 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 static_cast<Derived&>(*this).leave(x);
136 }
137
138 template <class T>
139 void apply(T& result, const pbes_system::exists& x)
140 {
141
142 static_cast<Derived&>(*this).enter(x);
143 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 static_cast<Derived&>(*this).leave(x);
145 }
146
147 template <class T>
148 void apply(T& result, const pbes_system::pbes_expression& x)
149 {
150
151 static_cast<Derived&>(*this).enter(x);
153 {
154 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
155 }
156 else if (data::is_variable(x))
157 {
158 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
159 }
161 {
162 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
163 }
165 {
166 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
167 }
168 else if (pbes_system::is_not(x))
169 {
170 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
171 }
172 else if (pbes_system::is_and(x))
173 {
174 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
175 }
176 else if (pbes_system::is_or(x))
177 {
178 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
179 }
180 else if (pbes_system::is_imp(x))
181 {
182 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
183 }
184 else if (pbes_system::is_forall(x))
185 {
186 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
187 }
188 else if (pbes_system::is_exists(x))
189 {
190 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
191 }
192 static_cast<Derived&>(*this).leave(x);
193 }
194
195};
196
198template <typename Derived>
199struct 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 ---//
206template <template <class> class Builder, class Derived>
207struct 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
216 {
217 static_cast<Derived&>(*this).enter(x);
218 pbes_expression result_formula;
219 static_cast<Derived&>(*this).apply(result_formula, x.formula());
220 x.formula() = result_formula;
221 static_cast<Derived&>(*this).leave(x);
222 }
223
225 {
226 static_cast<Derived&>(*this).enter(x);
227 static_cast<Derived&>(*this).update(x.equations());
228 propositional_variable_instantiation result_initial_state;
229 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
230 x.initial_state() = result_initial_state;
231 static_cast<Derived&>(*this).leave(x);
232 }
233
234 template <class T>
236 {
237
238 static_cast<Derived&>(*this).enter(x);
239 pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
240 static_cast<Derived&>(*this).leave(x);
241 }
242
243 template <class T>
244 void apply(T& result, const pbes_system::not_& x)
245 {
246
247 static_cast<Derived&>(*this).enter(x);
248 pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
249 static_cast<Derived&>(*this).leave(x);
250 }
251
252 template <class T>
253 void apply(T& result, const pbes_system::and_& x)
254 {
255
256 static_cast<Derived&>(*this).enter(x);
257 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 static_cast<Derived&>(*this).leave(x);
259 }
260
261 template <class T>
262 void apply(T& result, const pbes_system::or_& x)
263 {
264
265 static_cast<Derived&>(*this).enter(x);
266 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 static_cast<Derived&>(*this).leave(x);
268 }
269
270 template <class T>
271 void apply(T& result, const pbes_system::imp& x)
272 {
273
274 static_cast<Derived&>(*this).enter(x);
275 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 static_cast<Derived&>(*this).leave(x);
277 }
278
279 template <class T>
280 void apply(T& result, const pbes_system::forall& x)
281 {
282
283 static_cast<Derived&>(*this).enter(x);
284 pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
285 static_cast<Derived&>(*this).leave(x);
286 }
287
288 template <class T>
289 void apply(T& result, const pbes_system::exists& x)
290 {
291
292 static_cast<Derived&>(*this).enter(x);
293 pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
294 static_cast<Derived&>(*this).leave(x);
295 }
296
297 template <class T>
298 void apply(T& result, const pbes_system::pbes_expression& x)
299 {
300
301 static_cast<Derived&>(*this).enter(x);
303 {
304 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
305 }
306 else if (data::is_variable(x))
307 {
308 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
309 }
311 {
312 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
313 }
315 {
316 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
317 }
318 else if (pbes_system::is_not(x))
319 {
320 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
321 }
322 else if (pbes_system::is_and(x))
323 {
324 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
325 }
326 else if (pbes_system::is_or(x))
327 {
328 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
329 }
330 else if (pbes_system::is_imp(x))
331 {
332 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
333 }
334 else if (pbes_system::is_forall(x))
335 {
336 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
337 }
338 else if (pbes_system::is_exists(x))
339 {
340 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
341 }
342 static_cast<Derived&>(*this).leave(x);
343 }
344
345};
346
348template <typename Derived>
349struct 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 ---//
355template <template <class> class Builder, class Derived>
356struct 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>
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
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
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>
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);
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 }
473 {
474 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
475 }
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
510template <typename Derived>
511struct 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 ---//
518template <template <class> class Builder, class Derived>
519struct 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
528 {
529 static_cast<Derived&>(*this).enter(x);
530 pbes_expression result_formula;
531 static_cast<Derived&>(*this).apply(result_formula, x.formula());
532 x.formula() = result_formula;
533 static_cast<Derived&>(*this).leave(x);
534 }
535
537 {
538 static_cast<Derived&>(*this).enter(x);
539 static_cast<Derived&>(*this).update(x.equations());
540 static_cast<Derived&>(*this).leave(x);
541 }
542
543 template <class T>
545 {
546
547 result = x;
548 static_cast<Derived&>(*this).enter(x);
549 // skip
550 static_cast<Derived&>(*this).leave(x);
551 result = x;
552 }
553
554 template <class T>
555 void apply(T& result, const pbes_system::not_& x)
556 {
557
558 static_cast<Derived&>(*this).enter(x);
559 pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
560 static_cast<Derived&>(*this).leave(x);
561 }
562
563 template <class T>
564 void apply(T& result, const pbes_system::and_& x)
565 {
566
567 static_cast<Derived&>(*this).enter(x);
568 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 static_cast<Derived&>(*this).leave(x);
570 }
571
572 template <class T>
573 void apply(T& result, const pbes_system::or_& x)
574 {
575
576 static_cast<Derived&>(*this).enter(x);
577 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 static_cast<Derived&>(*this).leave(x);
579 }
580
581 template <class T>
582 void apply(T& result, const pbes_system::imp& x)
583 {
584
585 static_cast<Derived&>(*this).enter(x);
586 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 static_cast<Derived&>(*this).leave(x);
588 }
589
590 template <class T>
591 void apply(T& result, const pbes_system::forall& x)
592 {
593
594 static_cast<Derived&>(*this).enter(x);
595 pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
596 static_cast<Derived&>(*this).leave(x);
597 }
598
599 template <class T>
600 void apply(T& result, const pbes_system::exists& x)
601 {
602
603 static_cast<Derived&>(*this).enter(x);
604 pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
605 static_cast<Derived&>(*this).leave(x);
606 }
607
608 template <class T>
609 void apply(T& result, const pbes_system::pbes_expression& x)
610 {
611
612 static_cast<Derived&>(*this).enter(x);
614 {
615 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
616 }
617 else if (data::is_variable(x))
618 {
619 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
620 }
622 {
623 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
624 }
626 {
627 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
628 }
629 else if (pbes_system::is_not(x))
630 {
631 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
632 }
633 else if (pbes_system::is_and(x))
634 {
635 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
636 }
637 else if (pbes_system::is_or(x))
638 {
639 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
640 }
641 else if (pbes_system::is_imp(x))
642 {
643 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
644 }
645 else if (pbes_system::is_forall(x))
646 {
647 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
648 }
649 else if (pbes_system::is_exists(x))
650 {
651 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
652 }
653 static_cast<Derived&>(*this).leave(x);
654 }
655
656};
657
659template <typename Derived>
660struct 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
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
const propositional_variable & variable() const
Returns the pbes variable of the equation.
parameterized boolean equation system
Definition pbes.h:58
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:192
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
Definition pbes.h:178
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:164
\brief A propositional variable instantiation
\brief A propositional variable declaration
const core::identifier_string & name() const
add your file description here.
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_untyped_data_parameter(const atermpp::aterm &x)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
void make_propositional_variable(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_not(const atermpp::aterm &x)
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm &x)
bool is_or(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
void make_propositional_variable_instantiation(atermpp::aterm &t, const ARGUMENTS &... args)
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The class pbes.
expression builder that visits all sub expressions
Definition builder.h:42
void update(T &x, typename atermpp::disable_if_container< T >::type *=nullptr)
Definition builder.h:54
void leave(const T &)
Definition builder.h:50
void apply(atermpp::term_list< T > &result, const atermpp::term_list< U > &x)
Definition builder.h:89
void enter(const T &)
Definition builder.h:45
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:271
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:280
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:253
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:298
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:262
void update(pbes_system::pbes_equation &x)
Definition builder.h:215
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:235
void update(pbes_system::pbes &x)
Definition builder.h:224
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:289
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:244
void update(pbes_system::pbes &x)
Definition builder.h:536
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:609
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:591
void update(pbes_system::pbes_equation &x)
Definition builder.h:527
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:555
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:544
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:564
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:582
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:600
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:573
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:139
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:103
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:112
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:130
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:85
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:53
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:121
void update(pbes_system::pbes_equation &x)
Definition builder.h:61
void update(pbes_system::pbes &x)
Definition builder.h:73
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:148
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:94
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:433
void update(pbes_system::pbes &x)
Definition builder.h:385
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:460
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:442
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:365
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:406
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:415
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:424
void update(pbes_system::pbes_equation &x)
Definition builder.h:373
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:451
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:397
void apply(T &result, const data::data_expression &x)
Definition builder.h:35