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
19{
20
21namespace pbes_system
22{
23
24/// \brief Builder class
25template <typename Derived>
26struct pbes_expression_builder_base: public core::builder<Derived>
27{
28 typedef core::builder<Derived> super;
29 using super::enter;
30 using super::leave;
31 using super::update;
32 using super::apply;
33
34 template <class T>
35 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>
53 void apply(T& result, const pbes_system::propositional_variable& x)
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
61 void update(pbes_system::pbes_equation& x)
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
73 void update(pbes_system::pbes& x)
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>
85 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
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);
152 if (data::is_data_expression(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 }
160 else if (data::is_untyped_data_parameter(x))
161 {
162 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
163 }
164 else if (pbes_system::is_propositional_variable_instantiation(x))
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
197/// \\brief Builder class
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
215 void update(pbes_system::pbes_equation& x)
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
224 void update(pbes_system::pbes& x)
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>
235 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
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);
302 if (data::is_data_expression(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 }
310 else if (data::is_untyped_data_parameter(x))
311 {
312 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
313 }
314 else if (pbes_system::is_propositional_variable_instantiation(x))
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
347/// \\brief Builder class
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>
365 void apply(T& result, const pbes_system::propositional_variable& x)
366 {
367
368 static_cast<Derived&>(*this).enter(x);
369 pbes_system::make_propositional_variable(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
370 static_cast<Derived&>(*this).leave(x);
371 }
372
373 void update(pbes_system::pbes_equation& x)
374 {
375 static_cast<Derived&>(*this).enter(x);
376 propositional_variable result_variable;
377 static_cast<Derived&>(*this).apply(result_variable, x.variable());
378 x.variable() = result_variable;
379 pbes_expression result_formula;
380 static_cast<Derived&>(*this).apply(result_formula, x.formula());
381 x.formula() = result_formula;
382 static_cast<Derived&>(*this).leave(x);
383 }
384
385 void update(pbes_system::pbes& x)
386 {
387 static_cast<Derived&>(*this).enter(x);
388 static_cast<Derived&>(*this).update(x.global_variables());
389 static_cast<Derived&>(*this).update(x.equations());
390 propositional_variable_instantiation result_initial_state;
391 static_cast<Derived&>(*this).apply(result_initial_state, x.initial_state());
392 x.initial_state() = result_initial_state;
393 static_cast<Derived&>(*this).leave(x);
394 }
395
396 template <class T>
397 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
398 {
399
400 static_cast<Derived&>(*this).enter(x);
401 pbes_system::make_propositional_variable_instantiation(result, x.name(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.parameters()); });
402 static_cast<Derived&>(*this).leave(x);
403 }
404
405 template <class T>
406 void apply(T& result, const pbes_system::not_& x)
407 {
408
409 static_cast<Derived&>(*this).enter(x);
410 pbes_system::make_not_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
411 static_cast<Derived&>(*this).leave(x);
412 }
413
414 template <class T>
415 void apply(T& result, const pbes_system::and_& x)
416 {
417
418 static_cast<Derived&>(*this).enter(x);
419 pbes_system::make_and_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
420 static_cast<Derived&>(*this).leave(x);
421 }
422
423 template <class T>
424 void apply(T& result, const pbes_system::or_& x)
425 {
426
427 static_cast<Derived&>(*this).enter(x);
428 pbes_system::make_or_(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
429 static_cast<Derived&>(*this).leave(x);
430 }
431
432 template <class T>
433 void apply(T& result, const pbes_system::imp& x)
434 {
435
436 static_cast<Derived&>(*this).enter(x);
437 pbes_system::make_imp(result, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
438 static_cast<Derived&>(*this).leave(x);
439 }
440
441 template <class T>
442 void apply(T& result, const pbes_system::forall& x)
443 {
444
445 static_cast<Derived&>(*this).enter(x);
446 pbes_system::make_forall(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
447 static_cast<Derived&>(*this).leave(x);
448 }
449
450 template <class T>
451 void apply(T& result, const pbes_system::exists& x)
452 {
453
454 static_cast<Derived&>(*this).enter(x);
455 pbes_system::make_exists(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](pbes_expression& result){ static_cast<Derived&>(*this).apply(result, x.body()); });
456 static_cast<Derived&>(*this).leave(x);
457 }
458
459 template <class T>
460 void apply(T& result, const pbes_system::pbes_expression& x)
461 {
462
463 static_cast<Derived&>(*this).enter(x);
464 if (data::is_data_expression(x))
465 {
466 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::data_expression>(x));
467 }
468 else if (data::is_variable(x))
469 {
470 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::variable>(x));
471 }
472 else if (data::is_untyped_data_parameter(x))
473 {
474 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
475 }
476 else if (pbes_system::is_propositional_variable_instantiation(x))
477 {
478 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::propositional_variable_instantiation>(x));
479 }
480 else if (pbes_system::is_not(x))
481 {
482 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::not_>(x));
483 }
484 else if (pbes_system::is_and(x))
485 {
486 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::and_>(x));
487 }
488 else if (pbes_system::is_or(x))
489 {
490 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::or_>(x));
491 }
492 else if (pbes_system::is_imp(x))
493 {
494 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::imp>(x));
495 }
496 else if (pbes_system::is_forall(x))
497 {
498 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::forall>(x));
499 }
500 else if (pbes_system::is_exists(x))
501 {
502 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<pbes_system::exists>(x));
503 }
504 static_cast<Derived&>(*this).leave(x);
505 }
506
507};
508
509/// \\brief Builder class
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
527 void update(pbes_system::pbes_equation& x)
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
536 void update(pbes_system::pbes& x)
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>
544 void apply(T& result, const pbes_system::propositional_variable_instantiation& x)
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);
613 if (data::is_data_expression(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 }
621 else if (data::is_untyped_data_parameter(x))
622 {
623 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
624 }
625 else if (pbes_system::is_propositional_variable_instantiation(x))
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
658/// \\brief Builder class
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
atermpp::aterm_string
Term containing a string.
Definition aterm_string.h:20
atermpp::aterm::operator[]
const aterm & operator[](const size_type i) const
Returns the i-th argument.
Definition aterm.h:187
atermpp::aterm::function
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
atermpp::aterm::aterm
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
atermpp::aterm::aterm
aterm(const function_symbol &sym)
Constructor.
Definition aterm.h:128
atermpp::function_symbol::operator==
bool operator==(const function_symbol &f) const
Equality test.
Definition function_symbol.h:74
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:24
atermpp::unprotected_aterm_core::swap
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
atermpp::unprotected_aterm_core::operator<
bool operator<(const unprotected_aterm_core &t) const
Comparison operator for two unprotected aterms.
Definition aterm_core.h:104
atermpp::unprotected_aterm_core::operator==
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
mcrl2::data::abstraction
An abstraction expression.
Definition abstraction.h:26
mcrl2::data::abstraction::abstraction
abstraction(const atermpp::aterm &term)
Constructor.
Definition abstraction.h:35
mcrl2::data::data_expression
data expression.
Definition data_expression.h:131
mcrl2::data::data_expression::data_expression
data_expression(const data_expression &) noexcept=default
Move semantics.
mcrl2::data::data_specification
data specification.
Definition data_specification.h:48
mcrl2::data::data_specification::is_well_typed
bool is_well_typed() const
Returns true if.
Definition data_specification.cpp:779
mcrl2::data::sort_specification
Definition sort_specification.h:46
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:28
mcrl2::pbes_system::and_
\brief The and operator for pbes expressions
Definition pbes_expression.h:296
mcrl2::pbes_system::and_::and_
and_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
Definition pbes_expression.h:312
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:305
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:322
mcrl2::pbes_system::and_::right
const pbes_expression & right() const
Definition pbes_expression.h:327
mcrl2::pbes_system::and_::and_
and_()
\brief Default constructor X3.
Definition pbes_expression.h:299
mcrl2::pbes_system::exists
\brief The existential quantification operator for pbes expressions
Definition pbes_expression.h:600
mcrl2::pbes_system::exists::exists
exists(const atermpp::aterm &term)
Definition pbes_expression.h:609
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:616
mcrl2::pbes_system::exists::variables
const data::variable_list & variables() const
Definition pbes_expression.h:626
mcrl2::pbes_system::exists::exists
exists()
\brief Default constructor X3.
Definition pbes_expression.h:603
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:631
mcrl2::pbes_system::exists::operator=
exists & operator=(const exists &) noexcept=default
mcrl2::pbes_system::fixpoint_symbol
\brief A fixpoint symbol
Definition fixpoint_symbol.h:26
mcrl2::pbes_system::fixpoint_symbol::nu
static fixpoint_symbol nu()
Returns the nu symbol.
Definition fixpoint_symbol.h:56
mcrl2::pbes_system::fixpoint_symbol::fixpoint_symbol
fixpoint_symbol()
\brief Default constructor X3.
Definition fixpoint_symbol.h:29
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:70
mcrl2::pbes_system::fixpoint_symbol::is_mu
bool is_mu() const
Returns true if the symbol is mu.
Definition fixpoint_symbol.h:63
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:49
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:35
mcrl2::pbes_system::forall
\brief The universal quantification operator for pbes expressions
Definition pbes_expression.h:524
mcrl2::pbes_system::forall::forall
forall()
\brief Default constructor X3.
Definition pbes_expression.h:527
mcrl2::pbes_system::forall::body
const pbes_expression & body() const
Definition pbes_expression.h:555
mcrl2::pbes_system::forall::forall
forall(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor Z14.
Definition pbes_expression.h:540
mcrl2::pbes_system::forall::forall
forall(const atermpp::aterm &term)
Definition pbes_expression.h:533
mcrl2::pbes_system::forall::variables
const data::variable_list & variables() const
Definition pbes_expression.h:550
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:448
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:474
mcrl2::pbes_system::imp::imp
imp(imp &&) noexcept=default
mcrl2::pbes_system::imp::imp
imp(const atermpp::aterm &term)
Definition pbes_expression.h:457
mcrl2::pbes_system::imp::imp
imp()
\brief Default constructor X3.
Definition pbes_expression.h:451
mcrl2::pbes_system::imp::imp
imp(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
Definition pbes_expression.h:464
mcrl2::pbes_system::imp::right
const pbes_expression & right() const
Definition pbes_expression.h:479
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:225
mcrl2::pbes_system::not_::not_
not_()
\brief Default constructor X3.
Definition pbes_expression.h:228
mcrl2::pbes_system::not_::not_
not_(const pbes_expression &operand)
\brief Constructor Z14.
Definition pbes_expression.h:241
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:251
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:234
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:372
mcrl2::pbes_system::or_::left
const pbes_expression & left() const
Definition pbes_expression.h:398
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:388
mcrl2::pbes_system::or_::right
const pbes_expression & right() const
Definition pbes_expression.h:403
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:381
mcrl2::pbes_system::or_::or_
or_()
\brief Default constructor X3.
Definition pbes_expression.h:375
mcrl2::pbes_system::pbes_abstract_algorithm
Algorithm class for the abstract algorithm.
Definition abstract.h:120
mcrl2::pbes_system::pbes_abstract_algorithm::run
void run(pbes &p, const detail::pbes_parameter_map &parameter_map, bool value_true)
Runs the algorithm.
Definition abstract.h:126
mcrl2::pbes_system::pbes_equation
pbes equation.
Definition pbes_equation.h:32
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:98
mcrl2::pbes_system::pbes_equation::symbol
fixpoint_symbol & symbol()
Returns the fixpoint symbol of the equation.
Definition pbes_equation.h:77
mcrl2::pbes_system::pbes_equation::term_type
pbes_expression term_type
The expression type of the equation.
Definition pbes_equation.h:45
mcrl2::pbes_system::pbes_equation::symbol_type
fixpoint_symbol symbol_type
The symbol type of the equation.
Definition pbes_equation.h:51
mcrl2::pbes_system::pbes_equation::swap
void swap(pbes_equation &other)
Swaps the contents.
Definition pbes_equation.h:116
mcrl2::pbes_system::pbes_equation::variable_type
propositional_variable variable_type
The variable type of the equation.
Definition pbes_equation.h:48
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:60
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:103
mcrl2::pbes_system::pbes_equation::m_symbol
fixpoint_symbol m_symbol
The fixpoint symbol of the equation.
Definition pbes_equation.h:35
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:38
mcrl2::pbes_system::pbes_equation::symbol
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
Definition pbes_equation.h:70
mcrl2::pbes_system::pbes_equation::operator<
bool operator<(const pbes_equation &other) const
A comparison operator on pbes equations. \detail The comparison is on the addresses of aterm objects ...
Definition pbes_equation.h:128
mcrl2::pbes_system::pbes_equation::variable
propositional_variable & variable()
Returns the pbes variable of the equation.
Definition pbes_equation.h:91
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:41
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:105
mcrl2::pbes_system::pbes_equation::variable
const propositional_variable & variable() const
Returns the pbes variable of the equation.
Definition pbes_equation.h:84
mcrl2::pbes_system::pbes_expression
\brief A pbes expression
Definition pbes_expression.h:28
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:37
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:44
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
Definition pbes_expression.h:54
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(const data::variable &x)
\brief Constructor Z6.
Definition pbes_expression.h:49
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression()
\brief Default constructor X3.
Definition pbes_expression.h:31
mcrl2::pbes_system::pbes_expression::pbes_expression
pbes_expression(pbes_expression &&) noexcept=default
mcrl2::pbes_system::pbes
parameterized boolean equation system
Definition pbes.h:58
mcrl2::pbes_system::pbes::global_variables
std::set< data::variable > & global_variables()
Returns the declared free variables of the pbes.
Definition pbes.h:185
mcrl2::pbes_system::pbes::is_closed
bool is_closed() const
True if the pbes is closed.
Definition pbes.h:245
mcrl2::pbes_system::pbes::m_data
data::data_specification m_data
The data specification.
Definition pbes.h:64
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:116
mcrl2::pbes_system::pbes::m_global_variables
std::set< data::variable > m_global_variables
The set of global variables.
Definition pbes.h:70
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:77
mcrl2::pbes_system::pbes::equation_type
pbes_equation equation_type
Definition pbes.h:60
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:134
mcrl2::pbes_system::pbes::initial_state
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:192
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:207
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:227
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:108
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:178
mcrl2::pbes_system::pbes::equations
std::vector< pbes_equation > & equations()
Returns the equations.
Definition pbes.h:171
mcrl2::pbes_system::pbes::initial_state
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pbes.h:199
mcrl2::pbes_system::pbes::m_initial_state
propositional_variable_instantiation m_initial_state
The initial state.
Definition pbes.h:73
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:67
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:96
mcrl2::pbes_system::pbes::equations
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:164
mcrl2::pbes_system::pbes::is_well_typed
bool is_well_typed() const
Checks if the PBES is well typed.
Definition pbes.h:267
mcrl2::pbes_system::propositional_variable_instantiation
\brief A propositional variable instantiation
Definition pbes_expression.h:120
mcrl2::pbes_system::propositional_variable_instantiation::parameters
const data::data_expression_list & parameters() const
Definition pbes_expression.h:135
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:172
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation()
Default constructor.
Definition pbes_expression.h:141
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:154
mcrl2::pbes_system::propositional_variable_instantiation::name
const core::identifier_string & name() const
Definition pbes_expression.h:130
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:166
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:160
mcrl2::pbes_system::propositional_variable_instantiation::propositional_variable_instantiation
propositional_variable_instantiation(const atermpp::aterm &term)
Constructor.
Definition pbes_expression.h:147
mcrl2::pbes_system::propositional_variable
\brief A propositional variable declaration
Definition propositional_variable.h:27
mcrl2::pbes_system::propositional_variable::parameters
const data::variable_list & parameters() const
Definition propositional_variable.h:63
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const atermpp::aterm &term)
Definition propositional_variable.h:36
mcrl2::pbes_system::propositional_variable::propositional_variable
propositional_variable(const std::string &name)
Definition propositional_variable.h:73
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:48
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:58
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:30
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:69
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:43
mcrl2::runtime_error
Standard exception class for reporting runtime errors.
Definition exception.h:27
mcrl2::utilities::execution_timer
Simple timer to time the CPU time used by a piece of code.
Definition execution_timer.h:47
mcrl2::utilities::execution_timer::write_report
void write_report(std::ostream &s)
Write the report to an output stream.
Definition execution_timer.h:71
mcrl2::utilities::execution_timer::m_timings
std::map< std::string, timing > m_timings
collection of timings
Definition execution_timer.h:67
mcrl2::utilities::execution_timer::start
void start(const std::string &timing_name)
Start measurement with a hint.
Definition execution_timer.h:118
mcrl2::utilities::execution_timer::m_filename
std::string m_filename
name of the file to write timings to
Definition execution_timer.h:66
mcrl2::utilities::execution_timer::finish
void finish(const std::string &timing_name)
Finish a measurement with a hint.
Definition execution_timer.h:135
mcrl2::utilities::execution_timer::report
void report()
Write all timing information that has been recorded.
Definition execution_timer.h:158
mcrl2::utilities::execution_timer::execution_timer
execution_timer(const std::string &tool_name="", std::string const &filename="")
Constructor of a simple execution timer.
Definition execution_timer.h:105
mcrl2::utilities::execution_timer::~execution_timer
~execution_timer()
Destructor.
Definition execution_timer.h:111
mcrl2::utilities::execution_timer::m_tool_name
std::string m_tool_name
name of the tool we are timing
Definition execution_timer.h:65
mcrl2::utilities::file_format
Definition file_utility.h:40
mcrl2::utilities::file_format::m_description
std::string m_description
Definition file_utility.h:43
mcrl2::utilities::file_format::text_format
bool text_format() const
Definition file_utility.h:66
mcrl2::utilities::file_format::file_format
file_format()
Definition file_utility.h:48
mcrl2::utilities::file_format::m_extensions
std::vector< std::string > m_extensions
Definition file_utility.h:45
mcrl2::utilities::file_format::shortname
const std::string & shortname() const
Definition file_utility.h:62
mcrl2::utilities::file_format::m_shortname
std::string m_shortname
Definition file_utility.h:42
mcrl2::utilities::file_format::operator==
bool operator==(const file_format &other) const
Definition file_utility.h:80
mcrl2::utilities::file_format::m_text_format
bool m_text_format
Definition file_utility.h:44
mcrl2::utilities::file_format::operator<
bool operator<(const file_format &other) const
Definition file_utility.h:85
mcrl2::utilities::file_format::description
const std::string & description() const
Definition file_utility.h:64
atermpp
The main namespace for the aterm++ library.
Definition algorithm.h:21
mcrl2::core::detail::function_symbol_Mu
const atermpp::function_symbol & function_symbol_Mu()
Definition function_symbols.h:515
mcrl2::core::detail::function_symbol_PBESExists
const atermpp::function_symbol & function_symbol_PBESExists()
Definition function_symbols.h:571
mcrl2::core::detail::function_symbol_PBEqn
const atermpp::function_symbol & function_symbol_PBEqn()
Definition function_symbols.h:627
mcrl2::core::detail::function_symbol_Nu
const atermpp::function_symbol & function_symbol_Nu()
Definition function_symbols.h:539
mcrl2::core::detail::function_symbol_PropVarDecl
const atermpp::function_symbol & function_symbol_PropVarDecl()
Definition function_symbols.h:867
mcrl2::core::detail::function_symbol_PBESNot
const atermpp::function_symbol & function_symbol_PBESNot()
Definition function_symbols.h:603
mcrl2::core::detail::function_symbol_PBESAnd
const atermpp::function_symbol & function_symbol_PBESAnd()
Definition function_symbols.h:563
mcrl2::core::detail::function_symbol_PBESOr
const atermpp::function_symbol & function_symbol_PBESOr()
Definition function_symbols.h:611
mcrl2::core::detail::function_symbol_PBESImp
const atermpp::function_symbol & function_symbol_PBESImp()
Definition function_symbols.h:595
mcrl2::core::detail::function_symbol_PBESForall
const atermpp::function_symbol & function_symbol_PBESForall()
Definition function_symbols.h:587
mcrl2::core::detail::function_symbol_PropVarInst
const atermpp::function_symbol & function_symbol_PropVarInst()
Definition function_symbols.h:875
mcrl2::core::identifier_string
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
Definition identifier_string.h:26
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:28
mcrl2::data::sort_bool
Namespace for system defined sort bool_.
Definition bool.h:32
mcrl2::data::sort_bool::is_false_function_symbol
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
mcrl2::data::sort_bool::is_or_application
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
mcrl2::data::sort_bool::false_
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
mcrl2::data::sort_bool::is_and_application
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
mcrl2::data::sort_bool::is_true_function_symbol
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
mcrl2::data::sort_bool::is_not_application
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
mcrl2::data::sort_bool::true_
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
mcrl2::data
Namespace for all data library functionality.
Definition data.cpp:22
mcrl2::data::is_data_expression
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
Definition data_expression.h:233
mcrl2::data::is_abstraction
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
Definition data_expression.h:26
mcrl2::data::false_
const data_expression & false_()
Definition consistency.h:99
mcrl2::data::true_
const data_expression & true_()
Definition consistency.h:92
mcrl2::data::rewrite_strategy
rewrite_strategy
The strategy of the rewriter.
Definition rewrite_strategy.h:14
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:38
mcrl2::data::data_expression_list
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
Definition data_expression.h:199
mcrl2::data::is_untyped_data_parameter
bool is_untyped_data_parameter(const atermpp::aterm &x)
Definition untyped_data_parameter.h:84
mcrl2::data::variable_list
atermpp::term_list< variable > variable_list
\brief list of variables
Definition data_expression.h:278
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:44
mcrl2::data::is_application
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
Definition data_expression.h:90
mcrl2::data::is_variable
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
Definition data_expression.h:74
mcrl2::pbes_system::accessors
The namespace for accessor functions on pbes expressions.
Definition pbes_expression.h:802
mcrl2::pbes_system::accessors::data_left
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:853
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:808
mcrl2::pbes_system::accessors::data_arg
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:825
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:843
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:869
mcrl2::pbes_system::accessors::data_right
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:878
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:914
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:904
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:894
mcrl2::pbes_system::algorithms
Definition algorithms.cpp:24
mcrl2::pbes_system::algorithms::normalize
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
Definition algorithms.cpp:36
mcrl2::pbes_system::detail
Definition pbesinst_finite_algorithm.h:89
mcrl2::pbes_system::detail::pbes_parameter_map
std::map< core::identifier_string, std::vector< data::variable > > pbes_parameter_map
Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
Definition pbes_parameter_map.h:29
mcrl2::pbes_system::detail::parse_pbes_parameter_map
pbes_parameter_map parse_pbes_parameter_map(const pbes &p, const std::string &text)
Parses parameter selection for finite pbesinst algorithm.
Definition pbes_parameter_map.h:78
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:763
mcrl2::pbes_system::pbes_expression_list
atermpp::term_list< pbes_expression > pbes_expression_list
\brief list of pbes_expressions
Definition pbes_expression.h:66
mcrl2::pbes_system::pp
std::string pp(const pbes_system::forall &x)
Definition pbes.cpp:38
mcrl2::pbes_system::is_pbes_file_format
bool is_pbes_file_format(const utilities::file_format &format)
Definition io.h:29
mcrl2::pbes_system::is_universal_or
bool is_universal_or(const pbes_expression &t)
Test for a disjunction.
Definition pbes_expression.h:787
mcrl2::pbes_system::lps2pbes
void lps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename, bool timed, bool structured, bool unoptimized, bool preprocess_modal_operators, bool generate_counter_example, bool check_only)
Definition lps2pbes.h:42
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_equation &x)
Definition pbes.cpp:56
mcrl2::pbes_system::fixpoint_symbol_list
atermpp::term_list< fixpoint_symbol > fixpoint_symbol_list
\brief list of fixpoint_symbols
Definition fixpoint_symbol.h:78
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation &x)
Definition pbes.cpp:43
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:795
mcrl2::pbes_system::pp
std::string pp(const pbes_system::and_ &x)
Definition pbes.cpp:35
mcrl2::pbes_system::operator!=
bool operator!=(const pbes_equation &x, const pbes_equation &y)
Definition pbes_equation.h:174
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
Definition pbes.cpp:54
mcrl2::pbes_system::description
std::string description(const absinthe_strategy strategy)
Prints an absinthe strategy.
Definition absinthe_strategy.h:86
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
Definition pbes.cpp:47
mcrl2::pbes_system::swap
void swap(propositional_variable &t1, propositional_variable &t2)
\brief swap overload
Definition propositional_variable.h:117
mcrl2::pbes_system::operator>>
std::istream & operator>>(std::istream &is, pbesinst_strategy &s)
Definition pbesinst_strategy.h:53
mcrl2::pbes_system::operator>>
std::istream & operator>>(std::istream &is, absinthe_strategy &strategy)
Definition absinthe_strategy.h:62
mcrl2::pbes_system::parse_pbes_rewriter_type
pbes_rewriter_type parse_pbes_rewriter_type(const std::string &type)
Parses a pbes rewriter type.
Definition pbes_rewriter_type.h:38
mcrl2::pbes_system::pbesabstract
void pbesabstract(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &parameter_selection, bool value_true)
Definition pbesabstract.h:24
mcrl2::pbes_system::make_propositional_variable
void make_propositional_variable(atermpp::aterm &t, const ARGUMENTS &... args)
Definition propositional_variable.h:83
mcrl2::pbes_system::is_propositional_variable
bool is_propositional_variable(const atermpp::aterm &x)
Definition propositional_variable.h:98
mcrl2::pbes_system::swap
void swap(propositional_variable_instantiation &t1, propositional_variable_instantiation &t2)
\brief swap overload
Definition pbes_expression.h:217
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:49
mcrl2::pbes_system::pbes_rewriter_type
pbes_rewriter_type
An enumerated type for the available pbes rewriters.
Definition pbes_rewriter_type.h:24
mcrl2::pbes_system::quantifier_finite
@ quantifier_finite
Definition pbes_rewriter_type.h:27
mcrl2::pbes_system::quantifier_all
@ quantifier_all
Definition pbes_rewriter_type.h:26
mcrl2::pbes_system::quantifier_inside
@ quantifier_inside
Definition pbes_rewriter_type.h:28
mcrl2::pbes_system::bqnf_quantifier
@ bqnf_quantifier
Definition pbes_rewriter_type.h:33
mcrl2::pbes_system::prover
@ prover
Definition pbes_rewriter_type.h:30
mcrl2::pbes_system::ppg
@ ppg
Definition pbes_rewriter_type.h:32
mcrl2::pbes_system::quantifier_one_point
@ quantifier_one_point
Definition pbes_rewriter_type.h:29
mcrl2::pbes_system::pfnf
@ pfnf
Definition pbes_rewriter_type.h:31
mcrl2::pbes_system::simplify
@ simplify
Definition pbes_rewriter_type.h:25
mcrl2::pbes_system::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
Definition pbes.cpp:52
mcrl2::pbes_system::is_universal_and
bool is_universal_and(const pbes_expression &t)
Test for a conjunction.
Definition pbes_expression.h:779
mcrl2::pbes_system::is_pbes_expression
bool is_pbes_expression(const atermpp::aterm &x)
Definition pbes_expression.h:84
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:723
mcrl2::pbes_system::true_
const pbes_expression & true_()
Definition pbes_expression.h:688
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:755
mcrl2::pbes_system::make_exists_
pbes_expression make_exists_(const data::variable_list &l, const pbes_expression &p)
Make an existential quantification. It checks for an empty variable list, which is not allowed.
Definition pbes_expression.h:942
mcrl2::pbes_system::is_not
bool is_not(const atermpp::aterm &x)
Definition pbes_expression.h:269
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation_list &x)
Definition pbes.cpp:33
mcrl2::pbes_system::pbes_format_internal_bes
const utilities::file_format & pbes_format_internal_bes()
Definition io.h:46
mcrl2::pbes_system::txt2pbes
void txt2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, bool normalize)
Definition txt2pbes.h:21
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression_list &x)
Definition pbes.cpp:29
mcrl2::pbes_system::pp
std::string pp(const pbes_system::or_ &x)
Definition pbes.cpp:41
mcrl2::pbes_system::optimized_not
void optimized_not(pbes_expression &result, const pbes_expression &p)
Make a negation.
Definition pbes_expression.h:955
mcrl2::pbes_system::make_and_
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:336
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:58
mcrl2::pbes_system::propositional_variable_instantiation_vector
std::vector< propositional_variable_instantiation > propositional_variable_instantiation_vector
\brief vector of propositional_variable_instantiations
Definition pbes_expression.h:192
mcrl2::pbes_system::pbesstategraph
void pbesstategraph(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const pbesstategraph_options &options)
Definition pbesstategraph.h:22
mcrl2::pbes_system::lpsbisim2pbes
void lpsbisim2pbes(const std::string &input_filename1, const std::string &input_filename2, const std::string &output_filename, const utilities::file_format &output_format, bisimulation_type type, bool normalize)
Definition lpsbisim2pbes.h:25
mcrl2::pbes_system::pbes_format_pgsolver
const utilities::file_format & pbes_format_pgsolver()
Definition io.h:48
mcrl2::pbes_system::fixpoint_symbol_vector
std::vector< fixpoint_symbol > fixpoint_symbol_vector
\brief vector of fixpoint_symbols
Definition fixpoint_symbol.h:81
mcrl2::pbes_system::make_not_
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:260
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable &x)
Definition pbes.cpp:45
mcrl2::pbes_system::propositional_variable_vector
std::vector< propositional_variable > propositional_variable_vector
\brief vector of propositional_variables
Definition propositional_variable.h:92
mcrl2::pbes_system::is_exists
bool is_exists(const atermpp::aterm &x)
Definition pbes_expression.h:649
mcrl2::pbes_system::free_variables
data::variable_list free_variables(const pbes_expression &x)
Definition pbes_expression.h:1067
mcrl2::pbes_system::swap
void swap(or_ &t1, or_ &t2)
\brief swap overload
Definition pbes_expression.h:440
mcrl2::pbes_system::operator==
bool operator==(const pbes_equation &x, const pbes_equation &y)
Definition pbes_equation.h:166
mcrl2::pbes_system::is_constant
bool is_constant(const pbes_expression &x)
Definition pbes_expression.h:1047
mcrl2::pbes_system::complps2pbes
void complps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename)
Definition complps2pbes.h:24
mcrl2::pbes_system::normalize_sorts
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
Definition pbes.cpp:48
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_instantiation &x)
Definition pbes.cpp:46
mcrl2::pbes_system::propositional_variable_instantiation_list
atermpp::term_list< propositional_variable_instantiation > propositional_variable_instantiation_list
\brief list of propositional_variable_instantiations
Definition pbes_expression.h:189
mcrl2::pbes_system::pbesinst_strategy
pbesinst_strategy
pbesinst transformation strategies
Definition pbesinst_strategy.h:24
mcrl2::pbes_system::pbesinst_finite_strategy
@ pbesinst_finite_strategy
Definition pbesinst_strategy.h:27
mcrl2::pbes_system::pbesinst_lazy_strategy
@ pbesinst_lazy_strategy
Definition pbesinst_strategy.h:25
mcrl2::pbes_system::pbesinst_alternative_lazy_strategy
@ pbesinst_alternative_lazy_strategy
Definition pbesinst_strategy.h:26
mcrl2::pbes_system::pbesrewr
void pbesrewr(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type)
Definition pbesrewr.h:31
mcrl2::pbes_system::is_or
bool is_or(const atermpp::aterm &x)
Definition pbes_expression.h:421
mcrl2::pbes_system::operator>>
std::istream & operator>>(std::istream &is, pbes_rewriter_type &t)
Stream operator for rewriter type.
Definition pbes_rewriter_type.h:141
mcrl2::pbes_system::quantifier_variables
const data::variable_list & quantifier_variables(const pbes_expression &x)
Definition pbes_expression.h:1053
mcrl2::pbes_system::pp
std::string pp(const pbes_system::fixpoint_symbol &x)
Definition pbes.cpp:37
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:91
mcrl2::pbes_system::swap
void swap(imp &t1, imp &t2)
\brief swap overload
Definition pbes_expression.h:516
mcrl2::pbes_system::optimized_exists
void optimized_exists(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make an existential quantification If l is empty, p is returned.
Definition pbes_expression.h:1024
mcrl2::pbes_system::swap
void swap(and_ &t1, and_ &t2)
\brief swap overload
Definition pbes_expression.h:364
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_equation_vector &x)
Definition pbes.cpp:28
mcrl2::pbes_system::pbesinfo
void pbesinfo(const std::string &input_filename, const std::string &input_file_message, const utilities::file_format &file_format, bool opt_full)
Definition pbesinfo.h:22
mcrl2::pbes_system::find_function_symbols
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
Definition pbes.cpp:57
mcrl2::pbes_system::pbes_equation_vector
std::vector< pbes_equation > pbes_equation_vector
\brief vector of pbes_equations
Definition pbes_equation.h:143
mcrl2::pbes_system::has_propositional_variables
bool has_propositional_variables(const pbes_expression &x)
mcrl2::pbes_system::pbespareqelm
void pbespareqelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool ignore_initial_state)
Definition pbespareqelm.h:22
mcrl2::pbes_system::pbespp
void pbespp(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, core::print_format_type format, bool use_pfnf_printer)
Definition pbespp.h:22
mcrl2::pbes_system::swap
void swap(exists &t1, exists &t2)
\brief swap overload
Definition pbes_expression.h:668
mcrl2::pbes_system::is_forall
bool is_forall(const atermpp::aterm &x)
Definition pbes_expression.h:573
mcrl2::pbes_system::pbesparelm
void pbesparelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format)
Definition pbesparelm.h:22
mcrl2::pbes_system::make_propositional_variable_instantiation
void make_propositional_variable_instantiation(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:183
mcrl2::pbes_system::parse_pbesinst_strategy
pbesinst_strategy parse_pbesinst_strategy(const std::string &s)
Parse a pbesinst transformation strategy.
Definition pbesinst_strategy.h:32
mcrl2::pbes_system::make_or_
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:412
mcrl2::pbes_system::pbes_to_aterm
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
Definition io.cpp:328
mcrl2::pbes_system::is_universal_not
bool is_universal_not(const pbes_expression &t)
Test for a conjunction.
Definition pbes_expression.h:771
mcrl2::pbes_system::print_pbesinst_strategy
std::string print_pbesinst_strategy(const pbesinst_strategy strategy)
Returns a string representation of a pbesinst transformation strategy.
Definition pbesinst_strategy.h:70
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes_expression &x)
Definition pbes.cpp:44
mcrl2::pbes_system::operator>>
std::istream & operator>>(std::istream &is, bisimulation_type &t)
Definition bisimulation_type.h:80
mcrl2::pbes_system::operator==
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
Definition pbes.h:325
mcrl2::pbes_system::is_well_typed
bool is_well_typed(const pbes_equation &eqn)
Definition pbes.cpp:77
mcrl2::pbes_system::pbes_file_formats
const std::vector< utilities::file_format > & pbes_file_formats()
Definition io.cpp:26
mcrl2::pbes_system::find_free_variables
std::set< data::variable > find_free_variables(const pbes_system::pbes_expression &x)
Definition pbes.cpp:55
mcrl2::pbes_system::save_bes_pgsolver
void save_bes_pgsolver(const pbes &bes, std::ostream &stream, bool maxpg)
Definition pgsolver.cpp:142
mcrl2::pbes_system::translate_user_notation
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
Definition pbes.cpp:51
mcrl2::pbes_system::pbes_expression_vector
std::vector< pbes_expression > pbes_expression_vector
\brief vector of pbes_expressions
Definition pbes_expression.h:69
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:739
mcrl2::pbes_system::is_false
bool is_false(const pbes_expression &t)
Test for the value false.
Definition pbes_expression.h:715
mcrl2::pbes_system::optimized_forall
void optimized_forall(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make a universal quantification If l is empty, p is returned.
Definition pbes_expression.h:996
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:747
mcrl2::pbes_system::print_pbes_rewriter_type
std::string print_pbes_rewriter_type(const pbes_rewriter_type type)
Prints a pbes rewriter type.
Definition pbes_rewriter_type.h:81
mcrl2::pbes_system::pp
std::string pp(const pbes_system::pbes &x)
Definition pbes.cpp:42
mcrl2::pbes_system::optimized_or
void optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
Definition pbes_expression.h:975
mcrl2::pbes_system::print_absinthe_strategy
std::string print_absinthe_strategy(const absinthe_strategy strategy)
Prints an absinthe strategy.
Definition absinthe_strategy.h:49
mcrl2::pbes_system::pbes_equation_list
atermpp::term_list< pbes_equation > pbes_equation_list
\brief list of pbes_equations
Definition pbes_equation.h:140
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:731
mcrl2::pbes_system::pbes_equation_to_aterm
atermpp::aterm pbes_equation_to_aterm(const pbes_equation &eqn)
Conversion to atermaPpl.
Definition pbes_equation.h:182
mcrl2::pbes_system::save_pbes
void save_pbes(const pbes &pbes, std::ostream &stream, utilities::file_format format)
Save a PBES in the format specified.
Definition io.cpp:49
mcrl2::pbes_system::make_forall_
pbes_expression make_forall_(const data::variable_list &l, const pbes_expression &p)
Make a universal quantification. It checks for an empty variable list, which is not allowed.
Definition pbes_expression.h:927
mcrl2::pbes_system::search_variable
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
Definition pbes.cpp:60
mcrl2::pbes_system::pp
std::string pp(const pbes_system::imp &x)
Definition pbes.cpp:39
mcrl2::pbes_system::print_bisimulation_type
std::string print_bisimulation_type(const bisimulation_type t)
Returns a description of a bisimulation type.
Definition bisimulation_type.h:45
mcrl2::pbes_system::swap
void swap(forall &t1, forall &t2)
\brief swap overload
Definition pbes_expression.h:592
mcrl2::pbes_system::swap
void swap(pbes_expression &t1, pbes_expression &t2)
\brief swap overload
Definition pbes_expression.h:112
mcrl2::pbes_system::find_all_variables
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
Definition pbes.cpp:53
mcrl2::pbes_system::pp
std::string pp(const pbes_system::exists &x)
Definition pbes.cpp:36
mcrl2::pbes_system::propositional_variable_list
atermpp::term_list< propositional_variable > propositional_variable_list
\brief list of propositional_variables
Definition propositional_variable.h:89
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:314
mcrl2::pbes_system::swap
void swap(pbes_equation &t1, pbes_equation &t2)
\brief swap overload
Definition pbes_equation.h:159
mcrl2::pbes_system::bisimulation_type
bisimulation_type
An enumerated type for the available bisimulation types.
Definition bisimulation_type.h:24
mcrl2::pbes_system::weak_bisim
@ weak_bisim
Definition bisimulation_type.h:26
mcrl2::pbes_system::branching_sim
@ branching_sim
Definition bisimulation_type.h:28
mcrl2::pbes_system::branching_bisim
@ branching_bisim
Definition bisimulation_type.h:27
mcrl2::pbes_system::strong_bisim
@ strong_bisim
Definition bisimulation_type.h:25
mcrl2::pbes_system::swap
void swap(not_ &t1, not_ &t2)
\brief swap overload
Definition pbes_expression.h:288
mcrl2::pbes_system::pbes_format_internal
const utilities::file_format & pbes_format_internal()
Definition io.h:42
mcrl2::pbes_system::pbesconstelm
void pbesconstelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions, bool remove_redundant_equations, bool check_quantifiers)
Definition pbesconstelm.h:22
mcrl2::pbes_system::make_exists
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:640
mcrl2::pbes_system::find_identifiers
std::set< core::identifier_string > find_identifiers(const pbes_system::pbes_expression &x)
Definition pbes.cpp:59
mcrl2::pbes_system::is_propositional_variable_instantiation
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
Definition pbes_expression.h:198
mcrl2::pbes_system::pbes_format_text
const utilities::file_format & pbes_format_text()
Definition io.h:44
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:82
mcrl2::pbes_system::swap
void swap(fixpoint_symbol &t1, fixpoint_symbol &t2)
\brief swap overload
Definition fixpoint_symbol.h:97
mcrl2::pbes_system::parse_absinthe_strategy
absinthe_strategy parse_absinthe_strategy(const std::string &strategy)
Parses an absinthe strategy.
Definition absinthe_strategy.h:31
mcrl2::pbes_system::is_and
bool is_and(const atermpp::aterm &x)
Definition pbes_expression.h:345
mcrl2::pbes_system::description
std::string description(const pbes_rewriter_type type)
Returns a description of a pbes rewriter.
Definition pbes_rewriter_type.h:110
mcrl2::pbes_system::optimized_and
void optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
Definition pbes_expression.h:965
mcrl2::pbes_system::description
std::string description(const pbesinst_strategy strategy)
Returns a string representation of a pbesinst transformation strategy.
Definition pbesinst_strategy.h:96
mcrl2::pbes_system::translate_user_notation
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:50
mcrl2::pbes_system::description
std::string description(const bisimulation_type t)
Returns a description of a bisimulation type.
Definition bisimulation_type.h:63
mcrl2::pbes_system::is_imp
bool is_imp(const atermpp::aterm &x)
Definition pbes_expression.h:497
mcrl2::pbes_system::optimized_imp
void optimized_imp(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make an implication.
Definition pbes_expression.h:985
mcrl2::pbes_system::make_imp
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:488
mcrl2::pbes_system::pbesabsinthe
void pbesabsinthe(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &abstraction_file, absinthe_strategy strategy, bool print_used_function_symbols, bool enable_logging)
Definition pbesabsinthe.h:23
mcrl2::pbes_system::pp
std::string pp(const pbes_system::not_ &x)
Definition pbes.cpp:40
mcrl2::pbes_system::parse_bisimulation_type
bisimulation_type parse_bisimulation_type(const std::string &type)
Returns the string corresponding to a bisimulation type.
Definition bisimulation_type.h:33
mcrl2::pbes_system::is_true
bool is_true(const pbes_expression &t)
Test for the value true.
Definition pbes_expression.h:707
mcrl2::pbes_system::pp
std::string pp(const pbes_system::propositional_variable_list &x)
Definition pbes.cpp:31
mcrl2::pbes_system::false_
const pbes_expression & false_()
Definition pbes_expression.h:697
mcrl2::pbes_system::make_forall
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
Definition pbes_expression.h:564
mcrl2::pbes_system::absinthe_strategy
absinthe_strategy
The approximation strategies of the absinthe tool.
Definition absinthe_strategy.h:24
mcrl2::pbes_system::absinthe_over
@ absinthe_over
Definition absinthe_strategy.h:25
mcrl2::pbes_system::absinthe_under
@ absinthe_under
Definition absinthe_strategy.h:26
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition shared_mutex.h:25
mcrl2::core::builder
expression builder that visits all sub expressions
Definition builder.h:42
mcrl2::core::detail::default_values
Definition default_values.h:1603
mcrl2::core::detail::default_values::PBESForall
static const atermpp::aterm PBESForall
Definition default_values.h:1737
mcrl2::core::detail::default_values::PBExpr
static const atermpp::aterm PBExpr
Definition default_values.h:1775
mcrl2::core::detail::default_values::PBESOr
static const atermpp::aterm PBESOr
Definition default_values.h:1735
mcrl2::core::detail::default_values::PBESExists
static const atermpp::aterm PBESExists
Definition default_values.h:1738
mcrl2::core::detail::default_values::PBESImp
static const atermpp::aterm PBESImp
Definition default_values.h:1736
mcrl2::core::detail::default_values::PBESNot
static const atermpp::aterm PBESNot
Definition default_values.h:1733
mcrl2::core::detail::default_values::FixPoint
static const atermpp::aterm FixPoint
Definition default_values.h:1774
mcrl2::core::detail::default_values::PropVarInst
static const atermpp::aterm PropVarInst
Definition default_values.h:1739
mcrl2::core::detail::default_values::PropVarDecl
static const atermpp::aterm PropVarDecl
Definition default_values.h:1730
mcrl2::core::detail::default_values::PBESAnd
static const atermpp::aterm PBESAnd
Definition default_values.h:1734
mcrl2::core::detail::function_symbols
Definition function_symbols.h:1383
mcrl2::core::detail::function_symbols::PropVarDecl
static const atermpp::function_symbol PropVarDecl
Definition function_symbols.h:1510
mcrl2::core::detail::function_symbols::PBESForall
static const atermpp::function_symbol PBESForall
Definition function_symbols.h:1517
mcrl2::core::detail::function_symbols::PBESNot
static const atermpp::function_symbol PBESNot
Definition function_symbols.h:1513
mcrl2::core::detail::function_symbols::PBESImp
static const atermpp::function_symbol PBESImp
Definition function_symbols.h:1516
mcrl2::core::detail::function_symbols::PBESAnd
static const atermpp::function_symbol PBESAnd
Definition function_symbols.h:1514
mcrl2::core::detail::function_symbols::Nu
static const atermpp::function_symbol Nu
Definition function_symbols.h:1509
mcrl2::core::detail::function_symbols::PropVarInst
static const atermpp::function_symbol PropVarInst
Definition function_symbols.h:1519
mcrl2::core::detail::function_symbols::Mu
static const atermpp::function_symbol Mu
Definition function_symbols.h:1508
mcrl2::core::detail::function_symbols::PBESExists
static const atermpp::function_symbol PBESExists
Definition function_symbols.h:1518
mcrl2::core::detail::function_symbols::PBESOr
static const atermpp::function_symbol PBESOr
Definition function_symbols.h:1515
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_false
static bool is_false(const term_type &t)
Test for the value false.
Definition pbes_expression.h:1290
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_or_
static void make_or_(term_type &result, const term_type &p, const term_type &q)
Make a disjunction.
Definition pbes_expression.h:1180
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_imp
static bool is_imp(const term_type &t)
Test for an implication.
Definition pbes_expression.h:1326
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_exists
static void make_exists(term_type &result, const variable_sequence_type &l, const term_type &p)
Make an existential quantification.
Definition pbes_expression.h:1267
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_data
static bool is_data(const term_type &t)
Test for data term.
Definition pbes_expression.h:1353
mcrl2::core::term_traits< pbes_system::pbes_expression >::forall
static term_type forall(const variable_sequence_type &l, const term_type &p)
Make a universal quantification.
Definition pbes_expression.h:1224
mcrl2::core::term_traits< pbes_system::pbes_expression >::pp
static std::string pp(const term_type &t)
Pretty print function.
Definition pbes_expression.h:1450
mcrl2::core::term_traits< pbes_system::pbes_expression >::true_
static term_type true_()
Make the value true.
Definition pbes_expression.h:1114
mcrl2::core::term_traits< pbes_system::pbes_expression >::exists
static term_type exists(const variable_sequence_type &l, const term_type &p)
Make an existential quantification.
Definition pbes_expression.h:1253
mcrl2::core::term_traits< pbes_system::pbes_expression >::or_
static term_type or_(const term_type &p, const term_type &q)
Make a disjunction.
Definition pbes_expression.h:1170
mcrl2::core::term_traits< pbes_system::pbes_expression >::param
static const data_term_sequence_type & param(const term_type &t)
Returns the parameter list of a propositional variable instantiation.
Definition pbes_expression.h:1422
mcrl2::core::term_traits< pbes_system::pbes_expression >::variable_type
data::variable variable_type
The variable type.
Definition pbes_expression.h:1097
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_not
static bool is_not(const term_type &t)
Test for a negation.
Definition pbes_expression.h:1299
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_imp
static void make_imp(term_type &result, const term_type &p, const term_type &q)
Make an implication.
Definition pbes_expression.h:1214
mcrl2::core::term_traits< pbes_system::pbes_expression >::join_and
static term_type join_and(FwdIt first, FwdIt last)
Definition pbes_expression.h:1194
mcrl2::core::term_traits< pbes_system::pbes_expression >::propositional_variable_decl_type
pbes_system::propositional_variable propositional_variable_decl_type
The propositional variable declaration type.
Definition pbes_expression.h:1103
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_and
static bool is_and(const term_type &t)
Test for a conjunction.
Definition pbes_expression.h:1308
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_variable
static bool is_variable(const term_type &t)
Test if a term is a variable.
Definition pbes_expression.h:1441
mcrl2::core::term_traits< pbes_system::pbes_expression >::term_type
pbes_system::pbes_expression term_type
The term type.
Definition pbes_expression.h:1088
mcrl2::core::term_traits< pbes_system::pbes_expression >::not_
static term_type not_(const term_type &p)
Make a negation.
Definition pbes_expression.h:1131
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_exists
static bool is_exists(const term_type &t)
Test for an existential quantification.
Definition pbes_expression.h:1344
mcrl2::core::term_traits< pbes_system::pbes_expression >::propositional_variable_type
pbes_system::propositional_variable_instantiation propositional_variable_type
The propositional variable instantiation type.
Definition pbes_expression.h:1106
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_and_
static void make_and_(term_type &result, const term_type &p, const term_type &q)
Make a conjunction.
Definition pbes_expression.h:1160
mcrl2::core::term_traits< pbes_system::pbes_expression >::false_
static term_type false_()
Make the value false.
Definition pbes_expression.h:1122
mcrl2::core::term_traits< pbes_system::pbes_expression >::left
static term_type left(const term_type &t)
Returns the left argument of a term of type and, or or imp.
Definition pbes_expression.h:1371
mcrl2::core::term_traits< pbes_system::pbes_expression >::name
static const string_type & name(const term_type &t)
Returns the name of a propositional variable instantiation.
Definition pbes_expression.h:1412
mcrl2::core::term_traits< pbes_system::pbes_expression >::right
static term_type right(const term_type &t)
Returns the right argument of a term of type and, or or imp.
Definition pbes_expression.h:1380
mcrl2::core::term_traits< pbes_system::pbes_expression >::data_term_type
data::data_expression data_term_type
The data term type.
Definition pbes_expression.h:1091
mcrl2::core::term_traits< pbes_system::pbes_expression >::string_type
core::identifier_string string_type
The string type.
Definition pbes_expression.h:1109
mcrl2::core::term_traits< pbes_system::pbes_expression >::and_
static term_type and_(const term_type &p, const term_type &q)
Make a conjunction.
Definition pbes_expression.h:1150
mcrl2::core::term_traits< pbes_system::pbes_expression >::var
static const variable_sequence_type & var(const term_type &t)
Returns the quantifier variables of a quantifier expression.
Definition pbes_expression.h:1398
mcrl2::core::term_traits< pbes_system::pbes_expression >::variable2term
static const term_type & variable2term(const variable_type &v)
Conversion from variable to term.
Definition pbes_expression.h:1432
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_forall
static void make_forall(term_type &result, const variable_sequence_type &l, const term_type &p)
Make a universal quantification.
Definition pbes_expression.h:1238
mcrl2::core::term_traits< pbes_system::pbes_expression >::make_not_
static void make_not_(term_type &result, const term_type &p)
Make a negation.
Definition pbes_expression.h:1140
mcrl2::core::term_traits< pbes_system::pbes_expression >::not_arg
static const term_type & not_arg(const term_type &t)
Returns the argument of a term of type not.
Definition pbes_expression.h:1388
mcrl2::core::term_traits< pbes_system::pbes_expression >::variable_sequence_type
data::variable_list variable_sequence_type
The variable sequence type.
Definition pbes_expression.h:1100
mcrl2::core::term_traits< pbes_system::pbes_expression >::imp
static term_type imp(const term_type &p, const term_type &q)
Make an implication.
Definition pbes_expression.h:1204
mcrl2::core::term_traits< pbes_system::pbes_expression >::data_term_sequence_type
data::data_expression_list data_term_sequence_type
The data term sequence type.
Definition pbes_expression.h:1094
mcrl2::core::term_traits< pbes_system::pbes_expression >::join_or
static term_type join_or(FwdIt first, FwdIt last)
Definition pbes_expression.h:1187
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_forall
static bool is_forall(const term_type &t)
Test for an universal quantification.
Definition pbes_expression.h:1335
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_prop_var
static bool is_prop_var(const term_type &t)
Test for propositional variable instantiation.
Definition pbes_expression.h:1362
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_true
static bool is_true(const term_type &t)
Test for the value true.
Definition pbes_expression.h:1281
mcrl2::core::term_traits< pbes_system::pbes_expression >::is_or
static bool is_or(const term_type &t)
Test for a disjunction.
Definition pbes_expression.h:1317
mcrl2::core::term_traits
Contains type information for terms.
Definition term_traits.h:24
mcrl2::pbes_system::add_data_expressions
Definition builder.h:208
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:271
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:280
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:253
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:298
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:262
mcrl2::pbes_system::add_data_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:215
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:235
mcrl2::pbes_system::add_data_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:224
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:289
mcrl2::pbes_system::add_data_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:244
mcrl2::pbes_system::add_data_expressions::super
Builder< Derived > super
Definition builder.h:209
mcrl2::pbes_system::add_pbes_expressions
Definition builder.h:520
mcrl2::pbes_system::add_pbes_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:536
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:609
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:591
mcrl2::pbes_system::add_pbes_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:527
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:555
mcrl2::pbes_system::add_pbes_expressions::super
Builder< Derived > super
Definition builder.h:521
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:544
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:564
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:582
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:600
mcrl2::pbes_system::add_pbes_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:573
mcrl2::pbes_system::add_sort_expressions
Definition builder.h:45
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:139
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:103
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:112
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:130
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:85
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:53
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:121
mcrl2::pbes_system::add_sort_expressions::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:61
mcrl2::pbes_system::add_sort_expressions::update
void update(pbes_system::pbes &x)
Definition builder.h:73
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:148
mcrl2::pbes_system::add_sort_expressions::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:94
mcrl2::pbes_system::add_sort_expressions::super
Builder< Derived > super
Definition builder.h:46
mcrl2::pbes_system::add_variables
Definition builder.h:357
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::imp &x)
Definition builder.h:433
mcrl2::pbes_system::add_variables::update
void update(pbes_system::pbes &x)
Definition builder.h:385
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::pbes_expression &x)
Definition builder.h:460
mcrl2::pbes_system::add_variables::super
Builder< Derived > super
Definition builder.h:358
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::forall &x)
Definition builder.h:442
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::propositional_variable &x)
Definition builder.h:365
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::not_ &x)
Definition builder.h:406
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::and_ &x)
Definition builder.h:415
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::or_ &x)
Definition builder.h:424
mcrl2::pbes_system::add_variables::update
void update(pbes_system::pbes_equation &x)
Definition builder.h:373
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::exists &x)
Definition builder.h:451
mcrl2::pbes_system::add_variables::apply
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:397
mcrl2::pbes_system::data_expression_builder
\brief Builder class
Definition builder.h:350
mcrl2::pbes_system::detail::pbes_abstract_builder
Visitor that implements the pbes-abstract algorithm.
Definition abstract.h:30
mcrl2::pbes_system::detail::pbes_abstract_builder::is_bound
bool is_bound(const data::variable &v) const
Returns true if the m_quantifier_stack contains a given data variable.
Definition abstract.h:44
mcrl2::pbes_system::detail::pbes_abstract_builder::m_value
const data::data_expression m_value
Definition abstract.h:36
mcrl2::pbes_system::detail::pbes_abstract_builder::pbes_abstract_builder
pbes_abstract_builder(const std::vector< data::variable > &selected_variables, bool value_true)
Definition abstract.h:38
mcrl2::pbes_system::detail::pbes_abstract_builder::super
pbes_expression_builder< pbes_abstract_builder > super
Definition abstract.h:31
mcrl2::pbes_system::detail::pbes_abstract_builder::apply
void apply(T &result, const data::data_expression &d)
Visit data_expression node.
Definition abstract.h:73
mcrl2::pbes_system::detail::pbes_abstract_builder::apply
void apply(T &result, const exists &x)
Visit exists node.
Definition abstract.h:105
mcrl2::pbes_system::detail::pbes_abstract_builder::apply
void apply(T &result, const forall &x)
Visit forall node.
Definition abstract.h:94
mcrl2::pbes_system::detail::pbes_abstract_builder::m_quantifier_stack
std::vector< data::variable_list > m_quantifier_stack
Definition abstract.h:34
mcrl2::pbes_system::detail::pbes_abstract_builder::m_selected_variables
const std::vector< data::variable > m_selected_variables
Definition abstract.h:35
mcrl2::pbes_system::detail::pbes_abstract_builder::pop_variables
void pop_variables()
Removes the last added sequence of variables from the quantifier stack.
Definition abstract.h:66
mcrl2::pbes_system::detail::pbes_abstract_builder::push_variables
void push_variables(const data::variable_list &variables)
Adds a sequence of variables to the quantifier stack.
Definition abstract.h:60
mcrl2::pbes_system::pbes_expression_builder_base
Builder class.
Definition builder.h:27
mcrl2::pbes_system::pbes_expression_builder_base::apply
void apply(T &result, const data::data_expression &x)
Definition builder.h:35
mcrl2::pbes_system::pbes_expression_builder_base::super
core::builder< Derived > super
Definition builder.h:28
mcrl2::pbes_system::pbes_expression_builder
\brief Builder class
Definition builder.h:661
mcrl2::pbes_system::pbesstategraph_options
Definition pbesstategraph_options.h:23
mcrl2::pbes_system::pbesstategraph_options::timing_enabled
bool timing_enabled() const
Definition pbesstategraph_options.h:48
mcrl2::pbes_system::pbesstategraph_options::timer
utilities::execution_timer * timer
Definition pbesstategraph_options.h:33
mcrl2::pbes_system::pbesstategraph_options::print_influence_graph
bool print_influence_graph
Definition pbesstategraph_options.h:27
mcrl2::pbes_system::pbesstategraph_options::cache_marking_updates
bool cache_marking_updates
Definition pbesstategraph_options.h:28
mcrl2::pbes_system::pbesstategraph_options::use_alternative_gcfp_consistency
bool use_alternative_gcfp_consistency
Definition pbesstategraph_options.h:32
mcrl2::pbes_system::pbesstategraph_options::use_alternative_gcfp_relation
bool use_alternative_gcfp_relation
Definition pbesstategraph_options.h:31
mcrl2::pbes_system::pbesstategraph_options::simplify
bool simplify
Definition pbesstategraph_options.h:25
mcrl2::pbes_system::pbesstategraph_options::pbesstategraph_options
pbesstategraph_options()
Definition pbesstategraph_options.h:35
mcrl2::pbes_system::pbesstategraph_options::use_alternative_lcfp_criterion
bool use_alternative_lcfp_criterion
Definition pbesstategraph_options.h:30
mcrl2::pbes_system::pbesstategraph_options::marking_algorithm
int marking_algorithm
Definition pbesstategraph_options.h:29
mcrl2::pbes_system::pbesstategraph_options::use_global_variant
bool use_global_variant
Definition pbesstategraph_options.h:26
mcrl2::pbes_system::sort_expression_builder
\brief Builder class
Definition builder.h:200
mcrl2::pbes_system::variable_builder
\brief Builder class
Definition builder.h:512
mcrl2::utilities::execution_timer::timing
Pair of start and finish times.
Definition execution_timer.h:52
mcrl2::utilities::execution_timer::timing::finish
std::chrono::steady_clock::time_point finish
Definition execution_timer.h:54
mcrl2::utilities::execution_timer::timing::finish_user
clock_t finish_user
Definition execution_timer.h:57
mcrl2::utilities::execution_timer::timing::timing
timing()
Definition execution_timer.h:59
mcrl2::utilities::execution_timer::timing::start
std::chrono::steady_clock::time_point start
Definition execution_timer.h:53
mcrl2::utilities::execution_timer::timing::start_user
clock_t start_user
Definition execution_timer.h:56
std::hash< atermpp::aterm >::operator()
std::size_t operator()(const atermpp::aterm &t) const
Definition aterm.h:483
std::hash< atermpp::detail::reference_aterm< T > >::operator()
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
Definition aterm_container.h:495
std::hash< mcrl2::pbes_system::pbes_expression >::operator()
std::size_t operator()(const mcrl2::pbes_system::pbes_expression &x) const
Definition pbes_expression.h:1466
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:1475