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//
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
18namespace mcrl2::pbes_system
19{
20
21/// \brief Builder class
22template <typename Derived>
23struct pbes_expression_builder_base: public core::builder<Derived>
24{
25 using super = core::builder<Derived>;
26 using super::enter;
27 using super::leave;
28 using super::update;
29 using super::apply;
30
31 template <class T>
32 void apply(T& result, const data::data_expression& x)
33 {
34 result = atermpp::down_cast<T>(x);
35 }
36 template <class T>
37 void apply(T& result, const data::untyped_data_parameter& x)
38 {
39 result = atermpp::down_cast<T>(x);
40 }
41};
42
43// Adds sort expression traversal to a builder
44//--- start generated add_sort_expressions code ---//
45template <template <class> class Builder, class Derived>
46struct add_sort_expressions: public Builder<Derived>
47{
48 using super = Builder<Derived>;
49 using super::enter;
50 using super::leave;
51 using super::update;
52 using super::apply;
53
54 template <class T>
55 void apply(T& result, const pbes_system::propositional_variable& x)
56 {
57 static_cast<Derived&>(*this).enter(x);
58 pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
59 static_cast<Derived&>(*this).leave(x);
60 }
61
62 void update(pbes_system::pbes_equation& x)
63 {
64 static_cast<Derived&>(*this).enter(x);
65 propositional_variable result_variable;
66 static_cast<Derived&>(*this).apply(result_variable, x.variable());
67 x.variable() = result_variable;
68 pbes_expression result_formula;
69 static_cast<Derived&>(*this).apply(result_formula, x.formula());
70 x.formula() = result_formula;
71 static_cast<Derived&>(*this).leave(x);
72 }
73
74 void update(pbes_system::pbes& x)
75 {
76 static_cast<Derived&>(*this).enter(x);
77 static_cast<Derived&>(*this).update(x.global_variables());
78 static_cast<Derived&>(*this).update(x.equations());
79 propositional_variable_instantiation result_initial_state;
80 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
81 x.initial_state() = result_initial_state;
82 static_cast<Derived&>(*this).leave(x);
83 }
84
85 template <class T>
86 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
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 static_cast<Derived&>(*this).enter(x);
97 pbes_system::make_not(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
98 static_cast<Derived&>(*this).leave(x);
99 }
100
101 template <class T>
102 void apply(T& result, const pbes_system::and_& x)
103 {
104 static_cast<Derived&>(*this).enter(x);
105 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()); });
106 static_cast<Derived&>(*this).leave(x);
107 }
108
109 template <class T>
110 void apply(T& result, const pbes_system::or_& x)
111 {
112 static_cast<Derived&>(*this).enter(x);
113 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()); });
114 static_cast<Derived&>(*this).leave(x);
115 }
116
117 template <class T>
118 void apply(T& result, const pbes_system::imp& x)
119 {
120 static_cast<Derived&>(*this).enter(x);
121 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()); });
122 static_cast<Derived&>(*this).leave(x);
123 }
124
125 template <class T>
126 void apply(T& result, const pbes_system::forall& x)
127 {
128 static_cast<Derived&>(*this).enter(x);
129 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()); });
130 static_cast<Derived&>(*this).leave(x);
131 }
132
133 template <class T>
134 void apply(T& result, const pbes_system::exists& x)
135 {
136 static_cast<Derived&>(*this).enter(x);
137 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()); });
138 static_cast<Derived&>(*this).leave(x);
139 }
140
141 template <class T>
142 void apply(T& result, const pbes_system::pbes_expression& x)
143 {
144 static_cast<Derived&>(*this).enter(x);
145 if (data::is_data_expression(x))
146 {
147 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
148 }
149 else if (data::is_untyped_data_parameter(x))
150 {
151 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
152 }
153 else if (pbes_system::is_propositional_variable_instantiation(x))
154 {
155 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
156 }
157 else if (pbes_system::is_not(x))
158 {
159 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
160 }
161 else if (pbes_system::is_and(x))
162 {
163 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
164 }
165 else if (pbes_system::is_or(x))
166 {
167 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
168 }
169 else if (pbes_system::is_imp(x))
170 {
171 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
172 }
173 else if (pbes_system::is_forall(x))
174 {
175 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
176 }
177 else if (pbes_system::is_exists(x))
178 {
179 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
180 }
181 static_cast<Derived&>(*this).leave(x);
182 }
183
184};
185
186/// \\brief Builder class
187template <typename Derived>
188struct sort_expression_builder: public add_sort_expressions<data::sort_expression_builder, Derived>
189{
190};
191//--- end generated add_sort_expressions code ---//
192
193// Adds data expression traversal to a builder
194//--- start generated add_data_expressions code ---//
195template <template <class> class Builder, class Derived>
196struct add_data_expressions: public Builder<Derived>
197{
198 using super = Builder<Derived>;
199 using super::enter;
200 using super::leave;
201 using super::update;
202 using super::apply;
203
204 void update(pbes_system::pbes_equation& x)
205 {
206 static_cast<Derived&>(*this).enter(x);
207 pbes_expression result_formula;
208 static_cast<Derived&>(*this).apply(result_formula, x.formula());
209 x.formula() = result_formula;
210 static_cast<Derived&>(*this).leave(x);
211 }
212
213 void update(pbes_system::pbes& x)
214 {
215 static_cast<Derived&>(*this).enter(x);
216 static_cast<Derived&>(*this).update(x.equations());
217 propositional_variable_instantiation result_initial_state;
218 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
219 x.initial_state() = result_initial_state;
220 static_cast<Derived&>(*this).leave(x);
221 }
222
223 template <class T>
224 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
225 {
226 static_cast<Derived&>(*this).enter(x);
227 pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
228 static_cast<Derived&>(*this).leave(x);
229 }
230
231 template <class T>
232 void apply(T& result, const pbes_system::not_& x)
233 {
234 static_cast<Derived&>(*this).enter(x);
235 pbes_system::make_not(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
236 static_cast<Derived&>(*this).leave(x);
237 }
238
239 template <class T>
240 void apply(T& result, const pbes_system::and_& x)
241 {
242 static_cast<Derived&>(*this).enter(x);
243 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()); });
244 static_cast<Derived&>(*this).leave(x);
245 }
246
247 template <class T>
248 void apply(T& result, const pbes_system::or_& x)
249 {
250 static_cast<Derived&>(*this).enter(x);
251 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()); });
252 static_cast<Derived&>(*this).leave(x);
253 }
254
255 template <class T>
256 void apply(T& result, const pbes_system::imp& x)
257 {
258 static_cast<Derived&>(*this).enter(x);
259 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()); });
260 static_cast<Derived&>(*this).leave(x);
261 }
262
263 template <class T>
264 void apply(T& result, const pbes_system::forall& x)
265 {
266 static_cast<Derived&>(*this).enter(x);
267 pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
268 static_cast<Derived&>(*this).leave(x);
269 }
270
271 template <class T>
272 void apply(T& result, const pbes_system::exists& x)
273 {
274 static_cast<Derived&>(*this).enter(x);
275 pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
276 static_cast<Derived&>(*this).leave(x);
277 }
278
279 template <class T>
280 void apply(T& result, const pbes_system::pbes_expression& x)
281 {
282 static_cast<Derived&>(*this).enter(x);
283 if (data::is_data_expression(x))
284 {
285 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
286 }
287 else if (data::is_untyped_data_parameter(x))
288 {
289 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
290 }
291 else if (pbes_system::is_propositional_variable_instantiation(x))
292 {
293 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
294 }
295 else if (pbes_system::is_not(x))
296 {
297 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
298 }
299 else if (pbes_system::is_and(x))
300 {
301 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
302 }
303 else if (pbes_system::is_or(x))
304 {
305 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
306 }
307 else if (pbes_system::is_imp(x))
308 {
309 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
310 }
311 else if (pbes_system::is_forall(x))
312 {
313 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
314 }
315 else if (pbes_system::is_exists(x))
316 {
317 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
318 }
319 static_cast<Derived&>(*this).leave(x);
320 }
321
322};
323
324/// \\brief Builder class
325template <typename Derived>
326struct data_expression_builder: public add_data_expressions<data::data_expression_builder, Derived>
327{
328};
329//--- end generated add_data_expressions code ---//
330
331//--- start generated add_variables code ---//
332template <template <class> class Builder, class Derived>
333struct add_variables: public Builder<Derived>
334{
335 using super = Builder<Derived>;
336 using super::enter;
337 using super::leave;
338 using super::update;
339 using super::apply;
340
341 template <class T>
342 void apply(T& result, const pbes_system::propositional_variable& x)
343 {
344 static_cast<Derived&>(*this).enter(x);
345 pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
346 static_cast<Derived&>(*this).leave(x);
347 }
348
349 void update(pbes_system::pbes_equation& x)
350 {
351 static_cast<Derived&>(*this).enter(x);
352 propositional_variable result_variable;
353 static_cast<Derived&>(*this).apply(result_variable, x.variable());
354 x.variable() = result_variable;
355 pbes_expression result_formula;
356 static_cast<Derived&>(*this).apply(result_formula, x.formula());
357 x.formula() = result_formula;
358 static_cast<Derived&>(*this).leave(x);
359 }
360
361 void update(pbes_system::pbes& x)
362 {
363 static_cast<Derived&>(*this).enter(x);
364 static_cast<Derived&>(*this).update(x.global_variables());
365 static_cast<Derived&>(*this).update(x.equations());
366 propositional_variable_instantiation result_initial_state;
367 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
368 x.initial_state() = result_initial_state;
369 static_cast<Derived&>(*this).leave(x);
370 }
371
372 template <class T>
373 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
374 {
375 static_cast<Derived&>(*this).enter(x);
376 pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
377 static_cast<Derived&>(*this).leave(x);
378 }
379
380 template <class T>
381 void apply(T& result, const pbes_system::not_& x)
382 {
383 static_cast<Derived&>(*this).enter(x);
384 pbes_system::make_not(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
385 static_cast<Derived&>(*this).leave(x);
386 }
387
388 template <class T>
389 void apply(T& result, const pbes_system::and_& x)
390 {
391 static_cast<Derived&>(*this).enter(x);
392 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()); });
393 static_cast<Derived&>(*this).leave(x);
394 }
395
396 template <class T>
397 void apply(T& result, const pbes_system::or_& x)
398 {
399 static_cast<Derived&>(*this).enter(x);
400 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()); });
401 static_cast<Derived&>(*this).leave(x);
402 }
403
404 template <class T>
405 void apply(T& result, const pbes_system::imp& x)
406 {
407 static_cast<Derived&>(*this).enter(x);
408 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()); });
409 static_cast<Derived&>(*this).leave(x);
410 }
411
412 template <class T>
413 void apply(T& result, const pbes_system::forall& x)
414 {
415 static_cast<Derived&>(*this).enter(x);
416 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()); });
417 static_cast<Derived&>(*this).leave(x);
418 }
419
420 template <class T>
421 void apply(T& result, const pbes_system::exists& x)
422 {
423 static_cast<Derived&>(*this).enter(x);
424 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()); });
425 static_cast<Derived&>(*this).leave(x);
426 }
427
428 template <class T>
429 void apply(T& result, const pbes_system::pbes_expression& x)
430 {
431 static_cast<Derived&>(*this).enter(x);
432 if (data::is_data_expression(x))
433 {
434 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
435 }
436 else if (data::is_untyped_data_parameter(x))
437 {
438 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
439 }
440 else if (pbes_system::is_propositional_variable_instantiation(x))
441 {
442 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
443 }
444 else if (pbes_system::is_not(x))
445 {
446 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
447 }
448 else if (pbes_system::is_and(x))
449 {
450 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
451 }
452 else if (pbes_system::is_or(x))
453 {
454 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
455 }
456 else if (pbes_system::is_imp(x))
457 {
458 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
459 }
460 else if (pbes_system::is_forall(x))
461 {
462 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
463 }
464 else if (pbes_system::is_exists(x))
465 {
466 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
467 }
468 static_cast<Derived&>(*this).leave(x);
469 }
470
471};
472
473/// \\brief Builder class
474template <typename Derived>
475struct variable_builder: public add_variables<data::data_expression_builder, Derived>
476{
477};
478//--- end generated add_variables code ---//
479
480// Adds pbes expression traversal to a builder
481//--- start generated add_pbes_expressions code ---//
482template <template <class> class Builder, class Derived>
483struct add_pbes_expressions: public Builder<Derived>
484{
485 using super = Builder<Derived>;
486 using super::enter;
487 using super::leave;
488 using super::update;
489 using super::apply;
490
491 void update(pbes_system::pbes_equation& x)
492 {
493 static_cast<Derived&>(*this).enter(x);
494 pbes_expression result_formula;
495 static_cast<Derived&>(*this).apply(result_formula, x.formula());
496 x.formula() = result_formula;
497 static_cast<Derived&>(*this).leave(x);
498 }
499
500 void update(pbes_system::pbes& x)
501 {
502 static_cast<Derived&>(*this).enter(x);
503 static_cast<Derived&>(*this).update(x.equations());
504 static_cast<Derived&>(*this).leave(x);
505 }
506
507 template <class T>
508 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
509 {
510 static_cast<Derived&>(*this).enter(x);
511 // skip
512 static_cast<Derived&>(*this).leave(x);
513 result = atermpp::down_cast<T>(x);
514 }
515
516 template <class T>
517 void apply(T& result, const pbes_system::not_& x)
518 {
519 static_cast<Derived&>(*this).enter(x);
520 pbes_system::make_not(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
521 static_cast<Derived&>(*this).leave(x);
522 }
523
524 template <class T>
525 void apply(T& result, const pbes_system::and_& x)
526 {
527 static_cast<Derived&>(*this).enter(x);
528 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()); });
529 static_cast<Derived&>(*this).leave(x);
530 }
531
532 template <class T>
533 void apply(T& result, const pbes_system::or_& x)
534 {
535 static_cast<Derived&>(*this).enter(x);
536 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()); });
537 static_cast<Derived&>(*this).leave(x);
538 }
539
540 template <class T>
541 void apply(T& result, const pbes_system::imp& x)
542 {
543 static_cast<Derived&>(*this).enter(x);
544 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()); });
545 static_cast<Derived&>(*this).leave(x);
546 }
547
548 template <class T>
549 void apply(T& result, const pbes_system::forall& x)
550 {
551 static_cast<Derived&>(*this).enter(x);
552 pbes_system::make_forall(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
553 static_cast<Derived&>(*this).leave(x);
554 }
555
556 template <class T>
557 void apply(T& result, const pbes_system::exists& x)
558 {
559 static_cast<Derived&>(*this).enter(x);
560 pbes_system::make_exists(result, x.variables(), [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
561 static_cast<Derived&>(*this).leave(x);
562 }
563
564 template <class T>
565 void apply(T& result, const pbes_system::pbes_expression& x)
566 {
567 static_cast<Derived&>(*this).enter(x);
568 if (data::is_data_expression(x))
569 {
570 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
571 }
572 else if (data::is_untyped_data_parameter(x))
573 {
574 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
575 }
576 else if (pbes_system::is_propositional_variable_instantiation(x))
577 {
578 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
579 }
580 else if (pbes_system::is_not(x))
581 {
582 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
583 }
584 else if (pbes_system::is_and(x))
585 {
586 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
587 }
588 else if (pbes_system::is_or(x))
589 {
590 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
591 }
592 else if (pbes_system::is_imp(x))
593 {
594 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
595 }
596 else if (pbes_system::is_forall(x))
597 {
598 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
599 }
600 else if (pbes_system::is_exists(x))
601 {
602 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
603 }
604 static_cast<Derived&>(*this).leave(x);
605 }
606
607};
608
609/// \\brief Builder class
610template <typename Derived>
611struct pbes_expression_builder: public add_pbes_expressions<pbes_system::pbes_expression_builder_base, Derived>
612{
613};
614//--- end generated add_pbes_expressions code ---//
615
616} // namespace mcrl2::pbes_system
617
618#endif // MCRL2_PBES_BUILDER_H
atermpp::aterm_string
Term containing a string.
Definition aterm_string.h:20
atermpp::aterm::aterm
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:26
atermpp::unordered_map
A unordered_map class in which aterms can be stored.
Definition unordered_map.h:41
mcrl2::data::abstraction
An abstraction expression.
Definition abstraction.h:23
mcrl2::data::abstraction::abstraction
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:32
mcrl2::data::data_expression
data expression.
Definition data_expression.h:130
mcrl2::data::data_specification
data specification.
Definition data_specification.h:50
mcrl2::data::data_specification::is_well_typed
bool is_well_typed() const
Returns true if.
Definition data_specification.cpp:781
mcrl2::data::representative_generator
Components for generating an arbitrary element of a sort.
Definition representative_generator.h:50
mcrl2::data::representative_generator::representative_generator
representative_generator(const data_specification &specification)
Constructor with data specification as context.
Definition representative_generator.h:260
mcrl2::data::set_identifier_generator
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
Definition set_identifier_generator.h:27
mcrl2::data::sort_specification
Definition sort_specification.h:44
mcrl2::data::untyped_data_parameter
\brief An untyped parameter
Definition untyped_data_parameter.h:24
mcrl2::data::variable
\brief A data variable
Definition variable.h:25
mcrl2::pbes_system::and_
\brief The and operator for pbes expressions
Definition pbes_expression.h:287
mcrl2::pbes_system::and_::and_
and_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
Definition pbes_expression.h:303
mcrl2::pbes_system::and_::and_
and_(const and_ &) noexcept=default
Move semantics.
mcrl2::pbes_system::and_::and_
and_(and_ &&) noexcept=default
mcrl2::pbes_system::and_::operator=
and_ & operator=(and_ &&) noexcept=default
mcrl2::pbes_system::and_::and_
and_(const atermpp::aterm &term)
Definition pbes_expression.h:296
mcrl2::pbes_system::and_::operator=
and_ & operator=(const and_ &) noexcept=default
mcrl2::pbes_system::and_::left
const pbes_expression & left() const
Definition pbes_expression.h:313
mcrl2::pbes_system::and_::right
const pbes_expression & right() const
Definition pbes_expression.h:318
mcrl2::pbes_system::and_::and_
and_()
\brief Default constructor X3.
Definition pbes_expression.h:290
mcrl2::pbes_system::exists
\brief The existential quantification operator for pbes expressions
Definition pbes_expression.h:591
mcrl2::pbes_system::exists::exists
exists(const atermpp::aterm &term)
Definition pbes_expression.h:600
mcrl2::pbes_system::exists::operator=
exists & operator=(exists &&) noexcept=default
mcrl2::pbes_system::exists::exists
exists(exists &&) noexcept=default
mcrl2::pbes_system::exists::exists
exists(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor Z14.
Definition pbes_expression.h:607
mcrl2::pbes_system::exists::variables
const data::variable_list & variables() const
Definition pbes_expression.h:617
mcrl2::pbes_system::exists::exists
exists()
\brief Default constructor X3.
Definition pbes_expression.h:594
mcrl2::pbes_system::exists::exists
exists(const exists &) noexcept=default
Move semantics.
mcrl2::pbes_system::exists::body
const pbes_expression & body() const
Definition pbes_expression.h:622
mcrl2::pbes_system::exists::operator=
exists & operator=(const exists &) noexcept=default
mcrl2::pbes_system::fixpoint_symbol
\brief A fixpoint symbol
Definition fixpoint_symbol.h:23
mcrl2::pbes_system::fixpoint_symbol::nu
static fixpoint_symbol nu()
Returns the nu symbol.
Definition fixpoint_symbol.h:53
mcrl2::pbes_system::fixpoint_symbol::fixpoint_symbol
fixpoint_symbol()
\brief Default constructor X3.
Definition fixpoint_symbol.h:26
mcrl2::pbes_system::fixpoint_symbol::operator=
fixpoint_symbol & operator=(fixpoint_symbol &&) noexcept=default
mcrl2::pbes_system::fixpoint_symbol::fixpoint_symbol
fixpoint_symbol(const fixpoint_symbol &) noexcept=default
Move semantics.
mcrl2::pbes_system::fixpoint_symbol::is_nu
bool is_nu() const
Returns true if the symbol is nu.
Definition fixpoint_symbol.h:67
mcrl2::pbes_system::fixpoint_symbol::is_mu
bool is_mu() const
Returns true if the symbol is mu.
Definition fixpoint_symbol.h:60
mcrl2::pbes_system::fixpoint_symbol::fixpoint_symbol
fixpoint_symbol(fixpoint_symbol &&) noexcept=default
mcrl2::pbes_system::fixpoint_symbol::mu
static fixpoint_symbol mu()
Returns the mu symbol.
Definition fixpoint_symbol.h:46
mcrl2::pbes_system::fixpoint_symbol::operator=
fixpoint_symbol & operator=(const fixpoint_symbol &) noexcept=default
mcrl2::pbes_system::fixpoint_symbol::fixpoint_symbol
fixpoint_symbol(const atermpp::aterm &term)
Definition fixpoint_symbol.h:32
mcrl2::pbes_system::forall
\brief The universal quantification operator for pbes expressions
Definition pbes_expression.h:515
mcrl2::pbes_system::forall::forall
forall()
\brief Default constructor X3.
Definition pbes_expression.h:518
mcrl2::pbes_system::forall::body
const pbes_expression & body() const
Definition pbes_expression.h:546
mcrl2::pbes_system::forall::forall
forall(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor Z14.
Definition pbes_expression.h:531
mcrl2::pbes_system::forall::forall
forall(const atermpp::aterm &term)
Definition pbes_expression.h:524
mcrl2::pbes_system::forall::variables
const data::variable_list & variables() const
Definition pbes_expression.h:541
mcrl2::pbes_system::forall::operator=
forall & operator=(const forall &) noexcept=default
mcrl2::pbes_system::forall::operator=
forall & operator=(forall &&) noexcept=default
mcrl2::pbes_system::forall::forall
forall(const forall &) noexcept=default
Move semantics.
mcrl2::pbes_system::forall::forall
forall(forall &&) noexcept=default
mcrl2::pbes_system::imp
\brief The implication operator for pbes expressions
Definition pbes_expression.h:439
mcrl2::pbes_system::imp::operator=
imp & operator=(imp &&) noexcept=default
mcrl2::pbes_system::imp::imp
imp(const imp &) noexcept=default
Move semantics.
mcrl2::pbes_system::imp::left
const pbes_expression & left() const
Definition pbes_expression.h:465
mcrl2::pbes_system::imp::imp
imp(imp &&) noexcept=default
mcrl2::pbes_system::imp::imp
imp(const atermpp::aterm &term)
Definition pbes_expression.h:448
mcrl2::pbes_system::imp::imp
imp()
\brief Default constructor X3.
Definition pbes_expression.h:442
mcrl2::pbes_system::imp::imp
imp(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
Definition pbes_expression.h:455
mcrl2::pbes_system::imp::right
const pbes_expression & right() const
Definition pbes_expression.h:470
mcrl2::pbes_system::imp::operator=
imp & operator=(const imp &) noexcept=default
mcrl2::pbes_system::not_
\brief The not operator for pbes expressions
Definition pbes_expression.h:216
mcrl2::pbes_system::not_::not_
not_()
\brief Default constructor X3.
Definition pbes_expression.h:219
mcrl2::pbes_system::not_::not_
not_(const pbes_expression &operand)
\brief Constructor Z14.
Definition pbes_expression.h:232
mcrl2::pbes_system::not_::not_
not_(const not_ &) noexcept=default
Move semantics.
mcrl2::pbes_system::not_::operand
const pbes_expression & operand() const
Definition pbes_expression.h:242
mcrl2::pbes_system::not_::operator=
not_ & operator=(const not_ &) noexcept=default
mcrl2::pbes_system::not_::not_
not_(not_ &&) noexcept=default
mcrl2::pbes_system::not_::not_
not_(const atermpp::aterm &term)
Definition pbes_expression.h:225
mcrl2::pbes_system::not_::operator=
not_ & operator=(not_ &&) noexcept=default
mcrl2::pbes_system::or_
\brief The or operator for pbes expressions
Definition pbes_expression.h:363
mcrl2::pbes_system::or_::left
const pbes_expression & left() const
Definition pbes_expression.h:389
mcrl2::pbes_system::or_::or_
or_(const or_ &) noexcept=default
Move semantics.
mcrl2::pbes_system::or_::or_
or_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
Definition pbes_expression.h:379
mcrl2::pbes_system::or_::right
const pbes_expression & right() const
Definition pbes_expression.h:394
mcrl2::pbes_system::or_::or_
or_(or_ &&) noexcept=default
mcrl2::pbes_system::or_::operator=
or_ & operator=(or_ &&) noexcept=default
mcrl2::pbes_system::or_::operator=
or_ & operator=(const or_ &) noexcept=default
mcrl2::pbes_system::or_::or_
or_(const atermpp::aterm &term)
Definition pbes_expression.h:372
mcrl2::pbes_system::or_::or_
or_()
\brief Default constructor X3.
Definition pbes_expression.h:366
mcrl2::pbes_system::pbes_equation
pbes equation.
Definition pbes_equation.h:29
mcrl2::pbes_system::pbes_equation::formula
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
Definition pbes_equation.h:95
mcrl2::pbes_system::pbes_equation::symbol
fixpoint_symbol & symbol()
Returns the fixpoint symbol of the equation.
Definition pbes_equation.h:74
mcrl2::pbes_system::pbes_equation::pbes_equation
pbes_equation(const fixpoint_symbol &symbol, const propositional_variable &variable, const pbes_expression &expr)
Constructor.
Definition pbes_equation.h:57
mcrl2::pbes_system::pbes_equation::is_solved
bool is_solved() const
Returns true if the predicate formula on the right hand side contains no predicate variables.
Definition pbes.cpp:102
mcrl2::pbes_system::pbes_equation::m_symbol
fixpoint_symbol m_symbol
The fixpoint symbol of the equation.
Definition pbes_equation.h:32
mcrl2::pbes_system::pbes_equation::m_variable
propositional_variable m_variable
The variable on the left hand side of the equation.
Definition pbes_equation.h:35
mcrl2::pbes_system::pbes_equation::symbol
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
Definition pbes_equation.h:67
mcrl2::pbes_system::pbes_equation::operator<
bool operator<(const pbes_equation &other) const
A comparison operator on pbes equations.
Definition pbes_equation.h:125
mcrl2::pbes_system::pbes_equation::variable
propositional_variable & variable()
Returns the pbes variable of the equation.
Definition pbes_equation.h:88
mcrl2::pbes_system::pbes_equation::m_formula
pbes_expression m_formula
The expression on the right hand side of the equation.
Definition pbes_equation.h:38
mcrl2::pbes_system::pbes_equation::swap
void swap(pbes_equation &other) noexcept
Swaps the contents.
Definition pbes_equation.h:113
mcrl2::pbes_system::pbes_equation::pbes_equation
pbes_equation()=default
Constructor.
mcrl2::pbes_system::pbes_equation::formula
pbes_expression & formula()
Returns the predicate formula on the right hand side of the equation.
Definition pbes_equation.h:102
mcrl2::pbes_system::pbes_equation::variable
const propositional_variable & variable() const
Returns the pbes variable of the equation.
Definition pbes_equation.h:81
mcrl2::pbes_system::pbes_expression
\brief A pbes expression
Definition pbes_expression.h:25
mcrl2::pbes_system::pbes_expression::operator=
pbes_expression & operator=(pbes_expression &&) noexcept=default
mcrl2::pbes_system::pbes_expression::operator=
pbes_expression & operator=(const pbes_expression &) noexcept=default
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const atermpp::aterm &term)
Definition pbes_expression.h:34
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const pbes_expression &) noexcept=default
Move semantics.
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const data::data_expression &x)
\brief Constructor Z6.
Definition pbes_expression.h:41
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
Definition pbes_expression.h:46
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression()
\brief Default constructor X3.
Definition pbes_expression.h:28
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(pbes_expression &&) noexcept=default
mcrl2::pbes_system::pbes
parameterized boolean equation system
Definition pbes.h:54
mcrl2::pbes_system::pbes::global_variables
std::set< data::variable > & global_variables()
Returns the declared free variables of the pbes.
Definition pbes.h:180
mcrl2::pbes_system::pbes::is_closed
bool is_closed() const
True if the pbes is closed.
Definition pbes.h:238
mcrl2::pbes_system::pbes::m_data
data::data_specification m_data
The data specification.
Definition pbes.h:60
mcrl2::pbes_system::pbes::pbes
pbes(const data::data_specification &data, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
Definition pbes.h:111
mcrl2::pbes_system::pbes::m_global_variables
std::set< data::variable > m_global_variables
The set of global variables.
Definition pbes.h:66
mcrl2::pbes_system::pbes::compute_declared_variables
std::set< propositional_variable > compute_declared_variables() const
Returns the predicate variables appearing in the left hand side of an equation.
Definition pbes.h:73
mcrl2::pbes_system::pbes::pbes
pbes(const data::data_specification &data, const std::set< data::variable > &global_variables, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
Definition pbes.h:129
mcrl2::pbes_system::pbes::initial_state
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:187
mcrl2::pbes_system::pbes::binding_variables
std::set< propositional_variable > binding_variables() const
Returns the set of binding variables of the pbes. This is the set variables that occur on the left ha...
Definition pbes.h:202
mcrl2::pbes_system::pbes::occurring_variables
std::set< propositional_variable > occurring_variables() const
Returns the set of occurring propositional variable declarations of the pbes, i.e....
Definition pbes.h:220
mcrl2::pbes_system::pbes::occurring_variable_instantiations
std::set< propositional_variable_instantiation > occurring_variable_instantiations() const
Returns the set of occurring propositional variable instantiations of the pbes. This is the set of va...
Definition pbes.cpp:107
mcrl2::pbes_system::pbes::global_variables
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
Definition pbes.h:173
mcrl2::pbes_system::pbes::equations
std::vector< pbes_equation > & equations()
Returns the equations.
Definition pbes.h:166
mcrl2::pbes_system::pbes::initial_state
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pbes.h:194
mcrl2::pbes_system::pbes::m_initial_state
propositional_variable_instantiation m_initial_state
The initial state.
Definition pbes.h:69
mcrl2::pbes_system::pbes::pbes
pbes()=default
Constructor.
mcrl2::pbes_system::pbes::m_equations
std::vector< pbes_equation > m_equations
The sequence of pbes equations.
Definition pbes.h:63
mcrl2::pbes_system::pbes::is_declared_in
bool is_declared_in(Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec) const
Checks if the propositional variable instantiation v appears with the right type in the sequence of p...
Definition pbes.h:91
mcrl2::pbes_system::pbes::equations
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:159
mcrl2::pbes_system::pbes::is_well_typed
bool is_well_typed() const
Checks if the PBES is well typed.
Definition pbes.h:260
mcrl2::pbes_system::propositional_variable_instantiation
\brief A propositional variable instantiation
Definition pbes_expression.h:111
mcrl2::pbes_system::propositional_variable_instantiation::parameters
const data::data_expression_list & parameters() const
Definition pbes_expression.h:126
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const propositional_variable_instantiation &) noexcept=default
Move semantics.
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const std::string &name)
Constructor.
Definition pbes_expression.h:163
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation()
Default constructor.
Definition pbes_expression.h:132
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(propositional_variable_instantiation &&) noexcept=default
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const core::identifier_string &name, const data::data_expression_list &parameters)
Constructor.
Definition pbes_expression.h:145
mcrl2::pbes_system::propositional_variable_instantiation::name
const core::identifier_string & name() const
Definition pbes_expression.h:121
mcrl2::pbes_system::propositional_variable_instantiation::operator=
propositional_variable_instantiation & operator=(propositional_variable_instantiation &&) noexcept=default
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const core::identifier_string &name)
Constructor.
Definition pbes_expression.h:157
mcrl2::pbes_system::propositional_variable_instantiation::operator=
propositional_variable_instantiation & operator=(const propositional_variable_instantiation &) noexcept=default
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const std::string &name, const data::data_expression_list &parameters)
Constructor.
Definition pbes_expression.h:151
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const atermpp::aterm &term)
Constructor.
Definition pbes_expression.h:138
mcrl2::pbes_system::propositional_variable
\brief A propositional variable declaration
Definition propositional_variable.h:24
mcrl2::pbes_system::propositional_variable::parameters
const data::variable_list & parameters() const
Definition propositional_variable.h:60
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const atermpp::aterm &term)
Definition propositional_variable.h:33
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const std::string &name)
Definition propositional_variable.h:70
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const std::string &name, const data::variable_list &parameters)
\brief Constructor Z1.
Definition propositional_variable.h:45
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const propositional_variable &) noexcept=default
Move semantics.
mcrl2::pbes_system::propositional_variable::name
const core::identifier_string & name() const
Definition propositional_variable.h:55
mcrl2::pbes_system::propositional_variable::operator=
propositional_variable & operator=(propositional_variable &&) noexcept=default
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable()
\brief Default constructor X3.
Definition propositional_variable.h:27
mcrl2::pbes_system::propositional_variable::operator=
propositional_variable & operator=(const propositional_variable &) noexcept=default
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(propositional_variable &&) noexcept=default
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const atermpp::aterm_string &name)
Definition propositional_variable.h:66
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const core::identifier_string &name, const data::variable_list &parameters)
\brief Constructor Z12.
Definition propositional_variable.h:40
parser_tables_mcrl2
D_ParserTables parser_tables_mcrl2
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:435
mcrl2::core::warn_and_or
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
Definition parser_utility.h:215
mcrl2::data::detail::equal_sorts
bool equal_sorts(const data::variable_list &v, const data::data_expression_list &w, const data::data_specification &data_spec)
Checks if the sorts of the variables/expressions in both lists are equal.
Definition equal_sorts.h:25
mcrl2::data::sort_bool
Namespace for system defined sort bool_.
Definition bool.h:29
mcrl2::data::sort_bool::is_false_function_symbol
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:116
mcrl2::data::sort_bool::is_or_application
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:342
mcrl2::data::sort_bool::false_
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:106
mcrl2::data::sort_bool::is_and_application
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:278
mcrl2::data::sort_bool::is_true_function_symbol
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:84
mcrl2::data::sort_bool::is_not_application
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:214
mcrl2::data::sort_bool::true_
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:74
mcrl2::data::is_data_expression
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
Definition data_expression.h:232
mcrl2::data::is_abstraction
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
Definition data_expression.h:25
mcrl2::data::is_forall
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
Definition data_expression.h:37
mcrl2::data::is_untyped_data_parameter
bool is_untyped_data_parameter(const atermpp::aterm &x)
Definition untyped_data_parameter.h:84
mcrl2::data::is_exists
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
Definition data_expression.h:43
mcrl2::data::is_application
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
Definition data_expression.h:89
mcrl2::data::is_variable
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
Definition data_expression.h:73
mcrl2::pbes_system::accessors
The namespace for accessor functions on pbes expressions.
Definition pbes_expression.h:793
mcrl2::pbes_system::accessors::data_arg
const pbes_expression & data_arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
Definition pbes_expression.h:816
mcrl2::pbes_system::accessors::arg
const pbes_expression & arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
Definition pbes_expression.h:799
mcrl2::pbes_system::accessors::data_right
const pbes_expression & data_right(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
Definition pbes_expression.h:869
mcrl2::pbes_system::accessors::data_left
const pbes_expression & data_left(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
Definition pbes_expression.h:844
mcrl2::pbes_system::accessors::left
const pbes_expression & left(const pbes_expression &t)
Returns the left hand side of an expression of type and, or or imp.
Definition pbes_expression.h:834
mcrl2::pbes_system::accessors::right
const pbes_expression & right(const pbes_expression &t)
Returns the right hand side of an expression of type and, or or imp.
Definition pbes_expression.h:860
mcrl2::pbes_system::accessors::param
const data::data_expression_list & param(const pbes_expression &t)
Returns the parameters of a propositional variable instantiation.
Definition pbes_expression.h:905
mcrl2::pbes_system::accessors::name
const core::identifier_string & name(const pbes_expression &t)
Returns the name of a propositional variable expression.
Definition pbes_expression.h:895
mcrl2::pbes_system::accessors::var
const data::variable_list & var(const pbes_expression &t)
Returns the variables of a quantification expression.
Definition pbes_expression.h:885
mcrl2::pbes_system::algorithms::instantiate_global_variables
void instantiate_global_variables(pbes &p)
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them....
Definition pbes.cpp:64
mcrl2::pbes_system::algorithms::is_bes
bool is_bes(const pbes &x)
Returns true if a PBES is in BES form.
Definition pbes.cpp:69
mcrl2::pbes_system::detail
Definition pbesinst_finite_algorithm.h:88
mcrl2::pbes_system::detail::parse_pbes_new
untyped_pbes parse_pbes_new(const std::string &text)
Definition pbes.cpp:132
mcrl2::pbes_system::detail::replace_global_variables
void replace_global_variables(pbes &p, const data::mutable_map_substitution<> &sigma)
Applies a global variable substitution to a PBES.
Definition instantiate_global_variables.h:23
mcrl2::pbes_system::detail::complete_pbes
void complete_pbes(pbes &x)
Definition pbes.cpp:143
mcrl2::pbes_system::detail::instantiate_global_variables
data::mutable_map_substitution instantiate_global_variables(pbes &p)
Eliminates the global variables of a PBES, by substituting a constant value for them....
Definition instantiate_global_variables.h:34
mcrl2::pbes_system::detail::has_propositional_variables
bool has_propositional_variables(const pbes_expression &x)
Definition has_propositional_variables.h:36
mcrl2::pbes_system::detail::parse_propositional_variable
propositional_variable parse_propositional_variable(const std::string &text)
Definition pbes.cpp:150
mcrl2::pbes_system::detail::parse_pbes_expression
pbes_expression parse_pbes_expression(const std::string &text)
Definition pbes.cpp:159
mcrl2::pbes_system::detail::is_well_typed
bool is_well_typed(const pbes_equation &eqn)
Checks if the equation is well typed.
Definition is_well_typed.h:154
mcrl2::pbes_system::detail::parse_pbes_expression_new
pbes_expression parse_pbes_expression_new(const std::string &text)
Definition pbes.cpp:121
mcrl2::pbes_system
The main namespace for the PBES library.
Definition algorithms.cpp:22
mcrl2::pbes_system::is_pbes_exists
bool is_pbes_exists(const pbes_expression &t)
Returns true if the term t is an existential quantification.
Definition pbes_expression.h:754
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const exists &x)
Definition pbes_expression.h:653
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const pbes_equation &x)
Definition pbes_equation.h:150
mcrl2::pbes_system::is_universal_or
bool is_universal_or(const pbes_expression &t)
Test for a disjunction.
Definition pbes_expression.h:778
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_equation &x)
Definition pbes.cpp:55
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_list &x, bool arg0)
Definition pbes.cpp:30
mcrl2::pbes_system::pp
std::string pp(const pbes_system::or_ &x, bool arg0)
Definition pbes.cpp:40
mcrl2::pbes_system::make_and
void make_and(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:327
mcrl2::pbes_system::is_data
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
Definition pbes_expression.h:786
mcrl2::pbes_system::operator!=
bool operator!=(const pbes_equation &x, const pbes_equation &y)
Definition pbes_equation.h:171
mcrl2::pbes_system::swap
void swap(propositional_variable_instantiation &t1, propositional_variable_instantiation &t2) noexcept
\brief swap overload
Definition pbes_expression.h:208
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
Definition pbes.cpp:53
mcrl2::pbes_system::make_optimized_and
void make_optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
Definition pbes_expression.h:937
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
Definition pbes.cpp:46
mcrl2::pbes_system::pp
std::string pp(const pbes_system::imp &x, bool arg0)
Definition pbes.cpp:38
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
Definition pbes.cpp:32
mcrl2::pbes_system::make_propositional_variable
void make_propositional_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition propositional_variable.h:80
mcrl2::pbes_system::is_propositional_variable
bool is_propositional_variable(const atermpp::aterm &x)
Definition propositional_variable.h:95
mcrl2::pbes_system::optimized_or
pbes_expression optimized_or(const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
Definition pbes_expression.h:968
mcrl2::pbes_system::normalize_sorts
pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
Definition pbes.cpp:48
mcrl2::pbes_system::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
Definition pbes.cpp:51
mcrl2::pbes_system::is_universal_and
bool is_universal_and(const pbes_expression &t)
Test for a conjunction.
Definition pbes_expression.h:770
mcrl2::pbes_system::is_pbes_expression
bool is_pbes_expression(const atermpp::aterm &x)
Definition pbes_expression.h:76
mcrl2::pbes_system::is_pbes_not
bool is_pbes_not(const pbes_expression &t)
Returns true if the term t is a not expression.
Definition pbes_expression.h:714
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation_vector &x, bool arg0)
Definition pbes.cpp:27
mcrl2::pbes_system::true_
const pbes_expression & true_()
Definition pbes_expression.h:679
mcrl2::pbes_system::is_pbes_forall
bool is_pbes_forall(const pbes_expression &t)
Returns true if the term t is a universal quantification.
Definition pbes_expression.h:746
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression_list &x, bool arg0)
Definition pbes.cpp:28
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const not_ &x)
Definition pbes_expression.h:273
mcrl2::pbes_system::is_not
bool is_not(const atermpp::aterm &x)
Definition pbes_expression.h:260
mcrl2::pbes_system::find_propositional_variable_instantiations
std::set< pbes_system::propositional_variable_instantiation > find_propositional_variable_instantiations(const pbes_system::pbes_expression &x)
Definition pbes.cpp:57
mcrl2::pbes_system::make_or
void make_or(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:403
mcrl2::pbes_system::replace_variables_capture_avoiding
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
Definition replace_capture_avoiding.h:102
mcrl2::pbes_system::replace_variables_capture_avoiding
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
Definition replace_capture_avoiding.h:87
mcrl2::pbes_system::is_exists
bool is_exists(const atermpp::aterm &x)
Definition pbes_expression.h:640
mcrl2::pbes_system::free_variables
data::variable_list free_variables(const pbes_expression &x)
Definition pbes_expression.h:1062
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const forall &x)
Definition pbes_expression.h:577
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const fixpoint_symbol &x)
Definition fixpoint_symbol.h:88
mcrl2::pbes_system::operator==
bool operator==(const pbes_equation &x, const pbes_equation &y)
Definition pbes_equation.h:163
mcrl2::pbes_system::is_constant
bool is_constant(const pbes_expression &x)
Definition pbes_expression.h:1042
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
Definition pbes.cpp:47
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const pbes &x)
Definition pbes.h:297
mcrl2::pbes_system::is_or
bool is_or(const atermpp::aterm &x)
Definition pbes_expression.h:412
mcrl2::pbes_system::make_optimized_forall
void make_optimized_forall(pbes_expression &result, const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
Make a universal quantification If l is empty, p is returned.
Definition pbes_expression.h:1001
mcrl2::pbes_system::quantifier_variables
const data::variable_list & quantifier_variables(const pbes_expression &x)
Definition pbes_expression.h:1048
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const and_ &x)
Definition pbes_expression.h:349
mcrl2::pbes_system::optimized_imp
pbes_expression optimized_imp(const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
Definition pbes_expression.h:988
mcrl2::pbes_system::make_optimized_not
void make_optimized_not(pbes_expression &result, const pbes_expression &p)
Make a negation.
Definition pbes_expression.h:917
mcrl2::pbes_system::is_well_typed_pbes
bool is_well_typed_pbes(const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
Definition pbes.cpp:90
mcrl2::pbes_system::find_function_symbols
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
Definition pbes.cpp:56
mcrl2::pbes_system::has_propositional_variables
bool has_propositional_variables(const pbes_expression &x)
mcrl2::pbes_system::make_optimized_or
void make_optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
Definition pbes_expression.h:957
mcrl2::pbes_system::is_forall
bool is_forall(const atermpp::aterm &x)
Definition pbes_expression.h:564
mcrl2::pbes_system::typecheck_pbes
void typecheck_pbes(pbes &pbesspec)
Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.
Definition typecheck.h:272
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const or_ &x)
Definition pbes_expression.h:425
mcrl2::pbes_system::swap
void swap(not_ &t1, not_ &t2) noexcept
\brief swap overload
Definition pbes_expression.h:279
mcrl2::pbes_system::make_propositional_variable_instantiation
void make_propositional_variable_instantiation(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:174
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable &x, bool arg0)
Definition pbes.cpp:44
mcrl2::pbes_system::pp
std::string pp(const pbes_system::exists &x, bool arg0)
Definition pbes.cpp:35
mcrl2::pbes_system::optimized_and
pbes_expression optimized_and(const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
Definition pbes_expression.h:947
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression &x, bool arg0)
Definition pbes.cpp:43
mcrl2::pbes_system::pbes_to_aterm
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
Definition io.cpp:315
mcrl2::pbes_system::is_universal_not
bool is_universal_not(const pbes_expression &t)
Test for a conjunction.
Definition pbes_expression.h:762
mcrl2::pbes_system::operator==
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
Definition pbes.h:318
mcrl2::pbes_system::swap
void swap(pbes_equation &t1, pbes_equation &t2) noexcept
\brief swap overload
Definition pbes_equation.h:156
mcrl2::pbes_system::is_well_typed
bool is_well_typed(const pbes_equation &eqn)
Definition pbes.cpp:76
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const propositional_variable_instantiation &x)
Definition pbes_expression.h:202
mcrl2::pbes_system::replace_sort_expressions
T replace_sort_expressions(const T &x, const Substitution &sigma, bool innermost)
Definition replace.h:102
mcrl2::pbes_system::swap
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
Definition pbes_expression.h:659
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_expression &x)
Definition pbes.cpp:54
mcrl2::pbes_system::swap
void swap(or_ &t1, or_ &t2) noexcept
\brief swap overload
Definition pbes_expression.h:431
mcrl2::pbes_system::translate_user_notation
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
Definition pbes.cpp:50
mcrl2::pbes_system::is_pbes_or
bool is_pbes_or(const pbes_expression &t)
Returns true if the term t is an or expression.
Definition pbes_expression.h:730
mcrl2::pbes_system::is_false
bool is_false(const pbes_expression &t)
Test for the value false.
Definition pbes_expression.h:706
mcrl2::pbes_system::is_pbes_imp
bool is_pbes_imp(const pbes_expression &t)
Returns true if the term t is an imp expression.
Definition pbes_expression.h:738
mcrl2::pbes_system::swap
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
Definition pbes_expression.h:583
mcrl2::pbes_system::is_pbes_and
bool is_pbes_and(const pbes_expression &t)
Returns true if the term t is an and expression.
Definition pbes_expression.h:722
mcrl2::pbes_system::swap
void swap(propositional_variable &t1, propositional_variable &t2) noexcept
\brief swap overload
Definition propositional_variable.h:114
mcrl2::pbes_system::pbes_equation_to_aterm
atermpp::aterm pbes_equation_to_aterm(const pbes_equation &eqn)
Conversion to atermaPpl.
Definition pbes_equation.h:179
mcrl2::pbes_system::search_variable
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
Definition pbes.cpp:59
mcrl2::pbes_system::make_optimized_exists
void make_optimized_exists(pbes_expression &result, const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
Make an optimized existential quantification. If l is empty, p is returned.
Definition pbes_expression.h:1024
mcrl2::pbes_system::find_all_variables
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
Definition pbes.cpp:52
mcrl2::pbes_system::pp
std::string pp(const pbes_system::not_ &x, bool arg0)
Definition pbes.cpp:39
mcrl2::pbes_system::complete_data_specification
void complete_data_specification(pbes &)
Adds all sorts that appear in the PBES p to the data specification of p.
Definition pbes.h:307
mcrl2::pbes_system::optimized_exists
pbes_expression optimized_exists(const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
Make an existential quantification If l is empty, p is returned.
Definition pbes_expression.h:1036
mcrl2::pbes_system::swap
void swap(pbes_expression &t1, pbes_expression &t2) noexcept
\brief swap overload
Definition pbes_expression.h:103
mcrl2::pbes_system::optimized_not
pbes_expression optimized_not(const pbes_expression &p)
Make a negation.
Definition pbes_expression.h:926
mcrl2::pbes_system::make_not
void make_not(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:251
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation &x, bool arg0)
Definition pbes.cpp:42
mcrl2::pbes_system::swap
void swap(imp &t1, imp &t2) noexcept
\brief swap overload
Definition pbes_expression.h:507
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const pbes_expression &x)
Definition pbes_expression.h:97
mcrl2::pbes_system::make_exists
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:631
mcrl2::pbes_system::find_identifiers
std::set< core::identifier_string > find_identifiers(const pbes_system::pbes_expression &x)
Definition pbes.cpp:58
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const imp &x)
Definition pbes_expression.h:501
mcrl2::pbes_system::is_propositional_variable_instantiation
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
Definition pbes_expression.h:189
mcrl2::pbes_system::is_well_typed_equation
bool is_well_typed_equation(const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
Definition pbes.cpp:81
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation &x, bool arg0)
Definition pbes.cpp:45
mcrl2::pbes_system::is_and
bool is_and(const atermpp::aterm &x)
Definition pbes_expression.h:336
mcrl2::pbes_system::pp
std::string pp(const pbes_equation_vector &x)
mcrl2::pbes_system::make_optimized_imp
void make_optimized_imp(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make an implication.
Definition pbes_expression.h:978
mcrl2::pbes_system::swap
void swap(and_ &t1, and_ &t2) noexcept
\brief swap overload
Definition pbes_expression.h:355
mcrl2::pbes_system::translate_user_notation
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:49
mcrl2::pbes_system::swap
void swap(fixpoint_symbol &t1, fixpoint_symbol &t2) noexcept
\brief swap overload
Definition fixpoint_symbol.h:94
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes &x, bool arg0)
Definition pbes.cpp:41
mcrl2::pbes_system::is_imp
bool is_imp(const atermpp::aterm &x)
Definition pbes_expression.h:488
mcrl2::pbes_system::operator<<
std::ostream & operator<<(std::ostream &out, const propositional_variable &x)
Definition propositional_variable.h:108
mcrl2::pbes_system::make_imp
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:479
mcrl2::pbes_system::optimized_forall
pbes_expression optimized_forall(const data::variable_list &l, const pbes_expression &p, bool remove_variables=false)
Make a universal quantification If l is empty, p is returned.
Definition pbes_expression.h:1013
mcrl2::pbes_system::replace_sort_expressions
void replace_sort_expressions(T &x, const Substitution &sigma, bool innermost)
Definition replace.h:92
mcrl2::pbes_system::is_true
bool is_true(const pbes_expression &t)
Test for the value true.
Definition pbes_expression.h:698
mcrl2::pbes_system::false_
const pbes_expression & false_()
Definition pbes_expression.h:688
mcrl2::pbes_system::pp
std::string pp(const pbes_system::and_ &x, bool arg0)
Definition pbes.cpp:34
mcrl2::pbes_system::pp
std::string pp(const pbes_system::fixpoint_symbol &x, bool arg0)
Definition pbes.cpp:36
mcrl2::pbes_system::make_forall
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:555
mcrl2::pbes_system::pp
std::string pp(const pbes_system::forall &x, bool arg0)
Definition pbes.cpp:37
mcrl2::core::builder
expression builder that visits all sub expressions
Definition builder.h:32
mcrl2::core::detail::default_values
Definition default_values.h:1600
mcrl2::core::detail::default_values::PBESForall
static const atermpp::aterm PBESForall
Definition default_values.h:1734
mcrl2::core::detail::default_values::PBExpr
static const atermpp::aterm PBExpr
Definition default_values.h:1772
mcrl2::core::detail::default_values::PBESOr
static const atermpp::aterm PBESOr
Definition default_values.h:1732
mcrl2::core::detail::default_values::PBESExists
static const atermpp::aterm PBESExists
Definition default_values.h:1735
mcrl2::core::detail::default_values::PBESImp
static const atermpp::aterm PBESImp
Definition default_values.h:1733
mcrl2::core::detail::default_values::PBESNot
static const atermpp::aterm PBESNot
Definition default_values.h:1730
mcrl2::core::detail::default_values::FixPoint
static const atermpp::aterm FixPoint
Definition default_values.h:1771
mcrl2::core::detail::default_values::PropVarInst
static const atermpp::aterm PropVarInst
Definition default_values.h:1736
mcrl2::core::detail::default_values::PropVarDecl
static const atermpp::aterm PropVarDecl
Definition default_values.h:1727
mcrl2::core::detail::default_values::PBESAnd
static const atermpp::aterm PBESAnd
Definition default_values.h:1731
mcrl2::core::traverser
expression traverser that visits all sub expressions
Definition traverser.h:29
mcrl2::data::detail::capture_avoiding_substitution_updater
Definition replace_capture_avoiding.h:32
mcrl2::pbes_system::add_data_expressions
Definition builder.h:197
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:256
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:264
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:240
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:280
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:248
mcrl2::pbes_system::add_data_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:204
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:224
mcrl2::pbes_system::add_data_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:213
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:272
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:232
mcrl2::pbes_system::add_pbes_expressions
Definition builder.h:484
mcrl2::pbes_system::add_pbes_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:500
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:565
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:549
mcrl2::pbes_system::add_pbes_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:491
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:517
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:508
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:525
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:541
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:557
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:533
mcrl2::pbes_system::add_sort_expressions
Definition builder.h:47
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:134
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:102
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:110
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:126
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:86
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:55
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:118
mcrl2::pbes_system::add_sort_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:62
mcrl2::pbes_system::add_sort_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:74
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:142
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:94
mcrl2::pbes_system::add_traverser_data_expressions
Definition traverser.h:185
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:236
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:213
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:206
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:251
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:198
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:191
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:258
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:228
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:220
mcrl2::pbes_system::add_traverser_data_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:244
mcrl2::pbes_system::add_traverser_identifier_strings
Definition traverser.h:576
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:598
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:662
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:654
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:622
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:615
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:582
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:638
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:646
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:630
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:590
mcrl2::pbes_system::add_traverser_identifier_strings::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:607
mcrl2::pbes_system::add_traverser_pbes_expressions
Definition traverser.h:312
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:332
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:346
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:370
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:318
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:354
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:362
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:384
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:377
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:339
mcrl2::pbes_system::add_traverser_pbes_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:325
mcrl2::pbes_system::add_traverser_sort_expressions
Definition traverser.h:47
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:123
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:99
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:77
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:53
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:107
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:91
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:68
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:115
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:60
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:131
mcrl2::pbes_system::add_traverser_sort_expressions::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:84
mcrl2::pbes_system::add_traverser_variables
Definition traverser.h:438
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes &x)
Definition traverser.h:459
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:444
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::or_ &x)
Definition traverser.h:490
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:468
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::not_ &x)
Definition traverser.h:475
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::exists &x)
Definition traverser.h:514
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::and_ &x)
Definition traverser.h:482
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::imp &x)
Definition traverser.h:498
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:522
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:451
mcrl2::pbes_system::add_traverser_variables::apply
void apply(const pbes_system::forall &x)
Definition traverser.h:506
mcrl2::pbes_system::add_variables
Definition builder.h:334
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:405
mcrl2::pbes_system::add_variables::update
void update(pbes_system::pbes &x)
Definition builder.h:361
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:429
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:413
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:342
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:381
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:389
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:397
mcrl2::pbes_system::add_variables::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:349
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:421
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:373
mcrl2::pbes_system::data_expression_builder
\brief Builder class
Definition builder.h:327
mcrl2::pbes_system::data_expression_traverser
\brief Traverser class
Definition traverser.h:305
mcrl2::pbes_system::detail::add_capture_avoiding_replacement
Definition replace_capture_avoiding.h:28
mcrl2::pbes_system::detail::add_capture_avoiding_replacement::update
void update(pbes_equation &x)
Definition replace_capture_avoiding.h:60
mcrl2::pbes_system::detail::add_capture_avoiding_replacement::apply
void apply(T &result, const exists &x)
Definition replace_capture_avoiding.h:51
mcrl2::pbes_system::detail::add_capture_avoiding_replacement::add_capture_avoiding_replacement
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
Definition replace_capture_avoiding.h:36
mcrl2::pbes_system::detail::add_capture_avoiding_replacement::apply
void apply(T &result, const forall &x)
Definition replace_capture_avoiding.h:41
mcrl2::pbes_system::detail::add_capture_avoiding_replacement::update
void update(pbes &x)
Definition replace_capture_avoiding.h:70
mcrl2::pbes_system::detail::has_propositional_variables_traverser
Definition has_propositional_variables.h:21
mcrl2::pbes_system::detail::has_propositional_variables_traverser::result
bool result
Definition has_propositional_variables.h:27
mcrl2::pbes_system::detail::has_propositional_variables_traverser::enter
void enter(const propositional_variable_instantiation &)
Definition has_propositional_variables.h:29
mcrl2::pbes_system::detail::pbes_actions
Definition parse_impl.h:24
mcrl2::pbes_system::detail::pbes_actions::parse_PropVarDecl
pbes_system::propositional_variable parse_PropVarDecl(const core::parse_node &node) const
Definition parse_impl.h:47
mcrl2::pbes_system::detail::pbes_actions::pbes_actions
pbes_actions(const core::parser &parser_)
Definition parse_impl.h:25
mcrl2::pbes_system::detail::pbes_actions::parse_PbesSpec
untyped_pbes parse_PbesSpec(const core::parse_node &node) const
Definition parse_impl.h:84
mcrl2::pbes_system::detail::pbes_actions::parse_PbesExpr
pbes_system::pbes_expression parse_PbesExpr(const core::parse_node &node) const
Definition parse_impl.h:29
mcrl2::pbes_system::identifier_string_traverser
\brief Traverser class
Definition traverser.h:709
mcrl2::pbes_system::pbes_expression_builder_base
Builder class.
Definition builder.h:24
mcrl2::pbes_system::pbes_expression_builder_base::apply
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:37
mcrl2::pbes_system::pbes_expression_builder_base::apply
void apply(T &result, const data::data_expression &x)
Definition builder.h:32
mcrl2::pbes_system::pbes_expression_builder
\brief Builder class
Definition builder.h:612
mcrl2::pbes_system::pbes_expression_traverser_base
Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
Definition traverser.h:23
mcrl2::pbes_system::pbes_expression_traverser_base::apply
void apply(const data::data_expression &x)
Definition traverser.h:29
mcrl2::pbes_system::pbes_expression_traverser_base::apply
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:36
mcrl2::pbes_system::pbes_expression_traverser
\brief Traverser class
Definition traverser.h:431
mcrl2::pbes_system::pg_actions
Definition pg_parse.h:75
mcrl2::pbes_system::sort_expression_builder
\brief Builder class
Definition builder.h:189
mcrl2::pbes_system::sort_expression_traverser
\brief Traverser class
Definition traverser.h:178
mcrl2::pbes_system::untyped_pbes
Definition untyped_pbes.h:21
mcrl2::pbes_system::variable_builder
\brief Builder class
Definition builder.h:476
mcrl2::pbes_system::variable_traverser
\brief Traverser class
Definition traverser.h:569
std::hash< mcrl2::pbes_system::pbes_expression >::operator()
std::size_t operator()(const mcrl2::pbes_system::pbes_expression &x) const
Definition pbes_expression.h:1474
std::hash< mcrl2::pbes_system::propositional_variable_instantiation >::operator()
std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation &x) const
Definition pbes_expression.h:1483