mCRL2
Loading...
Searching...
No Matches
traverser.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12// To avoid circular inclusion problems
13
14#ifndef MCRL2_LPS_TRAVERSER_H
15#define MCRL2_LPS_TRAVERSER_H
16
17#include "mcrl2/lps/stochastic_specification.h"
18#include "mcrl2/process/traverser.h"
19
20namespace mcrl2
21{
22
23namespace lps
24{
25
26//--- start generated add_traverser_sort_expressions code ---//
27template <template <class> class Traverser, class Derived>
28struct add_traverser_sort_expressions: public Traverser<Derived>
29{
30 typedef Traverser<Derived> super;
31 using super::enter;
32 using super::leave;
33 using super::apply;
34
35 void apply(const lps::deadlock& x)
36 {
37 static_cast<Derived&>(*this).enter(x);
38 if (x.has_time())
39 {
40 static_cast<Derived&>(*this).apply(x.time());
41 }
42 static_cast<Derived&>(*this).leave(x);
43 }
44
45 void apply(const lps::multi_action& x)
46 {
47 static_cast<Derived&>(*this).enter(x);
48 static_cast<Derived&>(*this).apply(x.actions());
49 if (x.has_time())
50 {
51 static_cast<Derived&>(*this).apply(x.time());
52 }
53 static_cast<Derived&>(*this).leave(x);
54 }
55
56 void apply(const lps::deadlock_summand& x)
57 {
58 static_cast<Derived&>(*this).enter(x);
59 static_cast<Derived&>(*this).apply(x.summation_variables());
60 static_cast<Derived&>(*this).apply(x.condition());
61 static_cast<Derived&>(*this).apply(x.deadlock());
62 static_cast<Derived&>(*this).leave(x);
63 }
64
65 void apply(const lps::action_summand& x)
66 {
67 static_cast<Derived&>(*this).enter(x);
68 static_cast<Derived&>(*this).apply(x.summation_variables());
69 static_cast<Derived&>(*this).apply(x.condition());
70 static_cast<Derived&>(*this).apply(x.multi_action());
71 static_cast<Derived&>(*this).apply(x.assignments());
72 static_cast<Derived&>(*this).leave(x);
73 }
74
75 void apply(const lps::process_initializer& x)
76 {
77 static_cast<Derived&>(*this).enter(x);
78 static_cast<Derived&>(*this).apply(x.expressions());
79 static_cast<Derived&>(*this).leave(x);
80 }
81
82 void apply(const lps::linear_process& x)
83 {
84 static_cast<Derived&>(*this).enter(x);
85 static_cast<Derived&>(*this).apply(x.process_parameters());
86 static_cast<Derived&>(*this).apply(x.deadlock_summands());
87 static_cast<Derived&>(*this).apply(x.action_summands());
88 static_cast<Derived&>(*this).leave(x);
89 }
90
91 void apply(const lps::specification& x)
92 {
93 static_cast<Derived&>(*this).enter(x);
94 static_cast<Derived&>(*this).apply(x.action_labels());
95 static_cast<Derived&>(*this).apply(x.global_variables());
96 static_cast<Derived&>(*this).apply(x.process());
97 static_cast<Derived&>(*this).apply(x.initial_process());
98 static_cast<Derived&>(*this).leave(x);
99 }
100
101 void apply(const lps::stochastic_distribution& x)
102 {
103 static_cast<Derived&>(*this).enter(x);
104 static_cast<Derived&>(*this).apply(x.variables());
105 if (x.is_defined()) { static_cast<Derived&>(*this).apply(x.distribution()); }
106 static_cast<Derived&>(*this).leave(x);
107 }
108
109 void apply(const lps::stochastic_action_summand& x)
110 {
111 static_cast<Derived&>(*this).enter(x);
112 static_cast<Derived&>(*this).apply(x.summation_variables());
113 static_cast<Derived&>(*this).apply(x.condition());
114 static_cast<Derived&>(*this).apply(x.multi_action());
115 static_cast<Derived&>(*this).apply(x.assignments());
116 static_cast<Derived&>(*this).apply(x.distribution());
117 static_cast<Derived&>(*this).leave(x);
118 }
119
120 void apply(const lps::stochastic_linear_process& x)
121 {
122 static_cast<Derived&>(*this).enter(x);
123 static_cast<Derived&>(*this).apply(x.process_parameters());
124 static_cast<Derived&>(*this).apply(x.deadlock_summands());
125 static_cast<Derived&>(*this).apply(x.action_summands());
126 static_cast<Derived&>(*this).leave(x);
127 }
128
129 void apply(const lps::stochastic_specification& x)
130 {
131 static_cast<Derived&>(*this).enter(x);
132 static_cast<Derived&>(*this).apply(x.action_labels());
133 static_cast<Derived&>(*this).apply(x.global_variables());
134 static_cast<Derived&>(*this).apply(x.process());
135 static_cast<Derived&>(*this).apply(x.initial_process());
136 static_cast<Derived&>(*this).leave(x);
137 }
138
139 void apply(const lps::stochastic_process_initializer& x)
140 {
141 static_cast<Derived&>(*this).enter(x);
142 static_cast<Derived&>(*this).apply(x.expressions());
143 static_cast<Derived&>(*this).apply(x.distribution());
144 static_cast<Derived&>(*this).leave(x);
145 }
146
147};
148
150template <typename Derived>
151struct sort_expression_traverser: public add_traverser_sort_expressions<process::sort_expression_traverser, Derived>
152{
153};
154//--- end generated add_traverser_sort_expressions code ---//
155
156//--- start generated add_traverser_data_expressions code ---//
157template <template <class> class Traverser, class Derived>
158struct add_traverser_data_expressions: public Traverser<Derived>
159{
160 typedef Traverser<Derived> super;
161 using super::enter;
162 using super::leave;
163 using super::apply;
164
165 void apply(const lps::deadlock& x)
166 {
167 static_cast<Derived&>(*this).enter(x);
168 if (x.has_time())
169 {
170 static_cast<Derived&>(*this).apply(x.time());
171 }
172 static_cast<Derived&>(*this).leave(x);
173 }
174
175 void apply(const lps::multi_action& x)
176 {
177 static_cast<Derived&>(*this).enter(x);
178 static_cast<Derived&>(*this).apply(x.actions());
179 if (x.has_time())
180 {
181 static_cast<Derived&>(*this).apply(x.time());
182 }
183 static_cast<Derived&>(*this).leave(x);
184 }
185
186 void apply(const lps::deadlock_summand& x)
187 {
188 static_cast<Derived&>(*this).enter(x);
189 static_cast<Derived&>(*this).apply(x.condition());
190 static_cast<Derived&>(*this).apply(x.deadlock());
191 static_cast<Derived&>(*this).leave(x);
192 }
193
194 void apply(const lps::action_summand& x)
195 {
196 static_cast<Derived&>(*this).enter(x);
197 static_cast<Derived&>(*this).apply(x.condition());
198 static_cast<Derived&>(*this).apply(x.multi_action());
199 static_cast<Derived&>(*this).apply(x.assignments());
200 static_cast<Derived&>(*this).leave(x);
201 }
202
203 void apply(const lps::process_initializer& x)
204 {
205 static_cast<Derived&>(*this).enter(x);
206 static_cast<Derived&>(*this).apply(x.expressions());
207 static_cast<Derived&>(*this).leave(x);
208 }
209
210 void apply(const lps::linear_process& x)
211 {
212 static_cast<Derived&>(*this).enter(x);
213 static_cast<Derived&>(*this).apply(x.deadlock_summands());
214 static_cast<Derived&>(*this).apply(x.action_summands());
215 static_cast<Derived&>(*this).leave(x);
216 }
217
218 void apply(const lps::specification& x)
219 {
220 static_cast<Derived&>(*this).enter(x);
221 static_cast<Derived&>(*this).apply(x.process());
222 static_cast<Derived&>(*this).apply(x.initial_process());
223 static_cast<Derived&>(*this).leave(x);
224 }
225
226 void apply(const lps::stochastic_distribution& x)
227 {
228 static_cast<Derived&>(*this).enter(x);
229 if (x.is_defined()) { static_cast<Derived&>(*this).apply(x.distribution()); }
230 static_cast<Derived&>(*this).leave(x);
231 }
232
233 void apply(const lps::stochastic_action_summand& x)
234 {
235 static_cast<Derived&>(*this).enter(x);
236 static_cast<Derived&>(*this).apply(x.condition());
237 static_cast<Derived&>(*this).apply(x.multi_action());
238 static_cast<Derived&>(*this).apply(x.assignments());
239 static_cast<Derived&>(*this).apply(x.distribution());
240 static_cast<Derived&>(*this).leave(x);
241 }
242
243 void apply(const lps::stochastic_linear_process& x)
244 {
245 static_cast<Derived&>(*this).enter(x);
246 static_cast<Derived&>(*this).apply(x.deadlock_summands());
247 static_cast<Derived&>(*this).apply(x.action_summands());
248 static_cast<Derived&>(*this).leave(x);
249 }
250
251 void apply(const lps::stochastic_specification& x)
252 {
253 static_cast<Derived&>(*this).enter(x);
254 static_cast<Derived&>(*this).apply(x.process());
255 static_cast<Derived&>(*this).apply(x.initial_process());
256 static_cast<Derived&>(*this).leave(x);
257 }
258
259 void apply(const lps::stochastic_process_initializer& x)
260 {
261 static_cast<Derived&>(*this).enter(x);
262 static_cast<Derived&>(*this).apply(x.expressions());
263 static_cast<Derived&>(*this).apply(x.distribution());
264 static_cast<Derived&>(*this).leave(x);
265 }
266
267};
268
270template <typename Derived>
271struct data_expression_traverser: public add_traverser_data_expressions<process::data_expression_traverser, Derived>
272{
273};
274//--- end generated add_traverser_data_expressions code ---//
275
276//--- start generated add_traverser_variables code ---//
277template <template <class> class Traverser, class Derived>
278struct add_traverser_variables: public Traverser<Derived>
279{
280 typedef Traverser<Derived> super;
281 using super::enter;
282 using super::leave;
283 using super::apply;
284
285 void apply(const lps::deadlock& x)
286 {
287 static_cast<Derived&>(*this).enter(x);
288 if (x.has_time())
289 {
290 static_cast<Derived&>(*this).apply(x.time());
291 }
292 static_cast<Derived&>(*this).leave(x);
293 }
294
295 void apply(const lps::multi_action& x)
296 {
297 static_cast<Derived&>(*this).enter(x);
298 static_cast<Derived&>(*this).apply(x.actions());
299 if (x.has_time())
300 {
301 static_cast<Derived&>(*this).apply(x.time());
302 }
303 static_cast<Derived&>(*this).leave(x);
304 }
305
306 void apply(const lps::deadlock_summand& x)
307 {
308 static_cast<Derived&>(*this).enter(x);
309 static_cast<Derived&>(*this).apply(x.summation_variables());
310 static_cast<Derived&>(*this).apply(x.condition());
311 static_cast<Derived&>(*this).apply(x.deadlock());
312 static_cast<Derived&>(*this).leave(x);
313 }
314
315 void apply(const lps::action_summand& x)
316 {
317 static_cast<Derived&>(*this).enter(x);
318 static_cast<Derived&>(*this).apply(x.summation_variables());
319 static_cast<Derived&>(*this).apply(x.condition());
320 static_cast<Derived&>(*this).apply(x.multi_action());
321 static_cast<Derived&>(*this).apply(x.assignments());
322 static_cast<Derived&>(*this).leave(x);
323 }
324
325 void apply(const lps::process_initializer& x)
326 {
327 static_cast<Derived&>(*this).enter(x);
328 static_cast<Derived&>(*this).apply(x.expressions());
329 static_cast<Derived&>(*this).leave(x);
330 }
331
332 void apply(const lps::linear_process& x)
333 {
334 static_cast<Derived&>(*this).enter(x);
335 static_cast<Derived&>(*this).apply(x.process_parameters());
336 static_cast<Derived&>(*this).apply(x.deadlock_summands());
337 static_cast<Derived&>(*this).apply(x.action_summands());
338 static_cast<Derived&>(*this).leave(x);
339 }
340
341 void apply(const lps::specification& x)
342 {
343 static_cast<Derived&>(*this).enter(x);
344 static_cast<Derived&>(*this).apply(x.global_variables());
345 static_cast<Derived&>(*this).apply(x.process());
346 static_cast<Derived&>(*this).apply(x.initial_process());
347 static_cast<Derived&>(*this).leave(x);
348 }
349
350 void apply(const lps::stochastic_distribution& x)
351 {
352 static_cast<Derived&>(*this).enter(x);
353 static_cast<Derived&>(*this).apply(x.variables());
354 if (x.is_defined()) { static_cast<Derived&>(*this).apply(x.distribution()); }
355 static_cast<Derived&>(*this).leave(x);
356 }
357
358 void apply(const lps::stochastic_action_summand& x)
359 {
360 static_cast<Derived&>(*this).enter(x);
361 static_cast<Derived&>(*this).apply(x.summation_variables());
362 static_cast<Derived&>(*this).apply(x.condition());
363 static_cast<Derived&>(*this).apply(x.multi_action());
364 static_cast<Derived&>(*this).apply(x.assignments());
365 static_cast<Derived&>(*this).apply(x.distribution());
366 static_cast<Derived&>(*this).leave(x);
367 }
368
369 void apply(const lps::stochastic_linear_process& x)
370 {
371 static_cast<Derived&>(*this).enter(x);
372 static_cast<Derived&>(*this).apply(x.process_parameters());
373 static_cast<Derived&>(*this).apply(x.deadlock_summands());
374 static_cast<Derived&>(*this).apply(x.action_summands());
375 static_cast<Derived&>(*this).leave(x);
376 }
377
378 void apply(const lps::stochastic_specification& x)
379 {
380 static_cast<Derived&>(*this).enter(x);
381 static_cast<Derived&>(*this).apply(x.global_variables());
382 static_cast<Derived&>(*this).apply(x.process());
383 static_cast<Derived&>(*this).apply(x.initial_process());
384 static_cast<Derived&>(*this).leave(x);
385 }
386
387 void apply(const lps::stochastic_process_initializer& x)
388 {
389 static_cast<Derived&>(*this).enter(x);
390 static_cast<Derived&>(*this).apply(x.expressions());
391 static_cast<Derived&>(*this).apply(x.distribution());
392 static_cast<Derived&>(*this).leave(x);
393 }
394
395};
396
398template <typename Derived>
399struct variable_traverser: public add_traverser_variables<process::variable_traverser, Derived>
400{
401};
402//--- end generated add_traverser_variables code ---//
403
404//--- start generated add_traverser_identifier_strings code ---//
405template <template <class> class Traverser, class Derived>
406struct add_traverser_identifier_strings: public Traverser<Derived>
407{
408 typedef Traverser<Derived> super;
409 using super::enter;
410 using super::leave;
411 using super::apply;
412
413 void apply(const lps::deadlock& x)
414 {
415 static_cast<Derived&>(*this).enter(x);
416 if (x.has_time())
417 {
418 static_cast<Derived&>(*this).apply(x.time());
419 }
420 static_cast<Derived&>(*this).leave(x);
421 }
422
423 void apply(const lps::multi_action& x)
424 {
425 static_cast<Derived&>(*this).enter(x);
426 static_cast<Derived&>(*this).apply(x.actions());
427 if (x.has_time())
428 {
429 static_cast<Derived&>(*this).apply(x.time());
430 }
431 static_cast<Derived&>(*this).leave(x);
432 }
433
434 void apply(const lps::deadlock_summand& x)
435 {
436 static_cast<Derived&>(*this).enter(x);
437 static_cast<Derived&>(*this).apply(x.summation_variables());
438 static_cast<Derived&>(*this).apply(x.condition());
439 static_cast<Derived&>(*this).apply(x.deadlock());
440 static_cast<Derived&>(*this).leave(x);
441 }
442
443 void apply(const lps::action_summand& x)
444 {
445 static_cast<Derived&>(*this).enter(x);
446 static_cast<Derived&>(*this).apply(x.summation_variables());
447 static_cast<Derived&>(*this).apply(x.condition());
448 static_cast<Derived&>(*this).apply(x.multi_action());
449 static_cast<Derived&>(*this).apply(x.assignments());
450 static_cast<Derived&>(*this).leave(x);
451 }
452
453 void apply(const lps::process_initializer& x)
454 {
455 static_cast<Derived&>(*this).enter(x);
456 static_cast<Derived&>(*this).apply(x.expressions());
457 static_cast<Derived&>(*this).leave(x);
458 }
459
460 void apply(const lps::linear_process& x)
461 {
462 static_cast<Derived&>(*this).enter(x);
463 static_cast<Derived&>(*this).apply(x.process_parameters());
464 static_cast<Derived&>(*this).apply(x.deadlock_summands());
465 static_cast<Derived&>(*this).apply(x.action_summands());
466 static_cast<Derived&>(*this).leave(x);
467 }
468
469 void apply(const lps::specification& x)
470 {
471 static_cast<Derived&>(*this).enter(x);
472 static_cast<Derived&>(*this).apply(x.action_labels());
473 static_cast<Derived&>(*this).apply(x.global_variables());
474 static_cast<Derived&>(*this).apply(x.process());
475 static_cast<Derived&>(*this).apply(x.initial_process());
476 static_cast<Derived&>(*this).leave(x);
477 }
478
479 void apply(const lps::stochastic_distribution& x)
480 {
481 static_cast<Derived&>(*this).enter(x);
482 static_cast<Derived&>(*this).apply(x.variables());
483 if (x.is_defined()) { static_cast<Derived&>(*this).apply(x.distribution()); }
484 static_cast<Derived&>(*this).leave(x);
485 }
486
487 void apply(const lps::stochastic_action_summand& x)
488 {
489 static_cast<Derived&>(*this).enter(x);
490 static_cast<Derived&>(*this).apply(x.summation_variables());
491 static_cast<Derived&>(*this).apply(x.condition());
492 static_cast<Derived&>(*this).apply(x.multi_action());
493 static_cast<Derived&>(*this).apply(x.assignments());
494 static_cast<Derived&>(*this).apply(x.distribution());
495 static_cast<Derived&>(*this).leave(x);
496 }
497
498 void apply(const lps::stochastic_linear_process& x)
499 {
500 static_cast<Derived&>(*this).enter(x);
501 static_cast<Derived&>(*this).apply(x.process_parameters());
502 static_cast<Derived&>(*this).apply(x.deadlock_summands());
503 static_cast<Derived&>(*this).apply(x.action_summands());
504 static_cast<Derived&>(*this).leave(x);
505 }
506
507 void apply(const lps::stochastic_specification& x)
508 {
509 static_cast<Derived&>(*this).enter(x);
510 static_cast<Derived&>(*this).apply(x.action_labels());
511 static_cast<Derived&>(*this).apply(x.global_variables());
512 static_cast<Derived&>(*this).apply(x.process());
513 static_cast<Derived&>(*this).apply(x.initial_process());
514 static_cast<Derived&>(*this).leave(x);
515 }
516
517 void apply(const lps::stochastic_process_initializer& x)
518 {
519 static_cast<Derived&>(*this).enter(x);
520 static_cast<Derived&>(*this).apply(x.expressions());
521 static_cast<Derived&>(*this).apply(x.distribution());
522 static_cast<Derived&>(*this).leave(x);
523 }
524
525};
526
528template <typename Derived>
529struct identifier_string_traverser: public add_traverser_identifier_strings<process::identifier_string_traverser, Derived>
530{
531};
532//--- end generated add_traverser_identifier_strings code ---//
533
534//--- start generated add_traverser_action_labels code ---//
535template <template <class> class Traverser, class Derived>
536struct add_traverser_action_labels: public Traverser<Derived>
537{
538 typedef Traverser<Derived> super;
539 using super::enter;
540 using super::leave;
541 using super::apply;
542
543 void apply(const lps::multi_action& x)
544 {
545 static_cast<Derived&>(*this).enter(x);
546 static_cast<Derived&>(*this).apply(x.actions());
547 static_cast<Derived&>(*this).leave(x);
548 }
549
550 void apply(const lps::action_summand& x)
551 {
552 static_cast<Derived&>(*this).enter(x);
553 static_cast<Derived&>(*this).apply(x.multi_action());
554 static_cast<Derived&>(*this).leave(x);
555 }
556
557 void apply(const lps::linear_process& x)
558 {
559 static_cast<Derived&>(*this).enter(x);
560 static_cast<Derived&>(*this).apply(x.action_summands());
561 static_cast<Derived&>(*this).leave(x);
562 }
563
564 void apply(const lps::specification& x)
565 {
566 static_cast<Derived&>(*this).enter(x);
567 static_cast<Derived&>(*this).apply(x.action_labels());
568 static_cast<Derived&>(*this).apply(x.process());
569 static_cast<Derived&>(*this).leave(x);
570 }
571
572 void apply(const lps::stochastic_action_summand& x)
573 {
574 static_cast<Derived&>(*this).enter(x);
575 static_cast<Derived&>(*this).apply(x.multi_action());
576 static_cast<Derived&>(*this).leave(x);
577 }
578
579 void apply(const lps::stochastic_linear_process& x)
580 {
581 static_cast<Derived&>(*this).enter(x);
582 static_cast<Derived&>(*this).apply(x.action_summands());
583 static_cast<Derived&>(*this).leave(x);
584 }
585
586 void apply(const lps::stochastic_specification& x)
587 {
588 static_cast<Derived&>(*this).enter(x);
589 static_cast<Derived&>(*this).apply(x.action_labels());
590 static_cast<Derived&>(*this).apply(x.process());
591 static_cast<Derived&>(*this).leave(x);
592 }
593
594};
595
597template <typename Derived>
598struct action_label_traverser: public add_traverser_action_labels<process::action_label_traverser, Derived>
599{
600};
601//--- end generated add_traverser_action_labels code ---//
602
603} // namespace lps
604
605} // namespace mcrl2
606
607#endif // MCRL2_LPS_TRAVERSER_H
mcrl2::lps::action_summand
LPS summand containing a multi-action.
Definition action_summand.h:25
mcrl2::lps::action_summand::multi_action
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
Definition action_summand.h:55
mcrl2::lps::action_summand::assignments
const data::assignment_list & assignments() const
Returns the sequence of assignments.
Definition action_summand.h:68
mcrl2::lps::deadlock_summand
LPS summand containing a deadlock.
Definition deadlock_summand.h:25
mcrl2::lps::deadlock_summand::deadlock
const lps::deadlock & deadlock() const
Returns the deadlock of this summand.
Definition deadlock_summand.h:52
mcrl2::lps::deadlock
Represents a deadlock.
Definition deadlock.h:26
mcrl2::lps::deadlock::has_time
bool has_time() const
Returns true if time is available.
Definition deadlock.h:42
mcrl2::lps::deadlock::time
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:49
mcrl2::lps::linear_process_base::action_summands
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
Definition linear_process.h:138
mcrl2::lps::linear_process_base::deadlock_summands
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
Definition linear_process.h:152
mcrl2::lps::linear_process_base::process_parameters
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
Definition linear_process.h:166
mcrl2::lps::linear_process
linear process.
Definition linear_process.h:202
mcrl2::lps::multi_action
\brief A timed multi-action
Definition multi_action.h:30
mcrl2::lps::multi_action::has_time
bool has_time() const
Returns true if time is available.
Definition multi_action.h:73
mcrl2::lps::multi_action::actions
const process::action_list & actions() const
Definition multi_action.h:40
mcrl2::lps::multi_action::time
const data::data_expression & time() const
Definition multi_action.h:45
mcrl2::lps::process_initializer
A process initializer.
Definition process_initializer.h:29
mcrl2::lps::process_initializer::expressions
data::data_expression_list expressions() const
Definition process_initializer.h:61
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:146
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:131
mcrl2::lps::specification_base::initial_process
const InitialProcessExpression & initial_process() const
Returns the initial process.
Definition specification.h:160
mcrl2::lps::specification_base::process
const LinearProcess & process() const
Returns the linear process of the specification.
Definition specification.h:102
mcrl2::lps::specification
Linear process specification.
Definition specification.h:175
mcrl2::lps::stochastic_action_summand
LPS summand containing a multi-action.
Definition stochastic_action_summand.h:23
mcrl2::lps::stochastic_action_summand::distribution
const stochastic_distribution & distribution() const
Returns the distribution of this summand.
Definition stochastic_action_summand.h:51
mcrl2::lps::stochastic_distribution
\brief A stochastic distribution
Definition stochastic_distribution.h:24
mcrl2::lps::stochastic_distribution::variables
const data::variable_list & variables() const
Definition stochastic_distribution.h:50
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:62
mcrl2::lps::stochastic_distribution::distribution
const data::data_expression & distribution() const
Definition stochastic_distribution.h:55
mcrl2::lps::stochastic_linear_process
linear process.
Definition stochastic_linear_process.h:52
mcrl2::lps::stochastic_process_initializer
A stochastic process initializer.
Definition stochastic_process_initializer.h:23
mcrl2::lps::stochastic_process_initializer::distribution
const stochastic_distribution & distribution() const
Definition stochastic_process_initializer.h:45
mcrl2::lps::stochastic_specification
Linear process specification.
Definition stochastic_specification.h:36
mcrl2::lps::summand_base::condition
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
mcrl2::lps::summand_base::summation_variables
data::variable_list & summation_variables()
Returns the sequence of summation variables.
Definition summand.h:46
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
traverser.h
add your file description here.
stochastic_specification.h
mcrl2::lps::action_label_traverser
\brief Traverser class
Definition traverser.h:599
mcrl2::lps::add_traverser_action_labels
Definition traverser.h:537
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::action_summand &x)
Definition traverser.h:550
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::multi_action &x)
Definition traverser.h:543
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::specification &x)
Definition traverser.h:564
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:572
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:579
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::stochastic_specification &x)
Definition traverser.h:586
mcrl2::lps::add_traverser_action_labels::super
Traverser< Derived > super
Definition traverser.h:538
mcrl2::lps::add_traverser_action_labels::apply
void apply(const lps::linear_process &x)
Definition traverser.h:557
mcrl2::lps::add_traverser_data_expressions
Definition traverser.h:159
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:243
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::multi_action &x)
Definition traverser.h:175
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::deadlock &x)
Definition traverser.h:165
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::stochastic_specification &x)
Definition traverser.h:251
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::specification &x)
Definition traverser.h:218
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::deadlock_summand &x)
Definition traverser.h:186
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::action_summand &x)
Definition traverser.h:194
mcrl2::lps::add_traverser_data_expressions::super
Traverser< Derived > super
Definition traverser.h:160
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:233
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:226
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::linear_process &x)
Definition traverser.h:210
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:259
mcrl2::lps::add_traverser_data_expressions::apply
void apply(const lps::process_initializer &x)
Definition traverser.h:203
mcrl2::lps::add_traverser_identifier_strings
Definition traverser.h:407
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:498
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:487
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::action_summand &x)
Definition traverser.h:443
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::specification &x)
Definition traverser.h:469
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::process_initializer &x)
Definition traverser.h:453
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:479
mcrl2::lps::add_traverser_identifier_strings::super
Traverser< Derived > super
Definition traverser.h:408
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::linear_process &x)
Definition traverser.h:460
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::deadlock_summand &x)
Definition traverser.h:434
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:517
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::stochastic_specification &x)
Definition traverser.h:507
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::multi_action &x)
Definition traverser.h:423
mcrl2::lps::add_traverser_identifier_strings::apply
void apply(const lps::deadlock &x)
Definition traverser.h:413
mcrl2::lps::add_traverser_sort_expressions
Definition traverser.h:29
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:109
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:120
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::stochastic_specification &x)
Definition traverser.h:129
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:139
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:101
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::multi_action &x)
Definition traverser.h:45
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::process_initializer &x)
Definition traverser.h:75
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::action_summand &x)
Definition traverser.h:65
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::specification &x)
Definition traverser.h:91
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::deadlock_summand &x)
Definition traverser.h:56
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::deadlock &x)
Definition traverser.h:35
mcrl2::lps::add_traverser_sort_expressions::super
Traverser< Derived > super
Definition traverser.h:30
mcrl2::lps::add_traverser_sort_expressions::apply
void apply(const lps::linear_process &x)
Definition traverser.h:82
mcrl2::lps::add_traverser_variables
Definition traverser.h:279
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::linear_process &x)
Definition traverser.h:332
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::specification &x)
Definition traverser.h:341
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::stochastic_process_initializer &x)
Definition traverser.h:387
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::deadlock &x)
Definition traverser.h:285
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::stochastic_linear_process &x)
Definition traverser.h:369
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::multi_action &x)
Definition traverser.h:295
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::action_summand &x)
Definition traverser.h:315
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::stochastic_action_summand &x)
Definition traverser.h:358
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::deadlock_summand &x)
Definition traverser.h:306
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::stochastic_distribution &x)
Definition traverser.h:350
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::stochastic_specification &x)
Definition traverser.h:378
mcrl2::lps::add_traverser_variables::super
Traverser< Derived > super
Definition traverser.h:280
mcrl2::lps::add_traverser_variables::apply
void apply(const lps::process_initializer &x)
Definition traverser.h:325
mcrl2::lps::data_expression_traverser
\brief Traverser class
Definition traverser.h:272
mcrl2::lps::identifier_string_traverser
\brief Traverser class
Definition traverser.h:530
mcrl2::lps::sort_expression_traverser
\brief Traverser class
Definition traverser.h:152
mcrl2::lps::variable_traverser
\brief Traverser class
Definition traverser.h:400