mCRL2
Loading...
Searching...
No Matches
builder.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/process/builder.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_PROCESS_BUILDER_H
13#define MCRL2_PROCESS_BUILDER_H
14
15#include "mcrl2/data/builder.h"
16#include "mcrl2/process/process_specification.h"
17#include "mcrl2/process/untyped_multi_action.h"
18
19namespace mcrl2::process
20{
21
22/// \brief Base builder class for processes.
23template <typename Derived>
24struct process_builder_base: public core::builder<Derived>
25{
26 using super = core::builder<Derived>;
27 using super::apply;
28
29 template <class T>
30 void apply(T& result, const data::untyped_data_parameter& x)
31 {
32 static_cast<Derived&>(*this).enter(x);
33 // skip
34 static_cast<Derived&>(*this).leave(x);
35 result = atermpp::down_cast<T>(x);
36 }
37};
38
39
40// Adds sort expression traversal to a builder
41//--- start generated add_sort_expressions code ---//
42template <template <class> class Builder, class Derived>
43struct add_sort_expressions: public Builder<Derived>
44{
45 using super = Builder<Derived>;
46 using super::enter;
47 using super::leave;
48 using super::update;
49 using super::apply;
50
51 template <class T>
52 void apply(T& result, const process::action_label& x)
53 {
54 static_cast<Derived&>(*this).enter(x);
55 process::make_action_label(result, x.name(), [&](data::sort_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.sorts()); });
56 static_cast<Derived&>(*this).leave(x);
57 }
58
59 void update(process::process_specification& x)
60 {
61 static_cast<Derived&>(*this).enter(x);
62 process::action_label_list result_action_labels;
63 static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
64 x.action_labels() = result_action_labels;
65 static_cast<Derived&>(*this).update(x.global_variables());
66 static_cast<Derived&>(*this).update(x.equations());
67 process_expression result_init;
68 static_cast<Derived&>(*this).apply(result_init, x.init());
69 x.init() = result_init;
70 static_cast<Derived&>(*this).leave(x);
71 }
72
73 template <class T>
74 void apply(T& result, const process::process_identifier& x)
75 {
76 static_cast<Derived&>(*this).enter(x);
77 process::make_process_identifier(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); });
78 static_cast<Derived&>(*this).leave(x);
79 }
80
81 template <class T>
82 void apply(T& result, const process::process_equation& x)
83 {
84 static_cast<Derived&>(*this).enter(x);
85 process::make_process_equation(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.formal_parameters()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.expression()); });
86 static_cast<Derived&>(*this).leave(x);
87 }
88
89 template <class T>
90 void apply(T& result, const process::untyped_multi_action& x)
91 {
92 static_cast<Derived&>(*this).enter(x);
93 process::make_untyped_multi_action(result, [&](data::untyped_data_parameter_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
94 static_cast<Derived&>(*this).leave(x);
95 }
96
97 template <class T>
98 void apply(T& result, const process::action& x)
99 {
100 static_cast<Derived&>(*this).enter(x);
101 process::make_action(result, [&](action_label& result){ static_cast<Derived&>(*this).apply(result, x.label()); }, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
102 static_cast<Derived&>(*this).leave(x);
103 }
104
105 template <class T>
106 void apply(T& result, const process::process_instance& x)
107 {
108 static_cast<Derived&>(*this).enter(x);
109 process::make_process_instance(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.actual_parameters()); });
110 static_cast<Derived&>(*this).leave(x);
111 }
112
113 template <class T>
114 void apply(T& result, const process::process_instance_assignment& x)
115 {
116 static_cast<Derived&>(*this).enter(x);
117 process::make_process_instance_assignment(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
118 static_cast<Derived&>(*this).leave(x);
119 }
120
121 template <class T>
122 void apply(T& result, const process::delta& x)
123 {
124 static_cast<Derived&>(*this).enter(x);
125 // skip
126 static_cast<Derived&>(*this).leave(x);
127 result = atermpp::down_cast<T>(x);
128 }
129
130 template <class T>
131 void apply(T& result, const process::tau& x)
132 {
133 static_cast<Derived&>(*this).enter(x);
134 // skip
135 static_cast<Derived&>(*this).leave(x);
136 result = atermpp::down_cast<T>(x);
137 }
138
139 template <class T>
140 void apply(T& result, const process::sum& x)
141 {
142 static_cast<Derived&>(*this).enter(x);
143 process::make_sum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
144 static_cast<Derived&>(*this).leave(x);
145 }
146
147 template <class T>
148 void apply(T& result, const process::block& x)
149 {
150 static_cast<Derived&>(*this).enter(x);
151 process::make_block(result, x.block_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
152 static_cast<Derived&>(*this).leave(x);
153 }
154
155 template <class T>
156 void apply(T& result, const process::hide& x)
157 {
158 static_cast<Derived&>(*this).enter(x);
159 process::make_hide(result, x.hide_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
160 static_cast<Derived&>(*this).leave(x);
161 }
162
163 template <class T>
164 void apply(T& result, const process::rename& x)
165 {
166 static_cast<Derived&>(*this).enter(x);
167 process::make_rename(result, x.rename_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
168 static_cast<Derived&>(*this).leave(x);
169 }
170
171 template <class T>
172 void apply(T& result, const process::comm& x)
173 {
174 static_cast<Derived&>(*this).enter(x);
175 process::make_comm(result, x.comm_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
176 static_cast<Derived&>(*this).leave(x);
177 }
178
179 template <class T>
180 void apply(T& result, const process::allow& x)
181 {
182 static_cast<Derived&>(*this).enter(x);
183 process::make_allow(result, x.allow_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
184 static_cast<Derived&>(*this).leave(x);
185 }
186
187 template <class T>
188 void apply(T& result, const process::sync& x)
189 {
190 static_cast<Derived&>(*this).enter(x);
191 process::make_sync(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
192 static_cast<Derived&>(*this).leave(x);
193 }
194
195 template <class T>
196 void apply(T& result, const process::at& x)
197 {
198 static_cast<Derived&>(*this).enter(x);
199 process::make_at(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
200 static_cast<Derived&>(*this).leave(x);
201 }
202
203 template <class T>
204 void apply(T& result, const process::seq& x)
205 {
206 static_cast<Derived&>(*this).enter(x);
207 process::make_seq(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
208 static_cast<Derived&>(*this).leave(x);
209 }
210
211 template <class T>
212 void apply(T& result, const process::if_then& x)
213 {
214 static_cast<Derived&>(*this).enter(x);
215 process::make_if_then(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); });
216 static_cast<Derived&>(*this).leave(x);
217 }
218
219 template <class T>
220 void apply(T& result, const process::if_then_else& x)
221 {
222 static_cast<Derived&>(*this).enter(x);
223 process::make_if_then_else(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.else_case()); });
224 static_cast<Derived&>(*this).leave(x);
225 }
226
227 template <class T>
228 void apply(T& result, const process::bounded_init& x)
229 {
230 static_cast<Derived&>(*this).enter(x);
231 process::make_bounded_init(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
232 static_cast<Derived&>(*this).leave(x);
233 }
234
235 template <class T>
236 void apply(T& result, const process::merge& x)
237 {
238 static_cast<Derived&>(*this).enter(x);
239 process::make_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
240 static_cast<Derived&>(*this).leave(x);
241 }
242
243 template <class T>
244 void apply(T& result, const process::left_merge& x)
245 {
246 static_cast<Derived&>(*this).enter(x);
247 process::make_left_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
248 static_cast<Derived&>(*this).leave(x);
249 }
250
251 template <class T>
252 void apply(T& result, const process::choice& x)
253 {
254 static_cast<Derived&>(*this).enter(x);
255 process::make_choice(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
256 static_cast<Derived&>(*this).leave(x);
257 }
258
259 template <class T>
260 void apply(T& result, const process::stochastic_operator& x)
261 {
262 static_cast<Derived&>(*this).enter(x);
263 process::make_stochastic_operator(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
264 static_cast<Derived&>(*this).leave(x);
265 }
266
267 template <class T>
268 void apply(T& result, const process::untyped_process_assignment& x)
269 {
270 static_cast<Derived&>(*this).enter(x);
271 process::make_untyped_process_assignment(result, x.name(), [&](data::untyped_identifier_assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
272 static_cast<Derived&>(*this).leave(x);
273 }
274
275 template <class T>
276 void apply(T& result, const process::process_expression& x)
277 {
278 static_cast<Derived&>(*this).enter(x);
279 if (data::is_untyped_data_parameter(x))
280 {
281 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
282 }
283 else if (process::is_action(x))
284 {
285 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::action>(x));
286 }
287 else if (process::is_process_instance(x))
288 {
289 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance>(x));
290 }
291 else if (process::is_process_instance_assignment(x))
292 {
293 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance_assignment>(x));
294 }
295 else if (process::is_delta(x))
296 {
297 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::delta>(x));
298 }
299 else if (process::is_tau(x))
300 {
301 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::tau>(x));
302 }
303 else if (process::is_sum(x))
304 {
305 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sum>(x));
306 }
307 else if (process::is_block(x))
308 {
309 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::block>(x));
310 }
311 else if (process::is_hide(x))
312 {
313 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::hide>(x));
314 }
315 else if (process::is_rename(x))
316 {
317 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::rename>(x));
318 }
319 else if (process::is_comm(x))
320 {
321 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::comm>(x));
322 }
323 else if (process::is_allow(x))
324 {
325 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::allow>(x));
326 }
327 else if (process::is_sync(x))
328 {
329 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sync>(x));
330 }
331 else if (process::is_at(x))
332 {
333 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::at>(x));
334 }
335 else if (process::is_seq(x))
336 {
337 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::seq>(x));
338 }
339 else if (process::is_if_then(x))
340 {
341 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then>(x));
342 }
343 else if (process::is_if_then_else(x))
344 {
345 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then_else>(x));
346 }
347 else if (process::is_bounded_init(x))
348 {
349 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::bounded_init>(x));
350 }
351 else if (process::is_merge(x))
352 {
353 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::merge>(x));
354 }
355 else if (process::is_left_merge(x))
356 {
357 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::left_merge>(x));
358 }
359 else if (process::is_choice(x))
360 {
361 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::choice>(x));
362 }
363 else if (process::is_stochastic_operator(x))
364 {
365 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::stochastic_operator>(x));
366 }
367 else if (process::is_untyped_process_assignment(x))
368 {
369 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_process_assignment>(x));
370 }
371 static_cast<Derived&>(*this).leave(x);
372 }
373
374};
375
376/// \\brief Builder class
377template <typename Derived>
378struct sort_expression_builder: public add_sort_expressions<data::sort_expression_builder, Derived>
379{
380};
381//--- end generated add_sort_expressions code ---//
382
383// Adds data expression traversal to a builder
384//--- start generated add_data_expressions code ---//
385template <template <class> class Builder, class Derived>
386struct add_data_expressions: public Builder<Derived>
387{
388 using super = Builder<Derived>;
389 using super::enter;
390 using super::leave;
391 using super::update;
392 using super::apply;
393
394 void update(process::process_specification& x)
395 {
396 static_cast<Derived&>(*this).enter(x);
397 static_cast<Derived&>(*this).update(x.equations());
398 process_expression result_init;
399 static_cast<Derived&>(*this).apply(result_init, x.init());
400 x.init() = result_init;
401 static_cast<Derived&>(*this).leave(x);
402 }
403
404 template <class T>
405 void apply(T& result, const process::process_equation& x)
406 {
407 static_cast<Derived&>(*this).enter(x);
408 process::make_process_equation(result, x.identifier(), x.formal_parameters(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.expression()); });
409 static_cast<Derived&>(*this).leave(x);
410 }
411
412 template <class T>
413 void apply(T& result, const process::untyped_multi_action& x)
414 {
415 static_cast<Derived&>(*this).enter(x);
416 process::make_untyped_multi_action(result, [&](data::untyped_data_parameter_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
417 static_cast<Derived&>(*this).leave(x);
418 }
419
420 template <class T>
421 void apply(T& result, const process::action& x)
422 {
423 static_cast<Derived&>(*this).enter(x);
424 process::make_action(result, x.label(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
425 static_cast<Derived&>(*this).leave(x);
426 }
427
428 template <class T>
429 void apply(T& result, const process::process_instance& x)
430 {
431 static_cast<Derived&>(*this).enter(x);
432 process::make_process_instance(result, x.identifier(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.actual_parameters()); });
433 static_cast<Derived&>(*this).leave(x);
434 }
435
436 template <class T>
437 void apply(T& result, const process::process_instance_assignment& x)
438 {
439 static_cast<Derived&>(*this).enter(x);
440 process::make_process_instance_assignment(result, x.identifier(), [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
441 static_cast<Derived&>(*this).leave(x);
442 }
443
444 template <class T>
445 void apply(T& result, const process::delta& x)
446 {
447 static_cast<Derived&>(*this).enter(x);
448 // skip
449 static_cast<Derived&>(*this).leave(x);
450 result = atermpp::down_cast<T>(x);
451 }
452
453 template <class T>
454 void apply(T& result, const process::tau& x)
455 {
456 static_cast<Derived&>(*this).enter(x);
457 // skip
458 static_cast<Derived&>(*this).leave(x);
459 result = atermpp::down_cast<T>(x);
460 }
461
462 template <class T>
463 void apply(T& result, const process::sum& x)
464 {
465 static_cast<Derived&>(*this).enter(x);
466 process::make_sum(result, x.variables(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
467 static_cast<Derived&>(*this).leave(x);
468 }
469
470 template <class T>
471 void apply(T& result, const process::block& x)
472 {
473 static_cast<Derived&>(*this).enter(x);
474 process::make_block(result, x.block_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
475 static_cast<Derived&>(*this).leave(x);
476 }
477
478 template <class T>
479 void apply(T& result, const process::hide& x)
480 {
481 static_cast<Derived&>(*this).enter(x);
482 process::make_hide(result, x.hide_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
483 static_cast<Derived&>(*this).leave(x);
484 }
485
486 template <class T>
487 void apply(T& result, const process::rename& x)
488 {
489 static_cast<Derived&>(*this).enter(x);
490 process::make_rename(result, x.rename_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
491 static_cast<Derived&>(*this).leave(x);
492 }
493
494 template <class T>
495 void apply(T& result, const process::comm& x)
496 {
497 static_cast<Derived&>(*this).enter(x);
498 process::make_comm(result, x.comm_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
499 static_cast<Derived&>(*this).leave(x);
500 }
501
502 template <class T>
503 void apply(T& result, const process::allow& x)
504 {
505 static_cast<Derived&>(*this).enter(x);
506 process::make_allow(result, x.allow_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
507 static_cast<Derived&>(*this).leave(x);
508 }
509
510 template <class T>
511 void apply(T& result, const process::sync& x)
512 {
513 static_cast<Derived&>(*this).enter(x);
514 process::make_sync(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
515 static_cast<Derived&>(*this).leave(x);
516 }
517
518 template <class T>
519 void apply(T& result, const process::at& x)
520 {
521 static_cast<Derived&>(*this).enter(x);
522 process::make_at(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
523 static_cast<Derived&>(*this).leave(x);
524 }
525
526 template <class T>
527 void apply(T& result, const process::seq& x)
528 {
529 static_cast<Derived&>(*this).enter(x);
530 process::make_seq(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
531 static_cast<Derived&>(*this).leave(x);
532 }
533
534 template <class T>
535 void apply(T& result, const process::if_then& x)
536 {
537 static_cast<Derived&>(*this).enter(x);
538 process::make_if_then(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); });
539 static_cast<Derived&>(*this).leave(x);
540 }
541
542 template <class T>
543 void apply(T& result, const process::if_then_else& x)
544 {
545 static_cast<Derived&>(*this).enter(x);
546 process::make_if_then_else(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.else_case()); });
547 static_cast<Derived&>(*this).leave(x);
548 }
549
550 template <class T>
551 void apply(T& result, const process::bounded_init& x)
552 {
553 static_cast<Derived&>(*this).enter(x);
554 process::make_bounded_init(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
555 static_cast<Derived&>(*this).leave(x);
556 }
557
558 template <class T>
559 void apply(T& result, const process::merge& x)
560 {
561 static_cast<Derived&>(*this).enter(x);
562 process::make_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
563 static_cast<Derived&>(*this).leave(x);
564 }
565
566 template <class T>
567 void apply(T& result, const process::left_merge& x)
568 {
569 static_cast<Derived&>(*this).enter(x);
570 process::make_left_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
571 static_cast<Derived&>(*this).leave(x);
572 }
573
574 template <class T>
575 void apply(T& result, const process::choice& x)
576 {
577 static_cast<Derived&>(*this).enter(x);
578 process::make_choice(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
579 static_cast<Derived&>(*this).leave(x);
580 }
581
582 template <class T>
583 void apply(T& result, const process::stochastic_operator& x)
584 {
585 static_cast<Derived&>(*this).enter(x);
586 process::make_stochastic_operator(result, x.variables(), [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
587 static_cast<Derived&>(*this).leave(x);
588 }
589
590 template <class T>
591 void apply(T& result, const process::untyped_process_assignment& x)
592 {
593 static_cast<Derived&>(*this).enter(x);
594 process::make_untyped_process_assignment(result, x.name(), [&](data::untyped_identifier_assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
595 static_cast<Derived&>(*this).leave(x);
596 }
597
598 template <class T>
599 void apply(T& result, const process::process_expression& x)
600 {
601 static_cast<Derived&>(*this).enter(x);
602 if (data::is_untyped_data_parameter(x))
603 {
604 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
605 }
606 else if (process::is_action(x))
607 {
608 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::action>(x));
609 }
610 else if (process::is_process_instance(x))
611 {
612 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance>(x));
613 }
614 else if (process::is_process_instance_assignment(x))
615 {
616 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance_assignment>(x));
617 }
618 else if (process::is_delta(x))
619 {
620 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::delta>(x));
621 }
622 else if (process::is_tau(x))
623 {
624 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::tau>(x));
625 }
626 else if (process::is_sum(x))
627 {
628 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sum>(x));
629 }
630 else if (process::is_block(x))
631 {
632 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::block>(x));
633 }
634 else if (process::is_hide(x))
635 {
636 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::hide>(x));
637 }
638 else if (process::is_rename(x))
639 {
640 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::rename>(x));
641 }
642 else if (process::is_comm(x))
643 {
644 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::comm>(x));
645 }
646 else if (process::is_allow(x))
647 {
648 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::allow>(x));
649 }
650 else if (process::is_sync(x))
651 {
652 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sync>(x));
653 }
654 else if (process::is_at(x))
655 {
656 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::at>(x));
657 }
658 else if (process::is_seq(x))
659 {
660 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::seq>(x));
661 }
662 else if (process::is_if_then(x))
663 {
664 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then>(x));
665 }
666 else if (process::is_if_then_else(x))
667 {
668 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then_else>(x));
669 }
670 else if (process::is_bounded_init(x))
671 {
672 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::bounded_init>(x));
673 }
674 else if (process::is_merge(x))
675 {
676 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::merge>(x));
677 }
678 else if (process::is_left_merge(x))
679 {
680 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::left_merge>(x));
681 }
682 else if (process::is_choice(x))
683 {
684 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::choice>(x));
685 }
686 else if (process::is_stochastic_operator(x))
687 {
688 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::stochastic_operator>(x));
689 }
690 else if (process::is_untyped_process_assignment(x))
691 {
692 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_process_assignment>(x));
693 }
694 static_cast<Derived&>(*this).leave(x);
695 }
696
697};
698
699/// \\brief Builder class
700template <typename Derived>
701struct data_expression_builder: public add_data_expressions<data::data_expression_builder, Derived>
702{
703};
704//--- end generated add_data_expressions code ---//
705
706//--- start generated add_variables code ---//
707template <template <class> class Builder, class Derived>
708struct add_variables: public Builder<Derived>
709{
710 using super = Builder<Derived>;
711 using super::enter;
712 using super::leave;
713 using super::update;
714 using super::apply;
715
716 void update(process::process_specification& x)
717 {
718 static_cast<Derived&>(*this).enter(x);
719 static_cast<Derived&>(*this).update(x.global_variables());
720 static_cast<Derived&>(*this).update(x.equations());
721 process_expression result_init;
722 static_cast<Derived&>(*this).apply(result_init, x.init());
723 x.init() = result_init;
724 static_cast<Derived&>(*this).leave(x);
725 }
726
727 template <class T>
728 void apply(T& result, const process::process_identifier& x)
729 {
730 static_cast<Derived&>(*this).enter(x);
731 process::make_process_identifier(result, x.name(), [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); });
732 static_cast<Derived&>(*this).leave(x);
733 }
734
735 template <class T>
736 void apply(T& result, const process::process_equation& x)
737 {
738 static_cast<Derived&>(*this).enter(x);
739 process::make_process_equation(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.formal_parameters()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.expression()); });
740 static_cast<Derived&>(*this).leave(x);
741 }
742
743 template <class T>
744 void apply(T& result, const process::untyped_multi_action& x)
745 {
746 static_cast<Derived&>(*this).enter(x);
747 process::make_untyped_multi_action(result, [&](data::untyped_data_parameter_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); });
748 static_cast<Derived&>(*this).leave(x);
749 }
750
751 template <class T>
752 void apply(T& result, const process::action& x)
753 {
754 static_cast<Derived&>(*this).enter(x);
755 process::make_action(result, x.label(), [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.arguments()); });
756 static_cast<Derived&>(*this).leave(x);
757 }
758
759 template <class T>
760 void apply(T& result, const process::process_instance& x)
761 {
762 static_cast<Derived&>(*this).enter(x);
763 process::make_process_instance(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.actual_parameters()); });
764 static_cast<Derived&>(*this).leave(x);
765 }
766
767 template <class T>
768 void apply(T& result, const process::process_instance_assignment& x)
769 {
770 static_cast<Derived&>(*this).enter(x);
771 process::make_process_instance_assignment(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, [&](data::assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
772 static_cast<Derived&>(*this).leave(x);
773 }
774
775 template <class T>
776 void apply(T& result, const process::delta& x)
777 {
778 static_cast<Derived&>(*this).enter(x);
779 // skip
780 static_cast<Derived&>(*this).leave(x);
781 result = atermpp::down_cast<T>(x);
782 }
783
784 template <class T>
785 void apply(T& result, const process::tau& x)
786 {
787 static_cast<Derived&>(*this).enter(x);
788 // skip
789 static_cast<Derived&>(*this).leave(x);
790 result = atermpp::down_cast<T>(x);
791 }
792
793 template <class T>
794 void apply(T& result, const process::sum& x)
795 {
796 static_cast<Derived&>(*this).enter(x);
797 process::make_sum(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
798 static_cast<Derived&>(*this).leave(x);
799 }
800
801 template <class T>
802 void apply(T& result, const process::block& x)
803 {
804 static_cast<Derived&>(*this).enter(x);
805 process::make_block(result, x.block_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
806 static_cast<Derived&>(*this).leave(x);
807 }
808
809 template <class T>
810 void apply(T& result, const process::hide& x)
811 {
812 static_cast<Derived&>(*this).enter(x);
813 process::make_hide(result, x.hide_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
814 static_cast<Derived&>(*this).leave(x);
815 }
816
817 template <class T>
818 void apply(T& result, const process::rename& x)
819 {
820 static_cast<Derived&>(*this).enter(x);
821 process::make_rename(result, x.rename_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
822 static_cast<Derived&>(*this).leave(x);
823 }
824
825 template <class T>
826 void apply(T& result, const process::comm& x)
827 {
828 static_cast<Derived&>(*this).enter(x);
829 process::make_comm(result, x.comm_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
830 static_cast<Derived&>(*this).leave(x);
831 }
832
833 template <class T>
834 void apply(T& result, const process::allow& x)
835 {
836 static_cast<Derived&>(*this).enter(x);
837 process::make_allow(result, x.allow_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
838 static_cast<Derived&>(*this).leave(x);
839 }
840
841 template <class T>
842 void apply(T& result, const process::sync& x)
843 {
844 static_cast<Derived&>(*this).enter(x);
845 process::make_sync(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
846 static_cast<Derived&>(*this).leave(x);
847 }
848
849 template <class T>
850 void apply(T& result, const process::at& x)
851 {
852 static_cast<Derived&>(*this).enter(x);
853 process::make_at(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time_stamp()); });
854 static_cast<Derived&>(*this).leave(x);
855 }
856
857 template <class T>
858 void apply(T& result, const process::seq& x)
859 {
860 static_cast<Derived&>(*this).enter(x);
861 process::make_seq(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
862 static_cast<Derived&>(*this).leave(x);
863 }
864
865 template <class T>
866 void apply(T& result, const process::if_then& x)
867 {
868 static_cast<Derived&>(*this).enter(x);
869 process::make_if_then(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); });
870 static_cast<Derived&>(*this).leave(x);
871 }
872
873 template <class T>
874 void apply(T& result, const process::if_then_else& x)
875 {
876 static_cast<Derived&>(*this).enter(x);
877 process::make_if_then_else(result, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.condition()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.else_case()); });
878 static_cast<Derived&>(*this).leave(x);
879 }
880
881 template <class T>
882 void apply(T& result, const process::bounded_init& x)
883 {
884 static_cast<Derived&>(*this).enter(x);
885 process::make_bounded_init(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
886 static_cast<Derived&>(*this).leave(x);
887 }
888
889 template <class T>
890 void apply(T& result, const process::merge& x)
891 {
892 static_cast<Derived&>(*this).enter(x);
893 process::make_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
894 static_cast<Derived&>(*this).leave(x);
895 }
896
897 template <class T>
898 void apply(T& result, const process::left_merge& x)
899 {
900 static_cast<Derived&>(*this).enter(x);
901 process::make_left_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
902 static_cast<Derived&>(*this).leave(x);
903 }
904
905 template <class T>
906 void apply(T& result, const process::choice& x)
907 {
908 static_cast<Derived&>(*this).enter(x);
909 process::make_choice(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
910 static_cast<Derived&>(*this).leave(x);
911 }
912
913 template <class T>
914 void apply(T& result, const process::stochastic_operator& x)
915 {
916 static_cast<Derived&>(*this).enter(x);
917 process::make_stochastic_operator(result, [&](data::variable_list& result){ static_cast<Derived&>(*this).apply(result, x.variables()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
918 static_cast<Derived&>(*this).leave(x);
919 }
920
921 template <class T>
922 void apply(T& result, const process::untyped_process_assignment& x)
923 {
924 static_cast<Derived&>(*this).enter(x);
925 process::make_untyped_process_assignment(result, x.name(), [&](data::untyped_identifier_assignment_list& result){ static_cast<Derived&>(*this).apply(result, x.assignments()); });
926 static_cast<Derived&>(*this).leave(x);
927 }
928
929 template <class T>
930 void apply(T& result, const process::process_expression& x)
931 {
932 static_cast<Derived&>(*this).enter(x);
933 if (data::is_untyped_data_parameter(x))
934 {
935 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
936 }
937 else if (process::is_action(x))
938 {
939 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::action>(x));
940 }
941 else if (process::is_process_instance(x))
942 {
943 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance>(x));
944 }
945 else if (process::is_process_instance_assignment(x))
946 {
947 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance_assignment>(x));
948 }
949 else if (process::is_delta(x))
950 {
951 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::delta>(x));
952 }
953 else if (process::is_tau(x))
954 {
955 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::tau>(x));
956 }
957 else if (process::is_sum(x))
958 {
959 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sum>(x));
960 }
961 else if (process::is_block(x))
962 {
963 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::block>(x));
964 }
965 else if (process::is_hide(x))
966 {
967 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::hide>(x));
968 }
969 else if (process::is_rename(x))
970 {
971 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::rename>(x));
972 }
973 else if (process::is_comm(x))
974 {
975 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::comm>(x));
976 }
977 else if (process::is_allow(x))
978 {
979 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::allow>(x));
980 }
981 else if (process::is_sync(x))
982 {
983 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sync>(x));
984 }
985 else if (process::is_at(x))
986 {
987 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::at>(x));
988 }
989 else if (process::is_seq(x))
990 {
991 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::seq>(x));
992 }
993 else if (process::is_if_then(x))
994 {
995 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then>(x));
996 }
997 else if (process::is_if_then_else(x))
998 {
999 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then_else>(x));
1000 }
1001 else if (process::is_bounded_init(x))
1002 {
1003 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::bounded_init>(x));
1004 }
1005 else if (process::is_merge(x))
1006 {
1007 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::merge>(x));
1008 }
1009 else if (process::is_left_merge(x))
1010 {
1011 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::left_merge>(x));
1012 }
1013 else if (process::is_choice(x))
1014 {
1015 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::choice>(x));
1016 }
1017 else if (process::is_stochastic_operator(x))
1018 {
1019 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::stochastic_operator>(x));
1020 }
1021 else if (process::is_untyped_process_assignment(x))
1022 {
1023 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_process_assignment>(x));
1024 }
1025 static_cast<Derived&>(*this).leave(x);
1026 }
1027
1028};
1029
1030/// \\brief Builder class
1031template <typename Derived>
1032struct variable_builder: public add_variables<data::data_expression_builder, Derived>
1033{
1034};
1035//--- end generated add_variables code ---//
1036
1037// Adds process expression traversal to a builder
1038//--- start generated add_process_expressions code ---//
1039template <template <class> class Builder, class Derived>
1040struct add_process_expressions: public Builder<Derived>
1041{
1042 using super = Builder<Derived>;
1043 using super::enter;
1044 using super::leave;
1045 using super::update;
1046 using super::apply;
1047
1048 void update(process::process_specification& x)
1049 {
1050 static_cast<Derived&>(*this).enter(x);
1051 static_cast<Derived&>(*this).update(x.equations());
1052 process_expression result_init;
1053 static_cast<Derived&>(*this).apply(result_init, x.init());
1054 x.init() = result_init;
1055 static_cast<Derived&>(*this).leave(x);
1056 }
1057
1058 template <class T>
1059 void apply(T& result, const process::process_equation& x)
1060 {
1061 static_cast<Derived&>(*this).enter(x);
1062 process::make_process_equation(result, x.identifier(), x.formal_parameters(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.expression()); });
1063 static_cast<Derived&>(*this).leave(x);
1064 }
1065
1066 template <class T>
1067 void apply(T& result, const process::action& x)
1068 {
1069 static_cast<Derived&>(*this).enter(x);
1070 // skip
1071 static_cast<Derived&>(*this).leave(x);
1072 result = atermpp::down_cast<T>(x);
1073 }
1074
1075 template <class T>
1076 void apply(T& result, const process::process_instance& x)
1077 {
1078 static_cast<Derived&>(*this).enter(x);
1079 // skip
1080 static_cast<Derived&>(*this).leave(x);
1081 result = atermpp::down_cast<T>(x);
1082 }
1083
1084 template <class T>
1085 void apply(T& result, const process::process_instance_assignment& x)
1086 {
1087 static_cast<Derived&>(*this).enter(x);
1088 // skip
1089 static_cast<Derived&>(*this).leave(x);
1090 result = atermpp::down_cast<T>(x);
1091 }
1092
1093 template <class T>
1094 void apply(T& result, const process::delta& x)
1095 {
1096 static_cast<Derived&>(*this).enter(x);
1097 // skip
1098 static_cast<Derived&>(*this).leave(x);
1099 result = atermpp::down_cast<T>(x);
1100 }
1101
1102 template <class T>
1103 void apply(T& result, const process::tau& x)
1104 {
1105 static_cast<Derived&>(*this).enter(x);
1106 // skip
1107 static_cast<Derived&>(*this).leave(x);
1108 result = atermpp::down_cast<T>(x);
1109 }
1110
1111 template <class T>
1112 void apply(T& result, const process::sum& x)
1113 {
1114 static_cast<Derived&>(*this).enter(x);
1115 process::make_sum(result, x.variables(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1116 static_cast<Derived&>(*this).leave(x);
1117 }
1118
1119 template <class T>
1120 void apply(T& result, const process::block& x)
1121 {
1122 static_cast<Derived&>(*this).enter(x);
1123 process::make_block(result, x.block_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1124 static_cast<Derived&>(*this).leave(x);
1125 }
1126
1127 template <class T>
1128 void apply(T& result, const process::hide& x)
1129 {
1130 static_cast<Derived&>(*this).enter(x);
1131 process::make_hide(result, x.hide_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1132 static_cast<Derived&>(*this).leave(x);
1133 }
1134
1135 template <class T>
1136 void apply(T& result, const process::rename& x)
1137 {
1138 static_cast<Derived&>(*this).enter(x);
1139 process::make_rename(result, x.rename_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1140 static_cast<Derived&>(*this).leave(x);
1141 }
1142
1143 template <class T>
1144 void apply(T& result, const process::comm& x)
1145 {
1146 static_cast<Derived&>(*this).enter(x);
1147 process::make_comm(result, x.comm_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1148 static_cast<Derived&>(*this).leave(x);
1149 }
1150
1151 template <class T>
1152 void apply(T& result, const process::allow& x)
1153 {
1154 static_cast<Derived&>(*this).enter(x);
1155 process::make_allow(result, x.allow_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1156 static_cast<Derived&>(*this).leave(x);
1157 }
1158
1159 template <class T>
1160 void apply(T& result, const process::sync& x)
1161 {
1162 static_cast<Derived&>(*this).enter(x);
1163 process::make_sync(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1164 static_cast<Derived&>(*this).leave(x);
1165 }
1166
1167 template <class T>
1168 void apply(T& result, const process::at& x)
1169 {
1170 static_cast<Derived&>(*this).enter(x);
1171 process::make_at(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, x.time_stamp());
1172 static_cast<Derived&>(*this).leave(x);
1173 }
1174
1175 template <class T>
1176 void apply(T& result, const process::seq& x)
1177 {
1178 static_cast<Derived&>(*this).enter(x);
1179 process::make_seq(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1180 static_cast<Derived&>(*this).leave(x);
1181 }
1182
1183 template <class T>
1184 void apply(T& result, const process::if_then& x)
1185 {
1186 static_cast<Derived&>(*this).enter(x);
1187 process::make_if_then(result, x.condition(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); });
1188 static_cast<Derived&>(*this).leave(x);
1189 }
1190
1191 template <class T>
1192 void apply(T& result, const process::if_then_else& x)
1193 {
1194 static_cast<Derived&>(*this).enter(x);
1195 process::make_if_then_else(result, x.condition(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.else_case()); });
1196 static_cast<Derived&>(*this).leave(x);
1197 }
1198
1199 template <class T>
1200 void apply(T& result, const process::bounded_init& x)
1201 {
1202 static_cast<Derived&>(*this).enter(x);
1203 process::make_bounded_init(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1204 static_cast<Derived&>(*this).leave(x);
1205 }
1206
1207 template <class T>
1208 void apply(T& result, const process::merge& x)
1209 {
1210 static_cast<Derived&>(*this).enter(x);
1211 process::make_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1212 static_cast<Derived&>(*this).leave(x);
1213 }
1214
1215 template <class T>
1216 void apply(T& result, const process::left_merge& x)
1217 {
1218 static_cast<Derived&>(*this).enter(x);
1219 process::make_left_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1220 static_cast<Derived&>(*this).leave(x);
1221 }
1222
1223 template <class T>
1224 void apply(T& result, const process::choice& x)
1225 {
1226 static_cast<Derived&>(*this).enter(x);
1227 process::make_choice(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1228 static_cast<Derived&>(*this).leave(x);
1229 }
1230
1231 template <class T>
1232 void apply(T& result, const process::stochastic_operator& x)
1233 {
1234 static_cast<Derived&>(*this).enter(x);
1235 process::make_stochastic_operator(result, x.variables(), x.distribution(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1236 static_cast<Derived&>(*this).leave(x);
1237 }
1238
1239 template <class T>
1240 void apply(T& result, const process::untyped_process_assignment& x)
1241 {
1242 static_cast<Derived&>(*this).enter(x);
1243 // skip
1244 static_cast<Derived&>(*this).leave(x);
1245 result = atermpp::down_cast<T>(x);
1246 }
1247
1248 template <class T>
1249 void apply(T& result, const process::process_expression& x)
1250 {
1251 static_cast<Derived&>(*this).enter(x);
1252 if (data::is_untyped_data_parameter(x))
1253 {
1254 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1255 }
1256 else if (process::is_action(x))
1257 {
1258 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::action>(x));
1259 }
1260 else if (process::is_process_instance(x))
1261 {
1262 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance>(x));
1263 }
1264 else if (process::is_process_instance_assignment(x))
1265 {
1266 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance_assignment>(x));
1267 }
1268 else if (process::is_delta(x))
1269 {
1270 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::delta>(x));
1271 }
1272 else if (process::is_tau(x))
1273 {
1274 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::tau>(x));
1275 }
1276 else if (process::is_sum(x))
1277 {
1278 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sum>(x));
1279 }
1280 else if (process::is_block(x))
1281 {
1282 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::block>(x));
1283 }
1284 else if (process::is_hide(x))
1285 {
1286 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::hide>(x));
1287 }
1288 else if (process::is_rename(x))
1289 {
1290 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::rename>(x));
1291 }
1292 else if (process::is_comm(x))
1293 {
1294 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::comm>(x));
1295 }
1296 else if (process::is_allow(x))
1297 {
1298 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::allow>(x));
1299 }
1300 else if (process::is_sync(x))
1301 {
1302 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sync>(x));
1303 }
1304 else if (process::is_at(x))
1305 {
1306 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::at>(x));
1307 }
1308 else if (process::is_seq(x))
1309 {
1310 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::seq>(x));
1311 }
1312 else if (process::is_if_then(x))
1313 {
1314 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then>(x));
1315 }
1316 else if (process::is_if_then_else(x))
1317 {
1318 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then_else>(x));
1319 }
1320 else if (process::is_bounded_init(x))
1321 {
1322 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::bounded_init>(x));
1323 }
1324 else if (process::is_merge(x))
1325 {
1326 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::merge>(x));
1327 }
1328 else if (process::is_left_merge(x))
1329 {
1330 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::left_merge>(x));
1331 }
1332 else if (process::is_choice(x))
1333 {
1334 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::choice>(x));
1335 }
1336 else if (process::is_stochastic_operator(x))
1337 {
1338 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::stochastic_operator>(x));
1339 }
1340 else if (process::is_untyped_process_assignment(x))
1341 {
1342 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_process_assignment>(x));
1343 }
1344 static_cast<Derived&>(*this).leave(x);
1345 }
1346
1347};
1348
1349/// \\brief Builder class
1350template <typename Derived>
1351struct process_expression_builder: public add_process_expressions<process::process_builder_base, Derived>
1352{
1353};
1354//--- end generated add_process_expressions code ---//
1355
1356//--- start generated add_process_identifiers code ---//
1357template <template <class> class Builder, class Derived>
1358struct add_process_identifiers: public Builder<Derived>
1359{
1360 using super = Builder<Derived>;
1361 using super::enter;
1362 using super::leave;
1363 using super::update;
1364 using super::apply;
1365
1366 void update(process::process_specification& x)
1367 {
1368 static_cast<Derived&>(*this).enter(x);
1369 static_cast<Derived&>(*this).update(x.equations());
1370 process_expression result_init;
1371 static_cast<Derived&>(*this).apply(result_init, x.init());
1372 x.init() = result_init;
1373 static_cast<Derived&>(*this).leave(x);
1374 }
1375
1376 template <class T>
1377 void apply(T& result, const process::process_identifier& x)
1378 {
1379 static_cast<Derived&>(*this).enter(x);
1380 // skip
1381 static_cast<Derived&>(*this).leave(x);
1382 result = atermpp::down_cast<T>(x);
1383 }
1384
1385 template <class T>
1386 void apply(T& result, const process::process_equation& x)
1387 {
1388 static_cast<Derived&>(*this).enter(x);
1389 process::make_process_equation(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, x.formal_parameters(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.expression()); });
1390 static_cast<Derived&>(*this).leave(x);
1391 }
1392
1393 template <class T>
1394 void apply(T& result, const process::action& x)
1395 {
1396 static_cast<Derived&>(*this).enter(x);
1397 // skip
1398 static_cast<Derived&>(*this).leave(x);
1399 result = atermpp::down_cast<T>(x);
1400 }
1401
1402 template <class T>
1403 void apply(T& result, const process::process_instance& x)
1404 {
1405 static_cast<Derived&>(*this).enter(x);
1406 process::make_process_instance(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, x.actual_parameters());
1407 static_cast<Derived&>(*this).leave(x);
1408 }
1409
1410 template <class T>
1411 void apply(T& result, const process::process_instance_assignment& x)
1412 {
1413 static_cast<Derived&>(*this).enter(x);
1414 process::make_process_instance_assignment(result, [&](process_identifier& result){ static_cast<Derived&>(*this).apply(result, x.identifier()); }, x.assignments());
1415 static_cast<Derived&>(*this).leave(x);
1416 }
1417
1418 template <class T>
1419 void apply(T& result, const process::delta& x)
1420 {
1421 static_cast<Derived&>(*this).enter(x);
1422 // skip
1423 static_cast<Derived&>(*this).leave(x);
1424 result = atermpp::down_cast<T>(x);
1425 }
1426
1427 template <class T>
1428 void apply(T& result, const process::tau& x)
1429 {
1430 static_cast<Derived&>(*this).enter(x);
1431 // skip
1432 static_cast<Derived&>(*this).leave(x);
1433 result = atermpp::down_cast<T>(x);
1434 }
1435
1436 template <class T>
1437 void apply(T& result, const process::sum& x)
1438 {
1439 static_cast<Derived&>(*this).enter(x);
1440 process::make_sum(result, x.variables(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1441 static_cast<Derived&>(*this).leave(x);
1442 }
1443
1444 template <class T>
1445 void apply(T& result, const process::block& x)
1446 {
1447 static_cast<Derived&>(*this).enter(x);
1448 process::make_block(result, x.block_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1449 static_cast<Derived&>(*this).leave(x);
1450 }
1451
1452 template <class T>
1453 void apply(T& result, const process::hide& x)
1454 {
1455 static_cast<Derived&>(*this).enter(x);
1456 process::make_hide(result, x.hide_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1457 static_cast<Derived&>(*this).leave(x);
1458 }
1459
1460 template <class T>
1461 void apply(T& result, const process::rename& x)
1462 {
1463 static_cast<Derived&>(*this).enter(x);
1464 process::make_rename(result, x.rename_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1465 static_cast<Derived&>(*this).leave(x);
1466 }
1467
1468 template <class T>
1469 void apply(T& result, const process::comm& x)
1470 {
1471 static_cast<Derived&>(*this).enter(x);
1472 process::make_comm(result, x.comm_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1473 static_cast<Derived&>(*this).leave(x);
1474 }
1475
1476 template <class T>
1477 void apply(T& result, const process::allow& x)
1478 {
1479 static_cast<Derived&>(*this).enter(x);
1480 process::make_allow(result, x.allow_set(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1481 static_cast<Derived&>(*this).leave(x);
1482 }
1483
1484 template <class T>
1485 void apply(T& result, const process::sync& x)
1486 {
1487 static_cast<Derived&>(*this).enter(x);
1488 process::make_sync(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1489 static_cast<Derived&>(*this).leave(x);
1490 }
1491
1492 template <class T>
1493 void apply(T& result, const process::at& x)
1494 {
1495 static_cast<Derived&>(*this).enter(x);
1496 process::make_at(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); }, x.time_stamp());
1497 static_cast<Derived&>(*this).leave(x);
1498 }
1499
1500 template <class T>
1501 void apply(T& result, const process::seq& x)
1502 {
1503 static_cast<Derived&>(*this).enter(x);
1504 process::make_seq(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1505 static_cast<Derived&>(*this).leave(x);
1506 }
1507
1508 template <class T>
1509 void apply(T& result, const process::if_then& x)
1510 {
1511 static_cast<Derived&>(*this).enter(x);
1512 process::make_if_then(result, x.condition(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); });
1513 static_cast<Derived&>(*this).leave(x);
1514 }
1515
1516 template <class T>
1517 void apply(T& result, const process::if_then_else& x)
1518 {
1519 static_cast<Derived&>(*this).enter(x);
1520 process::make_if_then_else(result, x.condition(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.then_case()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.else_case()); });
1521 static_cast<Derived&>(*this).leave(x);
1522 }
1523
1524 template <class T>
1525 void apply(T& result, const process::bounded_init& x)
1526 {
1527 static_cast<Derived&>(*this).enter(x);
1528 process::make_bounded_init(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1529 static_cast<Derived&>(*this).leave(x);
1530 }
1531
1532 template <class T>
1533 void apply(T& result, const process::merge& x)
1534 {
1535 static_cast<Derived&>(*this).enter(x);
1536 process::make_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1537 static_cast<Derived&>(*this).leave(x);
1538 }
1539
1540 template <class T>
1541 void apply(T& result, const process::left_merge& x)
1542 {
1543 static_cast<Derived&>(*this).enter(x);
1544 process::make_left_merge(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1545 static_cast<Derived&>(*this).leave(x);
1546 }
1547
1548 template <class T>
1549 void apply(T& result, const process::choice& x)
1550 {
1551 static_cast<Derived&>(*this).enter(x);
1552 process::make_choice(result, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.left()); }, [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.right()); });
1553 static_cast<Derived&>(*this).leave(x);
1554 }
1555
1556 template <class T>
1557 void apply(T& result, const process::stochastic_operator& x)
1558 {
1559 static_cast<Derived&>(*this).enter(x);
1560 process::make_stochastic_operator(result, x.variables(), x.distribution(), [&](process_expression& result){ static_cast<Derived&>(*this).apply(result, x.operand()); });
1561 static_cast<Derived&>(*this).leave(x);
1562 }
1563
1564 template <class T>
1565 void apply(T& result, const process::untyped_process_assignment& x)
1566 {
1567 static_cast<Derived&>(*this).enter(x);
1568 // skip
1569 static_cast<Derived&>(*this).leave(x);
1570 result = atermpp::down_cast<T>(x);
1571 }
1572
1573 template <class T>
1574 void apply(T& result, const process::process_expression& x)
1575 {
1576 static_cast<Derived&>(*this).enter(x);
1577 if (data::is_untyped_data_parameter(x))
1578 {
1579 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<data::untyped_data_parameter>(x));
1580 }
1581 else if (process::is_action(x))
1582 {
1583 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::action>(x));
1584 }
1585 else if (process::is_process_instance(x))
1586 {
1587 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance>(x));
1588 }
1589 else if (process::is_process_instance_assignment(x))
1590 {
1591 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::process_instance_assignment>(x));
1592 }
1593 else if (process::is_delta(x))
1594 {
1595 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::delta>(x));
1596 }
1597 else if (process::is_tau(x))
1598 {
1599 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::tau>(x));
1600 }
1601 else if (process::is_sum(x))
1602 {
1603 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sum>(x));
1604 }
1605 else if (process::is_block(x))
1606 {
1607 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::block>(x));
1608 }
1609 else if (process::is_hide(x))
1610 {
1611 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::hide>(x));
1612 }
1613 else if (process::is_rename(x))
1614 {
1615 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::rename>(x));
1616 }
1617 else if (process::is_comm(x))
1618 {
1619 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::comm>(x));
1620 }
1621 else if (process::is_allow(x))
1622 {
1623 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::allow>(x));
1624 }
1625 else if (process::is_sync(x))
1626 {
1627 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::sync>(x));
1628 }
1629 else if (process::is_at(x))
1630 {
1631 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::at>(x));
1632 }
1633 else if (process::is_seq(x))
1634 {
1635 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::seq>(x));
1636 }
1637 else if (process::is_if_then(x))
1638 {
1639 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then>(x));
1640 }
1641 else if (process::is_if_then_else(x))
1642 {
1643 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::if_then_else>(x));
1644 }
1645 else if (process::is_bounded_init(x))
1646 {
1647 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::bounded_init>(x));
1648 }
1649 else if (process::is_merge(x))
1650 {
1651 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::merge>(x));
1652 }
1653 else if (process::is_left_merge(x))
1654 {
1655 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::left_merge>(x));
1656 }
1657 else if (process::is_choice(x))
1658 {
1659 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::choice>(x));
1660 }
1661 else if (process::is_stochastic_operator(x))
1662 {
1663 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::stochastic_operator>(x));
1664 }
1665 else if (process::is_untyped_process_assignment(x))
1666 {
1667 static_cast<Derived&>(*this).apply(result, atermpp::down_cast<process::untyped_process_assignment>(x));
1668 }
1669 static_cast<Derived&>(*this).leave(x);
1670 }
1671
1672};
1673
1674/// \\brief Builder class
1675template <typename Derived>
1676struct process_identifier_builder: public add_process_identifiers<process::process_builder_base, Derived>
1677{
1678};
1679//--- end generated add_process_identifiers code ---//
1680
1681} // namespace mcrl2::process
1682
1683#endif // MCRL2_PROCESS_BUILDER_H
atermpp::aterm_string::operator=
aterm_string & operator=(const aterm_string &t) noexcept=default
atermpp::aterm::aterm
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:26
atermpp::unordered_map
A unordered_map class in which aterms can be stored.
Definition unordered_map.h:41
mcrl2::data::abstraction
An abstraction expression.
Definition abstraction.h:23
mcrl2::data::abstraction::variables
const variable_list & variables() const
Definition abstraction.h:60
mcrl2::data::abstraction::body
const data_expression & body() const
Definition abstraction.h:65
mcrl2::data::abstraction::binding_operator
const binder_type & binding_operator() const
Definition abstraction.h:55
mcrl2::data::alias
\brief A sort alias
Definition alias.h:23
mcrl2::data::alias::alias
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:39
mcrl2::data::assignment
\brief Assignment of a data expression to a variable
Definition assignment.h:88
mcrl2::data::assignment::rhs
const data_expression & rhs() const
Definition assignment.h:119
mcrl2::data::assignment::lhs
const variable & lhs() const
Definition assignment.h:114
mcrl2::data::basic_sort
\brief A basic sort
Definition basic_sort.h:25
mcrl2::data::data_expression
data expression.
Definition data_expression.h:130
mcrl2::data::data_expression::operator=
data_expression & operator=(const data_expression &) noexcept=default
mcrl2::data::data_expression::data_expression
data_expression()
\brief Default constructor X3.
Definition data_expression.h:133
mcrl2::data::data_expression::operator=
data_expression & operator=(data_expression &&) noexcept=default
mcrl2::data::data_expression::sort
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
mcrl2::data::data_expression::data_expression
data_expression(const data_expression &) noexcept=default
Move semantics.
mcrl2::data::data_specification
data specification.
Definition data_specification.h:50
mcrl2::data::detail::inequality_consistency_cache
Definition linear_inequalities.h:1435
mcrl2::data::detail::inequality_consistency_cache::inequality_consistency_cache
inequality_consistency_cache()
Definition linear_inequalities.h:1444
mcrl2::data::detail::inequality_consistency_cache::add_consistent_inequality_set
void add_consistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
Definition linear_inequalities.h:1479
mcrl2::data::detail::inequality_consistency_cache::operator=
inequality_consistency_cache & operator=(const inequality_consistency_cache &)=delete
mcrl2::data::detail::inequality_consistency_cache::inequality_consistency_cache
inequality_consistency_cache(const inequality_consistency_cache &)=delete
mcrl2::data::detail::inequality_consistency_cache::is_consistent
bool is_consistent(const std::vector< linear_inequality > &inequalities_in_) const
Definition linear_inequalities.h:1449
mcrl2::data::detail::inequality_consistency_cache::m_cache
std::unique_ptr< inequality_inconsistency_cache_base > m_cache
Definition linear_inequalities.h:1437
mcrl2::data::detail::inequality_inconsistency_cache_base
Definition linear_inequalities.h:1306
mcrl2::data::detail::inequality_inconsistency_cache_base::operator=
inequality_inconsistency_cache_base & operator=(const inequality_inconsistency_cache_base &)=delete
mcrl2::data::detail::inequality_inconsistency_cache_base::m_inequality
linear_inequality m_inequality
Definition linear_inequalities.h:1312
mcrl2::data::detail::inequality_inconsistency_cache_base::m_present_branch
std::unique_ptr< inequality_inconsistency_cache_base > m_present_branch
Definition linear_inequalities.h:1313
mcrl2::data::detail::inequality_inconsistency_cache_base::m_non_present_branch
std::unique_ptr< inequality_inconsistency_cache_base > m_non_present_branch
Definition linear_inequalities.h:1314
mcrl2::data::detail::inequality_inconsistency_cache_base::inequality_inconsistency_cache_base
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)
Definition linear_inequalities.h:1325
mcrl2::data::detail::inequality_inconsistency_cache_base::inequality_inconsistency_cache_base
inequality_inconsistency_cache_base(const inequality_inconsistency_cache_base &)=delete
mcrl2::data::detail::inequality_inconsistency_cache_base::m_node
node_type m_node
Definition linear_inequalities.h:1311
mcrl2::data::detail::inequality_inconsistency_cache_base::inequality_inconsistency_cache_base
inequality_inconsistency_cache_base(const node_type node)
Definition linear_inequalities.h:1321
mcrl2::data::detail::inequality_inconsistency_cache
Definition linear_inequalities.h:1338
mcrl2::data::detail::inequality_inconsistency_cache::is_inconsistent
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in_) const
Definition linear_inequalities.h:1351
mcrl2::data::detail::inequality_inconsistency_cache::inequality_inconsistency_cache
inequality_inconsistency_cache()
Definition linear_inequalities.h:1347
mcrl2::data::detail::inequality_inconsistency_cache::operator=
inequality_inconsistency_cache & operator=(const inequality_consistency_cache &)=delete
mcrl2::data::detail::inequality_inconsistency_cache::inequality_inconsistency_cache
inequality_inconsistency_cache(const inequality_inconsistency_cache &)=delete
mcrl2::data::detail::inequality_inconsistency_cache::add_inconsistent_inequality_set
void add_inconsistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
Definition linear_inequalities.h:1379
mcrl2::data::detail::inequality_inconsistency_cache::m_cache
std::unique_ptr< inequality_inconsistency_cache_base > m_cache
Definition linear_inequalities.h:1340
mcrl2::data::detail::lhs_t
Definition linear_inequalities.h:174
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const aterm &t)
Constructor from an aterm.
Definition linear_inequalities.h:182
mcrl2::data::detail::lhs_t::operator[]
const data_expression & operator[](const variable &v) const
Give the factor of variable v.
Definition linear_inequalities.h:222
mcrl2::data::detail::lhs_t::transform_to_data_expression
data_expression transform_to_data_expression() const
Definition linear_inequalities.h:266
mcrl2::data::detail::lhs_t::erase
lhs_t erase(const variable &v) const
Erase a variable and its factor.
Definition linear_inequalities.h:208
mcrl2::data::detail::lhs_t::count
std::size_t count(const variable &v) const
Give the factor of variable v.
Definition linear_inequalities.h:233
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
Constructor.
Definition linear_inequalities.h:194
mcrl2::data::detail::lhs_t::evaluate
data_expression evaluate(const SubstitutionFunction &beta, const rewriter &r) const
Evaluate the variables in this lhs_t according to the subsitution function.
Definition linear_inequalities.h:245
mcrl2::data::detail::lhs_t::find
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.
Definition linear_inequalities.h:199
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const ITERATOR begin, const ITERATOR end)
Constructor.
Definition linear_inequalities.h:188
mcrl2::data::detail::lhs_t::lhs_t
lhs_t()
Constructor.
Definition linear_inequalities.h:177
mcrl2::data::detail::variable_with_a_rational_factor
Definition linear_inequalities.h:135
mcrl2::data::detail::variable_with_a_rational_factor::variable_with_a_rational_factor
variable_with_a_rational_factor(const variable &v, const data_expression &f)
Definition linear_inequalities.h:138
mcrl2::data::detail::variable_with_a_rational_factor::variable_name
const variable & variable_name() const
Definition linear_inequalities.h:145
mcrl2::data::detail::variable_with_a_rational_factor::transform_to_data_expression
data_expression transform_to_data_expression() const
Definition linear_inequalities.h:165
mcrl2::data::detail::variable_with_a_rational_factor::is_variable_with_a_rational_factor
bool is_variable_with_a_rational_factor() const
Definition linear_inequalities.h:159
mcrl2::data::detail::variable_with_a_rational_factor::factor
const data_expression & factor() const
Definition linear_inequalities.h:152
mcrl2::data::function_sort
\brief A function sort
Definition function_sort.h:25
mcrl2::data::function_symbol
\brief A function symbol
Definition function_symbol.h:27
mcrl2::data::function_symbol::operator=
function_symbol & operator=(function_symbol &&) noexcept=default
mcrl2::data::function_symbol::function_symbol
function_symbol()
Default constructor.
Definition function_symbol.h:48
mcrl2::data::linear_inequality
Definition linear_inequalities.h:559
mcrl2::data::linear_inequality::lhs
const detail::lhs_t & lhs() const
Definition linear_inequalities.h:774
mcrl2::data::linear_inequality::invert
linear_inequality invert(const rewriter &r)
Definition linear_inequalities.h:879
mcrl2::data::linear_inequality::typical_pair
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,...
Definition linear_inequalities.h:835
mcrl2::data::linear_inequality::linear_inequality
linear_inequality()
Constructor yielding an inconsistent inequality.
Definition linear_inequalities.h:641
mcrl2::data::linear_inequality::is_true
bool is_true(const rewriter &r) const
Definition linear_inequalities.h:825
mcrl2::data::linear_inequality::add_variables
void add_variables(std::set< variable > &variable_set) const
Definition linear_inequalities.h:900
mcrl2::data::linear_inequality::is_false
bool is_false(const rewriter &r) const
Definition linear_inequalities.h:818
mcrl2::data::linear_inequality::linear_inequality
linear_inequality(const data_expression &e, const rewriter &r)
Constructor that constructs a linear inequality out of a data expression.
Definition linear_inequalities.h:725
mcrl2::data::linear_inequality::linear_inequality
linear_inequality(const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false)
constructor.
Definition linear_inequalities.h:677
mcrl2::data::linear_inequality::transform_to_data_expression
data_expression transform_to_data_expression() const
Definition linear_inequalities.h:803
mcrl2::data::linear_inequality::parse_and_store_expression
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())
Definition linear_inequalities.h:569
mcrl2::data::linear_inequality::linear_inequality
linear_inequality(const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)
Basic constructor.
Definition linear_inequalities.h:646
mcrl2::data::linear_inequality::lhs_begin
detail::lhs_t::const_iterator lhs_begin() const
Definition linear_inequalities.h:764
mcrl2::data::linear_inequality::lhs_end
detail::lhs_t::const_iterator lhs_end() const
Definition linear_inequalities.h:769
mcrl2::data::linear_inequality::linear_inequality
linear_inequality(const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)
constructor.
Definition linear_inequalities.h:657
mcrl2::data::linear_inequality::rhs
const data_expression & rhs() const
Definition linear_inequalities.h:779
mcrl2::data::linear_inequality::get_factor_for_a_variable
data_expression get_factor_for_a_variable(const variable &x)
Definition linear_inequalities.h:784
mcrl2::data::linear_inequality::comparison
detail::comparison_t comparison() const
Definition linear_inequalities.h:789
mcrl2::data::maintain_variables_in_rhs::assignment
Wrapper clas s for internal storage and substitution updates using operator()
Definition maintain_variables_in_rhs.h:51
mcrl2::data::maintain_variables_in_rhs::assignment::m_variables_in_rhs
std::multiset< variable_type > & m_variables_in_rhs
Definition maintain_variables_in_rhs.h:55
mcrl2::data::maintain_variables_in_rhs::assignment::assignment
assignment(const variable_type &v, Substitution &sigma, std::multiset< variable_type > &variables_in_rhs, std::set< variable_type > &scratch_set)
Constructor.
Definition maintain_variables_in_rhs.h:64
mcrl2::data::maintain_variables_in_rhs::assignment::m_variable
const variable_type & m_variable
Definition maintain_variables_in_rhs.h:53
mcrl2::data::maintain_variables_in_rhs::assignment::operator=
assignment & operator=(const expression_type &e)
Actual assignment.
Definition maintain_variables_in_rhs.h:75
mcrl2::data::maintain_variables_in_rhs::assignment::m_scratch_set
std::set< variable_type > & m_scratch_set
Definition maintain_variables_in_rhs.h:56
mcrl2::data::maintain_variables_in_rhs::assignment::m_sigma
Substitution & m_sigma
Definition maintain_variables_in_rhs.h:54
mcrl2::data::maintain_variables_in_rhs
Wrapper that extends any substitution to a substitution maintaining the vars in its rhs.
Definition maintain_variables_in_rhs.h:34
mcrl2::data::maintain_variables_in_rhs::variable_occurs_in_a_rhs
bool variable_occurs_in_a_rhs(const variable_type &v)
Indicates whether a variable occurs in some rhs of this substitution.
Definition maintain_variables_in_rhs.h:125
mcrl2::data::maintain_variables_in_rhs::operator[]
assignment operator[](variable_type const &v)
Assigment operator.
Definition maintain_variables_in_rhs.h:105
mcrl2::data::maintain_variables_in_rhs::clear
void clear()
Clear substitutions.
Definition maintain_variables_in_rhs.h:111
mcrl2::data::maintain_variables_in_rhs::m_scratch_set
std::set< variable_type > m_scratch_set
Definition maintain_variables_in_rhs.h:43
mcrl2::data::maintain_variables_in_rhs::variables_in_rhs
const std::multiset< variable > & variables_in_rhs()
Provides a set of variables that occur in the right hand sides of the assignments.
Definition maintain_variables_in_rhs.h:118
mcrl2::data::maintain_variables_in_rhs::maintain_variables_in_rhs
maintain_variables_in_rhs()=default
Default constructor.
mcrl2::data::maintain_variables_in_rhs::m_variables_in_rhs
std::multiset< variable_type > m_variables_in_rhs
Definition maintain_variables_in_rhs.h:42
mcrl2::data::representative_generator
Components for generating an arbitrary element of a sort.
Definition representative_generator.h:50
mcrl2::data::representative_generator::operator()
data_expression operator()(const sort_expression &sort)
Returns a representative of a sort.
Definition representative_generator.h:266
mcrl2::data::rewriter
Rewriter that operates on data expressions.
Definition rewriter.h:84
mcrl2::data::rewriter::operator()
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Definition rewriter.h:161
mcrl2::data::set_identifier_generator
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
Definition set_identifier_generator.h:27
mcrl2::data::sort_expression
\brief A sort expression
Definition sort_expression.h:60
mcrl2::data::sort_expression::operator=
sort_expression & operator=(const sort_expression &) noexcept=default
mcrl2::data::sort_specification
Definition sort_specification.h:44
mcrl2::data::structured_sort_constructor
\brief A constructor for a structured sort
Definition structured_sort_constructor.h:26
mcrl2::data::structured_sort_constructor::constructor_function
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
Definition structured_sort_constructor.h:151
mcrl2::data::structured_sort_constructor::recogniser_function
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...
Definition structured_sort_constructor.h:180
mcrl2::data::structured_sort
structured sort.
Definition structured_sort.h:54
mcrl2::data::untyped_data_parameter
\brief An untyped parameter
Definition untyped_data_parameter.h:24
mcrl2::data::variable
\brief A data variable
Definition variable.h:25
mcrl2::data::variable::name
const core::identifier_string & name() const
Definition variable.h:35
mcrl2::data::variable::operator=
variable & operator=(variable &&) noexcept=default
mcrl2::data::variable::sort
const sort_expression & sort() const
Definition variable.h:40
mcrl2::data::where_clause
\brief A where expression
Definition where_clause.h:23
mcrl2::data::where_clause::where_clause
where_clause(const atermpp::aterm &term)
Definition where_clause.h:32
mcrl2::lps::action_summand
LPS summand containing a multi-action.
Definition action_summand.h:23
mcrl2::lps::action_summand::m_multi_action
lps::multi_action m_multi_action
The summation variables of the summand.
Definition action_summand.h:29
mcrl2::lps::action_summand::action_summand
action_summand(const action_summand &) noexcept=default
Move semantics.
mcrl2::lps::action_summand::assignments
data::assignment_list & assignments()
Returns the sequence of assignments.
Definition action_summand.h:72
mcrl2::lps::action_summand::swap
void swap(action_summand &other) noexcept
Swaps the contents.
Definition action_summand.h:102
mcrl2::lps::action_summand::action_summand
action_summand()=default
Constructor.
mcrl2::lps::action_summand::next_state
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
mcrl2::lps::action_summand::action_summand
action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments)
Constructor.
Definition action_summand.h:39
mcrl2::lps::action_summand::has_time
bool has_time() const
Returns true if time is available.
Definition action_summand.h:87
mcrl2::lps::action_summand::is_tau
bool is_tau() const
Returns true if the multi-action corresponding to this summand is equal to tau.
Definition action_summand.h:80
mcrl2::lps::action_summand::operator=
action_summand & operator=(const action_summand &) noexcept=default
mcrl2::lps::action_summand::operator=
action_summand & operator=(action_summand &&) noexcept=default
mcrl2::lps::action_summand::action_summand
action_summand(action_summand &&) noexcept=default
mcrl2::lps::action_summand::assignments
const data::assignment_list & assignments() const
Returns the sequence of assignments.
Definition action_summand.h:65
mcrl2::lps::action_summand::m_assignments
data::assignment_list m_assignments
The assignments of the next state.
Definition action_summand.h:32
mcrl2::lps::constelm_algorithm
Algorithm class for elimination of constant parameters.
Definition constelm.h:23
mcrl2::lps::constelm_algorithm::LOG_PARAMETER_CHANGE
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
mcrl2::lps::constelm_algorithm::is_constant
bool is_constant(const data::data_expression &x, const std::set< data::variable > &global_variables) const
Definition constelm.h:96
mcrl2::lps::constelm_algorithm::remove_parameters
void remove_parameters(data::mutable_map_substitution<> &sigma)
Applies the substitution computed by compute_constant_parameters.
Definition constelm.h:232
mcrl2::lps::constelm_algorithm::R
const DataRewriter & R
The rewriter used by the constelm algorithm.
Definition constelm.h:38
mcrl2::lps::constelm_algorithm::LOG_CONSTANT_PARAMETERS
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
mcrl2::lps::constelm_algorithm::m_ignore_conditions
bool m_ignore_conditions
If true, conditions are not evaluated and assumed to be true.
Definition constelm.h:32
mcrl2::lps::constelm_algorithm::constelm_algorithm
constelm_algorithm(Specification &spec, const DataRewriter &R_)
Constructor.
Definition constelm.h:113
mcrl2::lps::constelm_algorithm::LOG_CONDITION
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
mcrl2::lps::constelm_algorithm::run
void run(bool instantiate_global_variables=false, bool ignore_conditions=false)
Runs the constelm algorithm.
Definition constelm.h:257
mcrl2::lps::constelm_algorithm::m_index_of
std::map< data::variable, std::size_t > m_index_of
Maps process parameters to their index.
Definition constelm.h:35
mcrl2::lps::constelm_algorithm::compute_constant_parameters
data::mutable_map_substitution compute_constant_parameters(bool instantiate_global_variables=false, bool ignore_conditions=false)
Computes constant parameters.
Definition constelm.h:123
mcrl2::lps::constelm_algorithm::m_instantiate_global_variables
bool m_instantiate_global_variables
If true, then the algorithm is allowed to instantiate free variables as a side effect.
Definition constelm.h:29
mcrl2::lps::deadlock_summand
LPS summand containing a deadlock.
Definition deadlock_summand.h:23
mcrl2::lps::deadlock_summand::deadlock_summand
deadlock_summand()=default
Constructor.
mcrl2::lps::deadlock_summand::operator=
deadlock_summand & operator=(const deadlock_summand &) noexcept=default
mcrl2::lps::deadlock_summand::m_deadlock
lps::deadlock m_deadlock
The deadlock of the summand.
Definition deadlock_summand.h:29
mcrl2::lps::deadlock_summand::deadlock_summand
deadlock_summand(deadlock_summand &&) noexcept=default
mcrl2::lps::deadlock_summand::operator=
deadlock_summand & operator=(deadlock_summand &&) noexcept=default
mcrl2::lps::deadlock_summand::swap
void swap(deadlock_summand &other) noexcept
Swaps the contents.
Definition deadlock_summand.h:68
mcrl2::lps::deadlock_summand::deadlock_summand
deadlock_summand(const deadlock_summand &) noexcept=default
Move semantics.
mcrl2::lps::deadlock_summand::deadlock_summand
deadlock_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::deadlock &delta)
Constructor.
Definition deadlock_summand.h:37
mcrl2::lps::deadlock_summand::has_time
bool has_time() const
Returns true if time is available.
Definition deadlock_summand.h:62
mcrl2::lps::deadlock
Represents a deadlock.
Definition deadlock.h:23
mcrl2::lps::deadlock::operator!=
bool operator!=(const deadlock &other) const
Comparison operator.
Definition deadlock.h:71
mcrl2::lps::deadlock::m_time
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
mcrl2::lps::deadlock::deadlock
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:33
mcrl2::lps::deadlock::has_time
bool has_time() const
Returns true if time is available.
Definition deadlock.h:39
mcrl2::lps::deadlock::to_string
std::string to_string() const
Returns a string representation of the deadlock.
Definition deadlock.h:59
mcrl2::lps::deadlock::time
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:46
mcrl2::lps::deadlock::swap
void swap(deadlock &other) noexcept
Swaps the contents.
Definition deadlock.h:77
mcrl2::lps::deadlock::time
data::data_expression & time()
Returns the time.
Definition deadlock.h:53
mcrl2::lps::deadlock::operator==
bool operator==(const deadlock &other) const
Comparison operator.
Definition deadlock.h:65
mcrl2::lps::detail::lps_algorithm
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
Definition lps_algorithm.h:26
mcrl2::lps::detail::lps_algorithm::remove_parameters
void remove_parameters(const std::set< data::variable > &to_be_removed)
Removes formal parameters from the specification.
Definition lps_algorithm.h:106
mcrl2::lps::detail::lps_algorithm::remove_unused_summand_variables
void remove_unused_summand_variables()
Removes unused summand variables.
Definition lps_algorithm.h:124
mcrl2::lps::detail::lps_algorithm::sumelm_find_variables
void sumelm_find_variables(const action_summand &s, std::set< data::variable > &result) const
Definition lps_algorithm.h:31
mcrl2::lps::detail::lps_algorithm::summand_remove_unused_summand_variables
void summand_remove_unused_summand_variables(SummandType &summand_)
Definition lps_algorithm.h:57
mcrl2::lps::detail::lps_algorithm::sumelm_find_variables
void sumelm_find_variables(const deadlock_summand &s, std::set< data::variable > &result) const
Definition lps_algorithm.h:45
mcrl2::lps::detail::lps_algorithm::next_state
data::data_expression next_state(const action_summand &s, const data::variable &v) const
Applies the next state substitution to the variable v.
Definition lps_algorithm.h:85
mcrl2::lps::detail::lps_algorithm::verbose
bool verbose() const
Flag for verbose output.
Definition lps_algorithm.h:79
mcrl2::lps::detail::lps_algorithm::remove_singleton_sorts
void remove_singleton_sorts()
Removes parameters with a singleton sort.
Definition lps_algorithm.h:112
mcrl2::lps::detail::lps_algorithm::remove_trivial_summands
void remove_trivial_summands()
Removes summands with condition equal to false.
Definition lps_algorithm.h:118
mcrl2::lps::detail::lps_algorithm::instantiate_free_variables
void instantiate_free_variables()
Attempts to eliminate the free variables of the specification, by substituting a constant value for t...
Definition lps_algorithm.h:100
mcrl2::lps::detail::lps_algorithm::lps_algorithm
lps_algorithm(Specification &spec)
Constructor.
Definition lps_algorithm.h:74
mcrl2::lps::detail::lps_algorithm::m_spec
Specification & m_spec
The specification that is processed by the algorithm.
Definition lps_algorithm.h:29
mcrl2::lps::detail::ultimate_delay
Definition ultimate_delay.h:29
mcrl2::lps::detail::ultimate_delay::ultimate_delay
ultimate_delay()
Constructor.
Definition ultimate_delay.h:37
mcrl2::lps::detail::ultimate_delay::constraint
data_expression & constraint()
Obtain a reference to the constraint.
Definition ultimate_delay.h:76
mcrl2::lps::linear_process_base
Definition linear_process.h:60
mcrl2::lps::linear_process_base::deadlock_summands
deadlock_summand_vector & deadlock_summands()
Returns the sequence of deadlock summands.
Definition linear_process.h:155
mcrl2::lps::linear_process_base::action_summands
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
Definition linear_process.h:134
mcrl2::lps::linear_process_base::m_deadlock_summands
deadlock_summand_vector m_deadlock_summands
The deadlock summands of the process.
Definition linear_process.h:66
mcrl2::lps::linear_process_base::linear_process_base
linear_process_base()=default
Constructor.
mcrl2::lps::linear_process_base::m_process_parameters
data::variable_list m_process_parameters
The process parameters of the process.
Definition linear_process.h:63
mcrl2::lps::linear_process_base::linear_process_base
linear_process_base(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const std::vector< ActionSummand > &action_summands)
Constructor.
Definition linear_process.h:79
mcrl2::lps::linear_process_base::has_time
bool has_time() const
Returns true if time is available in at least one of the summands.
Definition linear_process.h:176
mcrl2::lps::linear_process_base::process_parameters
data::variable_list & process_parameters()
Returns the sequence of process parameters.
Definition linear_process.h:169
mcrl2::lps::linear_process_base::m_action_summands
std::vector< ActionSummand > m_action_summands
The action summands of the process.
Definition linear_process.h:69
mcrl2::lps::linear_process_base::linear_process_base
linear_process_base(const atermpp::aterm &lps, bool stochastic_distributions_allowed=true)
Constructor.
Definition linear_process.h:92
mcrl2::lps::linear_process_base::deadlock_summands
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
Definition linear_process.h:148
mcrl2::lps::linear_process_base::action_summands
std::vector< ActionSummand > & action_summands()
Returns the sequence of action summands.
Definition linear_process.h:141
mcrl2::lps::linear_process_base::summand_count
std::size_t summand_count() const
Returns the number of LPS summands.
Definition linear_process.h:127
mcrl2::lps::linear_process_base::process_parameters
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
Definition linear_process.h:162
mcrl2::lps::linear_process
linear process.
Definition linear_process.h:198
mcrl2::lps::linear_process::linear_process
linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const action_summand_vector &action_summands)
Constructor.
Definition linear_process.h:206
mcrl2::lps::linear_process::linear_process
linear_process(const atermpp::aterm &lps, bool=false)
Constructor.
Definition linear_process.h:214
mcrl2::lps::linear_process::linear_process
linear_process()=default
Constructor.
mcrl2::lps::multi_action
\brief A timed multi-action
Definition multi_action.h:27
mcrl2::lps::multi_action::multi_action
multi_action(const multi_action &) noexcept=default
Move semantics.
mcrl2::lps::multi_action::multi_action
multi_action(const atermpp::aterm &term)
Constructor.
Definition multi_action.h:59
mcrl2::lps::multi_action::has_time
bool has_time() const
Returns true if time is available.
Definition multi_action.h:72
mcrl2::lps::multi_action::actions
const process::action_list & actions() const
Definition multi_action.h:37
mcrl2::lps::multi_action::multi_action
multi_action(const process::action &l)
Constructor.
Definition multi_action.h:66
mcrl2::lps::multi_action::operator+
multi_action operator+(const multi_action &other) const
Joins the actions of both multi actions.
Definition multi_action.h:79
mcrl2::lps::multi_action::operator=
multi_action & operator=(multi_action &&) noexcept=default
mcrl2::lps::multi_action::time
const data::data_expression & time() const
Definition multi_action.h:42
mcrl2::lps::multi_action::operator=
multi_action & operator=(const multi_action &) noexcept=default
mcrl2::lps::multi_action::multi_action
multi_action(multi_action &&) noexcept=default
mcrl2::lps::multi_action::multi_action
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.
Definition multi_action.h:48
mcrl2::lps::process_initializer
A process initializer.
Definition process_initializer.h:26
mcrl2::lps::process_initializer::operator=
process_initializer & operator=(process_initializer &&) noexcept=default
mcrl2::lps::process_initializer::process_initializer
process_initializer(process_initializer &&) noexcept=default
mcrl2::lps::process_initializer::process_initializer
process_initializer(const process_initializer &) noexcept=default
Move semantics.
mcrl2::lps::process_initializer::process_initializer
process_initializer(const data::data_expression_list &expressions)
Constructor.
Definition process_initializer.h:48
mcrl2::lps::process_initializer::process_initializer
process_initializer(const atermpp::aterm &term, bool check_distribution=true)
Constructor.
Definition process_initializer.h:36
mcrl2::lps::process_initializer::expressions
data::data_expression_list expressions() const
Definition process_initializer.h:58
mcrl2::lps::process_initializer::operator=
process_initializer & operator=(const process_initializer &) noexcept=default
mcrl2::lps::process_initializer::process_initializer
process_initializer()
Default constructor.
Definition process_initializer.h:29
mcrl2::lps::specification_base::global_variables
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
Definition specification.h:142
mcrl2::lps::specification_base::process
LinearProcess & process()
Returns a reference to the linear process of the specification.
Definition specification.h:105
mcrl2::lps::specification_base::m_action_labels
process::action_label_list m_action_labels
The action specification of the specification.
Definition specification.h:54
mcrl2::lps::specification_base::specification_base
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.
Definition specification.h:81
mcrl2::lps::specification_base::action_labels
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
Definition specification.h:127
mcrl2::lps::specification_base::initial_process
const InitialProcessExpression & initial_process() const
Returns the initial process.
Definition specification.h:156
mcrl2::lps::specification_base::process
const LinearProcess & process() const
Returns the linear process of the specification.
Definition specification.h:98
mcrl2::lps::specification_base::action_labels
process::action_label_list & action_labels()
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
Definition specification.h:135
mcrl2::lps::specification_base::m_global_variables
std::set< data::variable > m_global_variables
The set of global variables.
Definition specification.h:57
mcrl2::lps::specification_base::initial_process
InitialProcessExpression & initial_process()
Returns a reference to the initial process.
Definition specification.h:163
mcrl2::lps::specification_base::specification_base
specification_base()=default
Constructor.
mcrl2::lps::specification_base::m_process
LinearProcess m_process
The linear process of the specification.
Definition specification.h:60
mcrl2::lps::specification_base::global_variables
std::set< data::variable > & global_variables()
Returns the declared free variables of the LPS.
Definition specification.h:149
mcrl2::lps::specification_base::m_data
data::data_specification m_data
The data specification of the specification.
Definition specification.h:51
mcrl2::lps::specification_base::m_initial_process
InitialProcessExpression m_initial_process
The initial state of the specification.
Definition specification.h:63
mcrl2::lps::specification
Linear process specification.
Definition specification.h:171
mcrl2::lps::specification::specification
specification()=default
Constructor.
mcrl2::lps::specification::specification
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.
Definition specification.h:185
mcrl2::lps::stochastic_action_summand
LPS summand containing a multi-action.
Definition stochastic_action_summand.h:21
mcrl2::lps::stochastic_action_summand::m_distribution
stochastic_distribution m_distribution
The distribution of the summand.
Definition stochastic_action_summand.h:24
mcrl2::lps::stochastic_action_summand::operator=
stochastic_action_summand & operator=(const stochastic_action_summand &) noexcept=default
mcrl2::lps::stochastic_action_summand::stochastic_action_summand
stochastic_action_summand()=default
Constructor.
mcrl2::lps::stochastic_action_summand::stochastic_action_summand
stochastic_action_summand(stochastic_action_summand &&) noexcept=default
mcrl2::lps::stochastic_action_summand::distribution
const stochastic_distribution & distribution() const
Returns the distribution of this summand.
Definition stochastic_action_summand.h:48
mcrl2::lps::stochastic_action_summand::stochastic_action_summand
stochastic_action_summand(const action_summand &s)
Constructor.
Definition stochastic_action_summand.h:37
mcrl2::lps::stochastic_action_summand::operator=
stochastic_action_summand & operator=(stochastic_action_summand &&) noexcept=default
mcrl2::lps::stochastic_action_summand::swap
void swap(stochastic_action_summand &other) noexcept
Swaps the contents.
Definition stochastic_action_summand.h:60
mcrl2::lps::stochastic_action_summand::stochastic_action_summand
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.
Definition stochastic_action_summand.h:31
mcrl2::lps::stochastic_action_summand::stochastic_action_summand
stochastic_action_summand(const stochastic_action_summand &) noexcept=default
Move semantics.
mcrl2::lps::stochastic_action_summand::distribution
stochastic_distribution & distribution()
Returns the distribution of this summand.
Definition stochastic_action_summand.h:54
mcrl2::lps::stochastic_distribution
\brief A stochastic distribution
Definition stochastic_distribution.h:22
mcrl2::lps::stochastic_distribution::operator=
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution(stochastic_distribution &&) noexcept=default
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution()
\brief Default constructor X3.
Definition stochastic_distribution.h:25
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution(const stochastic_distribution &) noexcept=default
Move semantics.
mcrl2::lps::stochastic_distribution::variables
const data::variable_list & variables() const
Definition stochastic_distribution.h:48
mcrl2::lps::stochastic_distribution::is_defined
bool is_defined() const
Returns true if the distribution is defined, i.e. it contains a valid distribution....
Definition stochastic_distribution.h:60
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
Definition stochastic_distribution.h:38
mcrl2::lps::stochastic_distribution::operator=
stochastic_distribution & operator=(const stochastic_distribution &) noexcept=default
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution(const atermpp::aterm &term)
Definition stochastic_distribution.h:31
mcrl2::lps::stochastic_distribution::distribution
const data::data_expression & distribution() const
Definition stochastic_distribution.h:53
mcrl2::lps::stochastic_linear_process
linear process.
Definition stochastic_linear_process.h:50
mcrl2::lps::stochastic_linear_process::stochastic_linear_process
stochastic_linear_process(const atermpp::aterm &t, bool stochastic_distributions_allowed=true)
Constructor.
Definition stochastic_linear_process.h:58
mcrl2::lps::stochastic_linear_process::stochastic_linear_process
stochastic_linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const stochastic_action_summand_vector &action_summands)
Constructor.
Definition stochastic_linear_process.h:63
mcrl2::lps::stochastic_linear_process::stochastic_linear_process
stochastic_linear_process()=default
Constructor.
mcrl2::lps::stochastic_linear_process::stochastic_linear_process
stochastic_linear_process(const linear_process &other)
Constructor.
Definition stochastic_linear_process.h:70
mcrl2::lps::stochastic_process_initializer
A stochastic process initializer.
Definition stochastic_process_initializer.h:21
mcrl2::lps::stochastic_process_initializer::stochastic_process_initializer
stochastic_process_initializer(const atermpp::aterm &term)
Constructor.
Definition stochastic_process_initializer.h:32
mcrl2::lps::stochastic_process_initializer::stochastic_process_initializer
stochastic_process_initializer(const data::data_expression_list &expressions, const stochastic_distribution &distribution)
Constructor.
Definition stochastic_process_initializer.h:39
mcrl2::lps::stochastic_process_initializer::stochastic_process_initializer
stochastic_process_initializer()
Default constructor.
Definition stochastic_process_initializer.h:26
mcrl2::lps::stochastic_process_initializer::distribution
const stochastic_distribution & distribution() const
Definition stochastic_process_initializer.h:43
mcrl2::lps::stochastic_specification
Linear process specification.
Definition stochastic_specification.h:34
mcrl2::lps::stochastic_specification::stochastic_specification
stochastic_specification(const specification &other)
Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.
Definition stochastic_specification.h:59
mcrl2::lps::stochastic_specification::stochastic_specification
stochastic_specification()=default
Constructor.
mcrl2::lps::stochastic_specification::stochastic_specification
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.
Definition stochastic_specification.h:48
mcrl2::lps::summand_base
Base class for LPS summands.
Definition summand.h:22
mcrl2::lps::summand_base::condition
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:56
mcrl2::lps::summand_base::summation_variables
const data::variable_list & summation_variables() const
Returns the sequence of summation variables.
Definition summand.h:49
mcrl2::lps::summand_base::m_summation_variables
data::variable_list m_summation_variables
The summation variables of the summand.
Definition summand.h:25
mcrl2::lps::summand_base::condition
data::data_expression & condition()
Returns the condition expression.
Definition summand.h:63
mcrl2::lps::summand_base::m_condition
data::data_expression m_condition
The condition of the summand.
Definition summand.h:28
mcrl2::lps::summand_base::swap
void swap(summand_base &other) noexcept
Swaps the contents.
Definition summand.h:69
mcrl2::lps::summand_base::summation_variables
data::variable_list & summation_variables()
Returns the sequence of summation variables.
Definition summand.h:42
mcrl2::lps::summand_base::summand_base
summand_base(const data::variable_list &summation_variables, const data::data_expression &condition)
Constructor.
Definition summand.h:35
mcrl2::lps::summand_base::summand_base
summand_base()=default
Constructor.
mcrl2::process::action_label
\brief An action label
Definition action_label.h:23
mcrl2::process::action_label::sorts
const data::sort_expression_list & sorts() const
Definition action_label.h:59
mcrl2::process::action_label::action_label
action_label()
\brief Default constructor X3.
Definition action_label.h:26
mcrl2::process::action_label::action_label
action_label(const atermpp::aterm &term)
Definition action_label.h:32
mcrl2::process::action_label::operator=
action_label & operator=(action_label &&) noexcept=default
mcrl2::process::action_label::action_label
action_label(const std::string &name, const data::sort_expression_list &sorts)
\brief Constructor Z1.
Definition action_label.h:44
mcrl2::process::action_label::action_label
action_label(action_label &&) noexcept=default
mcrl2::process::action_label::name
const core::identifier_string & name() const
Definition action_label.h:54
mcrl2::process::action_label::operator=
action_label & operator=(const action_label &) noexcept=default
mcrl2::process::action_label::action_label
action_label(const action_label &) noexcept=default
Move semantics.
mcrl2::process::action_label::action_label
action_label(const core::identifier_string &name, const data::sort_expression_list &sorts)
\brief Constructor Z12.
Definition action_label.h:39
mcrl2::process::action_name_multiset
\brief A multiset of action names
Definition action_name_multiset.h:24
mcrl2::process::action_name_multiset::operator=
action_name_multiset & operator=(action_name_multiset &&) noexcept=default
mcrl2::process::action_name_multiset::names
const core::identifier_string_list & names() const
Definition action_name_multiset.h:34
mcrl2::process::action_name_multiset::action_name_multiset
action_name_multiset()
Default constructor.
Definition action_name_multiset.h:40
mcrl2::process::action_name_multiset::operator=
action_name_multiset & operator=(const action_name_multiset &) noexcept=default
mcrl2::process::action_name_multiset::action_name_multiset
action_name_multiset(const atermpp::aterm &term)
Constructor from aterm.
Definition action_name_multiset.h:46
mcrl2::process::action_name_multiset::action_name_multiset
action_name_multiset(const action_name_multiset &) noexcept=default
Move semantics.
mcrl2::process::action_name_multiset::action_name_multiset
action_name_multiset(action_name_multiset &&) noexcept=default
mcrl2::process::action_name_multiset::action_name_multiset
action_name_multiset(const core::identifier_string_list &names)
Constructor. Names are sorted lexicographically to establish the sorted-storage invariant.
Definition action_name_multiset.h:53
mcrl2::process::action::action
action(const action_label &label, const data::data_expression_list &arguments)
\brief Constructor Z14.
Definition process_expression.h:155
mcrl2::process::action::operator=
action & operator=(action &&) noexcept=default
mcrl2::process::action::action
action()
\brief Default constructor X3.
Definition process_expression.h:142
mcrl2::process::action::action
action(const atermpp::aterm &term)
Definition process_expression.h:148
mcrl2::process::action::action
action(action &&) noexcept=default
mcrl2::process::action::operator=
action & operator=(const action &) noexcept=default
mcrl2::process::action::arguments
const data::data_expression_list & arguments() const
Definition process_expression.h:170
mcrl2::process::action::action
action(const action &) noexcept=default
Move semantics.
mcrl2::process::action::label
const action_label & label() const
Definition process_expression.h:165
mcrl2::process::allow
\brief The allow operator
Definition process_expression.h:853
mcrl2::process::allow::allow
allow(const allow &) noexcept=default
Move semantics.
mcrl2::process::allow::allow
allow()
\brief Default constructor X3.
Definition process_expression.h:856
mcrl2::process::allow::allow
allow(const atermpp::aterm &term)
Definition process_expression.h:862
mcrl2::process::allow::operand
const process_expression & operand() const
Definition process_expression.h:884
mcrl2::process::allow::allow
allow(const action_name_multiset_list &allow_set, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:869
mcrl2::process::allow::allow
allow(allow &&) noexcept=default
mcrl2::process::allow::allow_set
const action_name_multiset_list & allow_set() const
Definition process_expression.h:879
mcrl2::process::allow::operator=
allow & operator=(allow &&) noexcept=default
mcrl2::process::allow::operator=
allow & operator=(const allow &) noexcept=default
mcrl2::process::at
\brief The at operator
Definition process_expression.h:1005
mcrl2::process::at::at
at(at &&) noexcept=default
mcrl2::process::at::at
at(const atermpp::aterm &term)
Definition process_expression.h:1014
mcrl2::process::at::at
at(const at &) noexcept=default
Move semantics.
mcrl2::process::at::at
at()
\brief Default constructor X3.
Definition process_expression.h:1008
mcrl2::process::at::operator=
at & operator=(const at &) noexcept=default
mcrl2::process::at::at
at(const process_expression &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
Definition process_expression.h:1021
mcrl2::process::at::time_stamp
const data::data_expression & time_stamp() const
Definition process_expression.h:1036
mcrl2::process::at::operator=
at & operator=(at &&) noexcept=default
mcrl2::process::at::operand
const process_expression & operand() const
Definition process_expression.h:1031
mcrl2::process::block
\brief The block operator
Definition process_expression.h:555
mcrl2::process::block::operator=
block & operator=(block &&) noexcept=default
mcrl2::process::block::operator=
block & operator=(const block &) noexcept=default
mcrl2::process::block::operand
const process_expression & operand() const
Definition process_expression.h:570
mcrl2::process::block::block
block(block &&) noexcept=default
mcrl2::process::block::block
block(const block &) noexcept=default
Move semantics.
mcrl2::process::block::block
block(const atermpp::aterm &term)
Definition process_expression.h:579
mcrl2::process::block::block
block(const core::identifier_string_list &block_set, const process_expression &operand)
Constructor. block_set is sorted lexicographically to establish the sorted-storage invariant.
Definition process_expression.h:586
mcrl2::process::block::block_set
const core::identifier_string_list & block_set() const
Definition process_expression.h:565
mcrl2::process::bounded_init
\brief The bounded initialization
Definition process_expression.h:1314
mcrl2::process::bounded_init::bounded_init
bounded_init(const bounded_init &) noexcept=default
Move semantics.
mcrl2::process::bounded_init::operator=
bounded_init & operator=(const bounded_init &) noexcept=default
mcrl2::process::bounded_init::right
const process_expression & right() const
Definition process_expression.h:1345
mcrl2::process::bounded_init::bounded_init
bounded_init(bounded_init &&) noexcept=default
mcrl2::process::bounded_init::bounded_init
bounded_init(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1330
mcrl2::process::bounded_init::bounded_init
bounded_init(const atermpp::aterm &term)
Definition process_expression.h:1323
mcrl2::process::bounded_init::left
const process_expression & left() const
Definition process_expression.h:1340
mcrl2::process::bounded_init::bounded_init
bounded_init()
\brief Default constructor X3.
Definition process_expression.h:1317
mcrl2::process::bounded_init::operator=
bounded_init & operator=(bounded_init &&) noexcept=default
mcrl2::process::choice
\brief The choice operator
Definition process_expression.h:1542
mcrl2::process::choice::choice
choice(const atermpp::aterm &term)
Definition process_expression.h:1551
mcrl2::process::choice::operator=
choice & operator=(const choice &) noexcept=default
mcrl2::process::choice::choice
choice(const choice &) noexcept=default
Move semantics.
mcrl2::process::choice::choice
choice()
\brief Default constructor X3.
Definition process_expression.h:1545
mcrl2::process::choice::left
const process_expression & left() const
Definition process_expression.h:1568
mcrl2::process::choice::choice
choice(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1558
mcrl2::process::choice::choice
choice(choice &&) noexcept=default
mcrl2::process::choice::right
const process_expression & right() const
Definition process_expression.h:1573
mcrl2::process::choice::operator=
choice & operator=(choice &&) noexcept=default
mcrl2::process::comm
\brief The communication operator
Definition process_expression.h:777
mcrl2::process::comm::operator=
comm & operator=(const comm &) noexcept=default
mcrl2::process::comm::comm
comm(const atermpp::aterm &term)
Definition process_expression.h:786
mcrl2::process::comm::comm
comm(comm &&) noexcept=default
mcrl2::process::comm::operator=
comm & operator=(comm &&) noexcept=default
mcrl2::process::comm::comm
comm(const comm &) noexcept=default
Move semantics.
mcrl2::process::comm::comm_set
const communication_expression_list & comm_set() const
Definition process_expression.h:803
mcrl2::process::comm::comm
comm(const communication_expression_list &comm_set, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:793
mcrl2::process::comm::operand
const process_expression & operand() const
Definition process_expression.h:808
mcrl2::process::comm::comm
comm()
\brief Default constructor X3.
Definition process_expression.h:780
mcrl2::process::communication_expression
\brief A communication expression
Definition communication_expression.h:23
mcrl2::process::communication_expression::name
const core::identifier_string & name() const
Definition communication_expression.h:59
mcrl2::process::communication_expression::communication_expression
communication_expression()
\brief Default constructor X3.
Definition communication_expression.h:26
mcrl2::process::communication_expression::operator=
communication_expression & operator=(const communication_expression &) noexcept=default
mcrl2::process::communication_expression::communication_expression
communication_expression(const action_name_multiset &action_name, const std::string &name)
\brief Constructor Z1.
Definition communication_expression.h:44
mcrl2::process::communication_expression::communication_expression
communication_expression(const communication_expression &) noexcept=default
Move semantics.
mcrl2::process::communication_expression::communication_expression
communication_expression(const atermpp::aterm &term)
Definition communication_expression.h:32
mcrl2::process::communication_expression::communication_expression
communication_expression(communication_expression &&) noexcept=default
mcrl2::process::communication_expression::operator=
communication_expression & operator=(communication_expression &&) noexcept=default
mcrl2::process::communication_expression::communication_expression
communication_expression(const action_name_multiset &action_name, const core::identifier_string &name)
\brief Constructor Z12.
Definition communication_expression.h:39
mcrl2::process::communication_expression::action_name
const action_name_multiset & action_name() const
Definition communication_expression.h:54
mcrl2::process::delta
\brief The value delta
Definition process_expression.h:373
mcrl2::process::delta::operator=
delta & operator=(const delta &) noexcept=default
mcrl2::process::delta::delta
delta()
\brief Default constructor X3.
Definition process_expression.h:376
mcrl2::process::delta::delta
delta(const atermpp::aterm &term)
Definition process_expression.h:382
mcrl2::process::delta::delta
delta(delta &&) noexcept=default
mcrl2::process::delta::delta
delta(const delta &) noexcept=default
Move semantics.
mcrl2::process::delta::operator=
delta & operator=(delta &&) noexcept=default
mcrl2::process::hide
\brief The hide operator
Definition process_expression.h:625
mcrl2::process::hide::hide
hide(hide &&) noexcept=default
mcrl2::process::hide::hide
hide(const atermpp::aterm &term)
Definition process_expression.h:634
mcrl2::process::hide::hide
hide(const core::identifier_string_list &hide_set, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:641
mcrl2::process::hide::hide_set
const core::identifier_string_list & hide_set() const
Definition process_expression.h:651
mcrl2::process::hide::operator=
hide & operator=(const hide &) noexcept=default
mcrl2::process::hide::operand
const process_expression & operand() const
Definition process_expression.h:656
mcrl2::process::hide::hide
hide(const hide &) noexcept=default
Move semantics.
mcrl2::process::hide::operator=
hide & operator=(hide &&) noexcept=default
mcrl2::process::hide::hide
hide()
\brief Default constructor X3.
Definition process_expression.h:628
mcrl2::process::if_then_else
\brief The if-then-else operator
Definition process_expression.h:1233
mcrl2::process::if_then_else::else_case
const process_expression & else_case() const
Definition process_expression.h:1269
mcrl2::process::if_then_else::if_then_else
if_then_else(if_then_else &&) noexcept=default
mcrl2::process::if_then_else::then_case
const process_expression & then_case() const
Definition process_expression.h:1264
mcrl2::process::if_then_else::if_then_else
if_then_else(const atermpp::aterm &term)
Definition process_expression.h:1242
mcrl2::process::if_then_else::if_then_else
if_then_else()
\brief Default constructor X3.
Definition process_expression.h:1236
mcrl2::process::if_then_else::operator=
if_then_else & operator=(const if_then_else &) noexcept=default
mcrl2::process::if_then_else::if_then_else
if_then_else(const if_then_else &) noexcept=default
Move semantics.
mcrl2::process::if_then_else::condition
const data::data_expression & condition() const
Definition process_expression.h:1259
mcrl2::process::if_then_else::operator=
if_then_else & operator=(if_then_else &&) noexcept=default
mcrl2::process::if_then_else::if_then_else
if_then_else(const data::data_expression &condition, const process_expression &then_case, const process_expression &else_case)
\brief Constructor Z14.
Definition process_expression.h:1249
mcrl2::process::if_then
\brief The if-then operator
Definition process_expression.h:1157
mcrl2::process::if_then::then_case
const process_expression & then_case() const
Definition process_expression.h:1188
mcrl2::process::if_then::operator=
if_then & operator=(const if_then &) noexcept=default
mcrl2::process::if_then::if_then
if_then(const data::data_expression &condition, const process_expression &then_case)
\brief Constructor Z14.
Definition process_expression.h:1173
mcrl2::process::if_then::if_then
if_then(const atermpp::aterm &term)
Definition process_expression.h:1166
mcrl2::process::if_then::condition
const data::data_expression & condition() const
Definition process_expression.h:1183
mcrl2::process::if_then::if_then
if_then(const if_then &) noexcept=default
Move semantics.
mcrl2::process::if_then::operator=
if_then & operator=(if_then &&) noexcept=default
mcrl2::process::if_then::if_then
if_then(if_then &&) noexcept=default
mcrl2::process::if_then::if_then
if_then()
\brief Default constructor X3.
Definition process_expression.h:1160
mcrl2::process::left_merge
\brief The left merge operator
Definition process_expression.h:1466
mcrl2::process::left_merge::left_merge
left_merge(left_merge &&) noexcept=default
mcrl2::process::left_merge::right
const process_expression & right() const
Definition process_expression.h:1497
mcrl2::process::left_merge::operator=
left_merge & operator=(left_merge &&) noexcept=default
mcrl2::process::left_merge::left_merge
left_merge(const atermpp::aterm &term)
Definition process_expression.h:1475
mcrl2::process::left_merge::operator=
left_merge & operator=(const left_merge &) noexcept=default
mcrl2::process::left_merge::left_merge
left_merge(const left_merge &) noexcept=default
Move semantics.
mcrl2::process::left_merge::left_merge
left_merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1482
mcrl2::process::left_merge::left
const process_expression & left() const
Definition process_expression.h:1492
mcrl2::process::left_merge::left_merge
left_merge()
\brief Default constructor X3.
Definition process_expression.h:1469
mcrl2::process::merge
\brief The merge operator
Definition process_expression.h:1390
mcrl2::process::merge::merge
merge(const atermpp::aterm &term)
Definition process_expression.h:1399
mcrl2::process::merge::right
const process_expression & right() const
Definition process_expression.h:1421
mcrl2::process::merge::left
const process_expression & left() const
Definition process_expression.h:1416
mcrl2::process::merge::operator=
merge & operator=(const merge &) noexcept=default
mcrl2::process::merge::merge
merge(const merge &) noexcept=default
Move semantics.
mcrl2::process::merge::merge
merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1406
mcrl2::process::merge::operator=
merge & operator=(merge &&) noexcept=default
mcrl2::process::merge::merge
merge(merge &&) noexcept=default
mcrl2::process::merge::merge
merge()
\brief Default constructor X3.
Definition process_expression.h:1393
mcrl2::process::process_equation
\brief A process equation
Definition process_equation.h:23
mcrl2::process::process_equation::formal_parameters
const data::variable_list & formal_parameters() const
Definition process_equation.h:54
mcrl2::process::process_equation::identifier
const process_identifier & identifier() const
Definition process_equation.h:49
mcrl2::process::process_equation::expression
const process_expression & expression() const
Definition process_equation.h:59
mcrl2::process::process_expression
\brief A process expression
Definition process_expression.h:29
mcrl2::process::process_expression::operator=
process_expression & operator=(const process_expression &) noexcept=default
mcrl2::process::process_expression::process_expression
process_expression(const process_expression &) noexcept=default
Move semantics.
mcrl2::process::process_expression::process_expression
process_expression()
\brief Default constructor X3.
Definition process_expression.h:32
mcrl2::process::process_expression::process_expression
process_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
Definition process_expression.h:45
mcrl2::process::process_expression::process_expression
process_expression(process_expression &&) noexcept=default
mcrl2::process::process_expression::process_expression
process_expression(const atermpp::aterm &term)
Definition process_expression.h:38
mcrl2::process::process_expression::operator=
process_expression & operator=(process_expression &&) noexcept=default
mcrl2::process::process_identifier
\brief A process identifier
Definition process_identifier.h:23
mcrl2::process::process_identifier::process_identifier
process_identifier(const process_identifier &) noexcept=default
Move semantics.
mcrl2::process::process_identifier::variables
const data::variable_list & variables() const
Definition process_identifier.h:38
mcrl2::process::process_identifier::operator=
process_identifier & operator=(const process_identifier &) noexcept=default
mcrl2::process::process_identifier::process_identifier
process_identifier(process_identifier &&) noexcept=default
mcrl2::process::process_identifier::process_identifier
process_identifier(const core::identifier_string &name, const data::variable_list &variables)
Constructor.
Definition process_identifier.h:57
mcrl2::process::process_identifier::name
const core::identifier_string & name() const
Definition process_identifier.h:33
mcrl2::process::process_identifier::operator=
process_identifier & operator=(process_identifier &&) noexcept=default
mcrl2::process::process_identifier::process_identifier
process_identifier()
Default constructor.
Definition process_identifier.h:44
mcrl2::process::process_identifier::process_identifier
process_identifier(const std::string &name, const data::variable_list &variables)
Constructor.
Definition process_identifier.h:63
mcrl2::process::process_identifier::process_identifier
process_identifier(const atermpp::aterm &term)
Constructor.
Definition process_identifier.h:50
mcrl2::process::process_instance_assignment
\brief A process assignment
Definition process_expression.h:297
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment(const process_instance_assignment &) noexcept=default
Move semantics.
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment()
\brief Default constructor X3.
Definition process_expression.h:300
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment(const process_identifier &identifier, const data::assignment_list &assignments)
\brief Constructor Z14.
Definition process_expression.h:313
mcrl2::process::process_instance_assignment::operator=
process_instance_assignment & operator=(const process_instance_assignment &) noexcept=default
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment(process_instance_assignment &&) noexcept=default
mcrl2::process::process_instance_assignment::assignments
const data::assignment_list & assignments() const
Definition process_expression.h:328
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment(const atermpp::aterm &term)
Definition process_expression.h:306
mcrl2::process::process_instance_assignment::operator=
process_instance_assignment & operator=(process_instance_assignment &&) noexcept=default
mcrl2::process::process_instance_assignment::identifier
const process_identifier & identifier() const
Definition process_expression.h:323
mcrl2::process::process_instance
\brief A process
Definition process_expression.h:221
mcrl2::process::process_instance::actual_parameters
const data::data_expression_list & actual_parameters() const
Definition process_expression.h:252
mcrl2::process::process_instance::process_instance
process_instance(const process_identifier &identifier, const data::data_expression_list &actual_parameters)
\brief Constructor Z14.
Definition process_expression.h:237
mcrl2::process::process_instance::operator=
process_instance & operator=(const process_instance &) noexcept=default
mcrl2::process::process_instance::operator=
process_instance & operator=(process_instance &&) noexcept=default
mcrl2::process::process_instance::identifier
const process_identifier & identifier() const
Definition process_expression.h:247
mcrl2::process::process_instance::process_instance
process_instance(process_instance &&) noexcept=default
mcrl2::process::process_instance::process_instance
process_instance()
\brief Default constructor X3.
Definition process_expression.h:224
mcrl2::process::process_instance::process_instance
process_instance(const atermpp::aterm &term)
Definition process_expression.h:230
mcrl2::process::process_instance::process_instance
process_instance(const process_instance &) noexcept=default
Move semantics.
mcrl2::process::process_specification
Process specification consisting of a data specification, action labels, a sequence of process equati...
Definition process_specification.h:49
mcrl2::process::process_specification::init
process_expression & init()
Returns the initialization of the process specification.
Definition process_specification.h:181
mcrl2::process::process_specification::action_labels
process::action_label_list & action_labels()
Returns the action label specification.
Definition process_specification.h:139
mcrl2::process::rename_expression
\brief A rename expression
Definition rename_expression.h:24
mcrl2::process::rename_expression::source
const core::identifier_string & source() const
Definition rename_expression.h:55
mcrl2::process::rename_expression::rename_expression
rename_expression()
\brief Default constructor X3.
Definition rename_expression.h:27
mcrl2::process::rename_expression::operator=
rename_expression & operator=(rename_expression &&) noexcept=default
mcrl2::process::rename_expression::operator=
rename_expression & operator=(const rename_expression &) noexcept=default
mcrl2::process::rename_expression::rename_expression
rename_expression(core::identifier_string &source, core::identifier_string &target)
\brief Constructor Z12.
Definition rename_expression.h:40
mcrl2::process::rename_expression::target
const core::identifier_string & target() const
Definition rename_expression.h:60
mcrl2::process::rename_expression::rename_expression
rename_expression(const atermpp::aterm &term)
Definition rename_expression.h:33
mcrl2::process::rename_expression::rename_expression
rename_expression(rename_expression &&) noexcept=default
mcrl2::process::rename_expression::rename_expression
rename_expression(const std::string &source, const std::string &target)
\brief Constructor Z1.
Definition rename_expression.h:45
mcrl2::process::rename_expression::rename_expression
rename_expression(const rename_expression &) noexcept=default
Move semantics.
mcrl2::process::rename
\brief The rename operator
Definition process_expression.h:701
mcrl2::process::rename::rename
rename(const atermpp::aterm &term)
Definition process_expression.h:710
mcrl2::process::rename::operator=
rename & operator=(const rename &) noexcept=default
mcrl2::process::rename::rename
rename(const rename &) noexcept=default
Move semantics.
mcrl2::process::rename::rename
rename()
\brief Default constructor X3.
Definition process_expression.h:704
mcrl2::process::rename::operand
const process_expression & operand() const
Definition process_expression.h:732
mcrl2::process::rename::operator=
rename & operator=(rename &&) noexcept=default
mcrl2::process::rename::rename
rename(rename &&) noexcept=default
mcrl2::process::rename::rename
rename(const rename_expression_list &rename_set, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:717
mcrl2::process::rename::rename_set
const rename_expression_list & rename_set() const
Definition process_expression.h:727
mcrl2::process::seq
\brief The sequential composition
Definition process_expression.h:1081
mcrl2::process::seq::operator=
seq & operator=(seq &&) noexcept=default
mcrl2::process::seq::right
const process_expression & right() const
Definition process_expression.h:1112
mcrl2::process::seq::seq
seq(const atermpp::aterm &term)
Definition process_expression.h:1090
mcrl2::process::seq::seq
seq()
\brief Default constructor X3.
Definition process_expression.h:1084
mcrl2::process::seq::operator=
seq & operator=(const seq &) noexcept=default
mcrl2::process::seq::left
const process_expression & left() const
Definition process_expression.h:1107
mcrl2::process::seq::seq
seq(seq &&) noexcept=default
mcrl2::process::seq::seq
seq(const seq &) noexcept=default
Move semantics.
mcrl2::process::seq::seq
seq(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1097
mcrl2::process::stochastic_operator
\brief The distribution operator
Definition process_expression.h:1618
mcrl2::process::stochastic_operator::variables
const data::variable_list & variables() const
Definition process_expression.h:1644
mcrl2::process::stochastic_operator::distribution
const data::data_expression & distribution() const
Definition process_expression.h:1649
mcrl2::process::stochastic_operator::operator=
stochastic_operator & operator=(stochastic_operator &&) noexcept=default
mcrl2::process::stochastic_operator::stochastic_operator
stochastic_operator()
\brief Default constructor X3.
Definition process_expression.h:1621
mcrl2::process::stochastic_operator::stochastic_operator
stochastic_operator(const atermpp::aterm &term)
Definition process_expression.h:1627
mcrl2::process::stochastic_operator::stochastic_operator
stochastic_operator(stochastic_operator &&) noexcept=default
mcrl2::process::stochastic_operator::stochastic_operator
stochastic_operator(const stochastic_operator &) noexcept=default
Move semantics.
mcrl2::process::stochastic_operator::operator=
stochastic_operator & operator=(const stochastic_operator &) noexcept=default
mcrl2::process::stochastic_operator::operand
const process_expression & operand() const
Definition process_expression.h:1654
mcrl2::process::stochastic_operator::stochastic_operator
stochastic_operator(const data::variable_list &variables, const data::data_expression &distribution, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:1634
mcrl2::process::sum
\brief The sum operator
Definition process_expression.h:479
mcrl2::process::sum::operand
const process_expression & operand() const
Definition process_expression.h:510
mcrl2::process::sum::sum
sum(const data::variable_list &variables, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:495
mcrl2::process::sum::sum
sum(const atermpp::aterm &term)
Definition process_expression.h:488
mcrl2::process::sum::operator=
sum & operator=(sum &&) noexcept=default
mcrl2::process::sum::sum
sum()
\brief Default constructor X3.
Definition process_expression.h:482
mcrl2::process::sum::variables
const data::variable_list & variables() const
Definition process_expression.h:505
mcrl2::process::sum::sum
sum(sum &&) noexcept=default
mcrl2::process::sum::sum
sum(const sum &) noexcept=default
Move semantics.
mcrl2::process::sum::operator=
sum & operator=(const sum &) noexcept=default
mcrl2::process::sync
\brief The synchronization operator
Definition process_expression.h:929
mcrl2::process::sync::operator=
sync & operator=(const sync &) noexcept=default
mcrl2::process::sync::sync
sync(sync &&) noexcept=default
mcrl2::process::sync::sync
sync(const sync &) noexcept=default
Move semantics.
mcrl2::process::sync::left
const process_expression & left() const
Definition process_expression.h:955
mcrl2::process::sync::sync
sync()
\brief Default constructor X3.
Definition process_expression.h:932
mcrl2::process::sync::operator=
sync & operator=(sync &&) noexcept=default
mcrl2::process::sync::sync
sync(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:945
mcrl2::process::sync::right
const process_expression & right() const
Definition process_expression.h:960
mcrl2::process::sync::sync
sync(const atermpp::aterm &term)
Definition process_expression.h:938
mcrl2::process::tau
\brief The value tau
Definition process_expression.h:426
mcrl2::process::tau::tau
tau(const tau &) noexcept=default
Move semantics.
mcrl2::process::tau::tau
tau()
\brief Default constructor X3.
Definition process_expression.h:429
mcrl2::process::tau::tau
tau(const atermpp::aterm &term)
Definition process_expression.h:435
mcrl2::process::tau::operator=
tau & operator=(tau &&) noexcept=default
mcrl2::process::tau::operator=
tau & operator=(const tau &) noexcept=default
mcrl2::process::tau::tau
tau(tau &&) noexcept=default
mcrl2::process::untyped_multi_action
\brief An untyped multi action or data application
Definition untyped_multi_action.h:23
mcrl2::process::untyped_multi_action::actions
const data::untyped_data_parameter_list & actions() const
Definition untyped_multi_action.h:49
mcrl2::process::untyped_process_assignment
\brief An untyped process assginment
Definition process_expression.h:1699
mcrl2::process::untyped_process_assignment::operator=
untyped_process_assignment & operator=(untyped_process_assignment &&) noexcept=default
mcrl2::process::untyped_process_assignment::assignments
const data::untyped_identifier_assignment_list & assignments() const
Definition process_expression.h:1735
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment(const core::identifier_string &name, const data::untyped_identifier_assignment_list &assignments)
\brief Constructor Z14.
Definition process_expression.h:1715
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment(const atermpp::aterm &term)
Definition process_expression.h:1708
mcrl2::process::untyped_process_assignment::name
const core::identifier_string & name() const
Definition process_expression.h:1730
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment()
\brief Default constructor X3.
Definition process_expression.h:1702
mcrl2::process::untyped_process_assignment::operator=
untyped_process_assignment & operator=(const untyped_process_assignment &) noexcept=default
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment(const std::string &name, const data::untyped_identifier_assignment_list &assignments)
\brief Constructor Z2.
Definition process_expression.h:1720
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment(untyped_process_assignment &&) noexcept=default
mcrl2::process::untyped_process_assignment::untyped_process_assignment
untyped_process_assignment(const untyped_process_assignment &) noexcept=default
Move semantics.
objectdatatype::processbody
process_expression processbody
Definition linearise.cpp:114
objectdatatype::objectdatatype
objectdatatype(const objectdatatype &o)=default
objectdatatype::representedprocess
process_expression representedprocess
Definition linearise.cpp:111
objectdatatype::~objectdatatype
~objectdatatype()=default
objectdatatype::multi_action_names
process::action_label_list multi_action_names
Definition linearise.cpp:109
objectdatatype::processstatus
processstatustype processstatus
Definition linearise.cpp:115
objectdatatype::objectname
identifier_string objectname
Definition linearise.cpp:107
objectdatatype::get_free_variables
std::set< variable > get_free_variables() const
Definition linearise.cpp:120
objectdatatype::objectdatatype
objectdatatype()=default
objectdatatype::operator=
objectdatatype & operator=(const objectdatatype &o)=default
objectdatatype::object
objecttype object
Definition linearise.cpp:116
objectdatatype::process_representing_action
process_identifier process_representing_action
Definition linearise.cpp:112
objectdatatype::parameters
variable_list parameters
Definition linearise.cpp:108
specification_basic_type::enumeratedtype
Definition linearise.cpp:5356
specification_basic_type::enumeratedtype::functions
function_symbol_list functions
Definition linearise.cpp:5361
specification_basic_type::enumeratedtype::elementnames
data_expression_list elementnames
Definition linearise.cpp:5360
specification_basic_type::enumeratedtype::enumeratedtype
enumeratedtype(const enumeratedtype &e)
Definition linearise.cpp:5401
specification_basic_type::enumeratedtype::size
std::size_t size
Definition linearise.cpp:5358
specification_basic_type::enumeratedtype::enumeratedtype
enumeratedtype(const std::size_t n, specification_basic_type &spec)
Definition linearise.cpp:5363
specification_basic_type::enumeratedtype::operator=
enumeratedtype & operator=(const enumeratedtype &e)=default
specification_basic_type::enumeratedtype::~enumeratedtype
~enumeratedtype()=default
specification_basic_type::enumeratedtype::sortId
sort_expression sortId
Definition linearise.cpp:5359
specification_basic_type::enumtype
Definition linearise.cpp:5544
specification_basic_type::enumtype::enumtype
enumtype(const enumtype &)=delete
specification_basic_type::enumtype::~enumtype
~enumtype()=default
specification_basic_type::enumtype::operator=
enumtype & operator=(const enumtype &)=delete
specification_basic_type::enumtype::enumeratedtype_index
std::size_t enumeratedtype_index
Definition linearise.cpp:5550
specification_basic_type::enumtype::var
variable var
Definition linearise.cpp:5551
specification_basic_type::enumtype::enumtype
enumtype(std::size_t n, const sort_expression_list &fsorts, const sort_expression_list &gsorts, specification_basic_type &spec)
Definition linearise.cpp:5553
specification_basic_type::process_pid_pair
Definition linearise.cpp:3870
specification_basic_type::process_pid_pair::m_pid
process_identifier m_pid
Definition linearise.cpp:3873
specification_basic_type::process_pid_pair::m_process_body
process_expression m_process_body
Definition linearise.cpp:3872
specification_basic_type::process_pid_pair::operator=
process_pid_pair & operator=(const process_pid_pair &other)=default
specification_basic_type::process_pid_pair::process_body
const process_expression & process_body() const
Definition linearise.cpp:3885
specification_basic_type::process_pid_pair::process_id
const process_identifier & process_id() const
Definition linearise.cpp:3890
specification_basic_type::process_pid_pair::process_pid_pair
process_pid_pair(const process_pid_pair &other)=default
specification_basic_type::process_pid_pair::operator=
process_pid_pair & operator=(process_pid_pair &&other)=default
specification_basic_type::process_pid_pair::process_pid_pair
process_pid_pair(const process_expression &process_body, const process_identifier &pid)
Definition linearise.cpp:3876
specification_basic_type::process_pid_pair::process_pid_pair
process_pid_pair(process_pid_pair &&other)=default
specification_basic_type::stacklisttype
Definition linearise.cpp:4136
specification_basic_type::stacklisttype::booleanStateVariables
variable_list booleanStateVariables
Definition linearise.cpp:4145
specification_basic_type::stacklisttype::find_suitable_stack_operations
static stackoperations * find_suitable_stack_operations(const variable_list &parameters, stackoperations *stack_operations_list)
Definition linearise.cpp:4157
specification_basic_type::stacklisttype::opns
stackoperations * opns
Definition linearise.cpp:4138
specification_basic_type::stacklisttype::operator=
stacklisttype & operator=(const stacklisttype &)=delete
specification_basic_type::stacklisttype::no_of_states
std::size_t no_of_states
Definition linearise.cpp:4141
specification_basic_type::stacklisttype::stacklisttype
stacklisttype(const variable_list &parlist, specification_basic_type &spec, const bool regular, const std::set< process_identifier > &pCRLprocs, const bool singlecontrolstate)
Constructor.
Definition linearise.cpp:4173
specification_basic_type::stacklisttype::~stacklisttype
~stacklisttype()=default
specification_basic_type::stacklisttype::parameters
variable_list parameters
Definition linearise.cpp:4139
specification_basic_type::stacklisttype::stacklisttype
stacklisttype(const stacklisttype &)=delete
specification_basic_type::stacklisttype::stackvar
variable stackvar
Definition linearise.cpp:4140
specification_basic_type::stackoperations
Definition linearise.cpp:4076
specification_basic_type::stackoperations::operator=
stackoperations & operator=(const stackoperations &)=delete
specification_basic_type::stackoperations::pop
data::function_symbol pop
Definition linearise.cpp:4085
specification_basic_type::stackoperations::push
data::function_symbol push
Definition linearise.cpp:4082
specification_basic_type::stackoperations::stackoperations
stackoperations(const stackoperations &)=delete
specification_basic_type::stackoperations::sorts
sort_expression_list sorts
Definition linearise.cpp:4080
specification_basic_type::stackoperations::empty
data::function_symbol empty
Definition linearise.cpp:4084
specification_basic_type::stackoperations::getstate
data::function_symbol getstate
Definition linearise.cpp:4086
specification_basic_type::stackoperations::parameter_list
variable_list parameter_list
Definition linearise.cpp:4078
specification_basic_type::stackoperations::next
stackoperations * next
Definition linearise.cpp:4087
specification_basic_type::stackoperations::get
function_symbol_list get
Definition linearise.cpp:4081
specification_basic_type::stackoperations::~stackoperations
~stackoperations()=default
specification_basic_type::stackoperations::emptystack
data::function_symbol emptystack
Definition linearise.cpp:4083
specification_basic_type::stackoperations::stackoperations
stackoperations(const variable_list &pl, specification_basic_type &spec)
Definition linearise.cpp:4093
specification_basic_type::stackoperations::stacksort
sort_expression stacksort
Definition linearise.cpp:4079
specification_basic_type
Definition linearise.cpp:132
specification_basic_type::procstorealGNFbody
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)
Definition linearise.cpp:3349
specification_basic_type::construct_binary_case_tree
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)
Definition linearise.cpp:5869
specification_basic_type::make_unique_variables
data::maintain_variables_in_rhs< data::mutable_map_substitution<> > make_unique_variables(const variable_list &var_list, const std::string &hint)
Definition linearise.cpp:7380
specification_basic_type::parscollect
variable_list parscollect(const process_expression &oldbody, process_expression &newbody)
Definition linearise.cpp:2966
specification_basic_type::collect_sum_arg_arg_cond
stochastic_action_summand collect_sum_arg_arg_cond(const enumtype &e, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
Definition linearise.cpp:5952
specification_basic_type::linMergeMultiActionList
action_list linMergeMultiActionList(const action_list &ma1, const action_list &ma2)
Definition linearise.cpp:774
specification_basic_type::generateLPEpCRL
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)
Definition linearise.cpp:6952
specification_basic_type::get_fresh_variable
variable get_fresh_variable(const std::string &s, const sort_expression &sort, const int reuse_index=-1)
Definition linearise.cpp:2022
specification_basic_type::distributeActionOverConditions
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)
Definition linearise.cpp:2075
specification_basic_type::construct_binary_case_tree_rec
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)
Definition linearise.cpp:5814
specification_basic_type::complete_proc_identifier_map
static void complete_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map)
Definition linearise.cpp:3761
specification_basic_type::to_regular_form
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)
Definition linearise.cpp:3187
specification_basic_type::collectsumlistterm
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)
Definition linearise.cpp:5282
specification_basic_type::findarguments
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)
Definition linearise.cpp:4614
specification_basic_type::calculate_communication_merge
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)
Definition linearise.cpp:8001
specification_basic_type::insertvariable
void insertvariable(const variable &var, const bool mustbenew)
Definition linearise.cpp:478
specification_basic_type::storeinit
process_identifier storeinit(const process_expression &init)
Definition linearise.cpp:758
specification_basic_type::to_sorted_action_list
static action_list to_sorted_action_list(const process_expression &p)
Convert the process expression to a sorted action list.
Definition linearise.cpp:358
specification_basic_type::pCRLrewrite
process_expression pCRLrewrite(const process_expression &t)
Definition linearise.cpp:594
specification_basic_type::pushdummy_regular_data_expressions
data_expression_list pushdummy_regular_data_expressions(const variable_list &pars, const stacklisttype &stack)
Definition linearise.cpp:4852
specification_basic_type::define_equations_for_case_function
void define_equations_for_case_function(const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)
Definition linearise.cpp:5444
specification_basic_type::alphaconvert
void alphaconvert(variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
Definition linearise.cpp:1437
specification_basic_type::timeIsBeingUsed
bool timeIsBeingUsed
Definition linearise.cpp:166
specification_basic_type::canterminatebody
bool canterminatebody(const process_expression &t)
Definition linearise.cpp:9504
specification_basic_type::transform_matching_list
data_expression transform_matching_list(const variable_list &matchinglist)
Definition linearise.cpp:5717
specification_basic_type::add_summands
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)
Definition linearise.cpp:5059
specification_basic_type::isDeltaAtZero
bool isDeltaAtZero(const process_expression &t)
Definition linearise.cpp:257
specification_basic_type::find_case_function
data::function_symbol find_case_function(std::size_t index, const sort_expression &sort) const
Definition linearise.cpp:5428
specification_basic_type::make_initialstate
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)
Definition linearise.cpp:4963
specification_basic_type::summandsCanBeClustered
static bool summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
Definition linearise.cpp:5880
specification_basic_type::getActionSorts
static sort_expression_list getActionSorts(const action_list &actionlist)
Definition linearise.cpp:6827
specification_basic_type::filter_vars_by_multiaction
void filter_vars_by_multiaction(const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
Definition linearise.cpp:1302
specification_basic_type::get_last
static process_identifier get_last(const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
Definition linearise.cpp:3716
specification_basic_type::check_real_variable_occurrence
static bool check_real_variable_occurrence(const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)
Definition linearise.cpp:7155
specification_basic_type::newprocess
process_identifier newprocess(const variable_list &parameters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)
Definition linearise.cpp:1883
specification_basic_type::make_pCRL_procs
void make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)
Definition linearise.cpp:3639
specification_basic_type::filter_vars_by_term
void filter_vars_by_term(const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
Definition linearise.cpp:1203
specification_basic_type::pushdummy_stack
data_expression_list pushdummy_stack(const variable_list &parameters, const stacklisttype &stack, const variable_list &stochastic_variables)
Definition linearise.cpp:4955
specification_basic_type::procstorealGNFrec
void procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)
Definition linearise.cpp:3547
specification_basic_type::getnames
static action_label_list getnames(const process_expression &multiAction)
Definition linearise.cpp:364
specification_basic_type::getparameters_rec
variable_list getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)
Definition linearise.cpp:402
specification_basic_type::match_sequence
static int match_sequence(const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
Definition linearise.cpp:2870
specification_basic_type::argscollect_regular2
assignment_list argscollect_regular2(const process_expression &t, variable_list &vl)
Definition linearise.cpp:3032
specification_basic_type::make_optimised_assignment_list
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)
Definition linearise.cpp:5933
specification_basic_type::fresh_equation_added
bool fresh_equation_added
Definition linearise.cpp:168
specification_basic_type::calculate_left_merge_action
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)
Definition linearise.cpp:7531
specification_basic_type::split_body
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)
Definition linearise.cpp:9789
specification_basic_type::parallelcomposition
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)
Definition linearise.cpp:8130
specification_basic_type::occursintermlist
bool occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) const
Definition linearise.cpp:1263
specification_basic_type::transform_process_arguments
void transform_process_arguments(const process_identifier &procId)
Definition linearise.cpp:9645
specification_basic_type::insert_process_declaration
objectdatatype & insert_process_declaration(const process_identifier &procId, const variable_list &parameters, const process_expression &body, processstatustype s, const bool canterminate, const bool containstime)
Definition linearise.cpp:688
specification_basic_type::set_proc_identifier_map
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)
Definition linearise.cpp:3738
specification_basic_type::canterminate_rec
bool canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)
Definition linearise.cpp:9484
specification_basic_type::fresh_identifier_generator
set_identifier_generator fresh_identifier_generator
Definition linearise.cpp:173
specification_basic_type::remove_stochastic_operators_from_front
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)
Definition linearise.cpp:3904
specification_basic_type::filter_vars_by_termlist
void filter_vars_by_termlist(Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
Definition linearise.cpp:1290
specification_basic_type::searchProcDeclaration
bool searchProcDeclaration(const variable_list &parameters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p) const
Definition linearise.cpp:730
specification_basic_type::splitmCRLandpCRLprocsAndAddTerminatedAction
process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)
Definition linearise.cpp:9898
specification_basic_type::linMergeMultiActionListProcess
action_list linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)
Definition linearise.cpp:785
specification_basic_type::procs
std::vector< process_equation > procs
Definition linearise.cpp:150
specification_basic_type::adapt_multiaction_to_stack
action_list adapt_multiaction_to_stack(const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)
Definition linearise.cpp:4551
specification_basic_type::determinewhetherprocessescanterminate
void determinewhetherprocessescanterminate(const process_identifier &procId)
Definition linearise.cpp:9511
specification_basic_type::distribute_condition
process_expression distribute_condition(const process_expression &body1, const data_expression &condition)
Definition linearise.cpp:2614
specification_basic_type::containstime_rec
bool containstime_rec(const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)
Definition linearise.cpp:8847
specification_basic_type::collectsumlist
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)
Definition linearise.cpp:5326
specification_basic_type::correctstatecond
data_expression correctstatecond(const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)
Definition linearise.cpp:4386
specification_basic_type::calculate_communication_merge_action_summands
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)
Definition linearise.cpp:7742
specification_basic_type::determine_process_statusterm
processstatustype determine_process_statusterm(const process_expression &body, const processstatustype status)
Definition linearise.cpp:792
specification_basic_type::calculate_communication_merge_action_deadlock_summands
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)
Definition linearise.cpp:7846
specification_basic_type::getvar
data_expression getvar(const variable &var, const stacklisttype &stack) const
Definition linearise.cpp:4258
specification_basic_type::initdatavars
variable_list initdatavars
Definition linearise.cpp:137
specification_basic_type::combine_ultimate_delays
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,...
Definition linearise.cpp:7510
specification_basic_type::distributeTime
process_expression distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)
Definition linearise.cpp:3269
specification_basic_type::pushdummyrec_stack
data_expression_list pushdummyrec_stack(const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
Definition linearise.cpp:4917
specification_basic_type::to_action_list
static action_list to_action_list(const process_expression &p)
Definition linearise.cpp:336
specification_basic_type::sigma_variables
std::set< data::variable > sigma_variables(const Substitution &sigma)
Definition linearise.cpp:502
specification_basic_type::combine_summand_lists
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)
Definition linearise.cpp:8032
specification_basic_type::cut_off_unreachable_tail
process_expression cut_off_unreachable_tail(const process_expression &t)
Definition linearise.cpp:3074
specification_basic_type::enumeratedtypes
std::vector< enumeratedtype > enumeratedtypes
Definition linearise.cpp:174
specification_basic_type::find_
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)
Definition linearise.cpp:4581
specification_basic_type::acts
process::action_label_list acts
Definition linearise.cpp:134
specification_basic_type::make_procargs_regular
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)
Definition linearise.cpp:4706
specification_basic_type::create_enumeratedtype
std::size_t create_enumeratedtype(const std::size_t n)
Definition linearise.cpp:5415
specification_basic_type::generateLPEmCRL
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)
Definition linearise.cpp:8485
specification_basic_type::expand_process_instance_assignment
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)
Definition linearise.cpp:9603
specification_basic_type::delta_at_zero
static process_expression delta_at_zero()
Definition linearise.cpp:252
specification_basic_type::rewrite_assignments
assignment_list rewrite_assignments(const assignment_list &t)
Definition linearise.cpp:557
specification_basic_type::push_regular
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)
Definition linearise.cpp:4677
specification_basic_type::transform_process_arguments
void transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)
Definition linearise.cpp:9627
specification_basic_type::minimize_set_of_reachable_process_identifiers
std::set< process_identifier > minimize_set_of_reachable_process_identifiers(const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)
Definition linearise.cpp:3801
specification_basic_type::terminationAction
action terminationAction
Definition linearise.cpp:156
specification_basic_type::collectPcrlProcesses
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
Definition linearise.cpp:1176
specification_basic_type::make_binary_sums
variable_list make_binary_sums(std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)
Definition linearise.cpp:5787
specification_basic_type::SieveProcDataVarsAssignments
variable_list SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)
Definition linearise.cpp:9971
specification_basic_type::extend_conditions
data_expression_list extend_conditions(const variable &var, const data_expression_list &conditionlist)
Definition linearise.cpp:5696
specification_basic_type::check_valid_process_instance_assignment
bool check_valid_process_instance_assignment(const process_identifier &id, const assignment_list &assignments)
Definition linearise.cpp:1634
specification_basic_type::calculate_left_merge_deadlock
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)
Definition linearise.cpp:7609
specification_basic_type::addString
void addString(const identifier_string &str)
Definition linearise.cpp:314
specification_basic_type::procstovarheadGNF
void procstovarheadGNF(const std::vector< process_identifier > &procs)
Definition linearise.cpp:2499
specification_basic_type::action_list_to_process
static process_expression action_list_to_process(const action_list &ma)
Definition linearise.cpp:320
specification_basic_type::distribute_sum_over_a_stochastic_operator
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)
Definition linearise.cpp:2773
specification_basic_type::alphaconvertprocess
void alphaconvertprocess(variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
Definition linearise.cpp:1410
specification_basic_type::obtain_initial_distribution_term
process_expression obtain_initial_distribution_term(const process_expression &t)
Definition linearise.cpp:9149
specification_basic_type::push_stack
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)
Definition linearise.cpp:4735
specification_basic_type::calculate_left_merge
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)
Definition linearise.cpp:7709
specification_basic_type::stochastic_operator_is_being_used
bool stochastic_operator_is_being_used
Definition linearise.cpp:167
specification_basic_type::declare_control_state
void declare_control_state(const std::set< process_identifier > &pCRLprocs)
Definition linearise.cpp:4069
specification_basic_type::create_case_function_on_enumeratedtype
void create_case_function_on_enumeratedtype(const sort_expression &sort, const std::size_t enumeratedtype_index)
Definition linearise.cpp:5495
specification_basic_type::SieveProcDataVarsSummands
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)
Definition linearise.cpp:9926
specification_basic_type::extend
static data_expression_list extend(const data_expression &c, const data_expression_list &cl)
Definition linearise.cpp:5676
specification_basic_type::operator=
specification_basic_type & operator=(const specification_basic_type &)=delete
specification_basic_type::occursinvarandremove
static bool occursinvarandremove(const variable &var, variable_list &vl)
Definition linearise.cpp:7056
specification_basic_type::bodytovarheadGNF
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)
Definition linearise.cpp:2157
specification_basic_type::terminatedProcId
process_identifier terminatedProcId
Definition linearise.cpp:157
specification_basic_type::distribute_sum
process_expression distribute_sum(const variable_list &sumvars, const process_expression &body1)
Definition linearise.cpp:2816
specification_basic_type::variables_are_equal_to_default_values
data_expression variables_are_equal_to_default_values(const variable_list &vl)
Definition linearise.cpp:5684
specification_basic_type::procstorealGNF
void procstorealGNF(const process_identifier &procsIdDecl, const bool regular)
Definition linearise.cpp:3611
specification_basic_type::check_assignment_list
static bool check_assignment_list(const assignment_list &assignments, const variable_list &parameters)
Definition linearise.cpp:1489
specification_basic_type::RewriteTerm
data_expression RewriteTerm(const data_expression &t)
Definition linearise.cpp:533
specification_basic_type::alphaconversion
void alphaconversion(const process_identifier &procId, const variable_list &parameters)
Definition linearise.cpp:8693
specification_basic_type::all_equal
bool all_equal(const atermpp::term_list< T > &l)
Definition linearise.cpp:5851
specification_basic_type::cluster_actions
void cluster_actions(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)
Definition linearise.cpp:6838
specification_basic_type::transform_initial_distribution_term
process_expression transform_initial_distribution_term(const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)
Definition linearise.cpp:8908
specification_basic_type::create_regular_invocation
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)
Definition linearise.cpp:3102
specification_basic_type::transform_process_arguments_body
process_expression transform_process_arguments_body(const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)
Definition linearise.cpp:9653
specification_basic_type::parameters_to_assignment_list
static assignment_list parameters_to_assignment_list(const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)
Definition linearise.cpp:2143
specification_basic_type::dummyparameterlist
assignment_list dummyparameterlist(const stacklisttype &stack, const bool singlestate)
Definition linearise.cpp:5007
specification_basic_type::rewr
mcrl2::data::rewriter rewr
Definition linearise.cpp:155
specification_basic_type::make_pCRL_procs
void make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)
Definition linearise.cpp:3650
specification_basic_type::stack_operations_list
stackoperations * stack_operations_list
Definition linearise.cpp:175
specification_basic_type::wraptime
process_expression wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)
Definition linearise.cpp:1935
specification_basic_type::objectIndex
objectdatatype & objectIndex(const process_identifier &o)
Definition linearise.cpp:290
specification_basic_type::split_process
process_identifier split_process(const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)
Definition linearise.cpp:9524
specification_basic_type::mergeoccursin
bool mergeoccursin(variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)
Definition linearise.cpp:5597
specification_basic_type::occursintermlist
static bool occursintermlist(const variable &var, const data_expression_list &r)
Definition linearise.cpp:1251
specification_basic_type::exists_variable_for_sequence
bool exists_variable_for_sequence(const std::vector< process_instance_assignment > &process_names, process_identifier &result)
Definition linearise.cpp:2911
specification_basic_type::find_free_variables_process
std::set< variable > find_free_variables_process(const process_expression &p)
Definition linearise.cpp:1466
specification_basic_type::alphaconversionterm
process_expression alphaconversionterm(const process_expression &t, const variable_list &parameters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)
Definition linearise.cpp:8556
specification_basic_type::putbehind
process_expression putbehind(const process_expression &body1, const process_expression &body2)
Definition linearise.cpp:2530
specification_basic_type::substitute_assignmentlist
assignment_list substitute_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
Definition linearise.cpp:1509
specification_basic_type::transform_process_instance_to_process_instance_assignment
process_instance_assignment transform_process_instance_to_process_instance_assignment(const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())
Definition linearise.cpp:1814
specification_basic_type::RewriteProcess
process_instance_assignment RewriteProcess(const process_instance_assignment &t)
Definition linearise.cpp:572
specification_basic_type::delta_process
process_identifier delta_process
Definition linearise.cpp:160
specification_basic_type::objectIndex
const objectdatatype & objectIndex(const process_identifier &o) const
Definition linearise.cpp:306
specification_basic_type::insert_summand
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)
Definition linearise.cpp:5019
specification_basic_type::alreadypresent
bool alreadypresent(variable &var, const variable_list &vl, mutable_indexed_substitution<> &parameter_renaming)
Definition linearise.cpp:3979
specification_basic_type::parameters_that_occur_in_body
variable_list parameters_that_occur_in_body(const variable_list &parameters, const process_expression &body)
Definition linearise.cpp:1863
specification_basic_type::enumerate_distribution_and_sums
process_expression enumerate_distribution_and_sums(const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)
Definition linearise.cpp:2699
specification_basic_type::containstimebody
bool containstimebody(const process_expression &t)
Definition linearise.cpp:8879
specification_basic_type::make_procargs
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)
Definition linearise.cpp:4818
specification_basic_type::adapt_term_to_stack
data_expression adapt_term_to_stack(const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
Definition linearise.cpp:4453
specification_basic_type::processencoding
data_expression_list processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)
Definition linearise.cpp:4336
specification_basic_type::RewriteMultAct
process_expression RewriteMultAct(const process_expression &t)
Definition linearise.cpp:577
specification_basic_type::generateLPEmCRLterm
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.
Definition linearise.cpp:8215
specification_basic_type::~specification_basic_type
~specification_basic_type()
Definition linearise.cpp:220
specification_basic_type::make_pars
variable_list make_pars(const sort_expression_list &sortlist)
Definition linearise.cpp:2058
specification_basic_type::specification_basic_type
specification_basic_type(const specification_basic_type &)=delete
specification_basic_type::real_times_optimized
static data_expression real_times_optimized(const data_expression &r1, const data_expression &r2)
Definition linearise.cpp:234
specification_basic_type::occursinpCRLterm
bool occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)
Definition linearise.cpp:1328
specification_basic_type::collectPcrlProcesses
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)
Definition linearise.cpp:1193
specification_basic_type::upperpowerof2
static std::size_t upperpowerof2(std::size_t i)
Definition linearise.cpp:518
specification_basic_type::extract_names
void extract_names(const process_expression &sequence, std::vector< process_instance_assignment > &result)
Definition linearise.cpp:2931
specification_basic_type::objectdata
std::map< aterm, objectdatatype > objectdata
Definition linearise.cpp:169
specification_basic_type::RewriteAction
action RewriteAction(const action &t)
Definition linearise.cpp:567
specification_basic_type::adapt_termlist_to_stack
data_expression_vector adapt_termlist_to_stack(Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
Definition linearise.cpp:4533
specification_basic_type::make_procargs_stack
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)
Definition linearise.cpp:4765
specification_basic_type::specification_basic_type
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)
Definition linearise.cpp:178
specification_basic_type::getparameters
variable_list getparameters(const process_expression &multiAction)
Definition linearise.cpp:414
specification_basic_type::makesingleultimatedelaycondition
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)
Definition linearise.cpp:7182
specification_basic_type::collectPcrlProcesses_term
void collectPcrlProcesses_term(const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
Definition linearise.cpp:1067
specification_basic_type::representative_generator_internal
data_expression representative_generator_internal(const sort_expression &s, const bool allow_dont_care_var=true)
Definition linearise.cpp:4569
specification_basic_type::processencoding
assignment_list processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)
Definition linearise.cpp:4283
specification_basic_type::addMultiAction
objectdatatype & addMultiAction(const process_expression &multiAction, bool &isnew)
Definition linearise.cpp:452
specification_basic_type::storeprocs
void storeprocs(const std::vector< process_equation > &procs)
Definition linearise.cpp:718
specification_basic_type::substitute_pCRLproc
process_expression substitute_pCRLproc(const process_expression &p, Substitution &sigma)
Definition linearise.cpp:1669
specification_basic_type::make_parameters_and_sum_variables_unique
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="")
Definition linearise.cpp:7400
specification_basic_type::global_variables
std::set< variable > global_variables
Definition linearise.cpp:135
specification_basic_type::getRHSassignment
static data_expression getRHSassignment(const variable &var, const assignment_list &as)
Definition linearise.cpp:5916
specification_basic_type::construct_renaming
variable_list construct_renaming(const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
Definition linearise.cpp:7085
specification_basic_type::determine_process_status
void determine_process_status(const process_identifier &procDecl, const processstatustype status)
Definition linearise.cpp:1031
specification_basic_type::makemultiaction
static action_list makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)
Definition linearise.cpp:432
specification_basic_type::insertvariables
void insertvariables(const variable_list &vars, const bool mustbenew)
Definition linearise.cpp:493
specification_basic_type::collectparameterlist
variable_list collectparameterlist(std::set< process_identifier > &pCRLprocs)
Definition linearise.cpp:4042
specification_basic_type::RewriteTermList
data_expression_list RewriteTermList(const data_expression_list &t)
Definition linearise.cpp:547
specification_basic_type::data
data_specification data
Definition linearise.cpp:139
specification_basic_type::make_parameters_rec
variable_list make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)
Definition linearise.cpp:377
specification_basic_type::detail_check_objectdata
void detail_check_objectdata(const process_identifier &o) const
Definition linearise.cpp:281
specification_basic_type::filter_assignments
static assignment_list filter_assignments(const assignment_list &assignments, const variable_list &parameters)
Definition linearise.cpp:1475
specification_basic_type::merge_var
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)
Definition linearise.cpp:5752
specification_basic_type::containstimebody
bool containstimebody(const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)
Definition linearise.cpp:8727
specification_basic_type::options
t_lin_options options
Definition linearise.cpp:165
specification_basic_type::sort_assignments
static assignment_list sort_assignments(const assignment_list &ass, const variable_list &parameters)
Definition linearise.cpp:1614
specification_basic_type::find_dummy_arguments
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)
Definition linearise.cpp:4635
specification_basic_type::tau_process
process_identifier tau_process
Definition linearise.cpp:159
specification_basic_type::get_sorts
static sort_expression_list get_sorts(const List &l)
Definition linearise.cpp:7149
specification_basic_type::seq_varnames
std::vector< process_identifier > seq_varnames
Definition linearise.cpp:161
specification_basic_type::storeact
void storeact(const process::action_label_list &acts)
Definition linearise.cpp:678
specification_basic_type::is_global_variable
bool is_global_variable(const data_expression &d) const
Definition linearise.cpp:4253
specification_basic_type::joinparameters
variable_list joinparameters(const variable_list &par1, const variable_list &par2, mutable_indexed_substitution<> &parameter_renaming)
Definition linearise.cpp:4018
specification_basic_type::occursin
static bool occursin(const variable &name, const variable_list &pars)
Definition linearise.cpp:4837
specification_basic_type::canterminatebody
bool canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)
Definition linearise.cpp:9367
specification_basic_type::AddTerminationActionIfNecessary
void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)
Definition linearise.cpp:9908
specification_basic_type::determinewhetherprocessescontaintime
bool determinewhetherprocessescontaintime(const process_identifier &procId)
Definition linearise.cpp:8887
specification_basic_type::filter_vars_by_assignmentlist
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)
Definition linearise.cpp:1314
specification_basic_type::addcondition
data_expression_list addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)
Definition linearise.cpp:5736
specification_basic_type::calculate_communication_merge_deadlock_summands
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)
Definition linearise.cpp:7905
specification_basic_type::transform
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)
Definition linearise.cpp:9995
specification_basic_type::obtain_initial_distribution
process_expression obtain_initial_distribution(const process_identifier &procId)
Definition linearise.cpp:9342
specification_basic_type::insertAction
objectdatatype & insertAction(const action_label &actionId)
Definition linearise.cpp:659
specification_basic_type::replace_variables_capture_avoiding_alt
Expression replace_variables_capture_avoiding_alt(const Expression &e, Substitution &sigma)
Definition linearise.cpp:273
specification_basic_type::expand_process_instance_assignment
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t, std::set< process_identifier > &visited_processes)
Definition linearise.cpp:9574
specification_basic_type::pushdummy_regular
assignment_list pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
Definition linearise.cpp:4885
specification_basic_type::argscollect_regular
assignment_list argscollect_regular(const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)
Definition linearise.cpp:3015
specification_basic_type::getarguments
static data_expression_list getarguments(const action_list &multiAction)
Definition linearise.cpp:421
specification_basic_type::getUltimateDelayCondition
lps::detail::ultimate_delay getUltimateDelayCondition(const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)
Definition linearise.cpp:7261
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:435
mcrl2::data::detail::split_condition
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.
Definition linear_inequalities_utilities.h:226
mcrl2::data::detail::map_to_lhs_type
lhs_t map_to_lhs_type(const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
Definition linear_inequalities.h:345
mcrl2::data::detail::negate_inequality
data_expression negate_inequality(const data_expression &e)
Definition linear_inequalities_utilities.h:22
mcrl2::data::detail::map_to_lhs_type
lhs_t map_to_lhs_type(const map_based_lhs_t &lhs)
Definition linear_inequalities.h:335
mcrl2::data::detail::pp
std::string pp(const detail::comparison_t t)
Definition linear_inequalities.h:117
mcrl2::data::detail::set_factor_for_a_variable
lhs_t set_factor_for_a_variable(const lhs_t &lhs, const variable &x, const data_expression &e)
Definition linear_inequalities.h:306
mcrl2::data::detail::else_part
const data_expression & else_part(const data_expression &e)
Definition linear_inequalities_utilities.h:84
mcrl2::data::detail::is_well_formed
bool is_well_formed(const lhs_t &lhs)
Definition linear_inequalities.h:356
mcrl2::data::detail::is_inequality
bool is_inequality(const data_expression &e)
Determine whether a data expression is an inequality.
Definition linear_inequalities_utilities.h:60
mcrl2::data::detail::negate
detail::comparison_t negate(const detail::comparison_t t)
Definition linear_inequalities.h:106
mcrl2::data::detail::condition_part
const data_expression & condition_part(const data_expression &e)
Definition linear_inequalities_utilities.h:68
mcrl2::data::detail::remove_variable_and_divide
lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
Definition linear_inequalities.h:383
mcrl2::data::detail::pp
std::string pp(const detail::lhs_t &lhs)
Definition linear_inequalities.h:509
mcrl2::data::detail::then_part
const data_expression & then_part(const data_expression &e)
Definition linear_inequalities_utilities.h:76
mcrl2::data::detail::split_condition_aux
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.
Definition linear_inequalities_utilities.h:108
mcrl2::data::detail::set_factor_for_a_variable
void set_factor_for_a_variable(detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
Definition linear_inequalities.h:289
mcrl2::data::detail::f_variable_with_a_rational_factor
atermpp::function_symbol f_variable_with_a_rational_factor()
Definition linear_inequalities.h:128
mcrl2::data::lazy
A collection of utilities for lazy expression construction.
Definition standard_utility.h:62
mcrl2::data::lazy::and_
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
Definition standard_utility.h:106
mcrl2::data::sort_bool
Namespace for system defined sort bool_.
Definition bool.h:29
mcrl2::data::sort_bool::is_or_application
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:342
mcrl2::data::sort_bool::bool_
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
mcrl2::data::sort_bool::right
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:490
mcrl2::data::sort_bool::is_implies_application
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:406
mcrl2::data::sort_bool::not_
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:194
mcrl2::data::sort_bool::or_
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:321
mcrl2::data::sort_bool::false_
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:106
mcrl2::data::sort_bool::is_and_application
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:278
mcrl2::data::sort_bool::is_not_application
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:214
mcrl2::data::sort_bool::true_
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:74
mcrl2::data::sort_bool::left
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:478
mcrl2::data::sort_real
Namespace for system defined sort real_.
Definition real_utilities.h:19
mcrl2::data::sort_real::plus
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1056
mcrl2::data::sort_real::times
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1234
mcrl2::data::sort_real::is_zero
bool is_zero(const atermpp::aterm &e)
Definition real_utilities.h:33
mcrl2::data::sort_real::divides
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1404
mcrl2::data::sort_real::real_one
data_expression & real_one()
Definition real_utilities.h:27
mcrl2::data::sort_real::is_one
bool is_one(const atermpp::aterm &e)
Definition real_utilities.h:38
mcrl2::data::sort_real::is_plus_application
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1133
mcrl2::data::sort_real::real_zero
data_expression & real_zero()
Definition real_utilities.h:21
mcrl2::data::sort_real::is_creal_application
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:150
mcrl2::data::sort_real::minus
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1149
mcrl2::data::sort_real::real_
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:45
mcrl2::data::sort_real::is_real
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:55
mcrl2::data::sort_real::times
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1282
mcrl2::data::sort_real::is_larger_zero
bool is_larger_zero(const atermpp::aterm &e)
Functions that returns true if e is a closed real number larger than zero.
Definition real_utilities.h:44
mcrl2::data::sort_real::abs
function_symbol abs(const sort_expression &s0)
Definition real1.h:732
mcrl2::data::sort_real::is_times_application
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1303
mcrl2::data::sort_real::negate
function_symbol negate(const sort_expression &s0)
Definition real1.h:807
mcrl2::data::sort_real::is_negate_application
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:874
mcrl2::data::sort_real::is_minus_application
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1218
mcrl2::data::subtract
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,.
Definition linear_inequalities.h:916
mcrl2::data::optimized_imp
data_expression optimized_imp(const data_expression &p, const data_expression &q)
Make an implication and apply optimisations.
Definition optimized_boolean_operators.h:96
mcrl2::data::make_optimized_imp
void make_optimized_imp(data_expression &result, const data_expression &p, const data_expression &q)
Make an implication and apply optimisations.
Definition optimized_boolean_operators.h:86
mcrl2::data::make_optimized_and
void make_optimized_and(data_expression &result, const data_expression &p, const data_expression &q)
Make a conjunction, and optimize if possible.
Definition optimized_boolean_operators.h:45
mcrl2::data::make_optimized_or
void make_optimized_or(data_expression &result, const data_expression &p, const data_expression &q)
Make a disjunction.
Definition optimized_boolean_operators.h:65
mcrl2::data::real_times
application real_times(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:42
mcrl2::data::undefined_real
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
mcrl2::data::real_one
data_expression & real_one()
Definition linear_inequalities.h:941
mcrl2::data::make_optimized_exists
void make_optimized_exists(data_expression &result, const variable_list &l, const data_expression &p, bool remove_variables=false)
Make an existential quantification and apply optimisations.
Definition optimized_boolean_operators.h:130
mcrl2::data::is_closed_real_number
bool is_closed_real_number(const data_expression &e)
Definition linear_inequalities.h:979
mcrl2::data::is_application
bool is_application(const data_expression &t)
Returns true if the term t is an application.
Definition data_expression.h:296
mcrl2::data::real_plus
application real_plus(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:49
mcrl2::data::real_minus_one
data_expression & real_minus_one()
Definition linear_inequalities.h:947
mcrl2::data::is_simple_substitution
bool is_simple_substitution(const map_substitution< AssociativeContainer > &sigma)
Definition map_substitution.h:85
mcrl2::data::optimized_or
data_expression optimized_or(const data_expression &p, const data_expression &q)
Make a disjunction.
Definition optimized_boolean_operators.h:75
mcrl2::data::is_positive
bool is_positive(const data_expression &e, const rewriter &r)
Definition linear_inequalities.h:1004
mcrl2::data::is_where_clause
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
Definition data_expression.h:103
mcrl2::data::less_equal
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:300
mcrl2::data::optimized_not
data_expression optimized_not(const data_expression &arg)
Make a negation.
Definition optimized_boolean_operators.h:35
mcrl2::data::real_abs
application real_abs(const data_expression &arg)
Definition linear_inequalities.h:77
mcrl2::data::less
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:263
mcrl2::data::substitution_variables
std::set< data::variable > substitution_variables(const map_substitution< AssociativeContainer > &sigma)
Definition map_substitution.h:74
mcrl2::data::make_optimized_not
void make_optimized_not(data_expression &result, const data_expression &arg)
Make a negation.
Definition optimized_boolean_operators.h:26
mcrl2::data::pp_vector
std::string pp_vector(const TYPE &inequalities)
Print the vector of inequalities to stderr in readable form.
Definition linear_inequalities.h:1027
mcrl2::data::is_abstraction
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
Definition data_expression.h:25
mcrl2::data::if_
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:224
mcrl2::data::remove_redundant_inequalities
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.
Definition linear_inequalities.h:1155
mcrl2::data::real_minus
application real_minus(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:63
mcrl2::data::make_map_substitution
map_substitution< AssociativeContainer > make_map_substitution(const AssociativeContainer &m)
Utility function for creating a map_substitution.
Definition map_substitution.h:68
mcrl2::data::fourier_motzkin
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.
Definition fourier_motzkin.h:201
mcrl2::data::is_simple_substitution
bool is_simple_substitution(const assignment_sequence_substitution &sigma)
Definition assignment_sequence_substitution.h:51
mcrl2::data::pp
std::string pp(const linear_inequality &l)
Definition linear_inequalities.h:909
mcrl2::data::real_divides
application real_divides(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:56
mcrl2::data::gauss_elimination
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.
Definition linear_inequalities.h:1911
mcrl2::data::is_zero
bool is_zero(const data_expression &e)
Definition linear_inequalities.h:1018
mcrl2::data::is_function_symbol
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
Definition data_expression.h:67
mcrl2::data::fourier_motzkin
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)
Definition fourier_motzkin.h:27
mcrl2::data::rewrite_with_memory
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
Definition linear_inequalities.h:2082
mcrl2::data::real_zero
data_expression & real_zero()
Definition linear_inequalities.h:935
mcrl2::data::greater
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:337
mcrl2::data::is_untyped_data_parameter
bool is_untyped_data_parameter(const atermpp::aterm &x)
Definition untyped_data_parameter.h:84
mcrl2::data::optimized_exists
data_expression optimized_exists(const variable_list &l, const data_expression &p, bool remove_variables=false)
Make an existential quantification and apply optimisations.
Definition optimized_boolean_operators.h:141
mcrl2::data::make_optimized_forall
void make_optimized_forall(data_expression &result, const variable_list &l, const data_expression &p, bool remove_variables=false)
Make a universal quantification and apply optimisations.
Definition optimized_boolean_operators.h:107
mcrl2::data::real_negate
application real_negate(const data_expression &arg)
Definition linear_inequalities.h:70
mcrl2::data::optimized_and
data_expression optimized_and(const data_expression &p, const data_expression &q)
Make a conjunction, and optimize if possible.
Definition optimized_boolean_operators.h:55
mcrl2::data::is_inconsistent
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.
Definition linear_inequalities.h:1534
mcrl2::data::max
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
Definition linear_inequalities.h:966
mcrl2::data::is_machine_number
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
Definition data_expression.h:79
mcrl2::data::is_negative
bool is_negative(const data_expression &e, const rewriter &r)
Definition linear_inequalities.h:990
mcrl2::data::variable_list_to_data_expression_list
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
Definition data_expression.h:308
mcrl2::data::equal_to
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:149
mcrl2::data::min
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
Definition linear_inequalities.h:953
mcrl2::data::optimized_forall
data_expression optimized_forall(const variable_list &l, const data_expression &p, bool remove_variables=false)
Make a universal quantification and apply optimisations.
Definition optimized_boolean_operators.h:118
mcrl2::data::swap
void swap(data_expression &t1, data_expression &t2) noexcept
\brief swap overload
Definition data_expression.h:217
mcrl2::data::is_variable
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
Definition data_expression.h:73
mcrl2::lps::detail
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition linearise_allow_block.h:68
mcrl2::lps::detail::replace_global_variables
void replace_global_variables(Specification &lpsspec, const data::mutable_map_substitution<> &sigma)
Applies a global variable substitution to an LPS.
Definition instantiate_global_variables.h:23
mcrl2::lps::detail::convert_action_summands
stochastic_action_summand_vector convert_action_summands(const action_summand_vector &action_summands)
Definition stochastic_linear_process.h:36
mcrl2::lps::detail::instantiate_global_variables
data::mutable_map_substitution instantiate_global_variables(Specification &lpsspec)
Eliminates the global variables of an LPS, by substituting a constant value for them....
Definition instantiate_global_variables.h:34
mcrl2::lps::detail::make_action_summand
Summand make_action_summand(const data::variable_list &, const data::data_expression &, const multi_action &, const data::assignment_list &, const stochastic_distribution &)
Definition linear_process.h:26
mcrl2::lps
The main namespace for the LPS library.
Definition constelm.h:18
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_process_initializer &x)
Definition stochastic_process_initializer.h:80
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_distribution &x)
Definition stochastic_distribution.h:98
mcrl2::lps::pp
std::string pp(const lps::stochastic_specification &x, bool arg0)
Definition lps.cpp:40
mcrl2::lps::find_all_variables
std::set< data::variable > find_all_variables(const lps::linear_process &x)
Definition lps.cpp:47
mcrl2::lps::make_stochastic_distribution
void make_stochastic_distribution(atermpp::aterm &t, const ARGUMENTS &... args)
Definition stochastic_distribution.h:70
mcrl2::lps::pp
std::string pp(const lps::specification &x, bool arg0)
Definition lps.cpp:35
mcrl2::lps::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
Definition lps.cpp:46
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
Definition lps.cpp:56
mcrl2::lps::pp
std::string pp(const lps::stochastic_distribution &x, bool arg0)
Definition lps.cpp:37
mcrl2::lps::pp_extended
std::string pp_extended(const stochastic_specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:98
mcrl2::lps::complete_data_specification
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
Definition stochastic_specification.h:101
mcrl2::lps::replace_variables_capture_avoiding
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
Definition replace_capture_avoiding.h:187
mcrl2::lps::swap
void swap(action_summand &t1, action_summand &t2) noexcept
\brief swap overload
Definition action_summand.h:132
mcrl2::lps::swap
void swap(deadlock_summand &t1, deadlock_summand &t2) noexcept
\brief swap overload
Definition deadlock_summand.h:97
mcrl2::lps::operator!=
bool operator!=(const stochastic_specification &spec1, const stochastic_specification &spec2)
Inequality operator.
Definition stochastic_specification.h:91
mcrl2::lps::replace_sort_expressions
void replace_sort_expressions(T &x, const Substitution &sigma, bool innermost)
Definition replace.h:28
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_linear_process &x)
Definition stochastic_linear_process.h:86
mcrl2::lps::find_all_variables
std::set< data::variable > find_all_variables(const lps::stochastic_specification &x)
Definition lps.cpp:50
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const process_initializer &x)
Definition process_initializer.h:96
mcrl2::lps::check_well_typedness
bool check_well_typedness(const specification &x)
Definition lps.cpp:118
mcrl2::lps::is_stochastic_process_initializer
bool is_stochastic_process_initializer(const atermpp::aterm &x)
Definition stochastic_process_initializer.h:67
mcrl2::lps::complete_data_specification
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
Definition specification.h:252
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const specification &x)
Definition specification.h:205
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::linear_process &x)
Definition lps.cpp:53
mcrl2::lps::is_specification
bool is_specification(const atermpp::aterm &x)
Test for a specification expression.
Definition specification.h:41
mcrl2::lps::check_well_typedness
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:108
mcrl2::lps::swap
void swap(deadlock &t1, deadlock &t2) noexcept
\brief swap overload
Definition deadlock.h:105
mcrl2::lps::swap
void swap(multi_action &t1, multi_action &t2) noexcept
\brief swap overload
Definition multi_action.h:117
mcrl2::lps::replace_variables_capture_avoiding
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
Definition replace_capture_avoiding.h:202
mcrl2::lps::find_function_symbols
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
Definition lps.cpp:62
mcrl2::lps::occursinterm
bool occursinterm(const data::data_expression &t, const data::variable &var)
Definition linearise_utility.h:216
mcrl2::lps::pp_extended
std::string pp_extended(const specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:88
mcrl2::lps::operator<
bool operator<(const stochastic_action_summand &x, const stochastic_action_summand &y)
Comparison operator for action summands.
Definition stochastic_action_summand.h:97
mcrl2::lps::remove_parameters
void remove_parameters(Object &x, const std::set< data::variable > &to_be_removed)
Rewrites an LPS data type.
Definition remove.h:187
mcrl2::lps::specification_to_aterm
atermpp::aterm specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm.
Definition specification.h:224
mcrl2::lps::find_action_labels
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
Definition lps.cpp:66
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const deadlock &x)
Definition deadlock.h:99
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::specification &x)
Definition lps.cpp:55
mcrl2::lps::constelm
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
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const action_summand &x)
Definition action_summand.h:126
mcrl2::lps::normalize_sorts
void normalize_sorts(lps::specification &x, const data::sort_specification &)
Definition lps.cpp:42
mcrl2::lps::deadlock_summand_to_aterm
atermpp::aterm deadlock_summand_to_aterm(const deadlock_summand &s)
Conversion to atermappl.
Definition deadlock_summand.h:106
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:57
mcrl2::lps::operator==
bool operator==(const specification &spec1, const specification &spec2)
Equality operator.
Definition specification.h:237
mcrl2::lps::pp
std::string pp(const lps::deadlock_summand &x, bool arg0)
Definition lps.cpp:31
mcrl2::lps::find_action_labels
std::set< process::action_label > find_action_labels(const lps::linear_process &x)
Definition lps.cpp:65
mcrl2::lps::normalize_sorts
lps::multi_action normalize_sorts(const lps::multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:41
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:54
mcrl2::lps::find_function_symbols
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
Definition lps.cpp:61
mcrl2::lps::pp
std::string pp(const lps::stochastic_linear_process &x, bool arg0)
Definition lps.cpp:38
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::stochastic_process_initializer &x)
Definition lps.cpp:60
mcrl2::lps::operator==
bool operator==(const stochastic_specification &spec1, const stochastic_specification &spec2)
Definition stochastic_specification.h:84
mcrl2::lps::swap
void swap(stochastic_action_summand &t1, stochastic_action_summand &t2) noexcept
\brief swap overload
Definition stochastic_action_summand.h:89
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::multi_action &x)
Definition lps.cpp:58
mcrl2::lps::pp
std::string pp(const lps::deadlock &x, bool arg0)
Definition lps.cpp:30
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const multi_action &x)
Definition multi_action.h:111
mcrl2::lps::remove_redundant_assignments
void remove_redundant_assignments(Specification &lpsspec)
Removes redundant assignments of the form x = x from an LPS specification.
Definition remove.h:244
mcrl2::lps::operator!=
bool operator!=(const specification &spec1, const specification &spec2)
Inequality operator.
Definition specification.h:244
mcrl2::lps::normalize_sorts
void normalize_sorts(lps::stochastic_specification &x, const data::sort_specification &)
Definition lps.cpp:43
mcrl2::lps::find_free_variables
std::set< data::variable > find_free_variables(const lps::process_initializer &x)
Definition lps.cpp:59
mcrl2::lps::equal_multi_actions
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....
Definition multi_action.h:290
mcrl2::lps::is_stochastic_distribution
bool is_stochastic_distribution(const atermpp::aterm &x)
Definition stochastic_distribution.h:85
mcrl2::lps::remove_stochastic_operators
specification remove_stochastic_operators(const stochastic_specification &spec)
Converts a stochastic specification to a specification. Throws an exception if non-empty distribution...
Definition stochastic_specification.h:110
mcrl2::lps::operator==
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
Definition action_summand.h:159
mcrl2::lps::is_process_initializer
bool is_process_initializer(const atermpp::aterm &x)
Definition process_initializer.h:83
mcrl2::lps::remove_singleton_sorts
void remove_singleton_sorts(Specification &spec)
Removes parameters with a singleton sort from a linear process specification.
Definition remove.h:208
mcrl2::lps::check_well_typedness
bool check_well_typedness(const Object &o)
mcrl2::lps::pp
std::string pp(const lps::stochastic_action_summand &x, bool arg0)
Definition lps.cpp:36
mcrl2::lps::remove_redundant_assignments
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::replace_sort_expressions
T replace_sort_expressions(const T &x, const Substitution &sigma, bool innermost)
Definition replace.h:38
mcrl2::lps::linearise
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.
Definition linearise.cpp:10051
mcrl2::lps::pp
std::string pp(const lps::stochastic_process_initializer &x, bool arg0)
Definition lps.cpp:39
mcrl2::lps::pp
std::string pp(const lps::linear_process &x, bool arg0)
Definition lps.cpp:32
mcrl2::lps::pp
std::string pp(const lps::multi_action &x, bool arg0)
Definition lps.cpp:33
mcrl2::lps::make_stochastic_process_initializer
void make_stochastic_process_initializer(atermpp::aterm &t, ARGUMENTS... args)
Definition stochastic_process_initializer.h:50
mcrl2::lps::swap
void swap(stochastic_process_initializer &t1, stochastic_process_initializer &t2) noexcept
\brief swap overload
Definition stochastic_process_initializer.h:86
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_action_summand &x)
Definition stochastic_action_summand.h:83
mcrl2::lps::linear_process_to_aterm
atermpp::aterm linear_process_to_aterm(const linear_process_base< ActionSummand > &p)
Conversion to aterm.
Definition linear_process.h:222
mcrl2::lps::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:45
mcrl2::lps::make_process_initializer
void make_process_initializer(atermpp::aterm &t, EXPRESSION_LIST args)
Definition process_initializer.h:66
mcrl2::lps::operator==
bool operator==(const stochastic_action_summand &x, const stochastic_action_summand &y)
Equality operator of stochastic action summands.
Definition stochastic_action_summand.h:108
mcrl2::lps::make_multi_action
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
Definition multi_action.h:127
mcrl2::lps::not_equal_multi_actions
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...
Definition multi_action.h:327
mcrl2::lps::pp
std::string pp(const lps::action_summand &x, bool arg0)
Definition lps.cpp:29
mcrl2::lps::remove_trivial_summands
void remove_trivial_summands(Specification &spec)
Removes summands with condition equal to false from a linear process specification.
Definition remove.h:196
mcrl2::lps::operator<
bool operator<(const action_summand &x, const action_summand &y)
Comparison operator for action summands.
Definition action_summand.h:140
mcrl2::lps::find_all_variables
std::set< data::variable > find_all_variables(const lps::specification &x)
Definition lps.cpp:49
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const linear_process &x)
Definition linear_process.h:251
mcrl2::lps::check_well_typedness
bool check_well_typedness(const stochastic_specification &x)
Definition lps.cpp:123
mcrl2::lps::find_all_variables
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:51
mcrl2::lps::action_summand_to_aterm
atermpp::aterm action_summand_to_aterm(const action_summand &s)
Conversion to aterm.
Definition action_summand.h:169
mcrl2::lps::find_all_variables
std::set< data::variable > find_all_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:48
mcrl2::lps::check_well_typedness
bool check_well_typedness(const stochastic_linear_process &x)
Definition lps.cpp:113
mcrl2::lps::translate_user_notation
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:44
mcrl2::lps::swap
void swap(stochastic_distribution &t1, stochastic_distribution &t2) noexcept
\brief swap overload
Definition stochastic_distribution.h:104
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_specification &x)
Definition stochastic_specification.h:77
mcrl2::lps::find_identifiers
std::set< core::identifier_string > find_identifiers(const lps::stochastic_specification &x)
Definition lps.cpp:64
mcrl2::lps::action_summand_to_aterm
atermpp::aterm action_summand_to_aterm(const stochastic_action_summand &s)
Conversion to aterm.
Definition stochastic_action_summand.h:115
mcrl2::lps::swap
void swap(process_initializer &t1, process_initializer &t2) noexcept
\brief swap overload
Definition process_initializer.h:102
mcrl2::lps::find_identifiers
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
Definition lps.cpp:63
mcrl2::lps::operator<<
std::ostream & operator<<(std::ostream &out, const deadlock_summand &x)
Definition deadlock_summand.h:91
mcrl2::lps::find_action_labels
std::set< process::action_label > find_action_labels(const lps::specification &x)
Definition lps.cpp:67
mcrl2::lps::pp
std::string pp(const lps::process_initializer &x, bool arg0)
Definition lps.cpp:34
mcrl2::lps::is_multi_action
bool is_multi_action(const atermpp::aterm &x)
Definition multi_action.h:98
mcrl2::lps::is_linear_process
bool is_linear_process(const atermpp::aterm &x)
Test for a linear_process expression.
Definition linear_process.h:261
mcrl2::process
The main namespace for the Process library.
Definition alphabet_reduce.h:18
mcrl2::process::pp
std::string pp(const action_list &x, bool precedence_aware=true)
Definition process.cpp:24
mcrl2::process::is_at
bool is_at(const atermpp::aterm &x)
Definition process_expression.h:1054
mcrl2::process::swap
void swap(rename &t1, rename &t2) noexcept
\brief swap overload
Definition process_expression.h:769
mcrl2::process::make_allow
void make_allow(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:893
mcrl2::process::swap
void swap(at &t1, at &t2) noexcept
\brief swap overload
Definition process_expression.h:1073
mcrl2::process::swap
void swap(action &t1, action &t2) noexcept
\brief swap overload
Definition process_expression.h:213
mcrl2::process::operator<
bool operator<(const action_label &a1, const action_label &a2)
Total ordering on action labels: name first (string order), then sorts.
Definition action_label.h:126
mcrl2::process::find_all_variables
std::set< data::variable > find_all_variables(const action &x)
Definition process.cpp:76
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const sync &x)
Definition process_expression.h:991
mcrl2::process::normalize_sorts
void normalize_sorts(process::process_equation_vector &x, const data::sort_specification &sortspec)
Definition process.cpp:67
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const bounded_init &x)
Definition process_expression.h:1376
mcrl2::process::make_choice
void make_choice(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1582
mcrl2::process::pp
std::string pp(const process::action_name_multiset &x, bool arg0)
Definition process.cpp:36
mcrl2::process::pp
std::string pp(const process::action_label &x, bool arg0)
Definition process.cpp:35
mcrl2::process::pp
std::string pp(const process::process_identifier &x, bool arg0)
Definition process.cpp:52
mcrl2::process::swap
void swap(if_then &t1, if_then &t2) noexcept
\brief swap overload
Definition process_expression.h:1225
mcrl2::process::make_process_identifier
void make_process_identifier(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_identifier.h:73
mcrl2::process::swap
void swap(bounded_init &t1, bounded_init &t2) noexcept
\brief swap overload
Definition process_expression.h:1382
mcrl2::process::is_process_instance
bool is_process_instance(const atermpp::aterm &x)
Definition process_expression.h:270
mcrl2::process::swap
void swap(delta &t1, delta &t2) noexcept
\brief swap overload
Definition process_expression.h:418
mcrl2::process::pp
std::string pp(const tau &x, bool precedence_aware=true)
Definition process.cpp:62
mcrl2::process::normalize_sorts
process::action_label_list normalize_sorts(const process::action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:66
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const sum &x)
Definition process_expression.h:541
mcrl2::process::pp
std::string pp(const if_then &x, bool precedence_aware=true)
Definition process.cpp:46
mcrl2::process::make_merge
void make_merge(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1430
mcrl2::process::swap
void swap(rename_expression &t1, rename_expression &t2) noexcept
\brief swap overload
Definition rename_expression.h:103
mcrl2::process::pp
std::string pp(const stochastic_operator &x, bool precedence_aware=true)
Definition process.cpp:59
mcrl2::process::swap
void swap(merge &t1, merge &t2) noexcept
\brief swap overload
Definition process_expression.h:1458
mcrl2::process::make_at
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1045
mcrl2::process::is_process_expression
bool is_process_expression(const atermpp::aterm &x)
Definition process_expression.h:90
mcrl2::process::is_process_instance_assignment
bool is_process_instance_assignment(const atermpp::aterm &x)
Definition process_expression.h:346
mcrl2::process::swap
void swap(left_merge &t1, left_merge &t2) noexcept
\brief swap overload
Definition process_expression.h:1534
mcrl2::process::pp
std::string pp(const process::communication_expression &x, bool arg0)
Definition process.cpp:43
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const untyped_process_assignment &x)
Definition process_expression.h:1766
mcrl2::process::is_tau
bool is_tau(const atermpp::aterm &x)
Definition process_expression.h:452
mcrl2::process::pp
std::string pp(const process::rename_expression &x, bool arg0)
Definition process.cpp:57
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const stochastic_operator &x)
Definition process_expression.h:1685
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const left_merge &x)
Definition process_expression.h:1528
mcrl2::process::pp
std::string pp(const process_identifier_list &x)
mcrl2::process::make_action
void make_action(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:179
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const process_identifier &x)
Definition process_identifier.h:101
mcrl2::process::is_seq
bool is_seq(const atermpp::aterm &x)
Definition process_expression.h:1130
mcrl2::process::make_sync
void make_sync(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:969
mcrl2::process::swap
void swap(allow &t1, allow &t2) noexcept
\brief swap overload
Definition process_expression.h:921
mcrl2::process::is_merge
bool is_merge(const atermpp::aterm &x)
Definition process_expression.h:1439
mcrl2::process::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const process::action_label_list &x)
Definition process.cpp:72
mcrl2::process::make_if_then_else
void make_if_then_else(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1278
mcrl2::process::is_action_label
bool is_action_label(const atermpp::aterm &x)
Definition action_label.h:83
mcrl2::process::swap
void swap(process_identifier &t1, process_identifier &t2) noexcept
\brief swap overload
Definition process_identifier.h:107
mcrl2::process::make_hide
void make_hide(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:665
mcrl2::process::swap
void swap(hide &t1, hide &t2) noexcept
\brief swap overload
Definition process_expression.h:693
mcrl2::process::is_communication_expression
bool is_communication_expression(const atermpp::aterm &x)
Definition communication_expression.h:83
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const communication_expression &x)
Definition communication_expression.h:96
mcrl2::process::is_allow
bool is_allow(const atermpp::aterm &x)
Definition process_expression.h:902
mcrl2::process::pp
std::string pp(const process_expression &x, bool precedence_aware=true)
Definition process.cpp:51
mcrl2::process::pp
std::string pp(const merge &x, bool precedence_aware=true)
Definition process.cpp:49
mcrl2::process::pp
std::string pp(const rename &x, bool precedence_aware=true)
Definition process.cpp:56
mcrl2::process::swap
void swap(action_label &t1, action_label &t2) noexcept
\brief swap overload
Definition action_label.h:102
mcrl2::process::operator<
bool operator<(const action &a1, const action &a2)
Definition process_expression.h:1832
mcrl2::process::pp
std::string pp(const seq &x, bool precedence_aware=true)
Definition process.cpp:58
mcrl2::process::make_if_then
void make_if_then(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1197
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const choice &x)
Definition process_expression.h:1604
mcrl2::process::swap
void swap(seq &t1, seq &t2) noexcept
\brief swap overload
Definition process_expression.h:1149
mcrl2::process::pp
std::string pp(const sum &x, bool precedence_aware=true)
Definition process.cpp:60
mcrl2::process::is_bounded_init
bool is_bounded_init(const atermpp::aterm &x)
Definition process_expression.h:1363
mcrl2::process::is_delta
bool is_delta(const atermpp::aterm &x)
Definition process_expression.h:399
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const rename &x)
Definition process_expression.h:763
mcrl2::process::pp
std::string pp(const process_expression_list &x, bool precedence_aware=true)
Definition process.cpp:30
mcrl2::process::pp
std::string pp(const bounded_init &x, bool precedence_aware=true)
Definition process.cpp:40
mcrl2::process::swap
void swap(untyped_process_assignment &t1, untyped_process_assignment &t2) noexcept
\brief swap overload
Definition process_expression.h:1772
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const process_instance_assignment &x)
Definition process_expression.h:359
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const process_instance &x)
Definition process_expression.h:283
mcrl2::process::find_sort_expressions
std::set< data::sort_expression > find_sort_expressions(const process::process_expression &x)
Definition process.cpp:74
mcrl2::process::make_block
void make_block(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1781
mcrl2::process::translate_user_notation
process::process_expression translate_user_notation(const process::process_expression &x)
Definition process.cpp:70
mcrl2::process::is_sum
bool is_sum(const atermpp::aterm &x)
Definition process_expression.h:528
mcrl2::process::pp
std::string pp(const allow &x, bool precedence_aware=true)
Definition process.cpp:37
mcrl2::process::pp
std::string pp(const multi_action_name_set &A)
Pretty print function for a set of multi action names.
Definition multi_action_name.h:217
mcrl2::process::is_process_identifier
bool is_process_identifier(const atermpp::aterm &x)
Definition process_identifier.h:88
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const at &x)
Definition process_expression.h:1067
mcrl2::process::swap
void swap(block &t1, block &t2) noexcept
\brief swap overload
Definition process_expression.h:617
mcrl2::process::is_block
bool is_block(const atermpp::aterm &x)
Definition process_expression.h:598
mcrl2::process::is_if_then_else
bool is_if_then_else(const atermpp::aterm &x)
Definition process_expression.h:1287
mcrl2::process::make_action_label
void make_action_label(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_label.h:68
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const allow &x)
Definition process_expression.h:915
mcrl2::process::is_comm
bool is_comm(const atermpp::aterm &x)
Definition process_expression.h:826
mcrl2::process::normalize_sorts
action normalize_sorts(const action &x, const data::sort_specification &sortspec)
Definition process.cpp:65
mcrl2::process::alphabet_reduce
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
mcrl2::process::pp
std::string pp(const process_instance &x, bool precedence_aware=true)
Definition process.cpp:53
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const if_then_else &x)
Definition process_expression.h:1300
mcrl2::process::is_action
bool is_action(const atermpp::aterm &x)
Definition process_expression.h:194
mcrl2::process::pp
std::string pp(const left_merge &x, bool precedence_aware=true)
Definition process.cpp:48
mcrl2::process::swap
void swap(stochastic_operator &t1, stochastic_operator &t2) noexcept
\brief swap overload
Definition process_expression.h:1691
mcrl2::process::swap
void swap(if_then_else &t1, if_then_else &t2) noexcept
\brief swap overload
Definition process_expression.h:1306
mcrl2::process::is_left_merge
bool is_left_merge(const atermpp::aterm &x)
Definition process_expression.h:1515
mcrl2::process::pp
std::string pp(const sync &x, bool precedence_aware=true)
Definition process.cpp:61
mcrl2::process::pp
std::string pp(const action &x, bool precedence_aware=true)
Definition process.cpp:34
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const tau &x)
Definition process_expression.h:465
mcrl2::process::swap
void swap(process_instance &t1, process_instance &t2) noexcept
\brief swap overload
Definition process_expression.h:289
mcrl2::process::make_communication_expression
void make_communication_expression(atermpp::aterm &t, const ARGUMENTS &... args)
Definition communication_expression.h:68
mcrl2::process::pp
std::string pp(const at &x, bool precedence_aware=true)
Definition process.cpp:38
mcrl2::process::make_stochastic_operator
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1663
mcrl2::process::is_action_name_multiset
bool is_action_name_multiset(const atermpp::aterm &x)
Definition action_name_multiset.h:70
mcrl2::process::swap
void swap(communication_expression &t1, communication_expression &t2) noexcept
\brief swap overload
Definition communication_expression.h:102
mcrl2::process::pp
std::string pp(const comm &x, bool precedence_aware=true)
Definition process.cpp:42
mcrl2::process::swap
void swap(process_expression &t1, process_expression &t2) noexcept
\brief swap overload
Definition process_expression.h:131
mcrl2::process::make_process_instance
void make_process_instance(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:261
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const hide &x)
Definition process_expression.h:687
mcrl2::process::is_hide
bool is_hide(const atermpp::aterm &x)
Definition process_expression.h:674
mcrl2::process::pp
std::string pp(const untyped_process_assignment &x, bool precedence_aware=true)
Definition process.cpp:64
mcrl2::process::swap
void swap(tau &t1, tau &t2) noexcept
\brief swap overload
Definition process_expression.h:471
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const delta &x)
Definition process_expression.h:412
mcrl2::process::is_if_then
bool is_if_then(const atermpp::aterm &x)
Definition process_expression.h:1206
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const comm &x)
Definition process_expression.h:839
mcrl2::process::make_untyped_process_assignment
void make_untyped_process_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1744
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const action_name_multiset &x)
Definition action_name_multiset.h:83
mcrl2::process::make_process_instance_assignment
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:337
mcrl2::process::is_choice
bool is_choice(const atermpp::aterm &x)
Definition process_expression.h:1591
mcrl2::process::translate_user_notation
action translate_user_notation(const action &x)
Definition process.cpp:69
mcrl2::process::find_free_variables
std::set< data::variable > find_free_variables(const action &x)
Definition process.cpp:77
mcrl2::process::pp
std::string pp(const process_instance_assignment &x, bool precedence_aware=true)
Definition process.cpp:54
mcrl2::process::pp
std::string pp(const process_expression_vector &x, bool precedence_aware=true)
Definition process.cpp:31
mcrl2::process::make_comm
void make_comm(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:817
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const seq &x)
Definition process_expression.h:1143
mcrl2::process::is_stochastic_operator
bool is_stochastic_operator(const atermpp::aterm &x)
Definition process_expression.h:1672
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const rename_expression &x)
Definition rename_expression.h:97
mcrl2::process::pp
std::string pp(const block &x, bool precedence_aware=true)
Definition process.cpp:39
mcrl2::process::swap
void swap(sum &t1, sum &t2) noexcept
\brief swap overload
Definition process_expression.h:547
mcrl2::process::make_bounded_init
void make_bounded_init(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1354
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const process_expression &x)
Definition process_expression.h:125
mcrl2::process::swap
void swap(process_instance_assignment &t1, process_instance_assignment &t2) noexcept
\brief swap overload
Definition process_expression.h:365
mcrl2::process::is_rename_expression
bool is_rename_expression(const atermpp::aterm &x)
Definition rename_expression.h:84
mcrl2::process::swap
void swap(comm &t1, comm &t2) noexcept
\brief swap overload
Definition process_expression.h:845
mcrl2::process::make_rename_expression
void make_rename_expression(atermpp::aterm &t, const ARGUMENTS &... args)
Definition rename_expression.h:69
mcrl2::process::make_action_name_multiset
void make_action_name_multiset(atermpp::aterm &t, const ARGUMENTS &... args)
Definition action_name_multiset.h:98
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const action_label &x)
Definition action_label.h:96
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const block &x)
Definition process_expression.h:611
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const action &x)
Definition process_expression.h:207
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const merge &x)
Definition process_expression.h:1452
mcrl2::process::swap
void swap(choice &t1, choice &t2) noexcept
\brief swap overload
Definition process_expression.h:1610
mcrl2::process::pp
std::string pp(const choice &x, bool precedence_aware=true)
Definition process.cpp:41
mcrl2::process::is_rename
bool is_rename(const atermpp::aterm &x)
Definition process_expression.h:750
mcrl2::process::is_untyped_process_assignment
bool is_untyped_process_assignment(const atermpp::aterm &x)
Definition process_expression.h:1753
mcrl2::process::make_rename
void make_rename(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:741
mcrl2::process::make_seq
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1121
mcrl2::process::is_sync
bool is_sync(const atermpp::aterm &x)
Definition process_expression.h:978
mcrl2::process::pp
std::string pp(const delta &x, bool precedence_aware=true)
Definition process.cpp:44
mcrl2::process::make_sum
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:519
mcrl2::process::pp
std::string pp(const hide &x, bool precedence_aware=true)
Definition process.cpp:45
mcrl2::process::pp
std::string pp(const if_then_else &x, bool precedence_aware=true)
Definition process.cpp:47
mcrl2::process::swap
void swap(action_name_multiset &t1, action_name_multiset &t2) noexcept
\brief swap overload
Definition action_name_multiset.h:89
mcrl2::process::equal_signatures
bool equal_signatures(const action &a, const action &b)
Compares the signatures of two actions.
Definition process_expression.h:1807
mcrl2::process::swap
void swap(sync &t1, sync &t2) noexcept
\brief swap overload
Definition process_expression.h:997
mcrl2::process::operator<<
std::ostream & operator<<(std::ostream &out, const if_then &x)
Definition process_expression.h:1219
mcrl2::process::pp
std::string pp(const process::action_label_list &x, bool arg0)
Definition process.cpp:26
mcrl2::process::make_left_merge
void make_left_merge(atermpp::aterm &t, const ARGUMENTS &... args)
Definition process_expression.h:1506
std::swap
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
Definition aterm.h:364
mcrl2::core::builder
expression builder that visits all sub expressions
Definition builder.h:32
mcrl2::core::detail::default_values
Definition default_values.h:1600
mcrl2::core::detail::default_values::Delta
static const atermpp::aterm Delta
Definition default_values.h:1644
mcrl2::core::detail::default_values::UntypedProcessAssignment
static const atermpp::aterm UntypedProcessAssignment
Definition default_values.h:1662
mcrl2::core::detail::default_values::Distribution
static const atermpp::aterm Distribution
Definition default_values.h:1673
mcrl2::core::detail::default_values::Allow
static const atermpp::aterm Allow
Definition default_values.h:1651
mcrl2::core::detail::default_values::RenameExpr
static const atermpp::aterm RenameExpr
Definition default_values.h:1665
mcrl2::core::detail::default_values::Tau
static const atermpp::aterm Tau
Definition default_values.h:1645
mcrl2::core::detail::default_values::ActId
static const atermpp::aterm ActId
Definition default_values.h:1641
mcrl2::core::detail::default_values::Hide
static const atermpp::aterm Hide
Definition default_values.h:1648
mcrl2::core::detail::default_values::LinearProcessInit
static const atermpp::aterm LinearProcessInit
Definition default_values.h:1677
mcrl2::core::detail::default_values::Rename
static const atermpp::aterm Rename
Definition default_values.h:1649
mcrl2::core::detail::default_values::Process
static const atermpp::aterm Process
Definition default_values.h:1642
mcrl2::core::detail::default_values::IfThen
static const atermpp::aterm IfThen
Definition default_values.h:1655
mcrl2::core::detail::default_values::StochasticOperator
static const atermpp::aterm StochasticOperator
Definition default_values.h:1661
mcrl2::core::detail::default_values::BInit
static const atermpp::aterm BInit
Definition default_values.h:1657
mcrl2::core::detail::default_values::Merge
static const atermpp::aterm Merge
Definition default_values.h:1658
mcrl2::core::detail::default_values::Action
static const atermpp::aterm Action
Definition default_values.h:1640
mcrl2::core::detail::default_values::MultActName
static const atermpp::aterm MultActName
Definition default_values.h:1664
mcrl2::core::detail::default_values::AtTime
static const atermpp::aterm AtTime
Definition default_values.h:1653
mcrl2::core::detail::default_values::Choice
static const atermpp::aterm Choice
Definition default_values.h:1660
mcrl2::core::detail::default_values::Comm
static const atermpp::aterm Comm
Definition default_values.h:1650
mcrl2::core::detail::default_values::ProcessAssignment
static const atermpp::aterm ProcessAssignment
Definition default_values.h:1643
mcrl2::core::detail::default_values::Sync
static const atermpp::aterm Sync
Definition default_values.h:1652
mcrl2::core::detail::default_values::LMerge
static const atermpp::aterm LMerge
Definition default_values.h:1659
mcrl2::core::detail::default_values::ProcVarId
static const atermpp::aterm ProcVarId
Definition default_values.h:1663
mcrl2::core::detail::default_values::ProcExpr
static const atermpp::aterm ProcExpr
Definition default_values.h:1763
mcrl2::core::detail::default_values::Seq
static const atermpp::aterm Seq
Definition default_values.h:1654
mcrl2::core::detail::default_values::Sum
static const atermpp::aterm Sum
Definition default_values.h:1646
mcrl2::core::detail::default_values::Block
static const atermpp::aterm Block
Definition default_values.h:1647
mcrl2::core::detail::default_values::CommExpr
static const atermpp::aterm CommExpr
Definition default_values.h:1666
mcrl2::core::detail::default_values::IfThenElse
static const atermpp::aterm IfThenElse
Definition default_values.h:1656
mcrl2::data::assignment_sequence_substitution
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
Definition assignment_sequence_substitution.h:23
mcrl2::data::assignment_sequence_substitution::assignments
const assignment_list & assignments
Definition assignment_sequence_substitution.h:30
mcrl2::data::assignment_sequence_substitution::is_identity_substitution
static constexpr bool is_identity_substitution
Definition assignment_sequence_substitution.h:24
mcrl2::data::assignment_sequence_substitution::assignment_sequence_substitution
assignment_sequence_substitution(const assignment_list &assignments_)
Definition assignment_sequence_substitution.h:32
mcrl2::data::assignment_sequence_substitution::operator()
const data_expression & operator()(const variable &v) const
Definition assignment_sequence_substitution.h:36
mcrl2::data::detail::capture_avoiding_substitution_updater
Definition replace_capture_avoiding.h:32
mcrl2::data::fourier_motzkin_sigma
A unary function that can be used in combination with replace_data_expressions to eliminate real numb...
Definition fourier_motzkin.h:315
mcrl2::data::fourier_motzkin_sigma::fourier_motzkin_sigma
fourier_motzkin_sigma(const rewriter &rewr_)
Definition fourier_motzkin.h:343
mcrl2::data::fourier_motzkin_sigma::apply
data_expression apply(const abstraction &d, bool negate) const
Definition fourier_motzkin.h:320
mcrl2::data::fourier_motzkin_sigma::operator()
data_expression operator()(const data_expression &d) const
Definition fourier_motzkin.h:347
mcrl2::data::fourier_motzkin_sigma::rewr
rewriter rewr
Definition fourier_motzkin.h:318
mcrl2::data::fourier_motzkin_sigma::is_identity_substitution
static constexpr bool is_identity_substitution
Definition fourier_motzkin.h:341
mcrl2::data::map_substitution
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
Definition map_substitution.h:25
mcrl2::data::map_substitution::to_string
std::string to_string() const
Definition map_substitution.h:52
mcrl2::data::map_substitution::m_map
const AssociativeContainer & m_map
Definition map_substitution.h:31
mcrl2::data::map_substitution::map_substitution
map_substitution(const AssociativeContainer &m)
Definition map_substitution.h:33
mcrl2::data::map_substitution::is_identity_substitution
static constexpr bool is_identity_substitution
Definition map_substitution.h:50
mcrl2::data::map_substitution::operator()
expression_type operator()(const variable_type &v) const
Definition map_substitution.h:37
mcrl2::lps::add_data_expressions
Definition builder.h:188
mcrl2::lps::add_data_expressions::update
void update(lps::action_summand &x)
Definition builder.h:222
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:308
mcrl2::lps::add_data_expressions::update
void update(lps::linear_process &x)
Definition builder.h:245
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:205
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:264
mcrl2::lps::add_data_expressions::update
void update(lps::specification &x)
Definition builder.h:253
mcrl2::lps::add_data_expressions::update
void update(lps::deadlock &x)
Definition builder.h:195
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:289
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:238
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:271
mcrl2::lps::add_data_expressions::update
void update(lps::deadlock_summand &x)
Definition builder.h:212
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_specification &x)
Definition builder.h:297
mcrl2::lps::add_sort_expressions
Definition builder.h:25
mcrl2::lps::add_sort_expressions::update
void update(lps::deadlock &x)
Definition builder.h:32
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_specification &x)
Definition builder.h:153
mcrl2::lps::add_sort_expressions::update
void update(lps::specification &x)
Definition builder.h:99
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:81
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:168
mcrl2::lps::add_sort_expressions::update
void update(lps::action_summand &x)
Definition builder.h:62
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:114
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:142
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:121
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:42
mcrl2::lps::add_sort_expressions::update
void update(lps::linear_process &x)
Definition builder.h:88
mcrl2::lps::add_sort_expressions::update
void update(lps::deadlock_summand &x)
Definition builder.h:49
mcrl2::lps::add_variables
Definition builder.h:327
mcrl2::lps::add_variables::update
void update(lps::action_summand &x)
Definition builder.h:364
mcrl2::lps::add_variables::update
void update(lps::deadlock &x)
Definition builder.h:334
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:344
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:464
mcrl2::lps::add_variables::update
void update(lps::specification &x)
Definition builder.h:401
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:413
mcrl2::lps::add_variables::update
void update(lps::linear_process &x)
Definition builder.h:390
mcrl2::lps::add_variables::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:420
mcrl2::lps::add_variables::update
void update(lps::stochastic_specification &x)
Definition builder.h:452
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:383
mcrl2::lps::add_variables::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:441
mcrl2::lps::add_variables::update
void update(lps::deadlock_summand &x)
Definition builder.h:351
mcrl2::lps::data_expression_builder
\brief Builder class
Definition builder.h:320
mcrl2::lps::detail::add_capture_avoiding_replacement
Definition replace_capture_avoiding.h:26
mcrl2::lps::detail::add_capture_avoiding_replacement::do_linear_process
void do_linear_process(LinearProcess &x)
Definition replace_capture_avoiding.h:90
mcrl2::lps::detail::add_capture_avoiding_replacement::operator()
void operator()(specification &x)
Definition replace_capture_avoiding.h:131
mcrl2::lps::detail::add_capture_avoiding_replacement::apply
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...
Definition replace_capture_avoiding.h:165
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(action_summand &x)
Definition replace_capture_avoiding.h:55
mcrl2::lps::detail::add_capture_avoiding_replacement::apply
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...
Definition replace_capture_avoiding.h:150
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(linear_process &x)
Definition replace_capture_avoiding.h:100
mcrl2::lps::detail::add_capture_avoiding_replacement::do_specification
void do_specification(Specification &x)
Definition replace_capture_avoiding.h:111
mcrl2::lps::detail::add_capture_avoiding_replacement::apply
void apply(T &, const stochastic_distribution &)
Definition replace_capture_avoiding.h:142
mcrl2::lps::detail::add_capture_avoiding_replacement::do_action_summand
void do_action_summand(ActionSummand &x, const data::variable_list &v)
Definition replace_capture_avoiding.h:39
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(stochastic_linear_process &x)
Definition replace_capture_avoiding.h:105
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(deadlock_summand &x)
Definition replace_capture_avoiding.h:75
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(stochastic_action_summand &x)
Definition replace_capture_avoiding.h:63
mcrl2::lps::detail::add_capture_avoiding_replacement::add_capture_avoiding_replacement
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
Definition replace_capture_avoiding.h:34
mcrl2::lps::detail::add_capture_avoiding_replacement::operator()
void operator()(stochastic_specification &x)
Definition replace_capture_avoiding.h:136
mcrl2::lps::detail::is_singleton_sort
Function object that checks if a sort is a singleton sort. Note that it is an approximation,...
Definition remove.h:36
mcrl2::lps::detail::is_singleton_sort::is_singleton_sort
is_singleton_sort(const data::data_specification &data_spec)
Definition remove.h:39
mcrl2::lps::detail::is_singleton_sort::operator()
bool operator()(const data::sort_expression &s) const
Definition remove.h:43
mcrl2::lps::detail::is_singleton_sort::m_data_spec
const data::data_specification & m_data_spec
Definition remove.h:37
mcrl2::lps::detail::is_trivial_summand
Function object that checks if a summand has a false condition.
Definition remove.h:25
mcrl2::lps::detail::is_trivial_summand::operator()
bool operator()(const summand_base &s) const
Definition remove.h:26
mcrl2::lps::detail::remove_parameters_builder
Traverser for removing parameters from LPS data types. These parameters can be either process paramet...
Definition remove.h:58
mcrl2::lps::detail::remove_parameters_builder::apply
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
mcrl2::lps::detail::remove_parameters_builder::apply
void apply(T &result, const stochastic_process_initializer &x)
Definition remove.h:156
mcrl2::lps::detail::remove_parameters_builder::apply
void apply(T &result, const process_initializer &x)
Definition remove.h:149
mcrl2::lps::detail::remove_parameters_builder::update
void update(std::set< data::variable > &x)
Removes parameters from a set container.
Definition remove.h:73
mcrl2::lps::detail::remove_parameters_builder::to_be_removed
const std::set< data::variable > & to_be_removed
Definition remove.h:65
mcrl2::lps::detail::remove_parameters_builder::apply
void apply(atermpp::term_list< T > &result, const data::variable_list &x)
Removes parameters from a list of variables.
Definition remove.h:83
mcrl2::lps::detail::remove_parameters_builder::update
void update(linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:111
mcrl2::lps::detail::remove_parameters_builder::remove_expressions
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
mcrl2::lps::detail::remove_parameters_builder::process_parameters
data::variable_list process_parameters
Definition remove.h:66
mcrl2::lps::detail::remove_parameters_builder::update
void update(stochastic_specification &x)
Removes parameters from a linear process specification.
Definition remove.h:175
mcrl2::lps::detail::remove_parameters_builder::update
void update(specification &x)
Removes parameters from a linear process specification.
Definition remove.h:166
mcrl2::lps::detail::remove_parameters_builder::remove_parameters_builder
remove_parameters_builder(const std::set< data::variable > &to_be_removed_)
Definition remove.h:68
mcrl2::lps::detail::remove_parameters_builder::update
void update(stochastic_linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:121
mcrl2::lps::sort_expression_builder
\brief Builder class
Definition builder.h:180
mcrl2::lps::t_lin_options
Options for linearisation.
Definition linearise.h:25
mcrl2::lps::t_lin_options::apply_alphabet_axioms
bool apply_alphabet_axioms
Definition linearise.h:38
mcrl2::lps::t_lin_options::balance_summands
bool balance_summands
Definition linearise.h:39
mcrl2::lps::variable_builder
\brief Builder class
Definition builder.h:476
mcrl2::process::action_name_compare
Definition action_label.h:118
mcrl2::process::action_name_compare::operator()
bool operator()(const core::identifier_string &s1, const core::identifier_string &s2) const
Definition action_label.h:119
mcrl2::process::add_data_expressions
Definition builder.h:387
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::process_equation &x)
Definition builder.h:405
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::rename &x)
Definition builder.h:487
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::left_merge &x)
Definition builder.h:567
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::bounded_init &x)
Definition builder.h:551
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::process_expression &x)
Definition builder.h:599
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::block &x)
Definition builder.h:471
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::merge &x)
Definition builder.h:559
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::sync &x)
Definition builder.h:511
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::choice &x)
Definition builder.h:575
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::if_then &x)
Definition builder.h:535
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::action &x)
Definition builder.h:421
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::delta &x)
Definition builder.h:445
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:437
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:591
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:583
mcrl2::process::add_data_expressions::update
void update(process::process_specification &x)
Definition builder.h:394
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::allow &x)
Definition builder.h:503
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::at &x)
Definition builder.h:519
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::sum &x)
Definition builder.h:463
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::seq &x)
Definition builder.h:527
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::tau &x)
Definition builder.h:454
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::comm &x)
Definition builder.h:495
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:413
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::hide &x)
Definition builder.h:479
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::if_then_else &x)
Definition builder.h:543
mcrl2::process::add_data_expressions::apply
void apply(T &result, const process::process_instance &x)
Definition builder.h:429
mcrl2::process::add_process_expressions
Definition builder.h:1041
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::sync &x)
Definition builder.h:1160
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::rename &x)
Definition builder.h:1136
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::if_then_else &x)
Definition builder.h:1192
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::process_equation &x)
Definition builder.h:1059
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::bounded_init &x)
Definition builder.h:1200
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::at &x)
Definition builder.h:1168
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::if_then &x)
Definition builder.h:1184
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::choice &x)
Definition builder.h:1224
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::tau &x)
Definition builder.h:1103
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::merge &x)
Definition builder.h:1208
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::left_merge &x)
Definition builder.h:1216
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::sum &x)
Definition builder.h:1112
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::seq &x)
Definition builder.h:1176
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:1240
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::block &x)
Definition builder.h:1120
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::allow &x)
Definition builder.h:1152
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::action &x)
Definition builder.h:1067
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::hide &x)
Definition builder.h:1128
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::process_expression &x)
Definition builder.h:1249
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:1085
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::comm &x)
Definition builder.h:1144
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::delta &x)
Definition builder.h:1094
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::process_instance &x)
Definition builder.h:1076
mcrl2::process::add_process_expressions::update
void update(process::process_specification &x)
Definition builder.h:1048
mcrl2::process::add_process_expressions::apply
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:1232
mcrl2::process::add_process_identifiers
Definition builder.h:1359
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::process_expression &x)
Definition builder.h:1574
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::process_identifier &x)
Definition builder.h:1377
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::process_instance &x)
Definition builder.h:1403
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::delta &x)
Definition builder.h:1419
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:1411
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:1557
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::choice &x)
Definition builder.h:1549
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::at &x)
Definition builder.h:1493
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::merge &x)
Definition builder.h:1533
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::if_then &x)
Definition builder.h:1509
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::comm &x)
Definition builder.h:1469
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::process_equation &x)
Definition builder.h:1386
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::left_merge &x)
Definition builder.h:1541
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::sync &x)
Definition builder.h:1485
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::tau &x)
Definition builder.h:1428
mcrl2::process::add_process_identifiers::update
void update(process::process_specification &x)
Definition builder.h:1366
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::hide &x)
Definition builder.h:1453
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::if_then_else &x)
Definition builder.h:1517
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:1565
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::rename &x)
Definition builder.h:1461
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::seq &x)
Definition builder.h:1501
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::block &x)
Definition builder.h:1445
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::sum &x)
Definition builder.h:1437
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::bounded_init &x)
Definition builder.h:1525
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::action &x)
Definition builder.h:1394
mcrl2::process::add_process_identifiers::apply
void apply(T &result, const process::allow &x)
Definition builder.h:1477
mcrl2::process::add_sort_expressions
Definition builder.h:44
mcrl2::process::add_sort_expressions::update
void update(process::process_specification &x)
Definition builder.h:59
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::sync &x)
Definition builder.h:188
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::choice &x)
Definition builder.h:252
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:114
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::process_instance &x)
Definition builder.h:106
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::merge &x)
Definition builder.h:236
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::seq &x)
Definition builder.h:204
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::if_then &x)
Definition builder.h:212
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:90
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:260
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::action &x)
Definition builder.h:98
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::delta &x)
Definition builder.h:122
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::if_then_else &x)
Definition builder.h:220
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::left_merge &x)
Definition builder.h:244
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::process_equation &x)
Definition builder.h:82
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::hide &x)
Definition builder.h:156
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::allow &x)
Definition builder.h:180
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::rename &x)
Definition builder.h:164
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::comm &x)
Definition builder.h:172
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::sum &x)
Definition builder.h:140
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::bounded_init &x)
Definition builder.h:228
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::action_label &x)
Definition builder.h:52
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::block &x)
Definition builder.h:148
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::at &x)
Definition builder.h:196
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::tau &x)
Definition builder.h:131
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::process_identifier &x)
Definition builder.h:74
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::process_expression &x)
Definition builder.h:276
mcrl2::process::add_sort_expressions::apply
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:268
mcrl2::process::add_variables
Definition builder.h:709
mcrl2::process::add_variables::apply
void apply(T &result, const process::process_instance &x)
Definition builder.h:760
mcrl2::process::add_variables::apply
void apply(T &result, const process::choice &x)
Definition builder.h:906
mcrl2::process::add_variables::apply
void apply(T &result, const process::sync &x)
Definition builder.h:842
mcrl2::process::add_variables::apply
void apply(T &result, const process::sum &x)
Definition builder.h:794
mcrl2::process::add_variables::apply
void apply(T &result, const process::stochastic_operator &x)
Definition builder.h:914
mcrl2::process::add_variables::apply
void apply(T &result, const process::untyped_process_assignment &x)
Definition builder.h:922
mcrl2::process::add_variables::apply
void apply(T &result, const process::allow &x)
Definition builder.h:834
mcrl2::process::add_variables::apply
void apply(T &result, const process::bounded_init &x)
Definition builder.h:882
mcrl2::process::add_variables::apply
void apply(T &result, const process::comm &x)
Definition builder.h:826
mcrl2::process::add_variables::apply
void apply(T &result, const process::block &x)
Definition builder.h:802
mcrl2::process::add_variables::apply
void apply(T &result, const process::tau &x)
Definition builder.h:785
mcrl2::process::add_variables::apply
void apply(T &result, const process::action &x)
Definition builder.h:752
mcrl2::process::add_variables::apply
void apply(T &result, const process::left_merge &x)
Definition builder.h:898
mcrl2::process::add_variables::apply
void apply(T &result, const process::untyped_multi_action &x)
Definition builder.h:744
mcrl2::process::add_variables::apply
void apply(T &result, const process::merge &x)
Definition builder.h:890
mcrl2::process::add_variables::apply
void apply(T &result, const process::seq &x)
Definition builder.h:858
mcrl2::process::add_variables::apply
void apply(T &result, const process::delta &x)
Definition builder.h:776
mcrl2::process::add_variables::apply
void apply(T &result, const process::hide &x)
Definition builder.h:810
mcrl2::process::add_variables::apply
void apply(T &result, const process::at &x)
Definition builder.h:850
mcrl2::process::add_variables::apply
void apply(T &result, const process::process_identifier &x)
Definition builder.h:728
mcrl2::process::add_variables::apply
void apply(T &result, const process::if_then_else &x)
Definition builder.h:874
mcrl2::process::add_variables::update
void update(process::process_specification &x)
Definition builder.h:716
mcrl2::process::add_variables::apply
void apply(T &result, const process::process_equation &x)
Definition builder.h:736
mcrl2::process::add_variables::apply
void apply(T &result, const process::process_instance_assignment &x)
Definition builder.h:768
mcrl2::process::add_variables::apply
void apply(T &result, const process::rename &x)
Definition builder.h:818
mcrl2::process::add_variables::apply
void apply(T &result, const process::if_then &x)
Definition builder.h:866
mcrl2::process::add_variables::apply
void apply(T &result, const process::process_expression &x)
Definition builder.h:930
mcrl2::process::data_expression_builder
\brief Builder class
Definition builder.h:702
mcrl2::process::process_builder_base
Base builder class for processes.
Definition builder.h:25
mcrl2::process::process_builder_base::apply
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:30
mcrl2::process::process_expression_builder
\brief Builder class
Definition builder.h:1352
mcrl2::process::process_identifier_builder
\brief Builder class
Definition builder.h:1677
mcrl2::process::sort_expression_builder
\brief Builder class
Definition builder.h:379
mcrl2::process::variable_builder
\brief Builder class
Definition builder.h:1033
specification_basic_type::make_substitution
Definition linearise.cpp:3780
specification_basic_type::make_substitution::make_substitution
make_substitution(const std::map< process_identifier, process_identifier > &map)
Definition linearise.cpp:3785
specification_basic_type::make_substitution::operator()
process_identifier operator()(const process_identifier &id) const
Definition linearise.cpp:3789
specification_basic_type::make_substitution::m_map
const std::map< process_identifier, process_identifier > & m_map
Definition linearise.cpp:3783
std::hash< mcrl2::lps::multi_action >::operator()
std::size_t operator()(const mcrl2::lps::multi_action &ma) const
Definition multi_action.h:368
std::hash< mcrl2::process::action >::operator()
std::size_t operator()(const mcrl2::process::action &t) const
Definition process_expression.h:1848