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//
11
12#ifndef MCRL2_LPS_BUILDER_H
13#define MCRL2_LPS_BUILDER_H
14
15#include "mcrl2/lps/stochastic_specification.h"
16#include "mcrl2/process/builder.h"
17
18namespace mcrl2
19{
20
21namespace lps
22{
23
24// Adds sort expression traversal to a builder
25//--- start generated add_sort_expressions code ---//
26template <template <class> class Builder, class Derived>
27struct add_sort_expressions: public Builder<Derived>
28{
29 typedef Builder<Derived> super;
30 using super::enter;
31 using super::leave;
32 using super::update;
33 using super::apply;
34
35 void update(lps::deadlock& x)
36 {
37 static_cast<Derived&>(*this).enter(x);
38 data::data_expression result_time;
39 static_cast<Derived&>(*this).apply(result_time, x.time());
40 x.time() = result_time;
41 static_cast<Derived&>(*this).leave(x);
42 }
43
44 template <class T>
45 void apply(T& result, const lps::multi_action& x)
46 {
47
48 static_cast<Derived&>(*this).enter(x);
49 lps::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time()); });
50 static_cast<Derived&>(*this).leave(x);
51 }
52
53 void update(lps::deadlock_summand& x)
54 {
55 static_cast<Derived&>(*this).enter(x);
56 data::variable_list result_summation_variables;
57 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
58 x.summation_variables() = result_summation_variables;
59 data::data_expression result_condition;
60 static_cast<Derived&>(*this).apply(result_condition, x.condition());
61 x.condition() = result_condition;
62 static_cast<Derived&>(*this).update(x.deadlock());
63 static_cast<Derived&>(*this).leave(x);
64 }
65
66 void update(lps::action_summand& x)
67 {
68 static_cast<Derived&>(*this).enter(x);
69 data::variable_list result_summation_variables;
70 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
71 x.summation_variables() = result_summation_variables;
72 data::data_expression result_condition;
73 static_cast<Derived&>(*this).apply(result_condition, x.condition());
74 x.condition() = result_condition;
75 lps::multi_action result_multi_action;
76 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
77 x.multi_action() = result_multi_action;
78 data::assignment_list result_assignments;
79 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
80 x.assignments() = result_assignments;
81 static_cast<Derived&>(*this).leave(x);
82 }
83
84 template <class T>
85 void apply(T& result, const lps::process_initializer& x)
86 {
87
88 static_cast<Derived&>(*this).enter(x);
89 lps::make_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); });
90 static_cast<Derived&>(*this).leave(x);
91 }
92
93 void update(lps::linear_process& x)
94 {
95 static_cast<Derived&>(*this).enter(x);
96 data::variable_list result_process_parameters;
97 static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
98 x.process_parameters() = result_process_parameters;
99 static_cast<Derived&>(*this).update(x.deadlock_summands());
100 static_cast<Derived&>(*this).update(x.action_summands());
101 static_cast<Derived&>(*this).leave(x);
102 }
103
104 void update(lps::specification& x)
105 {
106 static_cast<Derived&>(*this).enter(x);
107 process::action_label_list result_action_labels;
108 static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
109 x.action_labels() = result_action_labels;
110 static_cast<Derived&>(*this).update(x.global_variables());
111 static_cast<Derived&>(*this).update(x.process());
112 process_initializer result_initial_process;
113 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
114 x.initial_process() = result_initial_process;
115 static_cast<Derived&>(*this).leave(x);
116 }
117
118 template <class T>
119 void apply(T& result, const lps::stochastic_distribution& x)
120 {
121
122 static_cast<Derived&>(*this).enter(x);
123 result = x; if (x.is_defined()) { lps::make_stochastic_distribution(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()); }); }
124 static_cast<Derived&>(*this).leave(x);
125 }
126
127 void update(lps::stochastic_action_summand& x)
128 {
129 static_cast<Derived&>(*this).enter(x);
130 data::variable_list result_summation_variables;
131 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
132 x.summation_variables() = result_summation_variables;
133 data::data_expression result_condition;
134 static_cast<Derived&>(*this).apply(result_condition, x.condition());
135 x.condition() = result_condition;
136 lps::multi_action result_multi_action;
137 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
138 x.multi_action() = result_multi_action;
139 data::assignment_list result_assignments;
140 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
141 x.assignments() = result_assignments;
142 stochastic_distribution result_distribution;
143 static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
144 x.distribution() = result_distribution;
145 static_cast<Derived&>(*this).leave(x);
146 }
147
148 void update(lps::stochastic_linear_process& x)
149 {
150 static_cast<Derived&>(*this).enter(x);
151 data::variable_list result_process_parameters;
152 static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
153 x.process_parameters() = result_process_parameters;
154 static_cast<Derived&>(*this).update(x.deadlock_summands());
155 static_cast<Derived&>(*this).update(x.action_summands());
156 static_cast<Derived&>(*this).leave(x);
157 }
158
159 void update(lps::stochastic_specification& x)
160 {
161 static_cast<Derived&>(*this).enter(x);
162 process::action_label_list result_action_labels;
163 static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
164 x.action_labels() = result_action_labels;
165 static_cast<Derived&>(*this).update(x.global_variables());
166 static_cast<Derived&>(*this).update(x.process());
167 stochastic_process_initializer result_initial_process;
168 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
169 x.initial_process() = result_initial_process;
170 static_cast<Derived&>(*this).leave(x);
171 }
172
173 template <class T>
174 void apply(T& result, const lps::stochastic_process_initializer& x)
175 {
176
177 static_cast<Derived&>(*this).enter(x);
178 lps::make_stochastic_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); }, [&](stochastic_distribution& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); });
179 static_cast<Derived&>(*this).leave(x);
180 }
181
182};
183
185template <typename Derived>
186struct sort_expression_builder: public add_sort_expressions<process::sort_expression_builder, Derived>
187{
188};
189//--- end generated add_sort_expressions code ---//
190
191// Adds data expression traversal to a builder
192//--- start generated add_data_expressions code ---//
193template <template <class> class Builder, class Derived>
194struct add_data_expressions: public Builder<Derived>
195{
196 typedef Builder<Derived> super;
197 using super::enter;
198 using super::leave;
199 using super::update;
200 using super::apply;
201
202 void update(lps::deadlock& x)
203 {
204 static_cast<Derived&>(*this).enter(x);
205 data::data_expression result_time;
206 static_cast<Derived&>(*this).apply(result_time, x.time());
207 x.time() = result_time;
208 static_cast<Derived&>(*this).leave(x);
209 }
210
211 template <class T>
212 void apply(T& result, const lps::multi_action& x)
213 {
214
215 static_cast<Derived&>(*this).enter(x);
216 lps::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time()); });
217 static_cast<Derived&>(*this).leave(x);
218 }
219
220 void update(lps::deadlock_summand& x)
221 {
222 static_cast<Derived&>(*this).enter(x);
223 data::data_expression result_condition;
224 static_cast<Derived&>(*this).apply(result_condition, x.condition());
225 x.condition() = result_condition;
226 static_cast<Derived&>(*this).update(x.deadlock());
227 static_cast<Derived&>(*this).leave(x);
228 }
229
230 void update(lps::action_summand& x)
231 {
232 static_cast<Derived&>(*this).enter(x);
233 data::data_expression result_condition;
234 static_cast<Derived&>(*this).apply(result_condition, x.condition());
235 x.condition() = result_condition;
236 lps::multi_action result_multi_action;
237 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
238 x.multi_action() = result_multi_action;
239 data::assignment_list result_assignments;
240 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
241 x.assignments() = result_assignments;
242 static_cast<Derived&>(*this).leave(x);
243 }
244
245 template <class T>
246 void apply(T& result, const lps::process_initializer& x)
247 {
248
249 static_cast<Derived&>(*this).enter(x);
250 lps::make_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); });
251 static_cast<Derived&>(*this).leave(x);
252 }
253
254 void update(lps::linear_process& x)
255 {
256 static_cast<Derived&>(*this).enter(x);
257 static_cast<Derived&>(*this).update(x.deadlock_summands());
258 static_cast<Derived&>(*this).update(x.action_summands());
259 static_cast<Derived&>(*this).leave(x);
260 }
261
262 void update(lps::specification& x)
263 {
264 static_cast<Derived&>(*this).enter(x);
265 static_cast<Derived&>(*this).update(x.process());
266 process_initializer result_initial_process;
267 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
268 x.initial_process() = result_initial_process;
269 static_cast<Derived&>(*this).leave(x);
270 }
271
272 template <class T>
273 void apply(T& result, const lps::stochastic_distribution& x)
274 {
275
276 static_cast<Derived&>(*this).enter(x);
277 result = x; if (x.is_defined()) { lps::make_stochastic_distribution(result, x.variables(), [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); }); }
278 static_cast<Derived&>(*this).leave(x);
279 }
280
281 void update(lps::stochastic_action_summand& x)
282 {
283 static_cast<Derived&>(*this).enter(x);
284 data::data_expression result_condition;
285 static_cast<Derived&>(*this).apply(result_condition, x.condition());
286 x.condition() = result_condition;
287 lps::multi_action result_multi_action;
288 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
289 x.multi_action() = result_multi_action;
290 data::assignment_list result_assignments;
291 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
292 x.assignments() = result_assignments;
293 stochastic_distribution result_distribution;
294 static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
295 x.distribution() = result_distribution;
296 static_cast<Derived&>(*this).leave(x);
297 }
298
299 void update(lps::stochastic_linear_process& x)
300 {
301 static_cast<Derived&>(*this).enter(x);
302 static_cast<Derived&>(*this).update(x.deadlock_summands());
303 static_cast<Derived&>(*this).update(x.action_summands());
304 static_cast<Derived&>(*this).leave(x);
305 }
306
307 void update(lps::stochastic_specification& x)
308 {
309 static_cast<Derived&>(*this).enter(x);
310 static_cast<Derived&>(*this).update(x.process());
311 stochastic_process_initializer result_initial_process;
312 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
313 x.initial_process() = result_initial_process;
314 static_cast<Derived&>(*this).leave(x);
315 }
316
317 template <class T>
318 void apply(T& result, const lps::stochastic_process_initializer& x)
319 {
320
321 static_cast<Derived&>(*this).enter(x);
322 lps::make_stochastic_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); }, [&](stochastic_distribution& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); });
323 static_cast<Derived&>(*this).leave(x);
324 }
325
326};
327
329template <typename Derived>
330struct data_expression_builder: public add_data_expressions<process::data_expression_builder, Derived>
331{
332};
333//--- end generated add_data_expressions code ---//
334
335//--- start generated add_variables code ---//
336template <template <class> class Builder, class Derived>
337struct add_variables: public Builder<Derived>
338{
339 typedef Builder<Derived> super;
340 using super::enter;
341 using super::leave;
342 using super::update;
343 using super::apply;
344
345 void update(lps::deadlock& x)
346 {
347 static_cast<Derived&>(*this).enter(x);
348 data::data_expression result_time;
349 static_cast<Derived&>(*this).apply(result_time, x.time());
350 x.time() = result_time;
351 static_cast<Derived&>(*this).leave(x);
352 }
353
354 template <class T>
355 void apply(T& result, const lps::multi_action& x)
356 {
357
358 static_cast<Derived&>(*this).enter(x);
359 lps::make_multi_action(result, [&](process::action_list& result){ static_cast<Derived&>(*this).apply(result, x.actions()); }, [&](data::data_expression& result){ static_cast<Derived&>(*this).apply(result, x.time()); });
360 static_cast<Derived&>(*this).leave(x);
361 }
362
363 void update(lps::deadlock_summand& x)
364 {
365 static_cast<Derived&>(*this).enter(x);
366 data::variable_list result_summation_variables;
367 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
368 x.summation_variables() = result_summation_variables;
369 data::data_expression result_condition;
370 static_cast<Derived&>(*this).apply(result_condition, x.condition());
371 x.condition() = result_condition;
372 static_cast<Derived&>(*this).update(x.deadlock());
373 static_cast<Derived&>(*this).leave(x);
374 }
375
376 void update(lps::action_summand& x)
377 {
378 static_cast<Derived&>(*this).enter(x);
379 data::variable_list result_summation_variables;
380 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
381 x.summation_variables() = result_summation_variables;
382 data::data_expression result_condition;
383 static_cast<Derived&>(*this).apply(result_condition, x.condition());
384 x.condition() = result_condition;
385 lps::multi_action result_multi_action;
386 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
387 x.multi_action() = result_multi_action;
388 data::assignment_list result_assignments;
389 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
390 x.assignments() = result_assignments;
391 static_cast<Derived&>(*this).leave(x);
392 }
393
394 template <class T>
395 void apply(T& result, const lps::process_initializer& x)
396 {
397
398 static_cast<Derived&>(*this).enter(x);
399 lps::make_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); });
400 static_cast<Derived&>(*this).leave(x);
401 }
402
403 void update(lps::linear_process& x)
404 {
405 static_cast<Derived&>(*this).enter(x);
406 data::variable_list result_process_parameters;
407 static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
408 x.process_parameters() = result_process_parameters;
409 static_cast<Derived&>(*this).update(x.deadlock_summands());
410 static_cast<Derived&>(*this).update(x.action_summands());
411 static_cast<Derived&>(*this).leave(x);
412 }
413
414 void update(lps::specification& x)
415 {
416 static_cast<Derived&>(*this).enter(x);
417 static_cast<Derived&>(*this).update(x.global_variables());
418 static_cast<Derived&>(*this).update(x.process());
419 process_initializer result_initial_process;
420 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
421 x.initial_process() = result_initial_process;
422 static_cast<Derived&>(*this).leave(x);
423 }
424
425 template <class T>
426 void apply(T& result, const lps::stochastic_distribution& x)
427 {
428
429 static_cast<Derived&>(*this).enter(x);
430 result = x; if (x.is_defined()) { lps::make_stochastic_distribution(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()); }); }
431 static_cast<Derived&>(*this).leave(x);
432 }
433
434 void update(lps::stochastic_action_summand& x)
435 {
436 static_cast<Derived&>(*this).enter(x);
437 data::variable_list result_summation_variables;
438 static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
439 x.summation_variables() = result_summation_variables;
440 data::data_expression result_condition;
441 static_cast<Derived&>(*this).apply(result_condition, x.condition());
442 x.condition() = result_condition;
443 lps::multi_action result_multi_action;
444 static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
445 x.multi_action() = result_multi_action;
446 data::assignment_list result_assignments;
447 static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
448 x.assignments() = result_assignments;
449 stochastic_distribution result_distribution;
450 static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
451 x.distribution() = result_distribution;
452 static_cast<Derived&>(*this).leave(x);
453 }
454
455 void update(lps::stochastic_linear_process& x)
456 {
457 static_cast<Derived&>(*this).enter(x);
458 data::variable_list result_process_parameters;
459 static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
460 x.process_parameters() = result_process_parameters;
461 static_cast<Derived&>(*this).update(x.deadlock_summands());
462 static_cast<Derived&>(*this).update(x.action_summands());
463 static_cast<Derived&>(*this).leave(x);
464 }
465
466 void update(lps::stochastic_specification& x)
467 {
468 static_cast<Derived&>(*this).enter(x);
469 static_cast<Derived&>(*this).update(x.global_variables());
470 static_cast<Derived&>(*this).update(x.process());
471 stochastic_process_initializer result_initial_process;
472 static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
473 x.initial_process() = result_initial_process;
474 static_cast<Derived&>(*this).leave(x);
475 }
476
477 template <class T>
478 void apply(T& result, const lps::stochastic_process_initializer& x)
479 {
480
481 static_cast<Derived&>(*this).enter(x);
482 lps::make_stochastic_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); }, [&](stochastic_distribution& result){ static_cast<Derived&>(*this).apply(result, x.distribution()); });
483 static_cast<Derived&>(*this).leave(x);
484 }
485
486};
487
489template <typename Derived>
490struct variable_builder: public add_variables<process::data_expression_builder, Derived>
491{
492};
493//--- end generated add_variables code ---//
494
495} // namespace lps
496
497} // namespace mcrl2
498
499#endif // MCRL2_LPS_BUILDER_H
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:24
mcrl2::data::data_expression
data expression.
Definition data_expression.h:131
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::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::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::lps::make_stochastic_distribution
void make_stochastic_distribution(atermpp::aterm &t, const ARGUMENTS &... args)
Definition stochastic_distribution.h:72
mcrl2::lps::make_stochastic_process_initializer
void make_stochastic_process_initializer(atermpp::aterm &t, ARGUMENTS... args)
Definition stochastic_process_initializer.h:52
mcrl2::lps::make_process_initializer
void make_process_initializer(atermpp::aterm &t, EXPRESSION_LIST args)
Definition process_initializer.h:69
mcrl2::lps::make_multi_action
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
Definition multi_action.h:103
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
builder.h
add your file description here.
stochastic_specification.h
mcrl2::lps::add_data_expressions
Definition builder.h:195
mcrl2::lps::add_data_expressions::update
void update(lps::action_summand &x)
Definition builder.h:230
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:318
mcrl2::lps::add_data_expressions::update
void update(lps::linear_process &x)
Definition builder.h:254
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:212
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:273
mcrl2::lps::add_data_expressions::update
void update(lps::specification &x)
Definition builder.h:262
mcrl2::lps::add_data_expressions::update
void update(lps::deadlock &x)
Definition builder.h:202
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:299
mcrl2::lps::add_data_expressions::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:246
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:281
mcrl2::lps::add_data_expressions::update
void update(lps::deadlock_summand &x)
Definition builder.h:220
mcrl2::lps::add_data_expressions::update
void update(lps::stochastic_specification &x)
Definition builder.h:307
mcrl2::lps::add_data_expressions::super
Builder< Derived > super
Definition builder.h:196
mcrl2::lps::add_sort_expressions
Definition builder.h:28
mcrl2::lps::add_sort_expressions::update
void update(lps::deadlock &x)
Definition builder.h:35
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_specification &x)
Definition builder.h:159
mcrl2::lps::add_sort_expressions::update
void update(lps::specification &x)
Definition builder.h:104
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:85
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:174
mcrl2::lps::add_sort_expressions::update
void update(lps::action_summand &x)
Definition builder.h:66
mcrl2::lps::add_sort_expressions::super
Builder< Derived > super
Definition builder.h:29
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:119
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:148
mcrl2::lps::add_sort_expressions::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:127
mcrl2::lps::add_sort_expressions::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:45
mcrl2::lps::add_sort_expressions::update
void update(lps::linear_process &x)
Definition builder.h:93
mcrl2::lps::add_sort_expressions::update
void update(lps::deadlock_summand &x)
Definition builder.h:53
mcrl2::lps::add_variables
Definition builder.h:338
mcrl2::lps::add_variables::super
Builder< Derived > super
Definition builder.h:339
mcrl2::lps::add_variables::update
void update(lps::action_summand &x)
Definition builder.h:376
mcrl2::lps::add_variables::update
void update(lps::deadlock &x)
Definition builder.h:345
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::multi_action &x)
Definition builder.h:355
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:478
mcrl2::lps::add_variables::update
void update(lps::specification &x)
Definition builder.h:414
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:426
mcrl2::lps::add_variables::update
void update(lps::linear_process &x)
Definition builder.h:403
mcrl2::lps::add_variables::update
void update(lps::stochastic_action_summand &x)
Definition builder.h:434
mcrl2::lps::add_variables::update
void update(lps::stochastic_specification &x)
Definition builder.h:466
mcrl2::lps::add_variables::apply
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:395
mcrl2::lps::add_variables::update
void update(lps::stochastic_linear_process &x)
Definition builder.h:455
mcrl2::lps::add_variables::update
void update(lps::deadlock_summand &x)
Definition builder.h:363
mcrl2::lps::data_expression_builder
\brief Builder class
Definition builder.h:331
mcrl2::lps::sort_expression_builder
\brief Builder class
Definition builder.h:187
mcrl2::lps::variable_builder
\brief Builder class
Definition builder.h:491