Line data Source code
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/lps/builder.h
10 : /// \brief add your file description here.
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 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace lps
22 : {
23 :
24 : // Adds sort expression traversal to a builder
25 : //--- start generated add_sort_expressions code ---//
26 : template <template <class> class Builder, class Derived>
27 : struct 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 10 : void update(lps::deadlock& x)
36 : {
37 10 : static_cast<Derived&>(*this).enter(x);
38 10 : data::data_expression result_time;
39 10 : static_cast<Derived&>(*this).apply(result_time, x.time());
40 10 : x.time() = result_time;
41 10 : static_cast<Derived&>(*this).leave(x);
42 10 : }
43 :
44 : template <class T>
45 94 : void apply(T& result, const lps::multi_action& x)
46 : {
47 :
48 94 : static_cast<Derived&>(*this).enter(x);
49 282 : 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 94 : static_cast<Derived&>(*this).leave(x);
51 94 : }
52 :
53 10 : void update(lps::deadlock_summand& x)
54 : {
55 10 : static_cast<Derived&>(*this).enter(x);
56 10 : data::variable_list result_summation_variables;
57 10 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
58 10 : x.summation_variables() = result_summation_variables;
59 10 : data::data_expression result_condition;
60 10 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
61 10 : x.condition() = result_condition;
62 10 : static_cast<Derived&>(*this).update(x.deadlock());
63 10 : static_cast<Derived&>(*this).leave(x);
64 10 : }
65 :
66 72 : void update(lps::action_summand& x)
67 : {
68 72 : static_cast<Derived&>(*this).enter(x);
69 72 : data::variable_list result_summation_variables;
70 72 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
71 72 : x.summation_variables() = result_summation_variables;
72 72 : data::data_expression result_condition;
73 72 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
74 72 : x.condition() = result_condition;
75 144 : lps::multi_action result_multi_action;
76 72 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
77 72 : x.multi_action() = result_multi_action;
78 72 : data::assignment_list result_assignments;
79 72 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
80 72 : x.assignments() = result_assignments;
81 72 : static_cast<Derived&>(*this).leave(x);
82 72 : }
83 :
84 : template <class T>
85 16 : void apply(T& result, const lps::process_initializer& x)
86 : {
87 :
88 16 : static_cast<Derived&>(*this).enter(x);
89 32 : lps::make_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); });
90 16 : static_cast<Derived&>(*this).leave(x);
91 16 : }
92 :
93 16 : void update(lps::linear_process& x)
94 : {
95 16 : static_cast<Derived&>(*this).enter(x);
96 16 : data::variable_list result_process_parameters;
97 16 : static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
98 16 : x.process_parameters() = result_process_parameters;
99 16 : static_cast<Derived&>(*this).update(x.deadlock_summands());
100 16 : static_cast<Derived&>(*this).update(x.action_summands());
101 16 : static_cast<Derived&>(*this).leave(x);
102 16 : }
103 :
104 16 : void update(lps::specification& x)
105 : {
106 16 : static_cast<Derived&>(*this).enter(x);
107 16 : process::action_label_list result_action_labels;
108 16 : static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
109 16 : x.action_labels() = result_action_labels;
110 16 : static_cast<Derived&>(*this).update(x.global_variables());
111 16 : static_cast<Derived&>(*this).update(x.process());
112 16 : process_initializer result_initial_process;
113 16 : static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
114 16 : x.initial_process() = result_initial_process;
115 16 : static_cast<Derived&>(*this).leave(x);
116 16 : }
117 :
118 : template <class T>
119 0 : void apply(T& result, const lps::stochastic_distribution& x)
120 : {
121 :
122 0 : static_cast<Derived&>(*this).enter(x);
123 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
125 0 : }
126 :
127 0 : void update(lps::stochastic_action_summand& x)
128 : {
129 0 : static_cast<Derived&>(*this).enter(x);
130 0 : data::variable_list result_summation_variables;
131 0 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
132 0 : x.summation_variables() = result_summation_variables;
133 0 : data::data_expression result_condition;
134 0 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
135 0 : x.condition() = result_condition;
136 0 : lps::multi_action result_multi_action;
137 0 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
138 0 : x.multi_action() = result_multi_action;
139 0 : data::assignment_list result_assignments;
140 0 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
141 0 : x.assignments() = result_assignments;
142 0 : stochastic_distribution result_distribution;
143 0 : static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
144 0 : x.distribution() = result_distribution;
145 0 : static_cast<Derived&>(*this).leave(x);
146 0 : }
147 :
148 0 : void update(lps::stochastic_linear_process& x)
149 : {
150 0 : static_cast<Derived&>(*this).enter(x);
151 0 : data::variable_list result_process_parameters;
152 0 : static_cast<Derived&>(*this).apply(result_process_parameters, x.process_parameters());
153 0 : x.process_parameters() = result_process_parameters;
154 0 : static_cast<Derived&>(*this).update(x.deadlock_summands());
155 0 : static_cast<Derived&>(*this).update(x.action_summands());
156 0 : static_cast<Derived&>(*this).leave(x);
157 0 : }
158 :
159 0 : void update(lps::stochastic_specification& x)
160 : {
161 0 : static_cast<Derived&>(*this).enter(x);
162 0 : process::action_label_list result_action_labels;
163 0 : static_cast<Derived&>(*this).apply(result_action_labels, x.action_labels());
164 0 : x.action_labels() = result_action_labels;
165 0 : static_cast<Derived&>(*this).update(x.global_variables());
166 0 : static_cast<Derived&>(*this).update(x.process());
167 0 : stochastic_process_initializer result_initial_process;
168 0 : static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
169 0 : x.initial_process() = result_initial_process;
170 0 : static_cast<Derived&>(*this).leave(x);
171 0 : }
172 :
173 : template <class T>
174 0 : void apply(T& result, const lps::stochastic_process_initializer& x)
175 : {
176 :
177 0 : static_cast<Derived&>(*this).enter(x);
178 0 : 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 0 : static_cast<Derived&>(*this).leave(x);
180 0 : }
181 :
182 : };
183 :
184 : /// \\brief Builder class
185 : template <typename Derived>
186 : struct 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 ---//
193 : template <template <class> class Builder, class Derived>
194 : struct 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 1588 : void update(lps::deadlock& x)
203 : {
204 1588 : static_cast<Derived&>(*this).enter(x);
205 1588 : data::data_expression result_time;
206 1588 : static_cast<Derived&>(*this).apply(result_time, x.time());
207 1588 : x.time() = result_time;
208 1588 : static_cast<Derived&>(*this).leave(x);
209 1588 : }
210 :
211 : template <class T>
212 4865 : void apply(T& result, const lps::multi_action& x)
213 : {
214 :
215 4865 : static_cast<Derived&>(*this).enter(x);
216 14595 : 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 4865 : static_cast<Derived&>(*this).leave(x);
218 4865 : }
219 :
220 1566 : void update(lps::deadlock_summand& x)
221 : {
222 1566 : static_cast<Derived&>(*this).enter(x);
223 1566 : data::data_expression result_condition;
224 1566 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
225 1566 : x.condition() = result_condition;
226 1566 : static_cast<Derived&>(*this).update(x.deadlock());
227 1566 : static_cast<Derived&>(*this).leave(x);
228 1566 : }
229 :
230 581 : void update(lps::action_summand& x)
231 : {
232 581 : static_cast<Derived&>(*this).enter(x);
233 581 : data::data_expression result_condition;
234 581 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
235 581 : x.condition() = result_condition;
236 1162 : lps::multi_action result_multi_action;
237 581 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
238 581 : x.multi_action() = result_multi_action;
239 581 : data::assignment_list result_assignments;
240 581 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
241 581 : x.assignments() = result_assignments;
242 581 : static_cast<Derived&>(*this).leave(x);
243 581 : }
244 :
245 : template <class T>
246 226 : void apply(T& result, const lps::process_initializer& x)
247 : {
248 :
249 226 : static_cast<Derived&>(*this).enter(x);
250 452 : lps::make_process_initializer(result, [&](data::data_expression_list& result){ static_cast<Derived&>(*this).apply(result, x.expressions()); });
251 226 : static_cast<Derived&>(*this).leave(x);
252 226 : }
253 :
254 251 : void update(lps::linear_process& x)
255 : {
256 251 : static_cast<Derived&>(*this).enter(x);
257 251 : static_cast<Derived&>(*this).update(x.deadlock_summands());
258 251 : static_cast<Derived&>(*this).update(x.action_summands());
259 251 : static_cast<Derived&>(*this).leave(x);
260 251 : }
261 :
262 78 : void update(lps::specification& x)
263 : {
264 78 : static_cast<Derived&>(*this).enter(x);
265 78 : static_cast<Derived&>(*this).update(x.process());
266 78 : process_initializer result_initial_process;
267 78 : static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
268 78 : x.initial_process() = result_initial_process;
269 78 : static_cast<Derived&>(*this).leave(x);
270 78 : }
271 :
272 : template <class T>
273 4073 : void apply(T& result, const lps::stochastic_distribution& x)
274 : {
275 :
276 4073 : static_cast<Derived&>(*this).enter(x);
277 4290 : 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 4073 : static_cast<Derived&>(*this).leave(x);
279 4073 : }
280 :
281 2605 : void update(lps::stochastic_action_summand& x)
282 : {
283 2605 : static_cast<Derived&>(*this).enter(x);
284 2605 : data::data_expression result_condition;
285 2605 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
286 2605 : x.condition() = result_condition;
287 5210 : lps::multi_action result_multi_action;
288 2605 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
289 2605 : x.multi_action() = result_multi_action;
290 2605 : data::assignment_list result_assignments;
291 2605 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
292 2605 : x.assignments() = result_assignments;
293 2605 : stochastic_distribution result_distribution;
294 2605 : static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
295 2605 : x.distribution() = result_distribution;
296 2605 : static_cast<Derived&>(*this).leave(x);
297 2605 : }
298 :
299 1468 : void update(lps::stochastic_linear_process& x)
300 : {
301 1468 : static_cast<Derived&>(*this).enter(x);
302 1468 : static_cast<Derived&>(*this).update(x.deadlock_summands());
303 1468 : static_cast<Derived&>(*this).update(x.action_summands());
304 1468 : static_cast<Derived&>(*this).leave(x);
305 1468 : }
306 :
307 1438 : void update(lps::stochastic_specification& x)
308 : {
309 1438 : static_cast<Derived&>(*this).enter(x);
310 1438 : static_cast<Derived&>(*this).update(x.process());
311 1438 : stochastic_process_initializer result_initial_process;
312 1438 : static_cast<Derived&>(*this).apply(result_initial_process, x.initial_process());
313 1438 : x.initial_process() = result_initial_process;
314 1438 : static_cast<Derived&>(*this).leave(x);
315 1438 : }
316 :
317 : template <class T>
318 750 : void apply(T& result, const lps::stochastic_process_initializer& x)
319 : {
320 :
321 750 : static_cast<Derived&>(*this).enter(x);
322 2250 : 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 750 : static_cast<Derived&>(*this).leave(x);
324 750 : }
325 :
326 : };
327 :
328 : /// \\brief Builder class
329 : template <typename Derived>
330 : struct 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 ---//
336 : template <template <class> class Builder, class Derived>
337 : struct 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 0 : void update(lps::deadlock& x)
346 : {
347 0 : static_cast<Derived&>(*this).enter(x);
348 0 : data::data_expression result_time;
349 0 : static_cast<Derived&>(*this).apply(result_time, x.time());
350 0 : x.time() = result_time;
351 0 : static_cast<Derived&>(*this).leave(x);
352 0 : }
353 :
354 : template <class T>
355 14 : void apply(T& result, const lps::multi_action& x)
356 : {
357 :
358 14 : static_cast<Derived&>(*this).enter(x);
359 42 : 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 14 : static_cast<Derived&>(*this).leave(x);
361 14 : }
362 :
363 0 : void update(lps::deadlock_summand& x)
364 : {
365 0 : static_cast<Derived&>(*this).enter(x);
366 0 : data::variable_list result_summation_variables;
367 0 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
368 0 : x.summation_variables() = result_summation_variables;
369 0 : data::data_expression result_condition;
370 0 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
371 0 : x.condition() = result_condition;
372 0 : static_cast<Derived&>(*this).update(x.deadlock());
373 0 : static_cast<Derived&>(*this).leave(x);
374 0 : }
375 :
376 14 : void update(lps::action_summand& x)
377 : {
378 14 : static_cast<Derived&>(*this).enter(x);
379 14 : data::variable_list result_summation_variables;
380 14 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
381 14 : x.summation_variables() = result_summation_variables;
382 14 : data::data_expression result_condition;
383 14 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
384 14 : x.condition() = result_condition;
385 28 : lps::multi_action result_multi_action;
386 14 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
387 14 : x.multi_action() = result_multi_action;
388 14 : data::assignment_list result_assignments;
389 14 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
390 14 : x.assignments() = result_assignments;
391 14 : static_cast<Derived&>(*this).leave(x);
392 14 : }
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 102 : void apply(T& result, const lps::stochastic_distribution& x)
427 : {
428 :
429 102 : static_cast<Derived&>(*this).enter(x);
430 306 : 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 102 : static_cast<Derived&>(*this).leave(x);
432 102 : }
433 :
434 0 : void update(lps::stochastic_action_summand& x)
435 : {
436 0 : static_cast<Derived&>(*this).enter(x);
437 0 : data::variable_list result_summation_variables;
438 0 : static_cast<Derived&>(*this).apply(result_summation_variables, x.summation_variables());
439 0 : x.summation_variables() = result_summation_variables;
440 0 : data::data_expression result_condition;
441 0 : static_cast<Derived&>(*this).apply(result_condition, x.condition());
442 0 : x.condition() = result_condition;
443 0 : lps::multi_action result_multi_action;
444 0 : static_cast<Derived&>(*this).apply(result_multi_action, x.multi_action());
445 0 : x.multi_action() = result_multi_action;
446 0 : data::assignment_list result_assignments;
447 0 : static_cast<Derived&>(*this).apply(result_assignments, x.assignments());
448 0 : x.assignments() = result_assignments;
449 0 : stochastic_distribution result_distribution;
450 0 : static_cast<Derived&>(*this).apply(result_distribution, x.distribution());
451 0 : x.distribution() = result_distribution;
452 0 : static_cast<Derived&>(*this).leave(x);
453 0 : }
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 :
488 : /// \\brief Builder class
489 : template <typename Derived>
490 : struct 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
|
