mCRL2
Loading...
Searching...
No Matches
traverser.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp, 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/process/traverser.h
10/// \brief add your file description here.
11
12// To avoid circular inclusion problems
13#ifndef MCRL2_PROCESS_SPECIFICATION_H
14#include "mcrl2/process/process_specification.h"
15#endif
16
17#ifndef MCRL2_PROCESS_TRAVERSER_H
18#define MCRL2_PROCESS_TRAVERSER_H
19
20#include "mcrl2/data/traverser.h"
21
22#include "mcrl2/process/untyped_multi_action.h"
23// #include "mcrl2/process/timed_multi_action.h"
24
25namespace mcrl2::process
26{
27
28/// \brief Base class for action_formula_traverser.
29template <typename Derived>
30struct process_traverser_base: public core::traverser<Derived>
31{
32 using super = core::traverser<Derived>;
33 using super::apply;
34 using super::enter;
35 using super::leave;
36
38 {
39 static_cast<Derived&>(*this).enter(x);
40 // skip
41 static_cast<Derived&>(*this).leave(x);
42 }
43};
44
45//--- start generated add_traverser_sort_expressions code ---//
46template <template <class> class Traverser, class Derived>
47struct add_traverser_sort_expressions: public Traverser<Derived>
48{
49 using super = Traverser<Derived>;
50 using super::enter;
51 using super::leave;
52 using super::apply;
53
54 void apply(const process::action_label& x)
55 {
56 static_cast<Derived&>(*this).enter(x);
57 static_cast<Derived&>(*this).apply(x.sorts());
58 static_cast<Derived&>(*this).leave(x);
59 }
60
62 {
63 static_cast<Derived&>(*this).enter(x);
64 static_cast<Derived&>(*this).apply(x.action_labels());
65 static_cast<Derived&>(*this).apply(x.global_variables());
66 static_cast<Derived&>(*this).apply(x.equations());
67 static_cast<Derived&>(*this).apply(x.init());
68 static_cast<Derived&>(*this).leave(x);
69 }
70
72 {
73 static_cast<Derived&>(*this).enter(x);
74 static_cast<Derived&>(*this).apply(x.variables());
75 static_cast<Derived&>(*this).leave(x);
76 }
77
79 {
80 static_cast<Derived&>(*this).enter(x);
81 static_cast<Derived&>(*this).apply(x.identifier());
82 static_cast<Derived&>(*this).apply(x.formal_parameters());
83 static_cast<Derived&>(*this).apply(x.expression());
84 static_cast<Derived&>(*this).leave(x);
85 }
86
88 {
89 static_cast<Derived&>(*this).enter(x);
90 static_cast<Derived&>(*this).apply(x.actions());
91 static_cast<Derived&>(*this).leave(x);
92 }
93
94 void apply(const process::action& x)
95 {
96 static_cast<Derived&>(*this).enter(x);
97 static_cast<Derived&>(*this).apply(x.label());
98 static_cast<Derived&>(*this).apply(x.arguments());
99 static_cast<Derived&>(*this).leave(x);
100 }
101
103 {
104 static_cast<Derived&>(*this).enter(x);
105 static_cast<Derived&>(*this).apply(x.identifier());
106 static_cast<Derived&>(*this).apply(x.actual_parameters());
107 static_cast<Derived&>(*this).leave(x);
108 }
109
111 {
112 static_cast<Derived&>(*this).enter(x);
113 static_cast<Derived&>(*this).apply(x.identifier());
114 static_cast<Derived&>(*this).apply(x.assignments());
115 static_cast<Derived&>(*this).leave(x);
116 }
117
118 void apply(const process::delta& x)
119 {
120 static_cast<Derived&>(*this).enter(x);
121 // skip
122 static_cast<Derived&>(*this).leave(x);
123 }
124
125 void apply(const process::tau& x)
126 {
127 static_cast<Derived&>(*this).enter(x);
128 // skip
129 static_cast<Derived&>(*this).leave(x);
130 }
131
132 void apply(const process::sum& x)
133 {
134 static_cast<Derived&>(*this).enter(x);
135 static_cast<Derived&>(*this).apply(x.variables());
136 static_cast<Derived&>(*this).apply(x.operand());
137 static_cast<Derived&>(*this).leave(x);
138 }
139
140 void apply(const process::block& x)
141 {
142 static_cast<Derived&>(*this).enter(x);
143 static_cast<Derived&>(*this).apply(x.operand());
144 static_cast<Derived&>(*this).leave(x);
145 }
146
147 void apply(const process::hide& x)
148 {
149 static_cast<Derived&>(*this).enter(x);
150 static_cast<Derived&>(*this).apply(x.operand());
151 static_cast<Derived&>(*this).leave(x);
152 }
153
154 void apply(const process::rename& x)
155 {
156 static_cast<Derived&>(*this).enter(x);
157 static_cast<Derived&>(*this).apply(x.operand());
158 static_cast<Derived&>(*this).leave(x);
159 }
160
161 void apply(const process::comm& x)
162 {
163 static_cast<Derived&>(*this).enter(x);
164 static_cast<Derived&>(*this).apply(x.operand());
165 static_cast<Derived&>(*this).leave(x);
166 }
167
168 void apply(const process::allow& x)
169 {
170 static_cast<Derived&>(*this).enter(x);
171 static_cast<Derived&>(*this).apply(x.operand());
172 static_cast<Derived&>(*this).leave(x);
173 }
174
175 void apply(const process::sync& x)
176 {
177 static_cast<Derived&>(*this).enter(x);
178 static_cast<Derived&>(*this).apply(x.left());
179 static_cast<Derived&>(*this).apply(x.right());
180 static_cast<Derived&>(*this).leave(x);
181 }
182
183 void apply(const process::at& x)
184 {
185 static_cast<Derived&>(*this).enter(x);
186 static_cast<Derived&>(*this).apply(x.operand());
187 static_cast<Derived&>(*this).apply(x.time_stamp());
188 static_cast<Derived&>(*this).leave(x);
189 }
190
191 void apply(const process::seq& x)
192 {
193 static_cast<Derived&>(*this).enter(x);
194 static_cast<Derived&>(*this).apply(x.left());
195 static_cast<Derived&>(*this).apply(x.right());
196 static_cast<Derived&>(*this).leave(x);
197 }
198
199 void apply(const process::if_then& x)
200 {
201 static_cast<Derived&>(*this).enter(x);
202 static_cast<Derived&>(*this).apply(x.condition());
203 static_cast<Derived&>(*this).apply(x.then_case());
204 static_cast<Derived&>(*this).leave(x);
205 }
206
207 void apply(const process::if_then_else& x)
208 {
209 static_cast<Derived&>(*this).enter(x);
210 static_cast<Derived&>(*this).apply(x.condition());
211 static_cast<Derived&>(*this).apply(x.then_case());
212 static_cast<Derived&>(*this).apply(x.else_case());
213 static_cast<Derived&>(*this).leave(x);
214 }
215
216 void apply(const process::bounded_init& x)
217 {
218 static_cast<Derived&>(*this).enter(x);
219 static_cast<Derived&>(*this).apply(x.left());
220 static_cast<Derived&>(*this).apply(x.right());
221 static_cast<Derived&>(*this).leave(x);
222 }
223
224 void apply(const process::merge& x)
225 {
226 static_cast<Derived&>(*this).enter(x);
227 static_cast<Derived&>(*this).apply(x.left());
228 static_cast<Derived&>(*this).apply(x.right());
229 static_cast<Derived&>(*this).leave(x);
230 }
231
232 void apply(const process::left_merge& x)
233 {
234 static_cast<Derived&>(*this).enter(x);
235 static_cast<Derived&>(*this).apply(x.left());
236 static_cast<Derived&>(*this).apply(x.right());
237 static_cast<Derived&>(*this).leave(x);
238 }
239
240 void apply(const process::choice& x)
241 {
242 static_cast<Derived&>(*this).enter(x);
243 static_cast<Derived&>(*this).apply(x.left());
244 static_cast<Derived&>(*this).apply(x.right());
245 static_cast<Derived&>(*this).leave(x);
246 }
247
249 {
250 static_cast<Derived&>(*this).enter(x);
251 static_cast<Derived&>(*this).apply(x.variables());
252 static_cast<Derived&>(*this).apply(x.distribution());
253 static_cast<Derived&>(*this).apply(x.operand());
254 static_cast<Derived&>(*this).leave(x);
255 }
256
258 {
259 static_cast<Derived&>(*this).enter(x);
260 static_cast<Derived&>(*this).apply(x.assignments());
261 static_cast<Derived&>(*this).leave(x);
262 }
263
265 {
266 static_cast<Derived&>(*this).enter(x);
268 {
269 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
270 }
271 else if (process::is_action(x))
272 {
273 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
274 }
276 {
277 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
278 }
280 {
281 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
282 }
283 else if (process::is_delta(x))
284 {
285 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
286 }
287 else if (process::is_tau(x))
288 {
289 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
290 }
291 else if (process::is_sum(x))
292 {
293 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
294 }
295 else if (process::is_block(x))
296 {
297 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
298 }
299 else if (process::is_hide(x))
300 {
301 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
302 }
303 else if (process::is_rename(x))
304 {
305 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
306 }
307 else if (process::is_comm(x))
308 {
309 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
310 }
311 else if (process::is_allow(x))
312 {
313 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
314 }
315 else if (process::is_sync(x))
316 {
317 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
318 }
319 else if (process::is_at(x))
320 {
321 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
322 }
323 else if (process::is_seq(x))
324 {
325 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
326 }
327 else if (process::is_if_then(x))
328 {
329 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
330 }
332 {
333 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
334 }
336 {
337 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
338 }
339 else if (process::is_merge(x))
340 {
341 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
342 }
343 else if (process::is_left_merge(x))
344 {
345 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
346 }
347 else if (process::is_choice(x))
348 {
349 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
350 }
352 {
353 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
354 }
356 {
357 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
358 }
359 static_cast<Derived&>(*this).leave(x);
360 }
361
362};
363
364/// \\brief Traverser class
365template <typename Derived>
367{
368};
369//--- end generated add_traverser_sort_expressions code ---//
370
371//--- start generated add_traverser_data_expressions code ---//
372template <template <class> class Traverser, class Derived>
373struct add_traverser_data_expressions: public Traverser<Derived>
374{
375 using super = Traverser<Derived>;
376 using super::enter;
377 using super::leave;
378 using super::apply;
379
381 {
382 static_cast<Derived&>(*this).enter(x);
383 static_cast<Derived&>(*this).apply(x.equations());
384 static_cast<Derived&>(*this).apply(x.init());
385 static_cast<Derived&>(*this).leave(x);
386 }
387
389 {
390 static_cast<Derived&>(*this).enter(x);
391 static_cast<Derived&>(*this).apply(x.expression());
392 static_cast<Derived&>(*this).leave(x);
393 }
394
396 {
397 static_cast<Derived&>(*this).enter(x);
398 static_cast<Derived&>(*this).apply(x.actions());
399 static_cast<Derived&>(*this).leave(x);
400 }
401
402 void apply(const process::action& x)
403 {
404 static_cast<Derived&>(*this).enter(x);
405 static_cast<Derived&>(*this).apply(x.arguments());
406 static_cast<Derived&>(*this).leave(x);
407 }
408
410 {
411 static_cast<Derived&>(*this).enter(x);
412 static_cast<Derived&>(*this).apply(x.actual_parameters());
413 static_cast<Derived&>(*this).leave(x);
414 }
415
417 {
418 static_cast<Derived&>(*this).enter(x);
419 static_cast<Derived&>(*this).apply(x.assignments());
420 static_cast<Derived&>(*this).leave(x);
421 }
422
423 void apply(const process::delta& x)
424 {
425 static_cast<Derived&>(*this).enter(x);
426 // skip
427 static_cast<Derived&>(*this).leave(x);
428 }
429
430 void apply(const process::tau& x)
431 {
432 static_cast<Derived&>(*this).enter(x);
433 // skip
434 static_cast<Derived&>(*this).leave(x);
435 }
436
437 void apply(const process::sum& x)
438 {
439 static_cast<Derived&>(*this).enter(x);
440 static_cast<Derived&>(*this).apply(x.operand());
441 static_cast<Derived&>(*this).leave(x);
442 }
443
444 void apply(const process::block& x)
445 {
446 static_cast<Derived&>(*this).enter(x);
447 static_cast<Derived&>(*this).apply(x.operand());
448 static_cast<Derived&>(*this).leave(x);
449 }
450
451 void apply(const process::hide& x)
452 {
453 static_cast<Derived&>(*this).enter(x);
454 static_cast<Derived&>(*this).apply(x.operand());
455 static_cast<Derived&>(*this).leave(x);
456 }
457
458 void apply(const process::rename& x)
459 {
460 static_cast<Derived&>(*this).enter(x);
461 static_cast<Derived&>(*this).apply(x.operand());
462 static_cast<Derived&>(*this).leave(x);
463 }
464
465 void apply(const process::comm& x)
466 {
467 static_cast<Derived&>(*this).enter(x);
468 static_cast<Derived&>(*this).apply(x.operand());
469 static_cast<Derived&>(*this).leave(x);
470 }
471
472 void apply(const process::allow& x)
473 {
474 static_cast<Derived&>(*this).enter(x);
475 static_cast<Derived&>(*this).apply(x.operand());
476 static_cast<Derived&>(*this).leave(x);
477 }
478
479 void apply(const process::sync& x)
480 {
481 static_cast<Derived&>(*this).enter(x);
482 static_cast<Derived&>(*this).apply(x.left());
483 static_cast<Derived&>(*this).apply(x.right());
484 static_cast<Derived&>(*this).leave(x);
485 }
486
487 void apply(const process::at& x)
488 {
489 static_cast<Derived&>(*this).enter(x);
490 static_cast<Derived&>(*this).apply(x.operand());
491 static_cast<Derived&>(*this).apply(x.time_stamp());
492 static_cast<Derived&>(*this).leave(x);
493 }
494
495 void apply(const process::seq& x)
496 {
497 static_cast<Derived&>(*this).enter(x);
498 static_cast<Derived&>(*this).apply(x.left());
499 static_cast<Derived&>(*this).apply(x.right());
500 static_cast<Derived&>(*this).leave(x);
501 }
502
503 void apply(const process::if_then& x)
504 {
505 static_cast<Derived&>(*this).enter(x);
506 static_cast<Derived&>(*this).apply(x.condition());
507 static_cast<Derived&>(*this).apply(x.then_case());
508 static_cast<Derived&>(*this).leave(x);
509 }
510
511 void apply(const process::if_then_else& x)
512 {
513 static_cast<Derived&>(*this).enter(x);
514 static_cast<Derived&>(*this).apply(x.condition());
515 static_cast<Derived&>(*this).apply(x.then_case());
516 static_cast<Derived&>(*this).apply(x.else_case());
517 static_cast<Derived&>(*this).leave(x);
518 }
519
520 void apply(const process::bounded_init& x)
521 {
522 static_cast<Derived&>(*this).enter(x);
523 static_cast<Derived&>(*this).apply(x.left());
524 static_cast<Derived&>(*this).apply(x.right());
525 static_cast<Derived&>(*this).leave(x);
526 }
527
528 void apply(const process::merge& x)
529 {
530 static_cast<Derived&>(*this).enter(x);
531 static_cast<Derived&>(*this).apply(x.left());
532 static_cast<Derived&>(*this).apply(x.right());
533 static_cast<Derived&>(*this).leave(x);
534 }
535
536 void apply(const process::left_merge& x)
537 {
538 static_cast<Derived&>(*this).enter(x);
539 static_cast<Derived&>(*this).apply(x.left());
540 static_cast<Derived&>(*this).apply(x.right());
541 static_cast<Derived&>(*this).leave(x);
542 }
543
544 void apply(const process::choice& x)
545 {
546 static_cast<Derived&>(*this).enter(x);
547 static_cast<Derived&>(*this).apply(x.left());
548 static_cast<Derived&>(*this).apply(x.right());
549 static_cast<Derived&>(*this).leave(x);
550 }
551
553 {
554 static_cast<Derived&>(*this).enter(x);
555 static_cast<Derived&>(*this).apply(x.distribution());
556 static_cast<Derived&>(*this).apply(x.operand());
557 static_cast<Derived&>(*this).leave(x);
558 }
559
561 {
562 static_cast<Derived&>(*this).enter(x);
563 static_cast<Derived&>(*this).apply(x.assignments());
564 static_cast<Derived&>(*this).leave(x);
565 }
566
568 {
569 static_cast<Derived&>(*this).enter(x);
571 {
572 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
573 }
574 else if (process::is_action(x))
575 {
576 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
577 }
579 {
580 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
581 }
583 {
584 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
585 }
586 else if (process::is_delta(x))
587 {
588 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
589 }
590 else if (process::is_tau(x))
591 {
592 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
593 }
594 else if (process::is_sum(x))
595 {
596 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
597 }
598 else if (process::is_block(x))
599 {
600 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
601 }
602 else if (process::is_hide(x))
603 {
604 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
605 }
606 else if (process::is_rename(x))
607 {
608 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
609 }
610 else if (process::is_comm(x))
611 {
612 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
613 }
614 else if (process::is_allow(x))
615 {
616 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
617 }
618 else if (process::is_sync(x))
619 {
620 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
621 }
622 else if (process::is_at(x))
623 {
624 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
625 }
626 else if (process::is_seq(x))
627 {
628 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
629 }
630 else if (process::is_if_then(x))
631 {
632 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
633 }
635 {
636 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
637 }
639 {
640 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
641 }
642 else if (process::is_merge(x))
643 {
644 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
645 }
646 else if (process::is_left_merge(x))
647 {
648 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
649 }
650 else if (process::is_choice(x))
651 {
652 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
653 }
655 {
656 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
657 }
659 {
660 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
661 }
662 static_cast<Derived&>(*this).leave(x);
663 }
664
665};
666
667/// \\brief Traverser class
668template <typename Derived>
670{
671};
672//--- end generated add_traverser_data_expressions code ---//
673
674//--- start generated add_traverser_process_expressions code ---//
675template <template <class> class Traverser, class Derived>
676struct add_traverser_process_expressions: public Traverser<Derived>
677{
678 using super = Traverser<Derived>;
679 using super::enter;
680 using super::leave;
681 using super::apply;
682
684 {
685 static_cast<Derived&>(*this).enter(x);
686 static_cast<Derived&>(*this).apply(x.equations());
687 static_cast<Derived&>(*this).apply(x.init());
688 static_cast<Derived&>(*this).leave(x);
689 }
690
692 {
693 static_cast<Derived&>(*this).enter(x);
694 static_cast<Derived&>(*this).apply(x.expression());
695 static_cast<Derived&>(*this).leave(x);
696 }
697
698 void apply(const process::action& x)
699 {
700 static_cast<Derived&>(*this).enter(x);
701 // skip
702 static_cast<Derived&>(*this).leave(x);
703 }
704
706 {
707 static_cast<Derived&>(*this).enter(x);
708 // skip
709 static_cast<Derived&>(*this).leave(x);
710 }
711
713 {
714 static_cast<Derived&>(*this).enter(x);
715 // skip
716 static_cast<Derived&>(*this).leave(x);
717 }
718
719 void apply(const process::delta& x)
720 {
721 static_cast<Derived&>(*this).enter(x);
722 // skip
723 static_cast<Derived&>(*this).leave(x);
724 }
725
726 void apply(const process::tau& x)
727 {
728 static_cast<Derived&>(*this).enter(x);
729 // skip
730 static_cast<Derived&>(*this).leave(x);
731 }
732
733 void apply(const process::sum& x)
734 {
735 static_cast<Derived&>(*this).enter(x);
736 static_cast<Derived&>(*this).apply(x.operand());
737 static_cast<Derived&>(*this).leave(x);
738 }
739
740 void apply(const process::block& x)
741 {
742 static_cast<Derived&>(*this).enter(x);
743 static_cast<Derived&>(*this).apply(x.operand());
744 static_cast<Derived&>(*this).leave(x);
745 }
746
747 void apply(const process::hide& x)
748 {
749 static_cast<Derived&>(*this).enter(x);
750 static_cast<Derived&>(*this).apply(x.operand());
751 static_cast<Derived&>(*this).leave(x);
752 }
753
754 void apply(const process::rename& x)
755 {
756 static_cast<Derived&>(*this).enter(x);
757 static_cast<Derived&>(*this).apply(x.operand());
758 static_cast<Derived&>(*this).leave(x);
759 }
760
761 void apply(const process::comm& x)
762 {
763 static_cast<Derived&>(*this).enter(x);
764 static_cast<Derived&>(*this).apply(x.operand());
765 static_cast<Derived&>(*this).leave(x);
766 }
767
768 void apply(const process::allow& x)
769 {
770 static_cast<Derived&>(*this).enter(x);
771 static_cast<Derived&>(*this).apply(x.operand());
772 static_cast<Derived&>(*this).leave(x);
773 }
774
775 void apply(const process::sync& x)
776 {
777 static_cast<Derived&>(*this).enter(x);
778 static_cast<Derived&>(*this).apply(x.left());
779 static_cast<Derived&>(*this).apply(x.right());
780 static_cast<Derived&>(*this).leave(x);
781 }
782
783 void apply(const process::at& x)
784 {
785 static_cast<Derived&>(*this).enter(x);
786 static_cast<Derived&>(*this).apply(x.operand());
787 static_cast<Derived&>(*this).leave(x);
788 }
789
790 void apply(const process::seq& x)
791 {
792 static_cast<Derived&>(*this).enter(x);
793 static_cast<Derived&>(*this).apply(x.left());
794 static_cast<Derived&>(*this).apply(x.right());
795 static_cast<Derived&>(*this).leave(x);
796 }
797
798 void apply(const process::if_then& x)
799 {
800 static_cast<Derived&>(*this).enter(x);
801 static_cast<Derived&>(*this).apply(x.then_case());
802 static_cast<Derived&>(*this).leave(x);
803 }
804
805 void apply(const process::if_then_else& x)
806 {
807 static_cast<Derived&>(*this).enter(x);
808 static_cast<Derived&>(*this).apply(x.then_case());
809 static_cast<Derived&>(*this).apply(x.else_case());
810 static_cast<Derived&>(*this).leave(x);
811 }
812
813 void apply(const process::bounded_init& x)
814 {
815 static_cast<Derived&>(*this).enter(x);
816 static_cast<Derived&>(*this).apply(x.left());
817 static_cast<Derived&>(*this).apply(x.right());
818 static_cast<Derived&>(*this).leave(x);
819 }
820
821 void apply(const process::merge& x)
822 {
823 static_cast<Derived&>(*this).enter(x);
824 static_cast<Derived&>(*this).apply(x.left());
825 static_cast<Derived&>(*this).apply(x.right());
826 static_cast<Derived&>(*this).leave(x);
827 }
828
829 void apply(const process::left_merge& x)
830 {
831 static_cast<Derived&>(*this).enter(x);
832 static_cast<Derived&>(*this).apply(x.left());
833 static_cast<Derived&>(*this).apply(x.right());
834 static_cast<Derived&>(*this).leave(x);
835 }
836
837 void apply(const process::choice& x)
838 {
839 static_cast<Derived&>(*this).enter(x);
840 static_cast<Derived&>(*this).apply(x.left());
841 static_cast<Derived&>(*this).apply(x.right());
842 static_cast<Derived&>(*this).leave(x);
843 }
844
846 {
847 static_cast<Derived&>(*this).enter(x);
848 static_cast<Derived&>(*this).apply(x.operand());
849 static_cast<Derived&>(*this).leave(x);
850 }
851
853 {
854 static_cast<Derived&>(*this).enter(x);
855 // skip
856 static_cast<Derived&>(*this).leave(x);
857 }
858
860 {
861 static_cast<Derived&>(*this).enter(x);
863 {
864 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
865 }
866 else if (process::is_action(x))
867 {
868 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
869 }
871 {
872 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
873 }
875 {
876 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
877 }
878 else if (process::is_delta(x))
879 {
880 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
881 }
882 else if (process::is_tau(x))
883 {
884 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
885 }
886 else if (process::is_sum(x))
887 {
888 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
889 }
890 else if (process::is_block(x))
891 {
892 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
893 }
894 else if (process::is_hide(x))
895 {
896 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
897 }
898 else if (process::is_rename(x))
899 {
900 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
901 }
902 else if (process::is_comm(x))
903 {
904 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
905 }
906 else if (process::is_allow(x))
907 {
908 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
909 }
910 else if (process::is_sync(x))
911 {
912 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
913 }
914 else if (process::is_at(x))
915 {
916 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
917 }
918 else if (process::is_seq(x))
919 {
920 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
921 }
922 else if (process::is_if_then(x))
923 {
924 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
925 }
927 {
928 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
929 }
931 {
932 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
933 }
934 else if (process::is_merge(x))
935 {
936 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
937 }
938 else if (process::is_left_merge(x))
939 {
940 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
941 }
942 else if (process::is_choice(x))
943 {
944 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
945 }
947 {
948 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
949 }
951 {
952 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
953 }
954 static_cast<Derived&>(*this).leave(x);
955 }
956
957};
958
959/// \\brief Traverser class
960template <typename Derived>
962{
963};
964//--- end generated add_traverser_process_expressions code ---//
965
966//--- start generated add_traverser_variables code ---//
967template <template <class> class Traverser, class Derived>
968struct add_traverser_variables: public Traverser<Derived>
969{
970 using super = Traverser<Derived>;
971 using super::enter;
972 using super::leave;
973 using super::apply;
974
976 {
977 static_cast<Derived&>(*this).enter(x);
978 static_cast<Derived&>(*this).apply(x.global_variables());
979 static_cast<Derived&>(*this).apply(x.equations());
980 static_cast<Derived&>(*this).apply(x.init());
981 static_cast<Derived&>(*this).leave(x);
982 }
983
985 {
986 static_cast<Derived&>(*this).enter(x);
987 static_cast<Derived&>(*this).apply(x.variables());
988 static_cast<Derived&>(*this).leave(x);
989 }
990
992 {
993 static_cast<Derived&>(*this).enter(x);
994 static_cast<Derived&>(*this).apply(x.identifier());
995 static_cast<Derived&>(*this).apply(x.formal_parameters());
996 static_cast<Derived&>(*this).apply(x.expression());
997 static_cast<Derived&>(*this).leave(x);
998 }
999
1001 {
1002 static_cast<Derived&>(*this).enter(x);
1003 static_cast<Derived&>(*this).apply(x.actions());
1004 static_cast<Derived&>(*this).leave(x);
1005 }
1006
1007 void apply(const process::action& x)
1008 {
1009 static_cast<Derived&>(*this).enter(x);
1010 static_cast<Derived&>(*this).apply(x.arguments());
1011 static_cast<Derived&>(*this).leave(x);
1012 }
1013
1015 {
1016 static_cast<Derived&>(*this).enter(x);
1017 static_cast<Derived&>(*this).apply(x.identifier());
1018 static_cast<Derived&>(*this).apply(x.actual_parameters());
1019 static_cast<Derived&>(*this).leave(x);
1020 }
1021
1023 {
1024 static_cast<Derived&>(*this).enter(x);
1025 static_cast<Derived&>(*this).apply(x.identifier());
1026 static_cast<Derived&>(*this).apply(x.assignments());
1027 static_cast<Derived&>(*this).leave(x);
1028 }
1029
1030 void apply(const process::delta& x)
1031 {
1032 static_cast<Derived&>(*this).enter(x);
1033 // skip
1034 static_cast<Derived&>(*this).leave(x);
1035 }
1036
1037 void apply(const process::tau& x)
1038 {
1039 static_cast<Derived&>(*this).enter(x);
1040 // skip
1041 static_cast<Derived&>(*this).leave(x);
1042 }
1043
1044 void apply(const process::sum& x)
1045 {
1046 static_cast<Derived&>(*this).enter(x);
1047 static_cast<Derived&>(*this).apply(x.variables());
1048 static_cast<Derived&>(*this).apply(x.operand());
1049 static_cast<Derived&>(*this).leave(x);
1050 }
1051
1052 void apply(const process::block& x)
1053 {
1054 static_cast<Derived&>(*this).enter(x);
1055 static_cast<Derived&>(*this).apply(x.operand());
1056 static_cast<Derived&>(*this).leave(x);
1057 }
1058
1059 void apply(const process::hide& x)
1060 {
1061 static_cast<Derived&>(*this).enter(x);
1062 static_cast<Derived&>(*this).apply(x.operand());
1063 static_cast<Derived&>(*this).leave(x);
1064 }
1065
1066 void apply(const process::rename& x)
1067 {
1068 static_cast<Derived&>(*this).enter(x);
1069 static_cast<Derived&>(*this).apply(x.operand());
1070 static_cast<Derived&>(*this).leave(x);
1071 }
1072
1073 void apply(const process::comm& x)
1074 {
1075 static_cast<Derived&>(*this).enter(x);
1076 static_cast<Derived&>(*this).apply(x.operand());
1077 static_cast<Derived&>(*this).leave(x);
1078 }
1079
1080 void apply(const process::allow& x)
1081 {
1082 static_cast<Derived&>(*this).enter(x);
1083 static_cast<Derived&>(*this).apply(x.operand());
1084 static_cast<Derived&>(*this).leave(x);
1085 }
1086
1087 void apply(const process::sync& x)
1088 {
1089 static_cast<Derived&>(*this).enter(x);
1090 static_cast<Derived&>(*this).apply(x.left());
1091 static_cast<Derived&>(*this).apply(x.right());
1092 static_cast<Derived&>(*this).leave(x);
1093 }
1094
1095 void apply(const process::at& x)
1096 {
1097 static_cast<Derived&>(*this).enter(x);
1098 static_cast<Derived&>(*this).apply(x.operand());
1099 static_cast<Derived&>(*this).apply(x.time_stamp());
1100 static_cast<Derived&>(*this).leave(x);
1101 }
1102
1103 void apply(const process::seq& x)
1104 {
1105 static_cast<Derived&>(*this).enter(x);
1106 static_cast<Derived&>(*this).apply(x.left());
1107 static_cast<Derived&>(*this).apply(x.right());
1108 static_cast<Derived&>(*this).leave(x);
1109 }
1110
1111 void apply(const process::if_then& x)
1112 {
1113 static_cast<Derived&>(*this).enter(x);
1114 static_cast<Derived&>(*this).apply(x.condition());
1115 static_cast<Derived&>(*this).apply(x.then_case());
1116 static_cast<Derived&>(*this).leave(x);
1117 }
1118
1120 {
1121 static_cast<Derived&>(*this).enter(x);
1122 static_cast<Derived&>(*this).apply(x.condition());
1123 static_cast<Derived&>(*this).apply(x.then_case());
1124 static_cast<Derived&>(*this).apply(x.else_case());
1125 static_cast<Derived&>(*this).leave(x);
1126 }
1127
1129 {
1130 static_cast<Derived&>(*this).enter(x);
1131 static_cast<Derived&>(*this).apply(x.left());
1132 static_cast<Derived&>(*this).apply(x.right());
1133 static_cast<Derived&>(*this).leave(x);
1134 }
1135
1136 void apply(const process::merge& x)
1137 {
1138 static_cast<Derived&>(*this).enter(x);
1139 static_cast<Derived&>(*this).apply(x.left());
1140 static_cast<Derived&>(*this).apply(x.right());
1141 static_cast<Derived&>(*this).leave(x);
1142 }
1143
1144 void apply(const process::left_merge& x)
1145 {
1146 static_cast<Derived&>(*this).enter(x);
1147 static_cast<Derived&>(*this).apply(x.left());
1148 static_cast<Derived&>(*this).apply(x.right());
1149 static_cast<Derived&>(*this).leave(x);
1150 }
1151
1152 void apply(const process::choice& x)
1153 {
1154 static_cast<Derived&>(*this).enter(x);
1155 static_cast<Derived&>(*this).apply(x.left());
1156 static_cast<Derived&>(*this).apply(x.right());
1157 static_cast<Derived&>(*this).leave(x);
1158 }
1159
1161 {
1162 static_cast<Derived&>(*this).enter(x);
1163 static_cast<Derived&>(*this).apply(x.variables());
1164 static_cast<Derived&>(*this).apply(x.distribution());
1165 static_cast<Derived&>(*this).apply(x.operand());
1166 static_cast<Derived&>(*this).leave(x);
1167 }
1168
1170 {
1171 static_cast<Derived&>(*this).enter(x);
1172 static_cast<Derived&>(*this).apply(x.assignments());
1173 static_cast<Derived&>(*this).leave(x);
1174 }
1175
1177 {
1178 static_cast<Derived&>(*this).enter(x);
1180 {
1181 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
1182 }
1183 else if (process::is_action(x))
1184 {
1185 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
1186 }
1188 {
1189 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
1190 }
1192 {
1193 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
1194 }
1195 else if (process::is_delta(x))
1196 {
1197 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
1198 }
1199 else if (process::is_tau(x))
1200 {
1201 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
1202 }
1203 else if (process::is_sum(x))
1204 {
1205 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
1206 }
1207 else if (process::is_block(x))
1208 {
1209 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
1210 }
1211 else if (process::is_hide(x))
1212 {
1213 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
1214 }
1215 else if (process::is_rename(x))
1216 {
1217 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
1218 }
1219 else if (process::is_comm(x))
1220 {
1221 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
1222 }
1223 else if (process::is_allow(x))
1224 {
1225 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
1226 }
1227 else if (process::is_sync(x))
1228 {
1229 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
1230 }
1231 else if (process::is_at(x))
1232 {
1233 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
1234 }
1235 else if (process::is_seq(x))
1236 {
1237 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
1238 }
1239 else if (process::is_if_then(x))
1240 {
1241 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
1242 }
1244 {
1245 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
1246 }
1248 {
1249 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
1250 }
1251 else if (process::is_merge(x))
1252 {
1253 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
1254 }
1255 else if (process::is_left_merge(x))
1256 {
1257 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
1258 }
1259 else if (process::is_choice(x))
1260 {
1261 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
1262 }
1264 {
1265 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
1266 }
1268 {
1269 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
1270 }
1271 static_cast<Derived&>(*this).leave(x);
1272 }
1273
1274};
1275
1276/// \\brief Traverser class
1277template <typename Derived>
1279{
1280};
1281//--- end generated add_traverser_variables code ---//
1282
1283//--- start generated add_traverser_identifier_strings code ---//
1284template <template <class> class Traverser, class Derived>
1285struct add_traverser_identifier_strings: public Traverser<Derived>
1286{
1287 using super = Traverser<Derived>;
1288 using super::enter;
1289 using super::leave;
1290 using super::apply;
1291
1293 {
1294 static_cast<Derived&>(*this).enter(x);
1295 static_cast<Derived&>(*this).apply(x.name());
1296 static_cast<Derived&>(*this).apply(x.sorts());
1297 static_cast<Derived&>(*this).leave(x);
1298 }
1299
1301 {
1302 static_cast<Derived&>(*this).enter(x);
1303 static_cast<Derived&>(*this).apply(x.action_labels());
1304 static_cast<Derived&>(*this).apply(x.global_variables());
1305 static_cast<Derived&>(*this).apply(x.equations());
1306 static_cast<Derived&>(*this).apply(x.init());
1307 static_cast<Derived&>(*this).leave(x);
1308 }
1309
1311 {
1312 static_cast<Derived&>(*this).enter(x);
1313 static_cast<Derived&>(*this).apply(x.name());
1314 static_cast<Derived&>(*this).apply(x.variables());
1315 static_cast<Derived&>(*this).leave(x);
1316 }
1317
1319 {
1320 static_cast<Derived&>(*this).enter(x);
1321 static_cast<Derived&>(*this).apply(x.identifier());
1322 static_cast<Derived&>(*this).apply(x.formal_parameters());
1323 static_cast<Derived&>(*this).apply(x.expression());
1324 static_cast<Derived&>(*this).leave(x);
1325 }
1326
1328 {
1329 static_cast<Derived&>(*this).enter(x);
1330 static_cast<Derived&>(*this).apply(x.source());
1331 static_cast<Derived&>(*this).apply(x.target());
1332 static_cast<Derived&>(*this).leave(x);
1333 }
1334
1336 {
1337 static_cast<Derived&>(*this).enter(x);
1338 static_cast<Derived&>(*this).apply(x.action_name());
1339 static_cast<Derived&>(*this).apply(x.name());
1340 static_cast<Derived&>(*this).leave(x);
1341 }
1342
1344 {
1345 static_cast<Derived&>(*this).enter(x);
1346 static_cast<Derived&>(*this).apply(x.names());
1347 static_cast<Derived&>(*this).leave(x);
1348 }
1349
1351 {
1352 static_cast<Derived&>(*this).enter(x);
1353 static_cast<Derived&>(*this).apply(x.actions());
1354 static_cast<Derived&>(*this).leave(x);
1355 }
1356
1357 void apply(const process::action& x)
1358 {
1359 static_cast<Derived&>(*this).enter(x);
1360 static_cast<Derived&>(*this).apply(x.label());
1361 static_cast<Derived&>(*this).apply(x.arguments());
1362 static_cast<Derived&>(*this).leave(x);
1363 }
1364
1366 {
1367 static_cast<Derived&>(*this).enter(x);
1368 static_cast<Derived&>(*this).apply(x.identifier());
1369 static_cast<Derived&>(*this).apply(x.actual_parameters());
1370 static_cast<Derived&>(*this).leave(x);
1371 }
1372
1374 {
1375 static_cast<Derived&>(*this).enter(x);
1376 static_cast<Derived&>(*this).apply(x.identifier());
1377 static_cast<Derived&>(*this).apply(x.assignments());
1378 static_cast<Derived&>(*this).leave(x);
1379 }
1380
1381 void apply(const process::delta& x)
1382 {
1383 static_cast<Derived&>(*this).enter(x);
1384 // skip
1385 static_cast<Derived&>(*this).leave(x);
1386 }
1387
1388 void apply(const process::tau& x)
1389 {
1390 static_cast<Derived&>(*this).enter(x);
1391 // skip
1392 static_cast<Derived&>(*this).leave(x);
1393 }
1394
1395 void apply(const process::sum& x)
1396 {
1397 static_cast<Derived&>(*this).enter(x);
1398 static_cast<Derived&>(*this).apply(x.variables());
1399 static_cast<Derived&>(*this).apply(x.operand());
1400 static_cast<Derived&>(*this).leave(x);
1401 }
1402
1403 void apply(const process::block& x)
1404 {
1405 static_cast<Derived&>(*this).enter(x);
1406 static_cast<Derived&>(*this).apply(x.block_set());
1407 static_cast<Derived&>(*this).apply(x.operand());
1408 static_cast<Derived&>(*this).leave(x);
1409 }
1410
1411 void apply(const process::hide& x)
1412 {
1413 static_cast<Derived&>(*this).enter(x);
1414 static_cast<Derived&>(*this).apply(x.hide_set());
1415 static_cast<Derived&>(*this).apply(x.operand());
1416 static_cast<Derived&>(*this).leave(x);
1417 }
1418
1419 void apply(const process::rename& x)
1420 {
1421 static_cast<Derived&>(*this).enter(x);
1422 static_cast<Derived&>(*this).apply(x.rename_set());
1423 static_cast<Derived&>(*this).apply(x.operand());
1424 static_cast<Derived&>(*this).leave(x);
1425 }
1426
1427 void apply(const process::comm& x)
1428 {
1429 static_cast<Derived&>(*this).enter(x);
1430 static_cast<Derived&>(*this).apply(x.comm_set());
1431 static_cast<Derived&>(*this).apply(x.operand());
1432 static_cast<Derived&>(*this).leave(x);
1433 }
1434
1435 void apply(const process::allow& x)
1436 {
1437 static_cast<Derived&>(*this).enter(x);
1438 static_cast<Derived&>(*this).apply(x.allow_set());
1439 static_cast<Derived&>(*this).apply(x.operand());
1440 static_cast<Derived&>(*this).leave(x);
1441 }
1442
1443 void apply(const process::sync& x)
1444 {
1445 static_cast<Derived&>(*this).enter(x);
1446 static_cast<Derived&>(*this).apply(x.left());
1447 static_cast<Derived&>(*this).apply(x.right());
1448 static_cast<Derived&>(*this).leave(x);
1449 }
1450
1451 void apply(const process::at& x)
1452 {
1453 static_cast<Derived&>(*this).enter(x);
1454 static_cast<Derived&>(*this).apply(x.operand());
1455 static_cast<Derived&>(*this).apply(x.time_stamp());
1456 static_cast<Derived&>(*this).leave(x);
1457 }
1458
1459 void apply(const process::seq& x)
1460 {
1461 static_cast<Derived&>(*this).enter(x);
1462 static_cast<Derived&>(*this).apply(x.left());
1463 static_cast<Derived&>(*this).apply(x.right());
1464 static_cast<Derived&>(*this).leave(x);
1465 }
1466
1467 void apply(const process::if_then& x)
1468 {
1469 static_cast<Derived&>(*this).enter(x);
1470 static_cast<Derived&>(*this).apply(x.condition());
1471 static_cast<Derived&>(*this).apply(x.then_case());
1472 static_cast<Derived&>(*this).leave(x);
1473 }
1474
1476 {
1477 static_cast<Derived&>(*this).enter(x);
1478 static_cast<Derived&>(*this).apply(x.condition());
1479 static_cast<Derived&>(*this).apply(x.then_case());
1480 static_cast<Derived&>(*this).apply(x.else_case());
1481 static_cast<Derived&>(*this).leave(x);
1482 }
1483
1485 {
1486 static_cast<Derived&>(*this).enter(x);
1487 static_cast<Derived&>(*this).apply(x.left());
1488 static_cast<Derived&>(*this).apply(x.right());
1489 static_cast<Derived&>(*this).leave(x);
1490 }
1491
1492 void apply(const process::merge& x)
1493 {
1494 static_cast<Derived&>(*this).enter(x);
1495 static_cast<Derived&>(*this).apply(x.left());
1496 static_cast<Derived&>(*this).apply(x.right());
1497 static_cast<Derived&>(*this).leave(x);
1498 }
1499
1500 void apply(const process::left_merge& x)
1501 {
1502 static_cast<Derived&>(*this).enter(x);
1503 static_cast<Derived&>(*this).apply(x.left());
1504 static_cast<Derived&>(*this).apply(x.right());
1505 static_cast<Derived&>(*this).leave(x);
1506 }
1507
1508 void apply(const process::choice& x)
1509 {
1510 static_cast<Derived&>(*this).enter(x);
1511 static_cast<Derived&>(*this).apply(x.left());
1512 static_cast<Derived&>(*this).apply(x.right());
1513 static_cast<Derived&>(*this).leave(x);
1514 }
1515
1517 {
1518 static_cast<Derived&>(*this).enter(x);
1519 static_cast<Derived&>(*this).apply(x.variables());
1520 static_cast<Derived&>(*this).apply(x.distribution());
1521 static_cast<Derived&>(*this).apply(x.operand());
1522 static_cast<Derived&>(*this).leave(x);
1523 }
1524
1526 {
1527 static_cast<Derived&>(*this).enter(x);
1528 static_cast<Derived&>(*this).apply(x.name());
1529 static_cast<Derived&>(*this).apply(x.assignments());
1530 static_cast<Derived&>(*this).leave(x);
1531 }
1532
1534 {
1535 static_cast<Derived&>(*this).enter(x);
1537 {
1538 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
1539 }
1540 else if (process::is_action(x))
1541 {
1542 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
1543 }
1545 {
1546 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
1547 }
1549 {
1550 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
1551 }
1552 else if (process::is_delta(x))
1553 {
1554 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
1555 }
1556 else if (process::is_tau(x))
1557 {
1558 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
1559 }
1560 else if (process::is_sum(x))
1561 {
1562 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
1563 }
1564 else if (process::is_block(x))
1565 {
1566 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
1567 }
1568 else if (process::is_hide(x))
1569 {
1570 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
1571 }
1572 else if (process::is_rename(x))
1573 {
1574 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
1575 }
1576 else if (process::is_comm(x))
1577 {
1578 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
1579 }
1580 else if (process::is_allow(x))
1581 {
1582 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
1583 }
1584 else if (process::is_sync(x))
1585 {
1586 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
1587 }
1588 else if (process::is_at(x))
1589 {
1590 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
1591 }
1592 else if (process::is_seq(x))
1593 {
1594 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
1595 }
1596 else if (process::is_if_then(x))
1597 {
1598 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
1599 }
1601 {
1602 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
1603 }
1605 {
1606 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
1607 }
1608 else if (process::is_merge(x))
1609 {
1610 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
1611 }
1612 else if (process::is_left_merge(x))
1613 {
1614 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
1615 }
1616 else if (process::is_choice(x))
1617 {
1618 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
1619 }
1621 {
1622 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
1623 }
1625 {
1626 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
1627 }
1628 static_cast<Derived&>(*this).leave(x);
1629 }
1630
1631};
1632
1633/// \\brief Traverser class
1634template <typename Derived>
1636{
1637};
1638//--- end generated add_traverser_identifier_strings code ---//
1639
1640//--- start generated add_traverser_action_labels code ---//
1641template <template <class> class Traverser, class Derived>
1642struct add_traverser_action_labels: public Traverser<Derived>
1643{
1644 using super = Traverser<Derived>;
1645 using super::enter;
1646 using super::leave;
1647 using super::apply;
1648
1650 {
1651 static_cast<Derived&>(*this).enter(x);
1652 // skip
1653 static_cast<Derived&>(*this).leave(x);
1654 }
1655
1657 {
1658 static_cast<Derived&>(*this).enter(x);
1659 static_cast<Derived&>(*this).apply(x.action_labels());
1660 static_cast<Derived&>(*this).apply(x.equations());
1661 static_cast<Derived&>(*this).apply(x.init());
1662 static_cast<Derived&>(*this).leave(x);
1663 }
1664
1666 {
1667 static_cast<Derived&>(*this).enter(x);
1668 static_cast<Derived&>(*this).apply(x.expression());
1669 static_cast<Derived&>(*this).leave(x);
1670 }
1671
1672 void apply(const process::action& x)
1673 {
1674 static_cast<Derived&>(*this).enter(x);
1675 static_cast<Derived&>(*this).apply(x.label());
1676 static_cast<Derived&>(*this).leave(x);
1677 }
1678
1680 {
1681 static_cast<Derived&>(*this).enter(x);
1682 // skip
1683 static_cast<Derived&>(*this).leave(x);
1684 }
1685
1687 {
1688 static_cast<Derived&>(*this).enter(x);
1689 // skip
1690 static_cast<Derived&>(*this).leave(x);
1691 }
1692
1693 void apply(const process::delta& x)
1694 {
1695 static_cast<Derived&>(*this).enter(x);
1696 // skip
1697 static_cast<Derived&>(*this).leave(x);
1698 }
1699
1700 void apply(const process::tau& x)
1701 {
1702 static_cast<Derived&>(*this).enter(x);
1703 // skip
1704 static_cast<Derived&>(*this).leave(x);
1705 }
1706
1707 void apply(const process::sum& x)
1708 {
1709 static_cast<Derived&>(*this).enter(x);
1710 static_cast<Derived&>(*this).apply(x.operand());
1711 static_cast<Derived&>(*this).leave(x);
1712 }
1713
1714 void apply(const process::block& x)
1715 {
1716 static_cast<Derived&>(*this).enter(x);
1717 static_cast<Derived&>(*this).apply(x.operand());
1718 static_cast<Derived&>(*this).leave(x);
1719 }
1720
1721 void apply(const process::hide& x)
1722 {
1723 static_cast<Derived&>(*this).enter(x);
1724 static_cast<Derived&>(*this).apply(x.operand());
1725 static_cast<Derived&>(*this).leave(x);
1726 }
1727
1728 void apply(const process::rename& x)
1729 {
1730 static_cast<Derived&>(*this).enter(x);
1731 static_cast<Derived&>(*this).apply(x.operand());
1732 static_cast<Derived&>(*this).leave(x);
1733 }
1734
1735 void apply(const process::comm& x)
1736 {
1737 static_cast<Derived&>(*this).enter(x);
1738 static_cast<Derived&>(*this).apply(x.operand());
1739 static_cast<Derived&>(*this).leave(x);
1740 }
1741
1742 void apply(const process::allow& x)
1743 {
1744 static_cast<Derived&>(*this).enter(x);
1745 static_cast<Derived&>(*this).apply(x.operand());
1746 static_cast<Derived&>(*this).leave(x);
1747 }
1748
1749 void apply(const process::sync& x)
1750 {
1751 static_cast<Derived&>(*this).enter(x);
1752 static_cast<Derived&>(*this).apply(x.left());
1753 static_cast<Derived&>(*this).apply(x.right());
1754 static_cast<Derived&>(*this).leave(x);
1755 }
1756
1757 void apply(const process::at& x)
1758 {
1759 static_cast<Derived&>(*this).enter(x);
1760 static_cast<Derived&>(*this).apply(x.operand());
1761 static_cast<Derived&>(*this).leave(x);
1762 }
1763
1764 void apply(const process::seq& x)
1765 {
1766 static_cast<Derived&>(*this).enter(x);
1767 static_cast<Derived&>(*this).apply(x.left());
1768 static_cast<Derived&>(*this).apply(x.right());
1769 static_cast<Derived&>(*this).leave(x);
1770 }
1771
1772 void apply(const process::if_then& x)
1773 {
1774 static_cast<Derived&>(*this).enter(x);
1775 static_cast<Derived&>(*this).apply(x.then_case());
1776 static_cast<Derived&>(*this).leave(x);
1777 }
1778
1780 {
1781 static_cast<Derived&>(*this).enter(x);
1782 static_cast<Derived&>(*this).apply(x.then_case());
1783 static_cast<Derived&>(*this).apply(x.else_case());
1784 static_cast<Derived&>(*this).leave(x);
1785 }
1786
1788 {
1789 static_cast<Derived&>(*this).enter(x);
1790 static_cast<Derived&>(*this).apply(x.left());
1791 static_cast<Derived&>(*this).apply(x.right());
1792 static_cast<Derived&>(*this).leave(x);
1793 }
1794
1795 void apply(const process::merge& x)
1796 {
1797 static_cast<Derived&>(*this).enter(x);
1798 static_cast<Derived&>(*this).apply(x.left());
1799 static_cast<Derived&>(*this).apply(x.right());
1800 static_cast<Derived&>(*this).leave(x);
1801 }
1802
1803 void apply(const process::left_merge& x)
1804 {
1805 static_cast<Derived&>(*this).enter(x);
1806 static_cast<Derived&>(*this).apply(x.left());
1807 static_cast<Derived&>(*this).apply(x.right());
1808 static_cast<Derived&>(*this).leave(x);
1809 }
1810
1811 void apply(const process::choice& x)
1812 {
1813 static_cast<Derived&>(*this).enter(x);
1814 static_cast<Derived&>(*this).apply(x.left());
1815 static_cast<Derived&>(*this).apply(x.right());
1816 static_cast<Derived&>(*this).leave(x);
1817 }
1818
1820 {
1821 static_cast<Derived&>(*this).enter(x);
1822 static_cast<Derived&>(*this).apply(x.operand());
1823 static_cast<Derived&>(*this).leave(x);
1824 }
1825
1827 {
1828 static_cast<Derived&>(*this).enter(x);
1829 // skip
1830 static_cast<Derived&>(*this).leave(x);
1831 }
1832
1834 {
1835 static_cast<Derived&>(*this).enter(x);
1837 {
1838 static_cast<Derived&>(*this).apply(atermpp::down_cast<data::untyped_data_parameter>(x));
1839 }
1840 else if (process::is_action(x))
1841 {
1842 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::action>(x));
1843 }
1845 {
1846 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance>(x));
1847 }
1849 {
1850 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::process_instance_assignment>(x));
1851 }
1852 else if (process::is_delta(x))
1853 {
1854 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::delta>(x));
1855 }
1856 else if (process::is_tau(x))
1857 {
1858 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::tau>(x));
1859 }
1860 else if (process::is_sum(x))
1861 {
1862 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sum>(x));
1863 }
1864 else if (process::is_block(x))
1865 {
1866 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::block>(x));
1867 }
1868 else if (process::is_hide(x))
1869 {
1870 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::hide>(x));
1871 }
1872 else if (process::is_rename(x))
1873 {
1874 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::rename>(x));
1875 }
1876 else if (process::is_comm(x))
1877 {
1878 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::comm>(x));
1879 }
1880 else if (process::is_allow(x))
1881 {
1882 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::allow>(x));
1883 }
1884 else if (process::is_sync(x))
1885 {
1886 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::sync>(x));
1887 }
1888 else if (process::is_at(x))
1889 {
1890 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::at>(x));
1891 }
1892 else if (process::is_seq(x))
1893 {
1894 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::seq>(x));
1895 }
1896 else if (process::is_if_then(x))
1897 {
1898 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then>(x));
1899 }
1901 {
1902 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::if_then_else>(x));
1903 }
1905 {
1906 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::bounded_init>(x));
1907 }
1908 else if (process::is_merge(x))
1909 {
1910 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::merge>(x));
1911 }
1912 else if (process::is_left_merge(x))
1913 {
1914 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::left_merge>(x));
1915 }
1916 else if (process::is_choice(x))
1917 {
1918 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::choice>(x));
1919 }
1921 {
1922 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::stochastic_operator>(x));
1923 }
1925 {
1926 static_cast<Derived&>(*this).apply(atermpp::down_cast<process::untyped_process_assignment>(x));
1927 }
1928 static_cast<Derived&>(*this).leave(x);
1929 }
1930
1931};
1932
1933/// \\brief Traverser class
1934template <typename Derived>
1936{
1937};
1938//--- end generated add_traverser_action_labels code ---//
1939
1940} // namespace mcrl2::process
1941
1942#endif // MCRL2_PROCESS_TRAVERSER_H
aterm_string & operator=(const aterm_string &t) noexcept=default
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
An abstraction expression.
Definition abstraction.h:23
const variable_list & variables() const
Definition abstraction.h:60
const data_expression & body() const
Definition abstraction.h:65
const binder_type & binding_operator() const
Definition abstraction.h:55
\brief A sort alias
Definition alias.h:23
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:39
\brief Assignment expression
Definition assignment.h:24
\brief Assignment of a data expression to a variable
Definition assignment.h:88
const data_expression & rhs() const
Definition assignment.h:119
const variable & lhs() const
Definition assignment.h:114
\brief A basic sort
Definition basic_sort.h:25
data_expression & operator=(const data_expression &) noexcept=default
data_expression()
\brief Default constructor X3.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
data_expression(const data_expression &) noexcept=default
Move semantics.
void add_consistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
inequality_consistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_consistency_cache(const inequality_consistency_cache &)=delete
bool is_consistent(const std::vector< linear_inequality > &inequalities_in_) const
std::unique_ptr< inequality_inconsistency_cache_base > m_cache
inequality_inconsistency_cache_base & operator=(const inequality_inconsistency_cache_base &)=delete
std::unique_ptr< inequality_inconsistency_cache_base > m_present_branch
std::unique_ptr< inequality_inconsistency_cache_base > m_non_present_branch
inequality_inconsistency_cache_base(const node_type node, const linear_inequality &inequality, std::unique_ptr< inequality_inconsistency_cache_base > present_branch, std::unique_ptr< inequality_inconsistency_cache_base > non_present_branch)
inequality_inconsistency_cache_base(const inequality_inconsistency_cache_base &)=delete
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in_) const
inequality_inconsistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_inconsistency_cache(const inequality_inconsistency_cache &)=delete
void add_inconsistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
std::unique_ptr< inequality_inconsistency_cache_base > m_cache
lhs_t(const aterm &t)
Constructor from an aterm.
const data_expression & operator[](const variable &v) const
Give the factor of variable v.
data_expression transform_to_data_expression() const
lhs_t erase(const variable &v) const
Erase a variable and its factor.
std::size_t count(const variable &v) const
Give the factor of variable v.
lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
Constructor.
data_expression evaluate(const SubstitutionFunction &beta, const rewriter &r) const
Evaluate the variables in this lhs_t according to the subsitution function.
lhs_t::const_iterator find(const variable &v) const
Give an iterator of the factor/variable pair for v, or end() if v does not occur.
lhs_t(const ITERATOR begin, const ITERATOR end)
Constructor.
variable_with_a_rational_factor(const variable &v, const data_expression &f)
\brief A function sort
\brief A function symbol
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
const detail::lhs_t & lhs() const
linear_inequality invert(const rewriter &r)
bool typical_pair(data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const
Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn,...
linear_inequality()
Constructor yielding an inconsistent inequality.
bool is_true(const rewriter &r) const
void add_variables(std::set< variable > &variable_set) const
bool is_false(const rewriter &r) const
linear_inequality(const data_expression &e, const rewriter &r)
Constructor that constructs a linear inequality out of a data expression.
linear_inequality(const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false)
constructor.
data_expression transform_to_data_expression() const
static void parse_and_store_expression(const data_expression &e, detail::map_based_lhs_t &new_lhs, data_expression &new_rhs, const rewriter &r, const bool negate=false, const data_expression &factor=real_one())
linear_inequality(const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)
Basic constructor.
detail::lhs_t::const_iterator lhs_begin() const
detail::lhs_t::const_iterator lhs_end() const
linear_inequality(const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)
constructor.
const data_expression & rhs() const
data_expression get_factor_for_a_variable(const variable &x)
detail::comparison_t comparison() const
Wrapper clas s for internal storage and substitution updates using operator()
assignment(const variable_type &v, Substitution &sigma, std::multiset< variable_type > &variables_in_rhs, std::set< variable_type > &scratch_set)
Constructor.
assignment & operator=(const expression_type &e)
Actual assignment.
Wrapper that extends any substitution to a substitution maintaining the vars in its rhs.
bool variable_occurs_in_a_rhs(const variable_type &v)
Indicates whether a variable occurs in some rhs of this substitution.
assignment operator[](variable_type const &v)
Assigment operator.
const std::multiset< variable > & variables_in_rhs()
Provides a set of variables that occur in the right hand sides of the assignments.
maintain_variables_in_rhs()=default
Default constructor.
std::multiset< variable_type > m_variables_in_rhs
Components for generating an arbitrary element of a sort.
data_expression operator()(const sort_expression &sort)
Returns a representative of a sort.
Rewriter that operates on data expressions.
Definition rewriter.h:84
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Definition rewriter.h:161
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A sort expression
sort_expression & operator=(const sort_expression &) noexcept=default
\brief A constructor for a structured sort
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
function_symbol recogniser_function(const sort_expression &s) const
Returns the function corresponding to the recogniser of this constructor, such that it is usable in t...
\brief A data variable
Definition variable.h:25
const core::identifier_string & name() const
Definition variable.h:35
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:40
\brief A where expression
where_clause(const atermpp::aterm &term)
const data_expression & body() const
const assignment_expression_list & declarations() const
LPS summand containing a multi-action.
lps::multi_action m_multi_action
The summation variables of the summand.
action_summand(const action_summand &) noexcept=default
Move semantics.
data::assignment_list & assignments()
Returns the sequence of assignments.
void swap(action_summand &other) noexcept
Swaps the contents.
action_summand()=default
Constructor.
data::data_expression_list next_state(const data::variable_list &process_parameters) const
Returns the next state corresponding to this summand.
Definition lps.cpp:71
action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments)
Constructor.
bool has_time() const
Returns true if time is available.
bool is_tau() const
Returns true if the multi-action corresponding to this summand is equal to tau.
action_summand & operator=(const action_summand &) noexcept=default
action_summand & operator=(action_summand &&) noexcept=default
action_summand(action_summand &&) noexcept=default
const data::assignment_list & assignments() const
Returns the sequence of assignments.
data::assignment_list m_assignments
The assignments of the next state.
Algorithm class for elimination of constant parameters.
Definition constelm.h:23
void LOG_PARAMETER_CHANGE(const data::data_expression &d_j, const data::data_expression &Rd_j, const data::data_expression &Rg_ij, const data::mutable_map_substitution<> &sigma, const std::string &msg="")
Definition constelm.h:61
bool is_constant(const data::data_expression &x, const std::set< data::variable > &global_variables) const
Definition constelm.h:96
void remove_parameters(data::mutable_map_substitution<> &sigma)
Applies the substitution computed by compute_constant_parameters.
Definition constelm.h:232
const DataRewriter & R
The rewriter used by the constelm algorithm.
Definition constelm.h:38
void LOG_CONSTANT_PARAMETERS(const data::mutable_map_substitution<> &sigma, const std::string &constant_removed_msg="", const std::string &nothing_removed_msg="")
Definition constelm.h:40
bool m_ignore_conditions
If true, conditions are not evaluated and assumed to be true.
Definition constelm.h:32
constelm_algorithm(Specification &spec, const DataRewriter &R_)
Constructor.
Definition constelm.h:113
void LOG_CONDITION(const data::data_expression &cond, const data::data_expression &c_i, const data::mutable_map_substitution<> &sigma, const std::string &msg="")
Definition constelm.h:78
void run(bool instantiate_global_variables=false, bool ignore_conditions=false)
Runs the constelm algorithm.
Definition constelm.h:257
std::map< data::variable, std::size_t > m_index_of
Maps process parameters to their index.
Definition constelm.h:35
data::mutable_map_substitution compute_constant_parameters(bool instantiate_global_variables=false, bool ignore_conditions=false)
Computes constant parameters.
Definition constelm.h:123
bool m_instantiate_global_variables
If true, then the algorithm is allowed to instantiate free variables as a side effect.
Definition constelm.h:29
LPS summand containing a deadlock.
deadlock_summand()=default
Constructor.
deadlock_summand & operator=(const deadlock_summand &) noexcept=default
lps::deadlock m_deadlock
The deadlock of the summand.
deadlock_summand(deadlock_summand &&) noexcept=default
deadlock_summand & operator=(deadlock_summand &&) noexcept=default
void swap(deadlock_summand &other) noexcept
Swaps the contents.
deadlock_summand(const deadlock_summand &) noexcept=default
Move semantics.
deadlock_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::deadlock &delta)
Constructor.
bool has_time() const
Returns true if time is available.
Represents a deadlock.
Definition deadlock.h:23
bool operator!=(const deadlock &other) const
Comparison operator.
Definition deadlock.h:71
data::data_expression m_time
The time of the deadlock. If m_time == data::undefined_real() the multi action has no time.
Definition deadlock.h:29
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:33
bool has_time() const
Returns true if time is available.
Definition deadlock.h:39
std::string to_string() const
Returns a string representation of the deadlock.
Definition deadlock.h:59
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:46
void swap(deadlock &other) noexcept
Swaps the contents.
Definition deadlock.h:77
data::data_expression & time()
Returns the time.
Definition deadlock.h:53
bool operator==(const deadlock &other) const
Comparison operator.
Definition deadlock.h:65
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
void remove_parameters(const std::set< data::variable > &to_be_removed)
Removes formal parameters from the specification.
void remove_unused_summand_variables()
Removes unused summand variables.
void sumelm_find_variables(const action_summand &s, std::set< data::variable > &result) const
void summand_remove_unused_summand_variables(SummandType &summand_)
void sumelm_find_variables(const deadlock_summand &s, std::set< data::variable > &result) const
data::data_expression next_state(const action_summand &s, const data::variable &v) const
Applies the next state substitution to the variable v.
bool verbose() const
Flag for verbose output.
void remove_singleton_sorts()
Removes parameters with a singleton sort.
void remove_trivial_summands()
Removes summands with condition equal to false.
void instantiate_free_variables()
Attempts to eliminate the free variables of the specification, by substituting a constant value for t...
lps_algorithm(Specification &spec)
Constructor.
Specification & m_spec
The specification that is processed by the algorithm.
data_expression & constraint()
Obtain a reference to the constraint.
deadlock_summand_vector & deadlock_summands()
Returns the sequence of deadlock summands.
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
deadlock_summand_vector m_deadlock_summands
The deadlock summands of the process.
linear_process_base()=default
Constructor.
data::variable_list m_process_parameters
The process parameters of the process.
linear_process_base(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const std::vector< ActionSummand > &action_summands)
Constructor.
bool has_time() const
Returns true if time is available in at least one of the summands.
data::variable_list & process_parameters()
Returns the sequence of process parameters.
std::vector< ActionSummand > m_action_summands
The action summands of the process.
linear_process_base(const atermpp::aterm &lps, bool stochastic_distributions_allowed=true)
Constructor.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
std::vector< ActionSummand > & action_summands()
Returns the sequence of action summands.
std::size_t summand_count() const
Returns the number of LPS summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const action_summand_vector &action_summands)
Constructor.
linear_process(const atermpp::aterm &lps, bool=false)
Constructor.
linear_process()=default
Constructor.
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
multi_action(const atermpp::aterm &term)
Constructor.
bool has_time() const
Returns true if time is available.
const process::action_list & actions() const
multi_action(const process::action &l)
Constructor.
multi_action operator+(const multi_action &other) const
Joins the actions of both multi actions.
multi_action & operator=(multi_action &&) noexcept=default
const data::data_expression & time() const
multi_action & operator=(const multi_action &) noexcept=default
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor. Actions are sorted to establish the sorted-storage invariant.
process_initializer & operator=(process_initializer &&) noexcept=default
process_initializer(process_initializer &&) noexcept=default
process_initializer(const process_initializer &) noexcept=default
Move semantics.
process_initializer(const data::data_expression_list &expressions)
Constructor.
process_initializer(const atermpp::aterm &term, bool check_distribution=true)
Constructor.
data::data_expression_list expressions() const
process_initializer & operator=(const process_initializer &) noexcept=default
process_initializer()
Default constructor.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
LinearProcess & process()
Returns a reference to the linear process of the specification.
process::action_label_list m_action_labels
The action specification of the specification.
specification_base(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const LinearProcess &lps, const InitialProcessExpression &initial_process)
Constructor.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const InitialProcessExpression & initial_process() const
Returns the initial process.
const LinearProcess & process() const
Returns the linear process of the specification.
process::action_label_list & action_labels()
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
std::set< data::variable > m_global_variables
The set of global variables.
InitialProcessExpression & initial_process()
Returns a reference to the initial process.
specification_base()=default
Constructor.
LinearProcess m_process
The linear process of the specification.
std::set< data::variable > & global_variables()
Returns the declared free variables of the LPS.
data::data_specification m_data
The data specification of the specification.
InitialProcessExpression m_initial_process
The initial state of the specification.
Linear process specification.
specification()=default
Constructor.
specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const linear_process &lps, const process_initializer &initial_process)
Constructor.
LPS summand containing a multi-action.
stochastic_distribution m_distribution
The distribution of the summand.
stochastic_action_summand & operator=(const stochastic_action_summand &) noexcept=default
stochastic_action_summand()=default
Constructor.
stochastic_action_summand(stochastic_action_summand &&) noexcept=default
const stochastic_distribution & distribution() const
Returns the distribution of this summand.
stochastic_action_summand(const action_summand &s)
Constructor.
stochastic_action_summand & operator=(stochastic_action_summand &&) noexcept=default
void swap(stochastic_action_summand &other) noexcept
Swaps the contents.
stochastic_action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments, const stochastic_distribution &distribution)
Constructor.
stochastic_action_summand(const stochastic_action_summand &) noexcept=default
Move semantics.
stochastic_distribution & distribution()
Returns the distribution of this summand.
\brief A stochastic distribution
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
stochastic_distribution(stochastic_distribution &&) noexcept=default
stochastic_distribution()
\brief Default constructor X3.
stochastic_distribution(const stochastic_distribution &) noexcept=default
Move semantics.
const data::variable_list & variables() const
bool is_defined() const
Returns true if the distribution is defined, i.e. it contains a valid distribution....
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
stochastic_distribution & operator=(const stochastic_distribution &) noexcept=default
stochastic_distribution(const atermpp::aterm &term)
const data::data_expression & distribution() const
stochastic_linear_process(const atermpp::aterm &t, bool stochastic_distributions_allowed=true)
Constructor.
stochastic_linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const stochastic_action_summand_vector &action_summands)
Constructor.
stochastic_linear_process()=default
Constructor.
stochastic_linear_process(const linear_process &other)
Constructor.
stochastic_process_initializer(const atermpp::aterm &term)
Constructor.
stochastic_process_initializer(const data::data_expression_list &expressions, const stochastic_distribution &distribution)
Constructor.
const stochastic_distribution & distribution() const
stochastic_specification(const specification &other)
Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.
stochastic_specification()=default
Constructor.
stochastic_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const stochastic_linear_process &lps, const stochastic_process_initializer &initial_process)
Constructor.
Base class for LPS summands.
Definition summand.h:22
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:56
const data::variable_list & summation_variables() const
Returns the sequence of summation variables.
Definition summand.h:49
data::variable_list m_summation_variables
The summation variables of the summand.
Definition summand.h:25
data::data_expression & condition()
Returns the condition expression.
Definition summand.h:63
data::data_expression m_condition
The condition of the summand.
Definition summand.h:28
void swap(summand_base &other) noexcept
Swaps the contents.
Definition summand.h:69
data::variable_list & summation_variables()
Returns the sequence of summation variables.
Definition summand.h:42
summand_base(const data::variable_list &summation_variables, const data::data_expression &condition)
Constructor.
Definition summand.h:35
summand_base()=default
Constructor.
\brief An action label
const data::sort_expression_list & sorts() const
action_label()
\brief Default constructor X3.
action_label(const atermpp::aterm &term)
action_label & operator=(action_label &&) noexcept=default
action_label(const std::string &name, const data::sort_expression_list &sorts)
\brief Constructor Z1.
action_label(action_label &&) noexcept=default
const core::identifier_string & name() const
action_label & operator=(const action_label &) noexcept=default
action_label(const action_label &) noexcept=default
Move semantics.
action_label(const core::identifier_string &name, const data::sort_expression_list &sorts)
\brief Constructor Z12.
\brief A multiset of action names
action_name_multiset & operator=(action_name_multiset &&) noexcept=default
const core::identifier_string_list & names() const
action_name_multiset & operator=(const action_name_multiset &) noexcept=default
action_name_multiset(const atermpp::aterm &term)
Constructor from aterm.
action_name_multiset(const action_name_multiset &) noexcept=default
Move semantics.
action_name_multiset(action_name_multiset &&) noexcept=default
action_name_multiset(const core::identifier_string_list &names)
Constructor. Names are sorted lexicographically to establish the sorted-storage invariant.
action(const action_label &label, const data::data_expression_list &arguments)
\brief Constructor Z14.
action & operator=(action &&) noexcept=default
action()
\brief Default constructor X3.
action(const atermpp::aterm &term)
action(action &&) noexcept=default
action & operator=(const action &) noexcept=default
const data::data_expression_list & arguments() const
action(const action &) noexcept=default
Move semantics.
const action_label & label() const
\brief The allow operator
allow(const allow &) noexcept=default
Move semantics.
allow()
\brief Default constructor X3.
allow(const atermpp::aterm &term)
const process_expression & operand() const
allow(const action_name_multiset_list &allow_set, const process_expression &operand)
\brief Constructor Z14.
allow(allow &&) noexcept=default
const action_name_multiset_list & allow_set() const
allow & operator=(allow &&) noexcept=default
allow & operator=(const allow &) noexcept=default
\brief The at operator
at(at &&) noexcept=default
at(const atermpp::aterm &term)
at(const at &) noexcept=default
Move semantics.
at()
\brief Default constructor X3.
at & operator=(const at &) noexcept=default
at(const process_expression &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
const data::data_expression & time_stamp() const
at & operator=(at &&) noexcept=default
const process_expression & operand() const
\brief The block operator
block & operator=(block &&) noexcept=default
block & operator=(const block &) noexcept=default
const process_expression & operand() const
block(block &&) noexcept=default
block(const block &) noexcept=default
Move semantics.
block(const atermpp::aterm &term)
block(const core::identifier_string_list &block_set, const process_expression &operand)
Constructor. block_set is sorted lexicographically to establish the sorted-storage invariant.
const core::identifier_string_list & block_set() const
\brief The bounded initialization
bounded_init(const bounded_init &) noexcept=default
Move semantics.
bounded_init & operator=(const bounded_init &) noexcept=default
const process_expression & right() const
bounded_init(bounded_init &&) noexcept=default
bounded_init(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
bounded_init(const atermpp::aterm &term)
const process_expression & left() const
bounded_init()
\brief Default constructor X3.
bounded_init & operator=(bounded_init &&) noexcept=default
\brief The choice operator
choice(const atermpp::aterm &term)
choice & operator=(const choice &) noexcept=default
choice(const choice &) noexcept=default
Move semantics.
choice()
\brief Default constructor X3.
const process_expression & left() const
choice(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
choice(choice &&) noexcept=default
const process_expression & right() const
choice & operator=(choice &&) noexcept=default
\brief The communication operator
comm & operator=(const comm &) noexcept=default
comm(const atermpp::aterm &term)
comm(comm &&) noexcept=default
comm & operator=(comm &&) noexcept=default
comm(const comm &) noexcept=default
Move semantics.
const communication_expression_list & comm_set() const
comm(const communication_expression_list &comm_set, const process_expression &operand)
\brief Constructor Z14.
const process_expression & operand() const
comm()
\brief Default constructor X3.
const core::identifier_string & name() const
communication_expression()
\brief Default constructor X3.
communication_expression & operator=(const communication_expression &) noexcept=default
communication_expression(const action_name_multiset &action_name, const std::string &name)
\brief Constructor Z1.
communication_expression(const communication_expression &) noexcept=default
Move semantics.
communication_expression(communication_expression &&) noexcept=default
communication_expression & operator=(communication_expression &&) noexcept=default
communication_expression(const action_name_multiset &action_name, const core::identifier_string &name)
\brief Constructor Z12.
const action_name_multiset & action_name() const
\brief The value delta
delta & operator=(const delta &) noexcept=default
delta()
\brief Default constructor X3.
delta(const atermpp::aterm &term)
delta(delta &&) noexcept=default
delta(const delta &) noexcept=default
Move semantics.
delta & operator=(delta &&) noexcept=default
\brief The hide operator
hide(hide &&) noexcept=default
hide(const atermpp::aterm &term)
hide(const core::identifier_string_list &hide_set, const process_expression &operand)
\brief Constructor Z14.
const core::identifier_string_list & hide_set() const
hide & operator=(const hide &) noexcept=default
const process_expression & operand() const
hide(const hide &) noexcept=default
Move semantics.
hide & operator=(hide &&) noexcept=default
hide()
\brief Default constructor X3.
\brief The if-then-else operator
const process_expression & else_case() const
if_then_else(if_then_else &&) noexcept=default
const process_expression & then_case() const
if_then_else(const atermpp::aterm &term)
if_then_else()
\brief Default constructor X3.
if_then_else & operator=(const if_then_else &) noexcept=default
if_then_else(const if_then_else &) noexcept=default
Move semantics.
const data::data_expression & condition() const
if_then_else & operator=(if_then_else &&) noexcept=default
if_then_else(const data::data_expression &condition, const process_expression &then_case, const process_expression &else_case)
\brief Constructor Z14.
\brief The if-then operator
const process_expression & then_case() const
if_then & operator=(const if_then &) noexcept=default
if_then(const data::data_expression &condition, const process_expression &then_case)
\brief Constructor Z14.
if_then(const atermpp::aterm &term)
const data::data_expression & condition() const
if_then(const if_then &) noexcept=default
Move semantics.
if_then & operator=(if_then &&) noexcept=default
if_then(if_then &&) noexcept=default
if_then()
\brief Default constructor X3.
\brief The left merge operator
left_merge(left_merge &&) noexcept=default
const process_expression & right() const
left_merge & operator=(left_merge &&) noexcept=default
left_merge(const atermpp::aterm &term)
left_merge & operator=(const left_merge &) noexcept=default
left_merge(const left_merge &) noexcept=default
Move semantics.
left_merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & left() const
left_merge()
\brief Default constructor X3.
\brief The merge operator
merge(const atermpp::aterm &term)
const process_expression & right() const
const process_expression & left() const
merge & operator=(const merge &) noexcept=default
merge(const merge &) noexcept=default
Move semantics.
merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
merge & operator=(merge &&) noexcept=default
merge(merge &&) noexcept=default
merge()
\brief Default constructor X3.
\brief A process equation
process_equation()
\brief Default constructor X3.
process_equation(const process_equation &) noexcept=default
Move semantics.
const data::variable_list & formal_parameters() const
process_equation & operator=(process_equation &&) noexcept=default
const process_identifier & identifier() const
const process_expression & expression() const
process_equation(process_equation &&) noexcept=default
process_equation & operator=(const process_equation &) noexcept=default
process_equation(const process_identifier &identifier, const data::variable_list &formal_parameters, const process_expression &expression)
\brief Constructor Z12.
process_equation(const atermpp::aterm &term)
\brief A process expression
process_expression & operator=(const process_expression &) noexcept=default
process_expression(const process_expression &) noexcept=default
Move semantics.
process_expression()
\brief Default constructor X3.
process_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
process_expression(process_expression &&) noexcept=default
process_expression(const atermpp::aterm &term)
process_expression & operator=(process_expression &&) noexcept=default
\brief A process identifier
process_identifier(const process_identifier &) noexcept=default
Move semantics.
const data::variable_list & variables() const
process_identifier & operator=(const process_identifier &) noexcept=default
process_identifier(process_identifier &&) noexcept=default
process_identifier(const core::identifier_string &name, const data::variable_list &variables)
Constructor.
const core::identifier_string & name() const
process_identifier & operator=(process_identifier &&) noexcept=default
process_identifier(const std::string &name, const data::variable_list &variables)
Constructor.
process_identifier(const atermpp::aterm &term)
Constructor.
process_instance_assignment(const process_instance_assignment &) noexcept=default
Move semantics.
process_instance_assignment()
\brief Default constructor X3.
process_instance_assignment(const process_identifier &identifier, const data::assignment_list &assignments)
\brief Constructor Z14.
process_instance_assignment & operator=(const process_instance_assignment &) noexcept=default
process_instance_assignment(process_instance_assignment &&) noexcept=default
const data::assignment_list & assignments() const
process_instance_assignment(const atermpp::aterm &term)
process_instance_assignment & operator=(process_instance_assignment &&) noexcept=default
const process_identifier & identifier() const
const data::data_expression_list & actual_parameters() const
process_instance(const process_identifier &identifier, const data::data_expression_list &actual_parameters)
\brief Constructor Z14.
process_instance & operator=(const process_instance &) noexcept=default
process_instance & operator=(process_instance &&) noexcept=default
const process_identifier & identifier() const
process_instance(process_instance &&) noexcept=default
process_instance()
\brief Default constructor X3.
process_instance(const atermpp::aterm &term)
process_instance(const process_instance &) noexcept=default
Move semantics.
Process specification consisting of a data specification, action labels, a sequence of process equati...
const std::vector< process_equation > & equations() const
Returns the equations of the process specification.
process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init)
Constructor that sets the global variables to empty;.
process::action_label_list m_action_labels
The action specification of the specification.
process_specification()=default
Constructor.
process_expression & init()
Returns the initialization of the process specification.
const process_expression & init() const
Returns the initialization of the process specification.
process_specification(data::data_specification data, process::action_label_list action_labels, data::variable_list global_variables, process_equation_list equations, process_expression init)
Constructor of a process specification.
std::vector< process_equation > & equations()
Returns the equations of the process specification.
process_specification(atermpp::aterm t)
Constructor.
std::set< data::variable > m_global_variables
The set of global variables.
std::vector< process_equation > m_equations
The equations of the specification.
const process::action_label_list & action_labels() const
Returns the action label specification.
data::data_specification m_data
The data specification of the specification.
process_expression m_initial_process
The initial state of the specification.
process::action_label_list & action_labels()
Returns the action label specification.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the process specification.
void construct_from_aterm(const atermpp::aterm &t)
Initializes the specification with an aterm.
std::set< data::variable > & global_variables()
Returns the declared free variables of the process specification.
\brief A rename expression
const core::identifier_string & source() const
rename_expression()
\brief Default constructor X3.
rename_expression & operator=(rename_expression &&) noexcept=default
rename_expression & operator=(const rename_expression &) noexcept=default
rename_expression(core::identifier_string &source, core::identifier_string &target)
\brief Constructor Z12.
const core::identifier_string & target() const
rename_expression(const atermpp::aterm &term)
rename_expression(rename_expression &&) noexcept=default
rename_expression(const std::string &source, const std::string &target)
\brief Constructor Z1.
rename_expression(const rename_expression &) noexcept=default
Move semantics.
\brief The rename operator
rename(const atermpp::aterm &term)
rename & operator=(const rename &) noexcept=default
rename(const rename &) noexcept=default
Move semantics.
rename()
\brief Default constructor X3.
const process_expression & operand() const
rename & operator=(rename &&) noexcept=default
rename(rename &&) noexcept=default
rename(const rename_expression_list &rename_set, const process_expression &operand)
\brief Constructor Z14.
const rename_expression_list & rename_set() const
\brief The sequential composition
seq & operator=(seq &&) noexcept=default
const process_expression & right() const
seq(const atermpp::aterm &term)
seq()
\brief Default constructor X3.
seq & operator=(const seq &) noexcept=default
const process_expression & left() const
seq(seq &&) noexcept=default
seq(const seq &) noexcept=default
Move semantics.
seq(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
stochastic_operator & operator=(stochastic_operator &&) noexcept=default
stochastic_operator()
\brief Default constructor X3.
stochastic_operator(const atermpp::aterm &term)
stochastic_operator(stochastic_operator &&) noexcept=default
stochastic_operator(const stochastic_operator &) noexcept=default
Move semantics.
stochastic_operator & operator=(const stochastic_operator &) noexcept=default
const process_expression & operand() const
stochastic_operator(const data::variable_list &variables, const data::data_expression &distribution, const process_expression &operand)
\brief Constructor Z14.
\brief The sum operator
const process_expression & operand() const
sum(const data::variable_list &variables, const process_expression &operand)
\brief Constructor Z14.
sum(const atermpp::aterm &term)
sum & operator=(sum &&) noexcept=default
sum()
\brief Default constructor X3.
const data::variable_list & variables() const
sum(sum &&) noexcept=default
sum(const sum &) noexcept=default
Move semantics.
sum & operator=(const sum &) noexcept=default
\brief The synchronization operator
sync & operator=(const sync &) noexcept=default
sync(sync &&) noexcept=default
sync(const sync &) noexcept=default
Move semantics.
const process_expression & left() const
sync()
\brief Default constructor X3.
sync & operator=(sync &&) noexcept=default
sync(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & right() const
sync(const atermpp::aterm &term)
\brief The value tau
tau(const tau &) noexcept=default
Move semantics.
tau()
\brief Default constructor X3.
tau(const atermpp::aterm &term)
tau & operator=(tau &&) noexcept=default
tau & operator=(const tau &) noexcept=default
tau(tau &&) noexcept=default
\brief An untyped multi action or data application
untyped_multi_action(const data::untyped_data_parameter_list &actions)
\brief Constructor Z12.
untyped_multi_action & operator=(untyped_multi_action &&) noexcept=default
untyped_multi_action(untyped_multi_action &&) noexcept=default
untyped_multi_action & operator=(const untyped_multi_action &) noexcept=default
const data::untyped_data_parameter_list & actions() const
untyped_multi_action(const atermpp::aterm &term)
untyped_multi_action()
\brief Default constructor X3.
untyped_multi_action(const untyped_multi_action &) noexcept=default
Move semantics.
\brief An untyped process assginment
untyped_process_assignment & operator=(untyped_process_assignment &&) noexcept=default
const data::untyped_identifier_assignment_list & assignments() const
untyped_process_assignment(const core::identifier_string &name, const data::untyped_identifier_assignment_list &assignments)
\brief Constructor Z14.
untyped_process_assignment(const atermpp::aterm &term)
const core::identifier_string & name() const
untyped_process_assignment()
\brief Default constructor X3.
untyped_process_assignment & operator=(const untyped_process_assignment &) noexcept=default
untyped_process_assignment(const std::string &name, const data::untyped_identifier_assignment_list &assignments)
\brief Constructor Z2.
untyped_process_assignment(untyped_process_assignment &&) noexcept=default
untyped_process_assignment(const untyped_process_assignment &) noexcept=default
Move semantics.
process_expression processbody
objectdatatype(const objectdatatype &o)=default
process_expression representedprocess
~objectdatatype()=default
process::action_label_list multi_action_names
processstatustype processstatus
identifier_string objectname
std::set< variable > get_free_variables() const
objectdatatype()=default
objectdatatype & operator=(const objectdatatype &o)=default
objecttype object
process_identifier process_representing_action
variable_list parameters
enumeratedtype(const enumeratedtype &e)
enumeratedtype(const std::size_t n, specification_basic_type &spec)
enumeratedtype & operator=(const enumeratedtype &e)=default
enumtype(const enumtype &)=delete
enumtype & operator=(const enumtype &)=delete
enumtype(std::size_t n, const sort_expression_list &fsorts, const sort_expression_list &gsorts, specification_basic_type &spec)
process_pid_pair & operator=(const process_pid_pair &other)=default
const process_expression & process_body() const
const process_identifier & process_id() const
process_pid_pair(const process_pid_pair &other)=default
process_pid_pair & operator=(process_pid_pair &&other)=default
process_pid_pair(const process_expression &process_body, const process_identifier &pid)
process_pid_pair(process_pid_pair &&other)=default
static stackoperations * find_suitable_stack_operations(const variable_list &parameters, stackoperations *stack_operations_list)
stacklisttype & operator=(const stacklisttype &)=delete
stacklisttype(const variable_list &parlist, specification_basic_type &spec, const bool regular, const std::set< process_identifier > &pCRLprocs, const bool singlecontrolstate)
Constructor.
stacklisttype(const stacklisttype &)=delete
stackoperations & operator=(const stackoperations &)=delete
stackoperations(const stackoperations &)=delete
stackoperations(const variable_list &pl, specification_basic_type &spec)
process_expression procstorealGNFbody(const process_expression &body, variableposition v, std::vector< process_identifier > &todo, const bool regular, processstatustype mode, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
data_expression construct_binary_case_tree(std::size_t n, const variable_list &sums, data_expression_list terms, const sort_expression &termsort, const enumtype &e)
data::maintain_variables_in_rhs< data::mutable_map_substitution<> > make_unique_variables(const variable_list &var_list, const std::string &hint)
variable_list parscollect(const process_expression &oldbody, process_expression &newbody)
stochastic_action_summand collect_sum_arg_arg_cond(const enumtype &e, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
action_list linMergeMultiActionList(const action_list &ma1, const action_list &ma2)
void generateLPEpCRL(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procId, const bool containstime, const bool regular, variable_list &parameters, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution)
variable get_fresh_variable(const std::string &s, const sort_expression &sort, const int reuse_index=-1)
process_expression distributeActionOverConditions(const process_expression &act, const data_expression &condition, const process_expression &restterm, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
data_expression construct_binary_case_tree_rec(std::size_t n, const variable_list &sums, data_expression_list &terms, const sort_expression &termsort, const enumtype &e)
static void complete_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map)
process_expression to_regular_form(const process_expression &t, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
void collectsumlistterm(const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &body, const variable_list &pars, const stacklisttype &stack, const bool regular, const bool singlestate, const std::set< process_identifier > &pCRLprocs)
data_expression_list findarguments(const variable_list &pars, const variable_list &parlist, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
void calculate_communication_merge(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void insertvariable(const variable &var, const bool mustbenew)
process_identifier storeinit(const process_expression &init)
static action_list to_sorted_action_list(const process_expression &p)
Convert the process expression to a sorted action list.
process_expression pCRLrewrite(const process_expression &t)
data_expression_list pushdummy_regular_data_expressions(const variable_list &pars, const stacklisttype &stack)
void define_equations_for_case_function(const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)
void alphaconvert(variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
bool canterminatebody(const process_expression &t)
data_expression transform_matching_list(const variable_list &matchinglist)
void add_summands(const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, process_expression summandterm, const std::set< process_identifier > &pCRLprocs, const stacklisttype &stack, const bool regular, const bool singlestate, const variable_list &process_parameters)
bool isDeltaAtZero(const process_expression &t)
data::function_symbol find_case_function(std::size_t index, const sort_expression &sort) const
data_expression_list make_initialstate(const process_identifier &initialProcId, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool regular, const bool singlecontrolstate, const stochastic_distribution &initial_stochastic_distribution)
static bool summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
static sort_expression_list getActionSorts(const action_list &actionlist)
void filter_vars_by_multiaction(const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
static process_identifier get_last(const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
static bool check_real_variable_occurrence(const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)
process_identifier newprocess(const variable_list &parameters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)
void make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)
void filter_vars_by_term(const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list pushdummy_stack(const variable_list &parameters, const stacklisttype &stack, const variable_list &stochastic_variables)
void procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)
static action_label_list getnames(const process_expression &multiAction)
variable_list getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)
static int match_sequence(const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
assignment_list argscollect_regular2(const process_expression &t, variable_list &vl)
assignment_list make_optimised_assignment_list(const variable_list &parameters, const data_expression_list &resultnextstate, const variable_list &sum_vars, const variable_list &stoch_vars)
void calculate_left_merge_action(const lps::detail::ultimate_delay &ultimate_delay_condition, const stochastic_action_summand_vector &action_summands1, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)
process_expression split_body(const process_expression &t, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc, const variable_list &parameters)
void parallelcomposition(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const variable_list &pars1, const data_expression_list &init1, const stochastic_distribution &initial_stochastic_distribution1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const variable_list &pars2, const data_expression_list &init2, const stochastic_distribution &initial_stochastic_distribution2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars_result, data_expression_list &init_result, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
bool occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) const
void transform_process_arguments(const process_identifier &procId)
objectdatatype & insert_process_declaration(const process_identifier &procId, const variable_list &parameters, const process_expression &body, processstatustype s, const bool canterminate, const bool containstime)
static void set_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map, const process_identifier &id1_, const process_identifier &id2_, const process_identifier &initial_process)
bool canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)
set_identifier_generator fresh_identifier_generator
std::set< process_identifier > remove_stochastic_operators_from_front(const std::set< process_identifier > &reachable_process_identifiers, process_identifier &initial_process_id, stochastic_distribution &initial_stochastic_distribution)
void filter_vars_by_termlist(Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
bool searchProcDeclaration(const variable_list &parameters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p) const
process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)
action_list linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)
std::vector< process_equation > procs
action_list adapt_multiaction_to_stack(const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)
void determinewhetherprocessescanterminate(const process_identifier &procId)
process_expression distribute_condition(const process_expression &body1, const data_expression &condition)
bool containstime_rec(const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)
void collectsumlist(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const std::set< process_identifier > &pCRLprocs, const variable_list &pars, const stacklisttype &stack, bool regular, bool singlestate)
data_expression correctstatecond(const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)
void calculate_communication_merge_action_summands(const stochastic_action_summand_vector &action_summands1, const stochastic_action_summand_vector &action_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)
processstatustype determine_process_statusterm(const process_expression &body, const processstatustype status)
void calculate_communication_merge_action_deadlock_summands(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
data_expression getvar(const variable &var, const stacklisttype &stack) const
variable_list initdatavars
lps::detail::ultimate_delay combine_ultimate_delays(const lps::detail::ultimate_delay &delay1, const lps::detail::ultimate_delay &delay2)
Returns the conjunction of the two delay conditions and the join of the variables,...
process_expression distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)
data_expression_list pushdummyrec_stack(const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
static action_list to_action_list(const process_expression &p)
std::set< data::variable > sigma_variables(const Substitution &sigma)
void combine_summand_lists(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const variable_list &par1, const variable_list &par3, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
process_expression cut_off_unreachable_tail(const process_expression &t)
std::vector< enumeratedtype > enumeratedtypes
data_expression find_(const variable &s, const assignment_list &args, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
process::action_label_list acts
assignment_list make_procargs_regular(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool singlestate, const variable_list &stochastic_variables)
std::size_t create_enumeratedtype(const std::size_t n)
void generateLPEmCRL(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procIdDecl, const bool regular, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)
static process_expression delta_at_zero()
assignment_list rewrite_assignments(const assignment_list &t)
assignment_list push_regular(const process_identifier &procId, const assignment_list &args, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, bool singlestate, const variable_list &stochastic_variables)
void transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)
std::set< process_identifier > minimize_set_of_reachable_process_identifiers(const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
variable_list make_binary_sums(std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)
variable_list SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)
data_expression_list extend_conditions(const variable &var, const data_expression_list &conditionlist)
bool check_valid_process_instance_assignment(const process_identifier &id, const assignment_list &assignments)
void calculate_left_merge_deadlock(const lps::detail::ultimate_delay &ultimate_delay_condition, const deadlock_summand_vector &deadlock_summands1, const bool is_allow, const bool is_block, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void addString(const identifier_string &str)
void procstovarheadGNF(const std::vector< process_identifier > &procs)
static process_expression action_list_to_process(const action_list &ma)
process_expression distribute_sum_over_a_stochastic_operator(const variable_list &sumvars, const variable_list &stochastic_variables, const data_expression &distribution, const process_expression &body)
void alphaconvertprocess(variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
process_expression obtain_initial_distribution_term(const process_expression &t)
data_expression push_stack(const process_identifier &procId, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, const variable_list &vars, const variable_list &stochastic_variables)
void calculate_left_merge(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void declare_control_state(const std::set< process_identifier > &pCRLprocs)
void create_case_function_on_enumeratedtype(const sort_expression &sort, const std::size_t enumeratedtype_index)
variable_list SieveProcDataVarsSummands(const std::set< variable > &vars, const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)
static data_expression_list extend(const data_expression &c, const data_expression_list &cl)
specification_basic_type & operator=(const specification_basic_type &)=delete
static bool occursinvarandremove(const variable &var, variable_list &vl)
process_expression bodytovarheadGNF(const process_expression &body, const state s, const variable_list &freevars, const variableposition v, const std::set< variable > &variables_bound_in_sum)
process_identifier terminatedProcId
process_expression distribute_sum(const variable_list &sumvars, const process_expression &body1)
data_expression variables_are_equal_to_default_values(const variable_list &vl)
void procstorealGNF(const process_identifier &procsIdDecl, const bool regular)
static bool check_assignment_list(const assignment_list &assignments, const variable_list &parameters)
data_expression RewriteTerm(const data_expression &t)
void alphaconversion(const process_identifier &procId, const variable_list &parameters)
bool all_equal(const atermpp::term_list< T > &l)
void cluster_actions(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)
process_expression transform_initial_distribution_term(const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)
process_expression create_regular_invocation(process_expression sequence, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
process_expression transform_process_arguments_body(const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)
static assignment_list parameters_to_assignment_list(const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)
assignment_list dummyparameterlist(const stacklisttype &stack, const bool singlestate)
mcrl2::data::rewriter rewr
void make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)
stackoperations * stack_operations_list
process_expression wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)
objectdatatype & objectIndex(const process_identifier &o)
process_identifier split_process(const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)
bool mergeoccursin(variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)
static bool occursintermlist(const variable &var, const data_expression_list &r)
bool exists_variable_for_sequence(const std::vector< process_instance_assignment > &process_names, process_identifier &result)
std::set< variable > find_free_variables_process(const process_expression &p)
process_expression alphaconversionterm(const process_expression &t, const variable_list &parameters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)
process_expression putbehind(const process_expression &body1, const process_expression &body2)
assignment_list substitute_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
process_instance_assignment transform_process_instance_to_process_instance_assignment(const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())
process_instance_assignment RewriteProcess(const process_instance_assignment &t)
process_identifier delta_process
const objectdatatype & objectIndex(const process_identifier &o) const
void insert_summand(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &sumvars, const data_expression &condition, const action_list &multiAction, const data_expression &actTime, const stochastic_distribution &distribution, const assignment_list &procargs, const bool has_time, const bool is_deadlock_summand)
bool alreadypresent(variable &var, const variable_list &vl, mutable_indexed_substitution<> &parameter_renaming)
variable_list parameters_that_occur_in_body(const variable_list &parameters, const process_expression &body)
process_expression enumerate_distribution_and_sums(const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)
bool containstimebody(const process_expression &t)
assignment_list make_procargs(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const bool regular, const bool singlestate, const variable_list &stochastic_variables)
data_expression adapt_term_to_stack(const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression_list processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)
process_expression RewriteMultAct(const process_expression &t)
void generateLPEmCRLterm(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &t, const bool regular, const bool rename_variables, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
Linearise a process indicated by procIdDecl.
variable_list make_pars(const sort_expression_list &sortlist)
specification_basic_type(const specification_basic_type &)=delete
static data_expression real_times_optimized(const data_expression &r1, const data_expression &r2)
bool occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)
static std::size_t upperpowerof2(std::size_t i)
void extract_names(const process_expression &sequence, std::vector< process_instance_assignment > &result)
std::map< aterm, objectdatatype > objectdata
action RewriteAction(const action &t)
data_expression_vector adapt_termlist_to_stack(Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression make_procargs_stack(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const variable_list &stochastic_variables)
specification_basic_type(const process::action_label_list &as, const std::vector< process_equation > &ps, const variable_list &idvs, const data_specification &ds, const std::set< data::variable > &glob_vars, const t_lin_options &opt, const process_specification &procspec)
variable_list getparameters(const process_expression &multiAction)
data_expression makesingleultimatedelaycondition(const variable_list &sumvars, const variable_list &freevars, const data_expression &condition, const bool has_time, const variable &timevariable, const data_expression &actiontime, variable_list &used_sumvars)
void collectPcrlProcesses_term(const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
data_expression representative_generator_internal(const sort_expression &s, const bool allow_dont_care_var=true)
assignment_list processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)
objectdatatype & addMultiAction(const process_expression &multiAction, bool &isnew)
void storeprocs(const std::vector< process_equation > &procs)
process_expression substitute_pCRLproc(const process_expression &p, Substitution &sigma)
void make_parameters_and_sum_variables_unique(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars, lps::detail::ultimate_delay &ultimate_delay_condition, const std::string &hint="")
std::set< variable > global_variables
static data_expression getRHSassignment(const variable &var, const assignment_list &as)
variable_list construct_renaming(const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
void determine_process_status(const process_identifier &procDecl, const processstatustype status)
static action_list makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)
void insertvariables(const variable_list &vars, const bool mustbenew)
variable_list collectparameterlist(std::set< process_identifier > &pCRLprocs)
data_expression_list RewriteTermList(const data_expression_list &t)
data_specification data
variable_list make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)
void detail_check_objectdata(const process_identifier &o) const
static assignment_list filter_assignments(const assignment_list &assignments, const variable_list &parameters)
variable_list merge_var(const variable_list &v1, const variable_list &v2, std::vector< variable_list > &renamings_pars, std::vector< data_expression_list > &renamings_args, data_expression_list &conditionlist, const variable_list &process_parameters)
bool containstimebody(const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)
static assignment_list sort_assignments(const assignment_list &ass, const variable_list &parameters)
assignment_list find_dummy_arguments(const variable_list &parlist, const assignment_list &args, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
process_identifier tau_process
static sort_expression_list get_sorts(const List &l)
std::vector< process_identifier > seq_varnames
void storeact(const process::action_label_list &acts)
bool is_global_variable(const data_expression &d) const
variable_list joinparameters(const variable_list &par1, const variable_list &par2, mutable_indexed_substitution<> &parameter_renaming)
static bool occursin(const variable &name, const variable_list &pars)
bool canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)
void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)
bool determinewhetherprocessescontaintime(const process_identifier &procId)
void filter_vars_by_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)
void calculate_communication_merge_deadlock_summands(const deadlock_summand_vector &deadlock_summands1, const deadlock_summand_vector &deadlock_summands2, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void transform(const process_identifier &init, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &parameters, data_expression_list &initial_state, stochastic_distribution &initial_stochastic_distribution)
process_expression obtain_initial_distribution(const process_identifier &procId)
objectdatatype & insertAction(const action_label &actionId)
Expression replace_variables_capture_avoiding_alt(const Expression &e, Substitution &sigma)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t, std::set< process_identifier > &visited_processes)
assignment_list pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
assignment_list argscollect_regular(const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)
static data_expression_list getarguments(const action_list &multiAction)
lps::detail::ultimate_delay getUltimateDelayCondition(const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:393
void optimized_forall(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make a universal quantification.
void split_condition(const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression > &non_real_conditions)
This function first splits the given condition e into real conditions and non real conditions....
lhs_t map_to_lhs_type(const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
data_expression negate_inequality(const data_expression &e)
void optimized_exists(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make an existential quantification.
void optimized_or(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a disjunction.
lhs_t map_to_lhs_type(const map_based_lhs_t &lhs)
std::string pp(const detail::comparison_t t)
variable_list set_intersection(const variable_list &x, const variable_list &y)
Returns the intersection of two unordered sets, that are stored in ATerm lists.
lhs_t set_factor_for_a_variable(const lhs_t &lhs, const variable &x, const data_expression &e)
void optimized_imp(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits t)
Make an implication.
const data_expression & else_part(const data_expression &e)
bool is_well_formed(const lhs_t &lhs)
bool is_inequality(const data_expression &e)
Determine whether a data expression is an inequality.
detail::comparison_t negate(const detail::comparison_t t)
const data_expression & condition_part(const data_expression &e)
lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
std::string pp(const detail::lhs_t &lhs)
const data_expression & then_part(const data_expression &e)
void optimized_not(typename TermTraits::term_type &result, const typename TermTraits::term_type &arg, TermTraits)
static bool split_condition_aux(const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression_list > &non_real_conditions, const bool negate=false)
Splits a condition in expressions ranging over reals and the others.
void set_factor_for_a_variable(detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
variable_list set_difference(const variable_list &x, const variable_list &y)
Returns the difference of two unordered sets, that are stored in aterm lists.
void optimized_and(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a conjunction and optimize it if possible.
atermpp::function_symbol f_variable_with_a_rational_factor()
A collection of utilities for lazy expression construction.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
Namespace for system defined sort bool_.
Definition bool.h:29
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:342
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:490
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:406
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:194
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:321
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:106
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:278
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:214
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:74
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:478
Namespace for system defined sort real_.
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1056
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1234
bool is_zero(const atermpp::aterm &e)
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1404
data_expression & real_one()
bool is_one(const atermpp::aterm &e)
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1133
data_expression & real_zero()
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:150
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1149
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:45
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:55
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1282
bool is_larger_zero(const atermpp::aterm &e)
Functions that returns true if e is a closed real number larger than zero.
function_symbol abs(const sort_expression &s0)
Definition real1.h:732
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1303
function_symbol negate(const sort_expression &s0)
Definition real1.h:807
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:874
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1218
linear_inequality subtract(const linear_inequality &e1, const linear_inequality &e2, const data_expression &f1, const data_expression &f2, const rewriter &r)
Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.
application real_times(const data_expression &arg0, const data_expression &arg1)
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
data_expression & real_one()
void optimized_exists_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
bool is_closed_real_number(const data_expression &e)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
application real_plus(const data_expression &arg0, const data_expression &arg1)
data_expression & real_minus_one()
bool is_simple_substitution(const map_substitution< AssociativeContainer > &sigma)
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
bool is_positive(const data_expression &e, const rewriter &r)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:291
application real_abs(const data_expression &arg)
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:254
std::set< data::variable > substitution_variables(const map_substitution< AssociativeContainer > &sigma)
std::string pp_vector(const TYPE &inequalities)
Print the vector of inequalities to stderr in readable form.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:215
void remove_redundant_inequalities(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
Remove every redundant inequality from a vector of inequalities.
application real_minus(const data_expression &arg0, const data_expression &arg1)
map_substitution< AssociativeContainer > make_map_substitution(const AssociativeContainer &m)
Utility function for creating a map_substitution.
void fourier_motzkin(const data_expression &e_in, const variable_list &vars_in, data_expression &e_out, variable_list &vars_out, const rewriter &r)
Eliminate variables from a data expression using Gauss elimination and Fourier-Motzkin elimination.
bool is_simple_substitution(const assignment_sequence_substitution &sigma)
std::string pp(const linear_inequality &l)
application real_divides(const data_expression &arg0, const data_expression &arg1)
std::set< variable > gauss_elimination(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_equalities, std::vector< linear_inequality > &resulting_inequalities, Variable_iterator variables_begin, Variable_iterator variables_end, const rewriter &r)
Try to eliminate variables from a system of inequalities using Gauss elimination.
void optimized_imp(Term &result, const Term &p, const Term &q)
Make an implication.
bool is_zero(const data_expression &e)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
void fourier_motzkin(const std::vector< linear_inequality > &inequalities_in, Data_variable_iterator variables_begin, Data_variable_iterator variables_end, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
data_expression & real_zero()
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:328
bool is_untyped_data_parameter(const atermpp::aterm &x)
void optimized_forall_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
application real_negate(const data_expression &arg)
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in, const rewriter &r, bool use_cache=true)
Determine whether a list of data expressions is inconsistent.
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_negative(const data_expression &e, const rewriter &r)
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:140
void optimized_not(Term &result, const Term &arg)
Make a negation.
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
void swap(data_expression &t1, data_expression &t2) noexcept
\brief swap overload
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
void replace_global_variables(Specification &lpsspec, const data::mutable_map_substitution<> &sigma)
Applies a global variable substitution to an LPS.
stochastic_action_summand_vector convert_action_summands(const action_summand_vector &action_summands)
data::mutable_map_substitution instantiate_global_variables(Specification &lpsspec)
Eliminates the global variables of an LPS, by substituting a constant value for them....
Summand make_action_summand(const data::variable_list &, const data::data_expression &, const multi_action &, const data::assignment_list &, const stochastic_distribution &)
The main namespace for the LPS library.
Definition constelm.h:18
std::set< core::identifier_string > find_identifiers(const T &x)
Definition find.h:102
std::ostream & operator<<(std::ostream &out, const stochastic_process_initializer &x)
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:135
std::ostream & operator<<(std::ostream &out, const stochastic_distribution &x)
std::string pp(const lps::stochastic_specification &x, bool arg0)
Definition lps.cpp:40
std::set< data::variable > find_all_variables(const lps::linear_process &x)
Definition lps.cpp:47
void make_stochastic_distribution(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const lps::specification &x, bool arg0)
Definition lps.cpp:35
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
Definition lps.cpp:46
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
Definition lps.cpp:56
std::string pp(const lps::stochastic_distribution &x, bool arg0)
Definition lps.cpp:37
std::string pp_extended(const stochastic_specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:98
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
std::set< process::action_label > find_action_labels(const T &x)
Returns all action labels that occur in an object.
Definition find.h:178
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Returns all variables inside a multi-action.
Definition lps.cpp:52
bool search_free_variable(const T &x, const data::variable &v)
Returns true if the term has a given free variable as subterm.
Definition find.h:157
void find_all_variables(const multi_action &x, OutputIterator o)
Returns all variables inside a multi-action.
Definition find.h:189
void swap(action_summand &t1, action_summand &t2) noexcept
\brief swap overload
void swap(deadlock_summand &t1, deadlock_summand &t2) noexcept
\brief swap overload
bool operator!=(const stochastic_specification &spec1, const stochastic_specification &spec2)
Inequality operator.
std::ostream & operator<<(std::ostream &out, const stochastic_linear_process &x)
std::set< data::variable > find_all_variables(const lps::stochastic_specification &x)
Definition lps.cpp:50
std::ostream & operator<<(std::ostream &out, const process_initializer &x)
bool check_well_typedness(const specification &x)
Definition lps.cpp:118
bool is_stochastic_process_initializer(const atermpp::aterm &x)
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
std::ostream & operator<<(std::ostream &out, const specification &x)
std::set< data::variable > find_free_variables(const lps::linear_process &x)
Definition lps.cpp:53
bool is_specification(const atermpp::aterm &x)
Test for a specification expression.
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:108
void swap(deadlock &t1, deadlock &t2) noexcept
\brief swap overload
Definition deadlock.h:105
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:49
void swap(multi_action &t1, multi_action &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const T &x)
Definition find.h:37
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
Definition lps.cpp:62
bool occursinterm(const data::data_expression &t, const data::variable &var)
void find_sort_expressions(const T &x, OutputIterator o)
Definition find.h:114
std::string pp_extended(const specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:88
bool operator<(const stochastic_action_summand &x, const stochastic_action_summand &y)
Comparison operator for action summands.
std::set< data::variable > find_free_variables_with_bound(const T &x, VariableContainer const &bound)
Definition find.h:81
void remove_parameters(Object &x, const std::set< data::variable > &to_be_removed)
Rewrites an LPS data type.
Definition remove.h:187
atermpp::aterm specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm.
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
Definition lps.cpp:66
std::ostream & operator<<(std::ostream &out, const deadlock &x)
Definition deadlock.h:99
std::set< data::variable > find_free_variables(const lps::specification &x)
Definition lps.cpp:55
void constelm(Specification &spec, const DataRewriter &R, bool instantiate_global_variables=false)
Removes zero or more constant parameters from the specification spec.
Definition constelm.h:269
std::ostream & operator<<(std::ostream &out, const action_summand &x)
void normalize_sorts(lps::specification &x, const data::sort_specification &)
Definition lps.cpp:42
atermpp::aterm deadlock_summand_to_aterm(const deadlock_summand &s)
Conversion to atermappl.
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:57
bool operator==(const specification &spec1, const specification &spec2)
Equality operator.
std::string pp(const lps::deadlock_summand &x, bool arg0)
Definition lps.cpp:31
std::set< process::action_label > find_action_labels(const lps::linear_process &x)
Definition lps.cpp:65
lps::multi_action normalize_sorts(const lps::multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:41
std::set< data::variable > find_free_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:54
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
Definition lps.cpp:61
std::string pp(const lps::stochastic_linear_process &x, bool arg0)
Definition lps.cpp:38
std::set< data::variable > find_free_variables(const lps::stochastic_process_initializer &x)
Definition lps.cpp:60
bool operator==(const stochastic_specification &spec1, const stochastic_specification &spec2)
void swap(stochastic_action_summand &t1, stochastic_action_summand &t2) noexcept
\brief swap overload
std::set< data::variable > find_free_variables(const lps::multi_action &x)
Definition lps.cpp:58
std::string pp(const lps::deadlock &x, bool arg0)
Definition lps.cpp:30
std::ostream & operator<<(std::ostream &out, const multi_action &x)
void remove_redundant_assignments(Specification &lpsspec)
Removes redundant assignments of the form x = x from an LPS specification.
Definition remove.h:244
bool operator!=(const specification &spec1, const specification &spec2)
Inequality operator.
void normalize_sorts(lps::stochastic_specification &x, const data::sort_specification &)
Definition lps.cpp:43
std::set< data::variable > find_free_variables(const lps::process_initializer &x)
Definition lps.cpp:59
data::data_expression equal_multi_actions(const multi_action &a, const multi_action &b)
Returns a data expression that expresses under which conditions the multi actions a and b are equal....
bool is_stochastic_distribution(const atermpp::aterm &x)
specification remove_stochastic_operators(const stochastic_specification &spec)
Converts a stochastic specification to a specification. Throws an exception if non-empty distribution...
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
bool is_process_initializer(const atermpp::aterm &x)
void remove_singleton_sorts(Specification &spec)
Removes parameters with a singleton sort from a linear process specification.
Definition remove.h:208
bool check_well_typedness(const Object &o)
std::string pp(const lps::stochastic_action_summand &x, bool arg0)
Definition lps.cpp:36
data::assignment_list remove_redundant_assignments(const data::assignment_list &assignments, const data::variable_list &do_not_remove)
Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove...
Definition remove.h:226
mcrl2::lps::stochastic_specification linearise(const mcrl2::process::process_specification &type_checked_spec, const mcrl2::lps::t_lin_options &lin_options=t_lin_options())
Linearises a process specification.
std::string pp(const lps::stochastic_process_initializer &x, bool arg0)
Definition lps.cpp:39
std::string pp(const lps::linear_process &x, bool arg0)
Definition lps.cpp:32
std::set< data::sort_expression > find_sort_expressions(const T &x)
Definition find.h:123
std::string pp(const lps::multi_action &x, bool arg0)
Definition lps.cpp:33
void make_stochastic_process_initializer(atermpp::aterm &t, ARGUMENTS... args)
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:93
void swap(stochastic_process_initializer &t1, stochastic_process_initializer &t2) noexcept
\brief swap overload
void find_free_variables_with_bound(const T &x, OutputIterator o, const VariableContainer &bound)
Definition find.h:60
std::set< data::variable > find_free_variables(const T &x)
Definition find.h:69
std::ostream & operator<<(std::ostream &out, const stochastic_action_summand &x)
atermpp::aterm linear_process_to_aterm(const linear_process_base< ActionSummand > &p)
Conversion to aterm.
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:45
void make_process_initializer(atermpp::aterm &t, EXPRESSION_LIST args)
bool operator==(const stochastic_action_summand &x, const stochastic_action_summand &y)
Equality operator of stochastic action summands.
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
data::data_expression not_equal_multi_actions(const multi_action &a, const multi_action &b)
Returns a pbes expression that expresses under which conditions the multi actions a and b are not equ...
std::string pp(const lps::action_summand &x, bool arg0)
Definition lps.cpp:29
void remove_trivial_summands(Specification &spec)
Removes summands with condition equal to false from a linear process specification.
Definition remove.h:196
bool operator<(const action_summand &x, const action_summand &y)
Comparison operator for action summands.
std::set< data::variable > find_all_variables(const lps::specification &x)
Definition lps.cpp:49
std::ostream & operator<<(std::ostream &out, const linear_process &x)
bool check_well_typedness(const stochastic_specification &x)
Definition lps.cpp:123
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:51
atermpp::aterm action_summand_to_aterm(const action_summand &s)
Conversion to aterm.
std::set< data::variable > find_all_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:48
bool check_well_typedness(const stochastic_linear_process &x)
Definition lps.cpp:113
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:44
void swap(stochastic_distribution &t1, stochastic_distribution &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const stochastic_specification &x)
void find_all_variables(const T &x, OutputIterator o)
Definition find.h:28
std::set< core::identifier_string > find_identifiers(const lps::stochastic_specification &x)
Definition lps.cpp:64
std::set< data::function_symbol > find_function_symbols(const T &x)
Definition find.h:144
void find_action_labels(const T &x, OutputIterator o)
Returns all action labels that occur in an object.
Definition find.h:169
atermpp::aterm action_summand_to_aterm(const stochastic_action_summand &s)
Conversion to aterm.
void swap(process_initializer &t1, process_initializer &t2) noexcept
\brief swap overload
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
Definition lps.cpp:63
std::ostream & operator<<(std::ostream &out, const deadlock_summand &x)
std::set< process::action_label > find_action_labels(const lps::specification &x)
Definition lps.cpp:67
std::string pp(const lps::process_initializer &x, bool arg0)
Definition lps.cpp:34
bool is_multi_action(const atermpp::aterm &x)
bool is_linear_process(const atermpp::aterm &x)
Test for a linear_process expression.
The main namespace for the Process library.
std::string pp(const action_list &x, bool precedence_aware=true)
Definition process.cpp:24
bool is_at(const atermpp::aterm &x)
std::set< core::identifier_string > find_identifiers(const process::process_specification &x)
Definition process.cpp:79
void swap(rename &t1, rename &t2) noexcept
\brief swap overload
void make_allow(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(at &t1, at &t2) noexcept
\brief swap overload
void swap(action &t1, action &t2) noexcept
\brief swap overload
void complete_data_specification(process_specification &)
Adds all sorts that appear in the process specification spec to the data specification of spec.
void swap(untyped_multi_action &t1, untyped_multi_action &t2) noexcept
\brief swap overload
bool operator<(const action_label &a1, const action_label &a2)
Total ordering on action labels: name first (string order), then sorts.
std::set< data::variable > find_all_variables(const action &x)
Definition process.cpp:76
std::ostream & operator<<(std::ostream &out, const sync &x)
void normalize_sorts(process::process_equation_vector &x, const data::sort_specification &sortspec)
Definition process.cpp:67
std::ostream & operator<<(std::ostream &out, const bounded_init &x)
void make_choice(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const process_specification &x)
std::string pp(const process::action_name_multiset &x, bool arg0)
Definition process.cpp:36
std::string pp(const process_equation_list &x)
std::string pp(const process::action_label &x, bool arg0)
Definition process.cpp:35
std::string pp(const process::process_equation &x, bool arg0)
Definition process.cpp:50
std::string pp(const process::process_identifier &x, bool arg0)
Definition process.cpp:52
void swap(if_then &t1, if_then &t2) noexcept
\brief swap overload
void make_process_identifier(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(bounded_init &t1, bounded_init &t2) noexcept
\brief swap overload
std::set< data::sort_expression > find_sort_expressions(const process::process_specification &x)
Definition process.cpp:75
bool is_process_instance(const atermpp::aterm &x)
void swap(delta &t1, delta &t2) noexcept
\brief swap overload
std::string pp(const tau &x, bool precedence_aware=true)
Definition process.cpp:62
process::action_label_list normalize_sorts(const process::action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:66
std::ostream & operator<<(std::ostream &out, const sum &x)
std::string pp(const if_then &x, bool precedence_aware=true)
Definition process.cpp:46
std::set< data::sort_expression > find_sort_expressions(const process::process_equation_vector &x)
Definition process.cpp:73
void make_merge(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(rename_expression &t1, rename_expression &t2) noexcept
\brief swap overload
std::string pp(const stochastic_operator &x, bool precedence_aware=true)
Definition process.cpp:59
void swap(merge &t1, merge &t2) noexcept
\brief swap overload
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
void normalize_sorts(process::process_specification &x, const data::sort_specification &)
Definition process.cpp:68
bool is_process_expression(const atermpp::aterm &x)
bool is_process_instance_assignment(const atermpp::aterm &x)
void swap(left_merge &t1, left_merge &t2) noexcept
\brief swap overload
std::string pp(const process::communication_expression &x, bool arg0)
Definition process.cpp:43
std::ostream & operator<<(std::ostream &out, const untyped_process_assignment &x)
std::ostream & operator<<(std::ostream &out, const process_equation &x)
bool is_tau(const atermpp::aterm &x)
std::string pp(const process::rename_expression &x, bool arg0)
Definition process.cpp:57
std::ostream & operator<<(std::ostream &out, const stochastic_operator &x)
std::ostream & operator<<(std::ostream &out, const left_merge &x)
std::string pp(const process_identifier_list &x)
void make_action(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const process_identifier &x)
bool is_seq(const atermpp::aterm &x)
void make_sync(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(allow &t1, allow &t2) noexcept
\brief swap overload
bool is_merge(const atermpp::aterm &x)
std::set< data::sort_expression > find_sort_expressions(const process::action_label_list &x)
Definition process.cpp:72
void make_if_then_else(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_action_label(const atermpp::aterm &x)
void swap(process_identifier &t1, process_identifier &t2) noexcept
\brief swap overload
void make_hide(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(hide &t1, hide &t2) noexcept
\brief swap overload
bool is_communication_expression(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const communication_expression &x)
bool is_allow(const atermpp::aterm &x)
std::string pp(const process_expression &x, bool precedence_aware=true)
Definition process.cpp:51
std::string pp(const merge &x, bool precedence_aware=true)
Definition process.cpp:49
bool is_process_specification(const atermpp::aterm &x)
Test for a process specification expression.
std::string pp(const rename &x, bool precedence_aware=true)
Definition process.cpp:56
void swap(action_label &t1, action_label &t2) noexcept
\brief swap overload
bool operator<(const action &a1, const action &a2)
std::string pp(const seq &x, bool precedence_aware=true)
Definition process.cpp:58
void make_if_then(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const choice &x)
void swap(seq &t1, seq &t2) noexcept
\brief swap overload
std::string pp(const sum &x, bool precedence_aware=true)
Definition process.cpp:60
std::string pp(const process::process_specification &x, bool arg0)
Definition process.cpp:55
bool is_bounded_init(const atermpp::aterm &x)
bool is_delta(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const rename &x)
std::string pp(const process_expression_list &x, bool precedence_aware=true)
Definition process.cpp:30
std::string pp(const bounded_init &x, bool precedence_aware=true)
Definition process.cpp:40
void swap(untyped_process_assignment &t1, untyped_process_assignment &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const process_instance_assignment &x)
std::ostream & operator<<(std::ostream &out, const process_instance &x)
std::set< data::sort_expression > find_sort_expressions(const process::process_expression &x)
Definition process.cpp:74
std::ostream & operator<<(std::ostream &out, const untyped_multi_action &x)
void make_block(atermpp::aterm &t, const ARGUMENTS &... args)
process::process_expression translate_user_notation(const process::process_expression &x)
Definition process.cpp:70
bool is_sum(const atermpp::aterm &x)
std::string pp(const allow &x, bool precedence_aware=true)
Definition process.cpp:37
std::string pp(const multi_action_name_set &A)
Pretty print function for a set of multi action names.
bool is_process_identifier(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const at &x)
void swap(block &t1, block &t2) noexcept
\brief swap overload
bool is_block(const atermpp::aterm &x)
void translate_user_notation(process::process_specification &x)
Definition process.cpp:71
bool is_if_then_else(const atermpp::aterm &x)
void make_action_label(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const allow &x)
bool is_comm(const atermpp::aterm &x)
action normalize_sorts(const action &x, const data::sort_specification &sortspec)
Definition process.cpp:65
atermpp::aterm process_specification_to_aterm(const process_specification &spec)
Conversion to aterm.
void alphabet_reduce(process_specification &procspec, std::size_t duplicate_equation_limit=(std::numeric_limits< size_t >::max)())
Applies alphabet reduction to a process specification.
Definition process.cpp:82
std::string pp(const process_instance &x, bool precedence_aware=true)
Definition process.cpp:53
std::ostream & operator<<(std::ostream &out, const if_then_else &x)
bool is_action(const atermpp::aterm &x)
std::string pp(const left_merge &x, bool precedence_aware=true)
Definition process.cpp:48
void swap(stochastic_operator &t1, stochastic_operator &t2) noexcept
\brief swap overload
void swap(if_then_else &t1, if_then_else &t2) noexcept
\brief swap overload
bool is_left_merge(const atermpp::aterm &x)
std::string pp(const sync &x, bool precedence_aware=true)
Definition process.cpp:61
std::string pp(const action &x, bool precedence_aware=true)
Definition process.cpp:34
std::ostream & operator<<(std::ostream &out, const tau &x)
std::string pp(const process::untyped_multi_action &x, bool arg0)
Definition process.cpp:63
void swap(process_instance &t1, process_instance &t2) noexcept
\brief swap overload
void make_communication_expression(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const at &x, bool precedence_aware=true)
Definition process.cpp:38
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_action_name_multiset(const atermpp::aterm &x)
void swap(communication_expression &t1, communication_expression &t2) noexcept
\brief swap overload
std::string pp(const comm &x, bool precedence_aware=true)
Definition process.cpp:42
void swap(process_expression &t1, process_expression &t2) noexcept
\brief swap overload
bool is_untyped_multi_action(const atermpp::aterm &x)
void make_process_instance(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const hide &x)
bool is_hide(const atermpp::aterm &x)
std::string pp(const untyped_process_assignment &x, bool precedence_aware=true)
Definition process.cpp:64
void swap(tau &t1, tau &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const delta &x)
bool is_if_then(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const comm &x)
void make_untyped_process_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const action_name_multiset &x)
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_choice(const atermpp::aterm &x)
action translate_user_notation(const action &x)
Definition process.cpp:69
std::set< data::variable > find_free_variables(const action &x)
Definition process.cpp:77
std::string pp(const process_instance_assignment &x, bool precedence_aware=true)
Definition process.cpp:54
bool operator==(const process_specification &spec1, const process_specification &spec2)
Equality operator.
std::string pp(const process_expression_vector &x, bool precedence_aware=true)
Definition process.cpp:31
void make_comm(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const seq &x)
bool is_stochastic_operator(const atermpp::aterm &x)
bool is_process_equation(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const rename_expression &x)
std::string pp(const block &x, bool precedence_aware=true)
Definition process.cpp:39
void make_untyped_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(sum &t1, sum &t2) noexcept
\brief swap overload
void make_bounded_init(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const process_expression &x)
void swap(process_instance_assignment &t1, process_instance_assignment &t2) noexcept
\brief swap overload
bool is_rename_expression(const atermpp::aterm &x)
void swap(comm &t1, comm &t2) noexcept
\brief swap overload
std::set< data::variable > find_free_variables(const process::process_specification &x)
Definition process.cpp:78
void make_rename_expression(atermpp::aterm &t, const ARGUMENTS &... args)
void make_process_equation(atermpp::aterm &t, const ARGUMENTS &... args)
void make_action_name_multiset(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const action_label &x)
std::ostream & operator<<(std::ostream &out, const block &x)
bool operator!=(const process_specification &spec1, const process_specification &spec2)
Inequality operator.
std::ostream & operator<<(std::ostream &out, const action &x)
std::ostream & operator<<(std::ostream &out, const merge &x)
void swap(choice &t1, choice &t2) noexcept
\brief swap overload
std::string pp(const choice &x, bool precedence_aware=true)
Definition process.cpp:41
bool is_rename(const atermpp::aterm &x)
bool is_untyped_process_assignment(const atermpp::aterm &x)
void make_rename(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(process_equation &t1, process_equation &t2) noexcept
\brief swap overload
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_sync(const atermpp::aterm &x)
std::string pp(const delta &x, bool precedence_aware=true)
Definition process.cpp:44
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const hide &x, bool precedence_aware=true)
Definition process.cpp:45
std::string pp(const if_then_else &x, bool precedence_aware=true)
Definition process.cpp:47
void swap(action_name_multiset &t1, action_name_multiset &t2) noexcept
\brief swap overload
bool equal_signatures(const action &a, const action &b)
Compares the signatures of two actions.
void swap(sync &t1, sync &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const if_then &x)
std::string pp(const process::action_label_list &x, bool arg0)
Definition process.cpp:26
void make_left_merge(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
Definition aterm.h:364
expression builder that visits all sub expressions
Definition builder.h:32
static const atermpp::aterm Delta
static const atermpp::aterm UntypedProcessAssignment
static const atermpp::aterm Distribution
static const atermpp::aterm Allow
static const atermpp::aterm RenameExpr
static const atermpp::aterm Tau
static const atermpp::aterm ActId
static const atermpp::aterm Hide
static const atermpp::aterm LinearProcessInit
static const atermpp::aterm Rename
static const atermpp::aterm Process
static const atermpp::aterm IfThen
static const atermpp::aterm StochasticOperator
static const atermpp::aterm BInit
static const atermpp::aterm Merge
static const atermpp::aterm Action
static const atermpp::aterm MultActName
static const atermpp::aterm AtTime
static const atermpp::aterm Choice
static const atermpp::aterm Comm
static const atermpp::aterm ProcessAssignment
static const atermpp::aterm Sync
static const atermpp::aterm LMerge
static const atermpp::aterm ProcVarId
static const atermpp::aterm ProcExpr
static const atermpp::aterm Seq
static const atermpp::aterm Sum
static const atermpp::aterm UntypedMultiAction
static const atermpp::aterm Block
static const atermpp::aterm ProcEqn
static const atermpp::aterm CommExpr
static const atermpp::aterm IfThenElse
expression traverser that visits all sub expressions
Definition traverser.h:29
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
assignment_sequence_substitution(const assignment_list &assignments_)
const data_expression & operator()(const variable &v) const
A unary function that can be used in combination with replace_data_expressions to eliminate real numb...
fourier_motzkin_sigma(const rewriter &rewr_)
data_expression apply(const abstraction &d, bool negate) const
data_expression operator()(const data_expression &d) const
static constexpr bool is_identity_substitution
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
const AssociativeContainer & m_map
map_substitution(const AssociativeContainer &m)
static constexpr bool is_identity_substitution
expression_type operator()(const variable_type &v) const
\brief Traverser class
Definition traverser.h:596
void update(lps::action_summand &x)
Definition builder.h:222
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:308
void update(lps::linear_process &x)
Definition builder.h:245
void apply(T &result, const lps::multi_action &x)
Definition builder.h:205
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:264
void update(lps::specification &x)
Definition builder.h:253
void update(lps::deadlock &x)
Definition builder.h:195
void update(lps::stochastic_linear_process &x)
Definition builder.h:289
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:238
void update(lps::stochastic_action_summand &x)
Definition builder.h:271
void update(lps::deadlock_summand &x)
Definition builder.h:212
void update(lps::stochastic_specification &x)
Definition builder.h:297
Maintains a multiset of bound data variables during traversal.
Definition add_binding.h:23
void enter(const stochastic_specification &x)
Definition add_binding.h:93
void leave(const stochastic_process_initializer &x)
void enter(const action_summand &x)
Definition add_binding.h:31
void leave(const stochastic_specification &x)
Definition add_binding.h:98
void leave(const deadlock_summand &x)
Definition add_binding.h:58
void leave(const linear_process &x)
Definition add_binding.h:68
void enter(const stochastic_linear_process &x)
Definition add_binding.h:73
void leave(const action_summand &x)
Definition add_binding.h:36
void leave(const stochastic_linear_process &x)
Definition add_binding.h:78
void enter(const specification &x)
Definition add_binding.h:83
void enter(const deadlock_summand &x)
Definition add_binding.h:53
void enter(const stochastic_action_summand &x)
Definition add_binding.h:41
void leave(const specification &x)
Definition add_binding.h:88
void enter(const linear_process &x)
Definition add_binding.h:63
void enter(const stochastic_process_initializer &x)
void leave(const stochastic_action_summand &x)
Definition add_binding.h:47
void apply(T &result, data::where_clause &x)
void apply(const data::where_clause &x)
void update(lps::deadlock &x)
Definition builder.h:32
void update(lps::stochastic_specification &x)
Definition builder.h:153
void update(lps::specification &x)
Definition builder.h:99
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:81
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:168
void update(lps::action_summand &x)
Definition builder.h:62
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:114
void update(lps::stochastic_linear_process &x)
Definition builder.h:142
void update(lps::stochastic_action_summand &x)
Definition builder.h:121
void apply(T &result, const lps::multi_action &x)
Definition builder.h:42
void update(lps::linear_process &x)
Definition builder.h:88
void update(lps::deadlock_summand &x)
Definition builder.h:49
void apply(const lps::action_summand &x)
Definition traverser.h:547
void apply(const lps::multi_action &x)
Definition traverser.h:540
void apply(const lps::specification &x)
Definition traverser.h:561
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:569
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:576
void apply(const lps::stochastic_specification &x)
Definition traverser.h:583
void apply(const lps::linear_process &x)
Definition traverser.h:554
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:240
void apply(const lps::multi_action &x)
Definition traverser.h:172
void apply(const lps::deadlock &x)
Definition traverser.h:162
void apply(const lps::stochastic_specification &x)
Definition traverser.h:248
void apply(const lps::specification &x)
Definition traverser.h:215
void apply(const lps::deadlock_summand &x)
Definition traverser.h:183
void apply(const lps::action_summand &x)
Definition traverser.h:191
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:230
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:223
void apply(const lps::linear_process &x)
Definition traverser.h:207
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:256
void apply(const lps::process_initializer &x)
Definition traverser.h:200
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:495
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:484
void apply(const lps::action_summand &x)
Definition traverser.h:440
void apply(const lps::specification &x)
Definition traverser.h:466
void apply(const lps::process_initializer &x)
Definition traverser.h:450
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:476
void apply(const lps::linear_process &x)
Definition traverser.h:457
void apply(const lps::deadlock_summand &x)
Definition traverser.h:431
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:514
void apply(const lps::stochastic_specification &x)
Definition traverser.h:504
void apply(const lps::multi_action &x)
Definition traverser.h:420
void apply(const lps::deadlock &x)
Definition traverser.h:410
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:106
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:117
void apply(const lps::stochastic_specification &x)
Definition traverser.h:126
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:136
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:98
void apply(const lps::multi_action &x)
Definition traverser.h:42
void apply(const lps::process_initializer &x)
Definition traverser.h:72
void apply(const lps::action_summand &x)
Definition traverser.h:62
void apply(const lps::specification &x)
Definition traverser.h:88
void apply(const lps::deadlock_summand &x)
Definition traverser.h:53
void apply(const lps::deadlock &x)
Definition traverser.h:32
void apply(const lps::linear_process &x)
Definition traverser.h:79
void apply(const lps::linear_process &x)
Definition traverser.h:329
void apply(const lps::specification &x)
Definition traverser.h:338
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:384
void apply(const lps::deadlock &x)
Definition traverser.h:282
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:366
void apply(const lps::multi_action &x)
Definition traverser.h:292
void apply(const lps::action_summand &x)
Definition traverser.h:312
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:355
void apply(const lps::deadlock_summand &x)
Definition traverser.h:303
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:347
void apply(const lps::stochastic_specification &x)
Definition traverser.h:375
void apply(const lps::process_initializer &x)
Definition traverser.h:322
void update(lps::action_summand &x)
Definition builder.h:364
void update(lps::deadlock &x)
Definition builder.h:334
void apply(T &result, const lps::multi_action &x)
Definition builder.h:344
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:464
void update(lps::specification &x)
Definition builder.h:401
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:413
void update(lps::linear_process &x)
Definition builder.h:390
void update(lps::stochastic_action_summand &x)
Definition builder.h:420
void update(lps::stochastic_specification &x)
Definition builder.h:452
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:383
void update(lps::stochastic_linear_process &x)
Definition builder.h:441
void update(lps::deadlock_summand &x)
Definition builder.h:351
void apply(T &result, const stochastic_distribution &x, data::data_expression_list &pars)
In the code below, it is essential that the assignments are also updated. They are passed by referenc...
void apply(T &result, const stochastic_distribution &x, data::assignment_list &assignments)
In the code below, it is essential that the assignments are also updated. They are passed by referenc...
void do_action_summand(ActionSummand &x, const data::variable_list &v)
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
Function object that checks if a sort is a singleton sort. Note that it is an approximation,...
Definition remove.h:36
is_singleton_sort(const data::data_specification &data_spec)
Definition remove.h:39
bool operator()(const data::sort_expression &s) const
Definition remove.h:43
const data::data_specification & m_data_spec
Definition remove.h:37
Function object that checks if a summand has a false condition.
Definition remove.h:25
bool operator()(const summand_base &s) const
Definition remove.h:26
Traverser for removing parameters from LPS data types. These parameters can be either process paramet...
Definition remove.h:58
void apply(atermpp::term_list< T > &result, const data::assignment_list &x)
Removes parameters from a list of assignments. Assignments to removed parameters are removed.
Definition remove.h:101
void apply(T &result, const stochastic_process_initializer &x)
Definition remove.h:156
void apply(T &result, const process_initializer &x)
Definition remove.h:149
void update(std::set< data::variable > &x)
Removes parameters from a set container.
Definition remove.h:73
const std::set< data::variable > & to_be_removed
Definition remove.h:65
void apply(atermpp::term_list< T > &result, const data::variable_list &x)
Removes parameters from a list of variables.
Definition remove.h:83
void update(linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:111
data::data_expression_list remove_expressions(const data::data_expression_list &e)
Removes expressions from e at the corresponding positions of process_parameters.
Definition remove.h:130
void update(stochastic_specification &x)
Removes parameters from a linear process specification.
Definition remove.h:175
void update(specification &x)
Removes parameters from a linear process specification.
Definition remove.h:166
remove_parameters_builder(const std::set< data::variable > &to_be_removed_)
Definition remove.h:68
void update(stochastic_linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:121
Options for linearisation.
Definition linearise.h:25
\brief Builder class
Definition builder.h:476
\brief Traverser class
Definition traverser.h:397
bool operator()(const core::identifier_string &s1, const core::identifier_string &s2) const
void apply(T &result, const process::process_equation &x)
Definition builder.h:405
void apply(T &result, const process::rename &x)
Definition builder.h:487
void apply(T &result, const process::left_merge &x)
Definition builder.h:567
void apply(T &result, const process::bounded_init &x)
Definition builder.h:551
void apply(T &result, const process::process_expression &x)
Definition builder.h:599
void apply(T &result, const process::block &x)
Definition builder.h:471
void apply(T &result, const process::merge &x)
Definition builder.h:559
void apply(T &result, const process::sync &x)
Definition builder.h:511
void apply(T &result, const process::choice &x)
Definition builder.h:575
void apply(T &result, const process::if_then &x)
Definition builder.h:535
void apply(T &result, const process::action &x)
Definition builder.h:421
void apply(T &result, const process::delta &x)
Definition builder.h:445
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:437
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:591
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:583
void update(process::process_specification &x)
Definition builder.h:394
void apply(T &result, const process::allow &x)
Definition builder.h:503
void apply(T &result, const process::at &x)
Definition builder.h:519
void apply(T &result, const process::sum &x)
Definition builder.h:463
void apply(T &result, const process::seq &x)
Definition builder.h:527
void apply(T &result, const process::tau &x)
Definition builder.h:454
void apply(T &result, const process::comm &x)
Definition builder.h:495
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:413
void apply(T &result, const process::hide &x)
Definition builder.h:479
void apply(T &result, const process::if_then_else &x)
Definition builder.h:543
void apply(T &result, const process::process_instance &x)
Definition builder.h:429
void apply(T &result, const process::sync &x)
Definition builder.h:1160
void apply(T &result, const process::rename &x)
Definition builder.h:1136
void apply(T &result, const process::if_then_else &x)
Definition builder.h:1192
void apply(T &result, const process::process_equation &x)
Definition builder.h:1059
void apply(T &result, const process::bounded_init &x)
Definition builder.h:1200
void apply(T &result, const process::at &x)
Definition builder.h:1168
void apply(T &result, const process::if_then &x)
Definition builder.h:1184
void apply(T &result, const process::choice &x)
Definition builder.h:1224
void apply(T &result, const process::tau &x)
Definition builder.h:1103
void apply(T &result, const process::merge &x)
Definition builder.h:1208
void apply(T &result, const process::left_merge &x)
Definition builder.h:1216
void apply(T &result, const process::sum &x)
Definition builder.h:1112
void apply(T &result, const process::seq &x)
Definition builder.h:1176
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:1240
void apply(T &result, const process::block &x)
Definition builder.h:1120
void apply(T &result, const process::allow &x)
Definition builder.h:1152
void apply(T &result, const process::action &x)
Definition builder.h:1067
void apply(T &result, const process::hide &x)
Definition builder.h:1128
void apply(T &result, const process::process_expression &x)
Definition builder.h:1249
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:1085
void apply(T &result, const process::comm &x)
Definition builder.h:1144
void apply(T &result, const process::delta &x)
Definition builder.h:1094
void apply(T &result, const process::process_instance &x)
Definition builder.h:1076
void update(process::process_specification &x)
Definition builder.h:1048
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:1232
void apply(T &result, const process::process_expression &x)
Definition builder.h:1574
void apply(T &result, const process::process_identifier &x)
Definition builder.h:1377
void apply(T &result, const process::process_instance &x)
Definition builder.h:1403
void apply(T &result, const process::delta &x)
Definition builder.h:1419
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:1411
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:1557
void apply(T &result, const process::choice &x)
Definition builder.h:1549
void apply(T &result, const process::at &x)
Definition builder.h:1493
void apply(T &result, const process::merge &x)
Definition builder.h:1533
void apply(T &result, const process::if_then &x)
Definition builder.h:1509
void apply(T &result, const process::comm &x)
Definition builder.h:1469
void apply(T &result, const process::process_equation &x)
Definition builder.h:1386
void apply(T &result, const process::left_merge &x)
Definition builder.h:1541
void apply(T &result, const process::sync &x)
Definition builder.h:1485
void apply(T &result, const process::tau &x)
Definition builder.h:1428
void update(process::process_specification &x)
Definition builder.h:1366
void apply(T &result, const process::hide &x)
Definition builder.h:1453
void apply(T &result, const process::if_then_else &x)
Definition builder.h:1517
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:1565
void apply(T &result, const process::rename &x)
Definition builder.h:1461
void apply(T &result, const process::seq &x)
Definition builder.h:1501
void apply(T &result, const process::block &x)
Definition builder.h:1445
void apply(T &result, const process::sum &x)
Definition builder.h:1437
void apply(T &result, const process::bounded_init &x)
Definition builder.h:1525
void apply(T &result, const process::action &x)
Definition builder.h:1394
void apply(T &result, const process::allow &x)
Definition builder.h:1477
void update(process::process_specification &x)
Definition builder.h:59
void apply(T &result, const process::sync &x)
Definition builder.h:188
void apply(T &result, const process::choice &x)
Definition builder.h:252
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:114
void apply(T &result, const process::process_instance &x)
Definition builder.h:106
void apply(T &result, const process::merge &x)
Definition builder.h:236
void apply(T &result, const process::seq &x)
Definition builder.h:204
void apply(T &result, const process::if_then &x)
Definition builder.h:212
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:90
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:260
void apply(T &result, const process::action &x)
Definition builder.h:98
void apply(T &result, const process::delta &x)
Definition builder.h:122
void apply(T &result, const process::if_then_else &x)
Definition builder.h:220
void apply(T &result, const process::left_merge &x)
Definition builder.h:244
void apply(T &result, const process::process_equation &x)
Definition builder.h:82
void apply(T &result, const process::hide &x)
Definition builder.h:156
void apply(T &result, const process::allow &x)
Definition builder.h:180
void apply(T &result, const process::rename &x)
Definition builder.h:164
void apply(T &result, const process::comm &x)
Definition builder.h:172
void apply(T &result, const process::sum &x)
Definition builder.h:140
void apply(T &result, const process::bounded_init &x)
Definition builder.h:228
void apply(T &result, const process::action_label &x)
Definition builder.h:52
void apply(T &result, const process::block &x)
Definition builder.h:148
void apply(T &result, const process::at &x)
Definition builder.h:196
void apply(T &result, const process::tau &x)
Definition builder.h:131
void apply(T &result, const process::process_identifier &x)
Definition builder.h:74
void apply(T &result, const process::process_expression &x)
Definition builder.h:276
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:268
void apply(const process::sync &x)
Definition traverser.h:1749
void apply(const process::if_then_else &x)
Definition traverser.h:1779
void apply(const process::block &x)
Definition traverser.h:1714
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:1826
void apply(const process::bounded_init &x)
Definition traverser.h:1787
void apply(const process::sum &x)
Definition traverser.h:1707
void apply(const process::hide &x)
Definition traverser.h:1721
void apply(const process::process_specification &x)
Definition traverser.h:1656
void apply(const process::action &x)
Definition traverser.h:1672
void apply(const process::left_merge &x)
Definition traverser.h:1803
void apply(const process::process_expression &x)
Definition traverser.h:1833
void apply(const process::comm &x)
Definition traverser.h:1735
void apply(const process::rename &x)
Definition traverser.h:1728
void apply(const process::tau &x)
Definition traverser.h:1700
void apply(const process::process_instance_assignment &x)
Definition traverser.h:1686
void apply(const process::action_label &x)
Definition traverser.h:1649
void apply(const process::stochastic_operator &x)
Definition traverser.h:1819
void apply(const process::choice &x)
Definition traverser.h:1811
void apply(const process::process_equation &x)
Definition traverser.h:1665
void apply(const process::if_then &x)
Definition traverser.h:1772
void apply(const process::process_instance &x)
Definition traverser.h:1679
void apply(const process::delta &x)
Definition traverser.h:1693
void apply(const process::merge &x)
Definition traverser.h:1795
void apply(const process::allow &x)
Definition traverser.h:1742
void apply(const process::seq &x)
Definition traverser.h:1764
void apply(const process::left_merge &x)
Definition traverser.h:536
void apply(const process::choice &x)
Definition traverser.h:544
void apply(const process::stochastic_operator &x)
Definition traverser.h:552
void apply(const process::action &x)
Definition traverser.h:402
void apply(const process::allow &x)
Definition traverser.h:472
void apply(const process::if_then_else &x)
Definition traverser.h:511
void apply(const process::process_specification &x)
Definition traverser.h:380
void apply(const process::bounded_init &x)
Definition traverser.h:520
void apply(const process::untyped_multi_action &x)
Definition traverser.h:395
void apply(const process::process_instance &x)
Definition traverser.h:409
void apply(const process::delta &x)
Definition traverser.h:423
void apply(const process::merge &x)
Definition traverser.h:528
void apply(const process::process_expression &x)
Definition traverser.h:567
void apply(const process::block &x)
Definition traverser.h:444
void apply(const process::process_equation &x)
Definition traverser.h:388
void apply(const process::if_then &x)
Definition traverser.h:503
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:560
void apply(const process::process_instance_assignment &x)
Definition traverser.h:416
void apply(const process::rename &x)
Definition traverser.h:458
void apply(const process::process_expression &x)
Definition traverser.h:1533
void apply(const process::process_specification &x)
Definition traverser.h:1300
void apply(const process::bounded_init &x)
Definition traverser.h:1484
void apply(const process::untyped_multi_action &x)
Definition traverser.h:1350
void apply(const process::process_identifier &x)
Definition traverser.h:1310
void apply(const process::communication_expression &x)
Definition traverser.h:1335
void apply(const process::process_equation &x)
Definition traverser.h:1318
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:1525
void apply(const process::if_then_else &x)
Definition traverser.h:1475
void apply(const process::rename_expression &x)
Definition traverser.h:1327
void apply(const process::action_name_multiset &x)
Definition traverser.h:1343
void apply(const process::left_merge &x)
Definition traverser.h:1500
void apply(const process::stochastic_operator &x)
Definition traverser.h:1516
void apply(const process::if_then &x)
Definition traverser.h:1467
void apply(const process::process_instance &x)
Definition traverser.h:1365
void apply(const process::process_instance_assignment &x)
Definition traverser.h:1373
void apply(const process::action_label &x)
Definition traverser.h:1292
void apply(const process::process_instance &x)
Definition traverser.h:705
void apply(const process::process_expression &x)
Definition traverser.h:859
void apply(const process::left_merge &x)
Definition traverser.h:829
void apply(const process::stochastic_operator &x)
Definition traverser.h:845
void apply(const process::if_then_else &x)
Definition traverser.h:805
void apply(const process::if_then &x)
Definition traverser.h:798
void apply(const process::process_instance_assignment &x)
Definition traverser.h:712
void apply(const process::bounded_init &x)
Definition traverser.h:813
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:852
void apply(const process::process_specification &x)
Definition traverser.h:683
void apply(const process::process_equation &x)
Definition traverser.h:691
void apply(const process::process_instance &x)
Definition traverser.h:102
void apply(const process::process_equation &x)
Definition traverser.h:78
void apply(const process::process_specification &x)
Definition traverser.h:61
void apply(const process::block &x)
Definition traverser.h:140
void apply(const process::process_identifier &x)
Definition traverser.h:71
void apply(const process::rename &x)
Definition traverser.h:154
void apply(const process::allow &x)
Definition traverser.h:168
void apply(const process::delta &x)
Definition traverser.h:118
void apply(const process::merge &x)
Definition traverser.h:224
void apply(const process::action &x)
Definition traverser.h:94
void apply(const process::action_label &x)
Definition traverser.h:54
void apply(const process::process_instance_assignment &x)
Definition traverser.h:110
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:257
void apply(const process::bounded_init &x)
Definition traverser.h:216
void apply(const process::choice &x)
Definition traverser.h:240
void apply(const process::if_then &x)
Definition traverser.h:199
void apply(const process::stochastic_operator &x)
Definition traverser.h:248
void apply(const process::process_expression &x)
Definition traverser.h:264
void apply(const process::left_merge &x)
Definition traverser.h:232
void apply(const process::untyped_multi_action &x)
Definition traverser.h:87
void apply(const process::if_then_else &x)
Definition traverser.h:207
void apply(const process::sync &x)
Definition traverser.h:1087
void apply(const process::process_equation &x)
Definition traverser.h:991
void apply(const process::comm &x)
Definition traverser.h:1073
void apply(const process::bounded_init &x)
Definition traverser.h:1128
void apply(const process::if_then_else &x)
Definition traverser.h:1119
void apply(const process::choice &x)
Definition traverser.h:1152
void apply(const process::tau &x)
Definition traverser.h:1037
void apply(const process::allow &x)
Definition traverser.h:1080
void apply(const process::process_instance &x)
Definition traverser.h:1014
void apply(const process::merge &x)
Definition traverser.h:1136
void apply(const process::process_specification &x)
Definition traverser.h:975
void apply(const process::process_identifier &x)
Definition traverser.h:984
void apply(const process::at &x)
Definition traverser.h:1095
void apply(const process::sum &x)
Definition traverser.h:1044
void apply(const process::untyped_multi_action &x)
Definition traverser.h:1000
void apply(const process::left_merge &x)
Definition traverser.h:1144
void apply(const process::stochastic_operator &x)
Definition traverser.h:1160
void apply(const process::process_instance_assignment &x)
Definition traverser.h:1022
void apply(const process::if_then &x)
Definition traverser.h:1111
void apply(const process::hide &x)
Definition traverser.h:1059
void apply(const process::seq &x)
Definition traverser.h:1103
void apply(const process::process_expression &x)
Definition traverser.h:1176
void apply(const process::rename &x)
Definition traverser.h:1066
void apply(const process::block &x)
Definition traverser.h:1052
void apply(const process::untyped_process_assignment &x)
Definition traverser.h:1169
void apply(const process::delta &x)
Definition traverser.h:1030
void apply(const process::action &x)
Definition traverser.h:1007
void apply(T &result, const process::process_instance &x)
Definition builder.h:760
void apply(T &result, const process::choice &x)
Definition builder.h:906
void apply(T &result, const process::sync &x)
Definition builder.h:842
void apply(T &result, const process::sum &x)
Definition builder.h:794
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:914
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:922
void apply(T &result, const process::allow &x)
Definition builder.h:834
void apply(T &result, const process::bounded_init &x)
Definition builder.h:882
void apply(T &result, const process::comm &x)
Definition builder.h:826
void apply(T &result, const process::block &x)
Definition builder.h:802
void apply(T &result, const process::tau &x)
Definition builder.h:785
void apply(T &result, const process::action &x)
Definition builder.h:752
void apply(T &result, const process::left_merge &x)
Definition builder.h:898
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:744
void apply(T &result, const process::merge &x)
Definition builder.h:890
void apply(T &result, const process::seq &x)
Definition builder.h:858
void apply(T &result, const process::delta &x)
Definition builder.h:776
void apply(T &result, const process::hide &x)
Definition builder.h:810
void apply(T &result, const process::at &x)
Definition builder.h:850
void apply(T &result, const process::process_identifier &x)
Definition builder.h:728
void apply(T &result, const process::if_then_else &x)
Definition builder.h:874
void update(process::process_specification &x)
Definition builder.h:716
void apply(T &result, const process::process_equation &x)
Definition builder.h:736
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:768
void apply(T &result, const process::rename &x)
Definition builder.h:818
void apply(T &result, const process::if_then &x)
Definition builder.h:866
void apply(T &result, const process::process_expression &x)
Definition builder.h:930
Base builder class for processes.
Definition builder.h:25
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:30
Base class for action_formula_traverser.
Definition traverser.h:31
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:37
\brief Builder class
Definition builder.h:1033
make_substitution(const std::map< process_identifier, process_identifier > &map)
process_identifier operator()(const process_identifier &id) const
const std::map< process_identifier, process_identifier > & m_map
std::size_t operator()(const mcrl2::lps::multi_action &ma) const
std::size_t operator()(const mcrl2::process::action &t) const