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/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
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
184/// \\brief Builder class
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
328/// \\brief Builder class
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
488/// \\brief Builder class
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::aterm_string::operator=
aterm_string & operator=(const aterm_string &t) noexcept=default
atermpp::aterm::operator[]
const aterm & operator[](const size_type i) const
Returns the i-th argument.
Definition aterm.h:187
atermpp::aterm::function
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
atermpp::function_symbol
Definition function_symbol.h:25
atermpp::function_symbol::operator==
bool operator==(const function_symbol &f) const
Equality test.
Definition function_symbol.h:74
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:24
atermpp::unprotected_aterm_core::swap
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
atermpp::unprotected_aterm_core::operator==
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
atermpp::unprotected_aterm_core::defined
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
Definition aterm_core.h:143
atermpp::unprotected_aterm_core::operator!=
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
mcrl2::data::abstraction
An abstraction expression.
Definition abstraction.h:26
mcrl2::data::abstraction::variables
const variable_list & variables() const
Definition abstraction.h:63
mcrl2::data::abstraction::body
const data_expression & body() const
Definition abstraction.h:68
mcrl2::data::abstraction::binding_operator
const binder_type & binding_operator() const
Definition abstraction.h:58
mcrl2::data::alias
\brief A sort alias
Definition alias.h:26
mcrl2::data::alias::alias
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:42
mcrl2::data::assignment
\brief Assignment of a data expression to a variable
Definition assignment.h:91
mcrl2::data::assignment::rhs
const data_expression & rhs() const
Definition assignment.h:122
mcrl2::data::assignment::lhs
const variable & lhs() const
Definition assignment.h:117
mcrl2::data::basic_sort
\brief A basic sort
Definition basic_sort.h:26
mcrl2::data::data_expression
data expression.
Definition data_expression.h:131
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:134
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:108
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:48
mcrl2::data::data_specification::constructors
const function_symbol_vector & constructors(const sort_expression &s, const bool do_not_normalize=false) const
Gets all constructors of a sort including those that are system defined.
Definition data_specification.h:356
mcrl2::data::detail::inequality_consistency_cache
Definition linear_inequalities.h:1460
mcrl2::data::detail::inequality_consistency_cache::~inequality_consistency_cache
~inequality_consistency_cache()
Definition linear_inequalities.h:1474
mcrl2::data::detail::inequality_consistency_cache::inequality_consistency_cache
inequality_consistency_cache()
Definition linear_inequalities.h:1469
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:1513
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::m_cache
inequality_inconsistency_cache_base * m_cache
Definition linear_inequalities.h:1462
mcrl2::data::detail::inequality_consistency_cache::is_consistent
bool is_consistent(const std::vector< linear_inequality > &inequalities_in_) const
Definition linear_inequalities.h:1483
mcrl2::data::detail::inequality_inconsistency_cache_base
Definition linear_inequalities.h:1308
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_present_branch
inequality_inconsistency_cache_base * m_present_branch
Definition linear_inequalities.h:1315
mcrl2::data::detail::inequality_inconsistency_cache_base::m_inequality
linear_inequality m_inequality
Definition linear_inequalities.h:1314
mcrl2::data::detail::inequality_inconsistency_cache_base::m_non_present_branch
inequality_inconsistency_cache_base * m_non_present_branch
Definition linear_inequalities.h:1316
mcrl2::data::detail::inequality_inconsistency_cache_base::inequality_inconsistency_cache_base
inequality_inconsistency_cache_base(const node_type node, const linear_inequality &inequality, inequality_inconsistency_cache_base *present_branch, inequality_inconsistency_cache_base *non_present_branch)
Definition linear_inequalities.h:1327
mcrl2::data::detail::inequality_inconsistency_cache_base::~inequality_inconsistency_cache_base
~inequality_inconsistency_cache_base()
Definition linear_inequalities.h:1338
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:1313
mcrl2::data::detail::inequality_inconsistency_cache_base::inequality_inconsistency_cache_base
inequality_inconsistency_cache_base(const node_type node)
Definition linear_inequalities.h:1323
mcrl2::data::detail::inequality_inconsistency_cache
Definition linear_inequalities.h:1352
mcrl2::data::detail::inequality_inconsistency_cache::~inequality_inconsistency_cache
~inequality_inconsistency_cache()
Definition linear_inequalities.h:1365
mcrl2::data::detail::inequality_inconsistency_cache::is_inconsistent
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in_) const
Definition linear_inequalities.h:1373
mcrl2::data::detail::inequality_inconsistency_cache::inequality_inconsistency_cache
inequality_inconsistency_cache()
Definition linear_inequalities.h:1361
mcrl2::data::detail::inequality_inconsistency_cache::operator=
inequality_inconsistency_cache & operator=(const inequality_consistency_cache &)=delete
mcrl2::data::detail::inequality_inconsistency_cache::m_cache
inequality_inconsistency_cache_base * m_cache
Definition linear_inequalities.h:1354
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:1401
mcrl2::data::detail::lhs_t
Definition linear_inequalities.h:175
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const aterm &t)
Constructor from an aterm.
Definition linear_inequalities.h:183
mcrl2::data::detail::lhs_t::operator[]
const data_expression & operator[](const variable &v) const
Give the factor of variable v.
Definition linear_inequalities.h:223
mcrl2::data::detail::lhs_t::transform_to_data_expression
data_expression transform_to_data_expression() const
Definition linear_inequalities.h:267
mcrl2::data::detail::lhs_t::erase
lhs_t erase(const variable &v) const
Erase a variable and its factor.
Definition linear_inequalities.h:209
mcrl2::data::detail::lhs_t::count
std::size_t count(const variable &v) const
Give the factor of variable v.
Definition linear_inequalities.h:234
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
Constructor.
Definition linear_inequalities.h:195
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:246
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:200
mcrl2::data::detail::lhs_t::lhs_t
lhs_t(const ITERATOR begin, const ITERATOR end)
Constructor.
Definition linear_inequalities.h:189
mcrl2::data::detail::lhs_t::lhs_t
lhs_t()
Constructor.
Definition linear_inequalities.h:178
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:26
mcrl2::data::function_symbol
\brief A function symbol
Definition function_symbol.h:28
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:49
mcrl2::data::linear_inequality
Definition linear_inequalities.h:557
mcrl2::data::linear_inequality::lhs
const detail::lhs_t & lhs() const
Definition linear_inequalities.h:772
mcrl2::data::linear_inequality::invert
linear_inequality invert(const rewriter &r)
Definition linear_inequalities.h:877
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:833
mcrl2::data::linear_inequality::linear_inequality
linear_inequality()
Constructor yielding an inconsistent inequality.
Definition linear_inequalities.h:639
mcrl2::data::linear_inequality::is_true
bool is_true(const rewriter &r) const
Definition linear_inequalities.h:823
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:816
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:723
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:675
mcrl2::data::linear_inequality::transform_to_data_expression
data_expression transform_to_data_expression() const
Definition linear_inequalities.h:801
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:567
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:644
mcrl2::data::linear_inequality::lhs_begin
detail::lhs_t::const_iterator lhs_begin() const
Definition linear_inequalities.h:762
mcrl2::data::linear_inequality::lhs_end
detail::lhs_t::const_iterator lhs_end() const
Definition linear_inequalities.h:767
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:655
mcrl2::data::linear_inequality::rhs
const data_expression & rhs() const
Definition linear_inequalities.h:777
mcrl2::data::linear_inequality::get_factor_for_a_variable
data_expression get_factor_for_a_variable(const variable &x)
Definition linear_inequalities.h:782
mcrl2::data::linear_inequality::comparison
detail::comparison_t comparison() const
Definition linear_inequalities.h:787
mcrl2::data::maintain_variables_in_rhs::assignment
Wrapper class for internal storage and substitution updates using operator()
Definition maintain_variables_in_rhs.h:54
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:58
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:67
mcrl2::data::maintain_variables_in_rhs::assignment::m_variable
const variable_type & m_variable
Definition maintain_variables_in_rhs.h:56
mcrl2::data::maintain_variables_in_rhs::assignment::m_scratch_set
std::set< variable_type > & m_scratch_set
Definition maintain_variables_in_rhs.h:59
mcrl2::data::maintain_variables_in_rhs::assignment::operator=
void operator=(const expression_type &e)
Actual assignment.
Definition maintain_variables_in_rhs.h:78
mcrl2::data::maintain_variables_in_rhs::assignment::m_sigma
Substitution & m_sigma
Definition maintain_variables_in_rhs.h:57
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:36
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:127
mcrl2::data::maintain_variables_in_rhs::operator[]
assignment operator[](variable_type const &v)
Assigment operator.
Definition maintain_variables_in_rhs.h:107
mcrl2::data::maintain_variables_in_rhs::clear
void clear()
Clear substitutions.
Definition maintain_variables_in_rhs.h:113
mcrl2::data::maintain_variables_in_rhs::super
Substitution super
Definition maintain_variables_in_rhs.h:38
mcrl2::data::maintain_variables_in_rhs::m_scratch_set
std::set< variable_type > m_scratch_set
Definition maintain_variables_in_rhs.h:44
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:120
mcrl2::data::maintain_variables_in_rhs::expression_type
super::expression_type expression_type
Definition maintain_variables_in_rhs.h:40
mcrl2::data::maintain_variables_in_rhs::m_variables_in_rhs
std::multiset< variable_type > m_variables_in_rhs
Definition maintain_variables_in_rhs.h:43
mcrl2::data::maintain_variables_in_rhs::maintain_variables_in_rhs
maintain_variables_in_rhs()
Default constructor.
Definition maintain_variables_in_rhs.h:48
mcrl2::data::maintain_variables_in_rhs::variable_type
super::variable_type variable_type
Definition maintain_variables_in_rhs.h:39
mcrl2::data::representative_generator
Components for generating an arbitrary element of a sort.
Definition representative_generator.h:53
mcrl2::data::representative_generator::operator()
data_expression operator()(const sort_expression &sort)
Returns a representative of a sort.
Definition representative_generator.h:269
mcrl2::data::rewriter
Rewriter that operates on data expressions.
Definition rewriter.h:81
mcrl2::data::rewriter::operator()
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Definition rewriter.h:158
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:30
mcrl2::data::set_identifier_generator::add_identifier
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
Definition set_identifier_generator.h:48
mcrl2::data::sort_expression
\brief A sort expression
Definition sort_expression.h:63
mcrl2::data::sort_expression::operator=
sort_expression & operator=(const sort_expression &) noexcept=default
mcrl2::data::structured_sort_constructor_argument
\brief An argument of a constructor of a structured sort
Definition structured_sort_constructor_argument.h:26
mcrl2::data::structured_sort_constructor
\brief A constructor for a structured sort
Definition structured_sort_constructor.h:29
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:154
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:183
mcrl2::data::structured_sort
structured sort.
Definition structured_sort.h:56
mcrl2::data::variable
\brief A data variable
Definition variable.h:28
mcrl2::data::variable::variable
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:69
mcrl2::data::variable::name
const core::identifier_string & name() const
Definition variable.h:38
mcrl2::data::variable::operator=
variable & operator=(variable &&) noexcept=default
mcrl2::data::variable::sort
const sort_expression & sort() const
Definition variable.h:43
mcrl2::data::variable::operator=
variable & operator=(const variable &) noexcept=default
mcrl2::data::where_clause
\brief A where expression
Definition where_clause.h:26
mcrl2::data::where_clause::where_clause
where_clause(const atermpp::aterm &term)
Definition where_clause.h:35
mcrl2::log::logger::logger
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
mcrl2::lps::action_summand
LPS summand containing a multi-action.
Definition action_summand.h:25
mcrl2::lps::action_summand::has_time
bool has_time() const
Returns true if time is available.
Definition action_summand.h:90
mcrl2::lps::constelm_algorithm
Algorithm class for elimination of constant parameters.
Definition constelm.h:26
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:62
mcrl2::lps::constelm_algorithm::super
lps::detail::lps_algorithm< Specification > super
Definition constelm.h:27
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:97
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:234
mcrl2::lps::constelm_algorithm::R
const DataRewriter & R
The rewriter used by the constelm algorithm.
Definition constelm.h:41
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:43
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:35
mcrl2::lps::constelm_algorithm::constelm_algorithm
constelm_algorithm(Specification &spec, const DataRewriter &R_)
Constructor.
Definition constelm.h:114
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:79
mcrl2::lps::constelm_algorithm::run
void run(bool instantiate_global_variables=false, bool ignore_conditions=false)
Runs the constelm algorithm.
Definition constelm.h:259
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:38
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:125
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:32
mcrl2::lps::deadlock_summand
LPS summand containing a deadlock.
Definition deadlock_summand.h:25
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:40
mcrl2::lps::deadlock
Represents a deadlock.
Definition deadlock.h:26
mcrl2::lps::deadlock::deadlock
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:36
mcrl2::lps::deadlock::time
data::data_expression & time()
Returns the time.
Definition deadlock.h:56
mcrl2::lps::detail::lps_algorithm
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
Definition lps_algorithm.h:32
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:112
mcrl2::lps::detail::lps_algorithm::remove_unused_summand_variables
void remove_unused_summand_variables()
Removes unused summand variables.
Definition lps_algorithm.h:130
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:37
mcrl2::lps::detail::lps_algorithm::summand_remove_unused_summand_variables
void summand_remove_unused_summand_variables(SummandType &summand_)
Definition lps_algorithm.h:63
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:51
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:91
mcrl2::lps::detail::lps_algorithm::verbose
bool verbose() const
Flag for verbose output.
Definition lps_algorithm.h:85
mcrl2::lps::detail::lps_algorithm::remove_singleton_sorts
void remove_singleton_sorts()
Removes parameters with a singleton sort.
Definition lps_algorithm.h:118
mcrl2::lps::detail::lps_algorithm::remove_trivial_summands
void remove_trivial_summands()
Removes summands with condition equal to false.
Definition lps_algorithm.h:124
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:106
mcrl2::lps::detail::lps_algorithm::lps_algorithm
lps_algorithm(Specification &spec)
Constructor.
Definition lps_algorithm.h:80
mcrl2::lps::detail::lps_algorithm::m_spec
Specification & m_spec
The specification that is processed by the algorithm.
Definition lps_algorithm.h:35
mcrl2::lps::detail::ultimate_delay
Definition ultimate_delay.h:33
mcrl2::lps::detail::ultimate_delay::ultimate_delay
ultimate_delay()
Constructor.
Definition ultimate_delay.h:41
mcrl2::lps::detail::ultimate_delay::constraint
data_expression & constraint()
Obtain a reference to the constraint.
Definition ultimate_delay.h:80
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::multi_action::operator=
multi_action & operator=(const 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.
Definition multi_action.h:51
mcrl2::lps::process_initializer
A process initializer.
Definition process_initializer.h:29
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::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:34
mcrl2::lps::stochastic_action_summand::distribution
stochastic_distribution & distribution()
Returns the distribution of this summand.
Definition stochastic_action_summand.h:57
mcrl2::lps::stochastic_distribution
\brief A stochastic distribution
Definition stochastic_distribution.h:24
mcrl2::lps::stochastic_distribution::operator=
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
mcrl2::lps::stochastic_distribution::stochastic_distribution
stochastic_distribution()
\brief Default constructor X3.
Definition stochastic_distribution.h:27
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::stochastic_distribution
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
Definition stochastic_distribution.h:40
mcrl2::lps::stochastic_distribution::operator=
stochastic_distribution & operator=(const stochastic_distribution &) noexcept=default
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_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:66
mcrl2::lps::stochastic_process_initializer
A stochastic process initializer.
Definition stochastic_process_initializer.h:23
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:41
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
Base class for LPS summands.
Definition summand.h:25
mcrl2::lps::summand_base::condition
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
mcrl2::process::action_label
\brief An action label
Definition action_label.h:26
mcrl2::process::action_label::name
const core::identifier_string & name() const
Definition action_label.h:57
mcrl2::process::action::action
action(const atermpp::aterm &term)
Definition process_expression.h:150
mcrl2::process::action::arguments
const data::data_expression_list & arguments() const
Definition process_expression.h:172
mcrl2::process::action::label
const action_label & label() const
Definition process_expression.h:167
mcrl2::process::allow
\brief The allow operator
Definition process_expression.h:861
mcrl2::process::allow::allow
allow(const atermpp::aterm &term)
Definition process_expression.h:870
mcrl2::process::allow::operand
const process_expression & operand() const
Definition process_expression.h:892
mcrl2::process::at
\brief The at operator
Definition process_expression.h:1013
mcrl2::process::at::at
at(const atermpp::aterm &term)
Definition process_expression.h:1022
mcrl2::process::at::at
at(const process_expression &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
Definition process_expression.h:1029
mcrl2::process::at::time_stamp
const data::data_expression & time_stamp() const
Definition process_expression.h:1044
mcrl2::process::at::operand
const process_expression & operand() const
Definition process_expression.h:1039
mcrl2::process::block
\brief The block operator
Definition process_expression.h:557
mcrl2::process::block::operand
const process_expression & operand() const
Definition process_expression.h:588
mcrl2::process::block::block
block(const atermpp::aterm &term)
Definition process_expression.h:566
mcrl2::process::choice
\brief The choice operator
Definition process_expression.h:1550
mcrl2::process::choice::choice
choice(const atermpp::aterm &term)
Definition process_expression.h:1559
mcrl2::process::choice::left
const process_expression & left() const
Definition process_expression.h:1576
mcrl2::process::choice::choice
choice(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1566
mcrl2::process::choice::right
const process_expression & right() const
Definition process_expression.h:1581
mcrl2::process::comm
\brief The communication operator
Definition process_expression.h:785
mcrl2::process::comm::comm
comm(const atermpp::aterm &term)
Definition process_expression.h:794
mcrl2::process::comm::operand
const process_expression & operand() const
Definition process_expression.h:816
mcrl2::process::delta
\brief The value delta
Definition process_expression.h:375
mcrl2::process::delta::delta
delta()
\brief Default constructor X3.
Definition process_expression.h:378
mcrl2::process::hide
\brief The hide operator
Definition process_expression.h:633
mcrl2::process::hide::hide
hide(const atermpp::aterm &term)
Definition process_expression.h:642
mcrl2::process::hide::hide_set
const core::identifier_string_list & hide_set() const
Definition process_expression.h:659
mcrl2::process::hide::operand
const process_expression & operand() const
Definition process_expression.h:664
mcrl2::process::if_then_else
\brief The if-then-else operator
Definition process_expression.h:1241
mcrl2::process::if_then_else::else_case
const process_expression & else_case() const
Definition process_expression.h:1277
mcrl2::process::if_then_else::then_case
const process_expression & then_case() const
Definition process_expression.h:1272
mcrl2::process::if_then_else::if_then_else
if_then_else(const atermpp::aterm &term)
Definition process_expression.h:1250
mcrl2::process::if_then_else::condition
const data::data_expression & condition() const
Definition process_expression.h:1267
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:1257
mcrl2::process::if_then
\brief The if-then operator
Definition process_expression.h:1165
mcrl2::process::if_then::then_case
const process_expression & then_case() const
Definition process_expression.h:1196
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:1181
mcrl2::process::if_then::if_then
if_then(const atermpp::aterm &term)
Definition process_expression.h:1174
mcrl2::process::if_then::condition
const data::data_expression & condition() const
Definition process_expression.h:1191
mcrl2::process::merge
\brief The merge operator
Definition process_expression.h:1398
mcrl2::process::merge::merge
merge(const atermpp::aterm &term)
Definition process_expression.h:1407
mcrl2::process::merge::right
const process_expression & right() const
Definition process_expression.h:1429
mcrl2::process::merge::left
const process_expression & left() const
Definition process_expression.h:1424
mcrl2::process::process_expression
\brief A process expression
Definition process_expression.h:31
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:34
mcrl2::process::process_expression::operator=
process_expression & operator=(process_expression &&) noexcept=default
mcrl2::process::process_identifier
\brief A process identifier
Definition process_identifier.h:26
mcrl2::process::process_identifier::process_identifier
process_identifier(const process_identifier &) noexcept=default
Move semantics.
mcrl2::process::process_identifier::operator=
process_identifier & operator=(const process_identifier &) noexcept=default
mcrl2::process::process_identifier::name
const core::identifier_string & name() const
Definition process_identifier.h:36
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:47
mcrl2::process::process_identifier::process_identifier
process_identifier(const std::string &name, const data::variable_list &variables)
Constructor.
Definition process_identifier.h:66
mcrl2::process::process_identifier::process_identifier
process_identifier(const atermpp::aterm &term)
Constructor.
Definition process_identifier.h:53
mcrl2::process::process_instance_assignment
\brief A process assignment
Definition process_expression.h:299
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:315
mcrl2::process::process_instance_assignment::assignments
const data::assignment_list & assignments() const
Definition process_expression.h:330
mcrl2::process::process_instance_assignment::process_instance_assignment
process_instance_assignment(const atermpp::aterm &term)
Definition process_expression.h:308
mcrl2::process::process_instance_assignment::identifier
const process_identifier & identifier() const
Definition process_expression.h:325
mcrl2::process::process_instance
\brief A process
Definition process_expression.h:223
mcrl2::process::process_instance::actual_parameters
const data::data_expression_list & actual_parameters() const
Definition process_expression.h:254
mcrl2::process::process_instance::identifier
const process_identifier & identifier() const
Definition process_expression.h:249
mcrl2::process::process_specification
Process specification consisting of a data specification, action labels, a sequence of process equati...
Definition process_specification.h:52
mcrl2::process::process_specification::init
process_expression & init()
Returns the initialization of the process specification.
Definition process_specification.h:185
mcrl2::process::process_specification::action_labels
process::action_label_list & action_labels()
Returns the action label specification.
Definition process_specification.h:143
mcrl2::process::rename
\brief The rename operator
Definition process_expression.h:709
mcrl2::process::rename::rename
rename(const atermpp::aterm &term)
Definition process_expression.h:718
mcrl2::process::rename::operand
const process_expression & operand() const
Definition process_expression.h:740
mcrl2::process::rename::rename_set
const rename_expression_list & rename_set() const
Definition process_expression.h:735
mcrl2::process::seq
\brief The sequential composition
Definition process_expression.h:1089
mcrl2::process::seq::right
const process_expression & right() const
Definition process_expression.h:1120
mcrl2::process::seq::seq
seq(const atermpp::aterm &term)
Definition process_expression.h:1098
mcrl2::process::seq::left
const process_expression & left() const
Definition process_expression.h:1115
mcrl2::process::seq::seq
seq(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:1105
mcrl2::process::stochastic_operator
\brief The distribution operator
Definition process_expression.h:1626
mcrl2::process::stochastic_operator::variables
const data::variable_list & variables() const
Definition process_expression.h:1652
mcrl2::process::stochastic_operator::distribution
const data::data_expression & distribution() const
Definition process_expression.h:1657
mcrl2::process::stochastic_operator::operand
const process_expression & operand() const
Definition process_expression.h:1662
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:1642
mcrl2::process::sum
\brief The sum operator
Definition process_expression.h:481
mcrl2::process::sum::operand
const process_expression & operand() const
Definition process_expression.h:512
mcrl2::process::sum::sum
sum(const data::variable_list &variables, const process_expression &operand)
\brief Constructor Z14.
Definition process_expression.h:497
mcrl2::process::sum::sum
sum(const atermpp::aterm &term)
Definition process_expression.h:490
mcrl2::process::sum::variables
const data::variable_list & variables() const
Definition process_expression.h:507
mcrl2::process::sync
\brief The synchronization operator
Definition process_expression.h:937
mcrl2::process::sync::left
const process_expression & left() const
Definition process_expression.h:963
mcrl2::process::sync::sync
sync(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
Definition process_expression.h:953
mcrl2::process::sync::right
const process_expression & right() const
Definition process_expression.h:968
mcrl2::process::sync::sync
sync(const atermpp::aterm &term)
Definition process_expression.h:946
mcrl2::process::tau
\brief The value tau
Definition process_expression.h:428
mcrl2::process::tau::tau
tau()
\brief Default constructor X3.
Definition process_expression.h:431
mcrl2::runtime_error
Standard exception class for reporting runtime errors.
Definition exception.h:27
objectdatatype::processbody
process_expression processbody
Definition linearise.cpp:106
objectdatatype::objectdatatype
objectdatatype(const objectdatatype &o)=default
objectdatatype::representedprocess
process_expression representedprocess
Definition linearise.cpp:103
objectdatatype::old_parameters
variable_list old_parameters
Definition linearise.cpp:110
objectdatatype::free_variables_defined
bool free_variables_defined
Definition linearise.cpp:108
objectdatatype::~objectdatatype
~objectdatatype()=default
objectdatatype::multi_action_names
process::action_label_list multi_action_names
Definition linearise.cpp:101
objectdatatype::processstatus
processstatustype processstatus
Definition linearise.cpp:111
objectdatatype::objectname
identifier_string objectname
Definition linearise.cpp:100
objectdatatype::objectdatatype
objectdatatype()=default
objectdatatype::operator=
objectdatatype & operator=(const objectdatatype &o)=default
objectdatatype::object
objecttype object
Definition linearise.cpp:112
objectdatatype::free_variables
std::set< variable > free_variables
Definition linearise.cpp:107
objectdatatype::process_representing_action
process_identifier process_representing_action
Definition linearise.cpp:104
objectdatatype::parameters
variable_list parameters
Definition linearise.cpp:109
specification_basic_type::enumeratedtype
Definition linearise.cpp:5521
specification_basic_type::enumeratedtype::functions
function_symbol_list functions
Definition linearise.cpp:5526
specification_basic_type::enumeratedtype::elementnames
data_expression_list elementnames
Definition linearise.cpp:5525
specification_basic_type::enumeratedtype::~enumeratedtype
~enumeratedtype()
Definition linearise.cpp:5582
specification_basic_type::enumeratedtype::enumeratedtype
enumeratedtype(const enumeratedtype &e)
Definition linearise.cpp:5566
specification_basic_type::enumeratedtype::size
std::size_t size
Definition linearise.cpp:5523
specification_basic_type::enumeratedtype::enumeratedtype
enumeratedtype(const std::size_t n, specification_basic_type &spec)
Definition linearise.cpp:5528
specification_basic_type::enumeratedtype::operator=
void operator=(const enumeratedtype &e)
Definition linearise.cpp:5574
specification_basic_type::enumeratedtype::sortId
sort_expression sortId
Definition linearise.cpp:5524
specification_basic_type::enumtype
Definition linearise.cpp:5716
specification_basic_type::enumtype::enumtype
enumtype(const enumtype &)=delete
specification_basic_type::enumtype::operator=
enumtype & operator=(const enumtype &)=delete
specification_basic_type::enumtype::enumeratedtype_index
std::size_t enumeratedtype_index
Definition linearise.cpp:5722
specification_basic_type::enumtype::var
variable var
Definition linearise.cpp:5723
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:5725
specification_basic_type::enumtype::~enumtype
~enumtype()
Definition linearise.cpp:5753
specification_basic_type::process_pid_pair
Definition linearise.cpp:4062
specification_basic_type::process_pid_pair::m_pid
process_identifier m_pid
Definition linearise.cpp:4065
specification_basic_type::process_pid_pair::m_process_body
process_expression m_process_body
Definition linearise.cpp:4064
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:4077
specification_basic_type::process_pid_pair::process_id
const process_identifier & process_id() const
Definition linearise.cpp:4082
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:4068
specification_basic_type::process_pid_pair::process_pid_pair
process_pid_pair(process_pid_pair &&other)=default
specification_basic_type::stacklisttype
Definition linearise.cpp:4302
specification_basic_type::stacklisttype::booleanStateVariables
variable_list booleanStateVariables
Definition linearise.cpp:4311
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:4323
specification_basic_type::stacklisttype::opns
stackoperations * opns
Definition linearise.cpp:4304
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:4307
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:4339
specification_basic_type::stacklisttype::~stacklisttype
~stacklisttype()
Definition linearise.cpp:4416
specification_basic_type::stacklisttype::parameters
variable_list parameters
Definition linearise.cpp:4305
specification_basic_type::stacklisttype::stacklisttype
stacklisttype(const stacklisttype &)=delete
specification_basic_type::stacklisttype::stackvar
variable stackvar
Definition linearise.cpp:4306
specification_basic_type::stackoperations
Definition linearise.cpp:4240
specification_basic_type::stackoperations::~stackoperations
~stackoperations()
Definition linearise.cpp:4296
specification_basic_type::stackoperations::operator=
stackoperations & operator=(const stackoperations &)=delete
specification_basic_type::stackoperations::pop
data::function_symbol pop
Definition linearise.cpp:4249
specification_basic_type::stackoperations::push
data::function_symbol push
Definition linearise.cpp:4246
specification_basic_type::stackoperations::stackoperations
stackoperations(const stackoperations &)=delete
specification_basic_type::stackoperations::sorts
sort_expression_list sorts
Definition linearise.cpp:4244
specification_basic_type::stackoperations::empty
data::function_symbol empty
Definition linearise.cpp:4248
specification_basic_type::stackoperations::getstate
data::function_symbol getstate
Definition linearise.cpp:4250
specification_basic_type::stackoperations::parameter_list
variable_list parameter_list
Definition linearise.cpp:4242
specification_basic_type::stackoperations::next
stackoperations * next
Definition linearise.cpp:4251
specification_basic_type::stackoperations::get
function_symbol_list get
Definition linearise.cpp:4245
specification_basic_type::stackoperations::emptystack
data::function_symbol emptystack
Definition linearise.cpp:4247
specification_basic_type::stackoperations::stackoperations
stackoperations(const variable_list &pl, specification_basic_type &spec)
Definition linearise.cpp:4257
specification_basic_type::stackoperations::stacksort
sort_expression stacksort
Definition linearise.cpp:4243
specification_basic_type
Definition linearise.cpp:124
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:3533
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:6044
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:7595
specification_basic_type::parscollect
variable_list parscollect(const process_expression &oldbody, process_expression &newbody)
Definition linearise.cpp:3151
specification_basic_type::linMergeMultiActionList
action_list linMergeMultiActionList(const action_list &ma1, const action_list &ma2)
Definition linearise.cpp:775
specification_basic_type::objectIndex
const objectdatatype & objectIndex(const aterm &o) const
Definition linearise.cpp:296
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:7106
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:2209
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:2262
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:5989
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:3946
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:3371
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:5454
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:4783
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:8208
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:759
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:346
specification_basic_type::guarantee_that_parameters_have_unique_type_body
process_expression guarantee_that_parameters_have_unique_type_body(const process_expression &t, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)
Definition linearise.cpp:10040
specification_basic_type::hide_
static action_list hide_(const identifier_string_list &hidelist, const action_list &multiaction)
Definition linearise.cpp:7231
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:5023
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:5616
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:158
specification_basic_type::canterminatebody
bool canterminatebody(const process_expression &t)
Definition linearise.cpp:9693
specification_basic_type::transform_matching_list
data_expression transform_matching_list(const variable_list &matchinglist)
Definition linearise.cpp:5892
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:5232
specification_basic_type::isDeltaAtZero
bool isDeltaAtZero(const process_expression &t)
Definition linearise.cpp:252
specification_basic_type::find_case_function
data::function_symbol find_case_function(std::size_t index, const sort_expression &sort) const
Definition linearise.cpp:5600
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:5134
specification_basic_type::summandsCanBeClustered
static bool summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
Definition linearise.cpp:6055
specification_basic_type::getActionSorts
static sort_expression_list getActionSorts(const action_list &actionlist)
Definition linearise.cpp:6980
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:1305
specification_basic_type::collect_sum_arg_arg_cond
stochastic_action_summand collect_sum_arg_arg_cond(const enumtype &e, std::size_t n, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
Definition linearise.cpp:6103
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:3900
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:7370
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:2078
specification_basic_type::make_pCRL_procs
void make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)
Definition linearise.cpp:3823
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:1204
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:5126
specification_basic_type::procstorealGNFrec
void procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)
Definition linearise.cpp:3731
specification_basic_type::getnames
static action_label_list getnames(const process_expression &multiAction)
Definition linearise.cpp:352
specification_basic_type::getparameters_rec
variable_list getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)
Definition linearise.cpp:390
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:3055
specification_basic_type::detail_check_objectdata
void detail_check_objectdata(const aterm &o) const
Definition linearise.cpp:276
specification_basic_type::argscollect_regular2
assignment_list argscollect_regular2(const process_expression &t, variable_list &vl)
Definition linearise.cpp:3216
specification_basic_type::guarantee_that_parameters_have_unique_type
void guarantee_that_parameters_have_unique_type(const process_identifier &procId, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)
Definition linearise.cpp:9983
specification_basic_type::fresh_equation_added
bool fresh_equation_added
Definition linearise.cpp:160
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:7747
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:10207
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:8337
specification_basic_type::occursintermlist
bool occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) const
Definition linearise.cpp:1266
specification_basic_type::transform_process_arguments
void transform_process_arguments(const process_identifier &procId)
Definition linearise.cpp:9833
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:3922
specification_basic_type::canterminate_rec
bool canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)
Definition linearise.cpp:9673
specification_basic_type::fresh_identifier_generator
set_identifier_generator fresh_identifier_generator
Definition linearise.cpp:165
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:4096
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:1293
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:731
specification_basic_type::splitmCRLandpCRLprocsAndAddTerminatedAction
process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)
Definition linearise.cpp:10316
specification_basic_type::linMergeMultiActionListProcess
action_list linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)
Definition linearise.cpp:786
specification_basic_type::guarantee_that_parameters_have_unique_type
void guarantee_that_parameters_have_unique_type(const process_identifier &procId)
Definition linearise.cpp:10027
specification_basic_type::procs
std::vector< process_equation > procs
Definition linearise.cpp:142
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:4720
specification_basic_type::determinewhetherprocessescanterminate
void determinewhetherprocessescanterminate(const process_identifier &procId)
Definition linearise.cpp:9700
specification_basic_type::distribute_condition
process_expression distribute_condition(const process_expression &body1, const data_expression &condition)
Definition linearise.cpp:2799
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:9036
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:5491
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:4555
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:7954
specification_basic_type::determine_process_statusterm
processstatustype determine_process_statusterm(const process_expression &body, const processstatustype status)
Definition linearise.cpp:793
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:8053
specification_basic_type::getvar
data_expression getvar(const variable &var, const stacklisttype &stack) const
Definition linearise.cpp:4427
specification_basic_type::initdatavars
variable_list initdatavars
Definition linearise.cpp:129
specification_basic_type::find_free_variables_process
void find_free_variables_process(const process_expression &p, std::set< variable > &free_variables_in_p)
Definition linearise.cpp:1476
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:7726
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:3453
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:5088
specification_basic_type::to_action_list
static action_list to_action_list(const process_expression &p)
Definition linearise.cpp:324
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:8239
specification_basic_type::cut_off_unreachable_tail
process_expression cut_off_unreachable_tail(const process_expression &t)
Definition linearise.cpp:3258
specification_basic_type::enumeratedtypes
std::vector< enumeratedtype > enumeratedtypes
Definition linearise.cpp:166
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:4750
specification_basic_type::acts
process::action_label_list acts
Definition linearise.cpp:126
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:4877
specification_basic_type::hidecomposition
static void hidecomposition(const identifier_string_list &hidelist, stochastic_action_summand_vector &action_summands)
Definition linearise.cpp:7249
specification_basic_type::create_enumeratedtype
std::size_t create_enumeratedtype(const std::size_t n)
Definition linearise.cpp:5587
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:8674
specification_basic_type::expand_process_instance_assignment
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)
Definition linearise.cpp:9791
specification_basic_type::delta_at_zero
static process_expression delta_at_zero()
Definition linearise.cpp:247
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:4848
specification_basic_type::transform_process_arguments
void transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)
Definition linearise.cpp:9815
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:3986
specification_basic_type::terminationAction
action terminationAction
Definition linearise.cpp:148
specification_basic_type::collectPcrlProcesses
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
Definition linearise.cpp:1177
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:5962
specification_basic_type::SieveProcDataVarsAssignments
variable_list SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)
Definition linearise.cpp:10390
specification_basic_type::extend_conditions
data_expression_list extend_conditions(const variable &var, const data_expression_list &conditionlist)
Definition linearise.cpp:5871
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:1827
specification_basic_type::joinparameters
static variable_list joinparameters(const variable_list &par1, const variable_list &par2)
Definition linearise.cpp:4199
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:7821
specification_basic_type::addString
void addString(const identifier_string &str)
Definition linearise.cpp:302
specification_basic_type::procstovarheadGNF
void procstovarheadGNF(const std::vector< process_identifier > &procs)
Definition linearise.cpp:2687
specification_basic_type::action_list_to_process
static process_expression action_list_to_process(const action_list &ma)
Definition linearise.cpp:308
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:2958
specification_basic_type::collectparameterlist
variable_list collectparameterlist(const std::set< process_identifier > &pCRLprocs)
Definition linearise.cpp:4220
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:9338
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:4906
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:7921
specification_basic_type::stochastic_operator_is_being_used
bool stochastic_operator_is_being_used
Definition linearise.cpp:159
specification_basic_type::declare_control_state
void declare_control_state(const std::set< process_identifier > &pCRLprocs)
Definition linearise.cpp:4233
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:5667
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:10344
specification_basic_type::extend
static data_expression_list extend(const data_expression &c, const data_expression_list &cl)
Definition linearise.cpp:5851
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:7273
specification_basic_type::alt_state
@ alt_state
Definition linearise.cpp:2207
specification_basic_type::multiaction_state
@ multiaction_state
Definition linearise.cpp:2207
specification_basic_type::sum_state
@ sum_state
Definition linearise.cpp:2207
specification_basic_type::seq_state
@ seq_state
Definition linearise.cpp:2207
specification_basic_type::name_state
@ name_state
Definition linearise.cpp:2207
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:2344
specification_basic_type::terminatedProcId
process_identifier terminatedProcId
Definition linearise.cpp:149
specification_basic_type::distribute_sum
process_expression distribute_sum(const variable_list &sumvars, const process_expression &body1)
Definition linearise.cpp:3001
specification_basic_type::variables_are_equal_to_default_values
data_expression variables_are_equal_to_default_values(const variable_list &vl)
Definition linearise.cpp:5859
specification_basic_type::procstorealGNF
void procstorealGNF(const process_identifier &procsIdDecl, const bool regular)
Definition linearise.cpp:3795
specification_basic_type::check_assignment_list
static bool check_assignment_list(const assignment_list &assignments, const variable_list &parameters)
Definition linearise.cpp:1681
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:8882
specification_basic_type::all_equal
bool all_equal(const atermpp::term_list< T > &l)
Definition linearise.cpp:6026
specification_basic_type::alreadypresent
static bool alreadypresent(variable &var, const variable_list &vl)
Definition linearise.cpp:4172
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:6991
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:9097
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:3286
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:9841
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:2330
specification_basic_type::dummyparameterlist
assignment_list dummyparameterlist(const stacklisttype &stack, const bool singlestate)
Definition linearise.cpp:5178
specification_basic_type::rewr
mcrl2::data::rewriter rewr
Definition linearise.cpp:147
specification_basic_type::make_pCRL_procs
void make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)
Definition linearise.cpp:3834
specification_basic_type::stack_operations_list
stackoperations * stack_operations_list
Definition linearise.cpp:167
specification_basic_type::wraptime
process_expression wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)
Definition linearise.cpp:2129
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:9713
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:5771
specification_basic_type::occursintermlist
static bool occursintermlist(const variable &var, const data_expression_list &r)
Definition linearise.cpp:1254
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:3096
specification_basic_type::find_free_variables_process
std::set< variable > find_free_variables_process(const process_expression &p)
Definition linearise.cpp:1658
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:8745
specification_basic_type::terminating
@ terminating
Definition linearise.cpp:2712
specification_basic_type::infinite
@ infinite
Definition linearise.cpp:2712
specification_basic_type::putbehind
process_expression putbehind(const process_expression &body1, const process_expression &body2)
Definition linearise.cpp:2714
specification_basic_type::representedprocesses
std::vector< std::vector< process_instance_assignment > > representedprocesses
Definition linearise.cpp:155
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:1701
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:2013
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:152
specification_basic_type::objectIndex
objectdatatype & objectIndex(const aterm &o)
Definition linearise.cpp:290
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:5190
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:2058
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:2884
specification_basic_type::containstimebody
bool containstimebody(const process_expression &t)
Definition linearise.cpp:9068
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:4989
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:4622
specification_basic_type::processencoding
data_expression_list processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)
Definition linearise.cpp:4505
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:8422
specification_basic_type::~specification_basic_type
~specification_basic_type()
Definition linearise.cpp:215
specification_basic_type::make_pars
variable_list make_pars(const sort_expression_list &sortlist)
Definition linearise.cpp:2245
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:229
specification_basic_type::occursinpCRLterm
bool occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)
Definition linearise.cpp:1331
specification_basic_type::collectPcrlProcesses
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)
Definition linearise.cpp:1194
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:3116
specification_basic_type::objectdata
std::map< aterm, objectdatatype > objectdata
Definition linearise.cpp:161
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:4702
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:4936
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:170
specification_basic_type::getparameters
variable_list getparameters(const process_expression &multiAction)
Definition linearise.cpp:402
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:7397
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:1068
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:4738
specification_basic_type::processencoding
assignment_list processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)
Definition linearise.cpp:4452
specification_basic_type::addMultiAction
objectdatatype & addMultiAction(const process_expression &multiAction, bool &isnew)
Definition linearise.cpp:440
specification_basic_type::storeprocs
void storeprocs(const std::vector< process_equation > &procs)
Definition linearise.cpp:719
specification_basic_type::substitute_pCRLproc
process_expression substitute_pCRLproc(const process_expression &p, Substitution &sigma)
Definition linearise.cpp:1862
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:7615
specification_basic_type::get_free_variables
const std::set< variable > & get_free_variables(objectdatatype &object)
Definition linearise.cpp:468
specification_basic_type::global_variables
std::set< variable > global_variables
Definition linearise.cpp:127
specification_basic_type::getRHSassignment
static data_expression getRHSassignment(const variable &var, const assignment_list &as)
Definition linearise.cpp:6091
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:7302
specification_basic_type::determine_process_status
void determine_process_status(const process_identifier &procDecl, const processstatustype status)
Definition linearise.cpp:1032
specification_basic_type::makemultiaction
static action_list makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)
Definition linearise.cpp:420
specification_basic_type::insertvariables
void insertvariables(const variable_list &vars, const bool mustbenew)
Definition linearise.cpp:493
specification_basic_type::later
@ later
Definition linearise.cpp:2054
specification_basic_type::first
@ first
Definition linearise.cpp:2054
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:131
specification_basic_type::make_parameters_rec
variable_list make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)
Definition linearise.cpp:365
specification_basic_type::filter_assignments
static assignment_list filter_assignments(const assignment_list &assignments, const variable_list &parameters)
Definition linearise.cpp:1667
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:5927
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:8916
specification_basic_type::options
t_lin_options options
Definition linearise.cpp:157
specification_basic_type::sort_assignments
static assignment_list sort_assignments(const assignment_list &ass, const variable_list &parameters)
Definition linearise.cpp:1807
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:4804
specification_basic_type::tau_process
process_identifier tau_process
Definition linearise.cpp:151
specification_basic_type::get_sorts
static sort_expression_list get_sorts(const List &l)
Definition linearise.cpp:7364
specification_basic_type::seq_varnames
std::vector< process_identifier > seq_varnames
Definition linearise.cpp:153
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:4422
specification_basic_type::occursin
static bool occursin(const variable &name, const variable_list &pars)
Definition linearise.cpp:5008
specification_basic_type::canterminatebody
bool canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)
Definition linearise.cpp:9556
specification_basic_type::AddTerminationActionIfNecessary
void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)
Definition linearise.cpp:10326
specification_basic_type::determinewhetherprocessescontaintime
bool determinewhetherprocessescontaintime(const process_identifier &procId)
Definition linearise.cpp:9076
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:1317
specification_basic_type::addcondition
data_expression_list addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)
Definition linearise.cpp:5911
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:8112
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:10415
specification_basic_type::obtain_initial_distribution
process_expression obtain_initial_distribution(const process_identifier &procId)
Definition linearise.cpp:9531
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:268
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:9763
specification_basic_type::pushdummy_regular
assignment_list pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
Definition linearise.cpp:5056
specification_basic_type::sigma_variables
std::set< data::variable > sigma_variables(const SUBSTITUTION &sigma)
Definition linearise.cpp:502
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:3199
specification_basic_type::getarguments
static data_expression_list getarguments(const action_list &multiAction)
Definition linearise.cpp:409
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:7476
multiAction
@ multiAction
Definition linearise.cpp:76
GNFalpha
@ GNFalpha
Definition linearise.cpp:78
mCRLbusy
@ mCRLbusy
Definition linearise.cpp:73
mCRL
@ mCRL
Definition linearise.cpp:71
GNF
@ GNF
Definition linearise.cpp:77
mCRLlin
@ mCRLlin
Definition linearise.cpp:74
pCRL
@ pCRL
Definition linearise.cpp:75
mCRLdone
@ mCRLdone
Definition linearise.cpp:72
GNFbusy
@ GNFbusy
Definition linearise.cpp:79
unknown
@ unknown
Definition linearise.cpp:70
error
@ error
Definition linearise.cpp:80
func
@ func
Definition linearise.cpp:89
act
@ act
Definition linearise.cpp:90
sorttype
@ sorttype
Definition linearise.cpp:93
multiact
@ multiact
Definition linearise.cpp:94
proc
@ proc
Definition linearise.cpp:91
_map
@ _map
Definition linearise.cpp:88
none
@ none
Definition linearise.cpp:87
variable_
@ variable_
Definition linearise.cpp:92
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
atermpp
The main namespace for the aterm++ library.
Definition algorithm.h:21
mcrl2::core::identifier_string_list
atermpp::term_list< identifier_string > identifier_string_list
\brief list of identifier_strings
Definition identifier_string.h:30
mcrl2::core::identifier_string
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
Definition identifier_string.h:26
mcrl2::data::detail::linear_inequality_equal
atermpp::function_symbol linear_inequality_equal()
Definition linear_inequalities.h:548
mcrl2::data::detail::map_to_lhs_type
const lhs_t map_to_lhs_type(const map_based_lhs_t &lhs)
Definition linear_inequalities.h:333
mcrl2::data::detail::optimized_forall
void optimized_forall(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make a universal quantification.
Definition optimized_boolean_operators.h:212
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:230
mcrl2::data::detail::remove_variable_and_divide
const lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
Definition linear_inequalities.h:381
mcrl2::data::detail::negate_inequality
data_expression negate_inequality(const data_expression &e)
Definition linear_inequalities_utilities.h:28
mcrl2::data::detail::subtract
const lhs_t subtract(const lhs_t &argument, const lhs_t &e, const rewriter &r)
Definition linear_inequalities.h:498
mcrl2::data::detail::map_to_lhs_type
const lhs_t map_to_lhs_type(const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
Definition linear_inequalities.h:343
mcrl2::data::detail::optimized_exists
void optimized_exists(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make an existential quantification.
Definition optimized_boolean_operators.h:270
mcrl2::data::detail::optimized_or
void optimized_or(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a disjunction.
Definition optimized_boolean_operators.h:132
mcrl2::data::detail::linear_inequality_less
atermpp::function_symbol linear_inequality_less()
Definition linear_inequalities.h:534
mcrl2::data::detail::emplace_back_if_not_zero
void emplace_back_if_not_zero(std::vector< detail::variable_with_a_rational_factor > &r, const variable &v, const data_expression &f)
Definition linear_inequalities.h:394
mcrl2::data::detail::pp
std::string pp(const detail::comparison_t t)
Definition linear_inequalities.h:117
mcrl2::data::detail::set_intersection
variable_list set_intersection(const variable_list &x, const variable_list &y)
Returns the intersection of two unordered sets, that are stored in ATerm lists.
Definition data_sequence_algorithm.h:31
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:307
mcrl2::data::detail::optimized_imp
void optimized_imp(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits t)
Make an implication.
Definition optimized_boolean_operators.h:170
mcrl2::data::detail::add
const lhs_t add(const data_expression &v, const lhs_t &argument, const rewriter &r)
Definition linear_inequalities.h:469
mcrl2::data::detail::else_part
const data_expression & else_part(const data_expression &e)
Definition linear_inequalities_utilities.h:90
mcrl2::data::detail::is_well_formed
bool is_well_formed(const lhs_t &lhs)
Definition linear_inequalities.h:354
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:66
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:74
mcrl2::data::detail::map_based_lhs_t
std::map< variable, data_expression > map_based_lhs_t
Definition linear_inequalities.h:172
mcrl2::data::detail::add
const lhs_t add(const lhs_t &argument, const lhs_t &e, const rewriter &r)
Definition linear_inequalities.h:489
mcrl2::data::detail::linear_inequality_less_equal
atermpp::function_symbol linear_inequality_less_equal()
Definition linear_inequalities.h:541
mcrl2::data::detail::meta_operation_lhs
lhs_t meta_operation_lhs(const lhs_t &argument1, const lhs_t &argument2, OPERATION operation, const rewriter &r)
Definition linear_inequalities.h:418
mcrl2::data::detail::subtract
const lhs_t subtract(const lhs_t &argument, const data_expression &v, const rewriter &r)
Definition linear_inequalities.h:474
mcrl2::data::detail::pp
std::string pp(const detail::lhs_t &lhs)
Definition linear_inequalities.h:507
mcrl2::data::detail::meta_operation_constant
const lhs_t meta_operation_constant(const lhs_t &argument, const data_expression &v, const rewriter &r)
Definition linear_inequalities.h:404
mcrl2::data::detail::then_part
const data_expression & then_part(const data_expression &e)
Definition linear_inequalities_utilities.h:82
mcrl2::data::detail::optimized_not
void optimized_not(typename TermTraits::term_type &result, const typename TermTraits::term_type &arg, TermTraits)
Definition optimized_boolean_operators.h:29
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:114
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:290
mcrl2::data::detail::set_difference
variable_list set_difference(const variable_list &x, const variable_list &y)
Returns the difference of two unordered sets, that are stored in aterm lists.
Definition data_sequence_algorithm.h:54
mcrl2::data::detail::optimized_and
void optimized_and(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a conjunction and optimize it if possible.
Definition optimized_boolean_operators.h:59
mcrl2::data::detail::multiply
const lhs_t multiply(const lhs_t &argument, const data_expression &v, const rewriter &r)
Definition linear_inequalities.h:479
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::detail::divide
const lhs_t divide(const lhs_t &argument, const data_expression &v, const rewriter &r)
Definition linear_inequalities.h:484
mcrl2::data::lazy
A collection of utilities for lazy expression construction.
Definition standard_utility.h:63
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:107
mcrl2::data::lazy::or_
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
Definition standard_utility.h:85
mcrl2::data::sort_bool
Namespace for system defined sort bool_.
Definition bool.h:32
mcrl2::data::sort_bool::is_or_application
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
mcrl2::data::sort_bool::bool_
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
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:493
mcrl2::data::sort_bool::is_implies_application
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:409
mcrl2::data::sort_bool::not_
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:197
mcrl2::data::sort_bool::or_
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:324
mcrl2::data::sort_bool::false_
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
mcrl2::data::sort_bool::is_and_application
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
mcrl2::data::sort_bool::is_not_application
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
mcrl2::data::sort_bool::true_
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
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:481
mcrl2::data::sort_int
Namespace for system defined sort int_.
Definition standard_numbers_utility.h:665
mcrl2::data::sort_int::is_cint_application
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
mcrl2::data::sort_nat
Namespace for system defined sort nat.
Definition standard_numbers_utility.h:478
mcrl2::data::sort_nat::is_natural_constant
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
Definition standard_numbers_utility.h:531
mcrl2::data::sort_pos
Namespace for system defined sort pos.
Definition standard_numbers_utility.h:288
mcrl2::data::sort_pos::pos
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
mcrl2::data::sort_real
Namespace for system defined sort real_.
Definition real_utilities.h:23
mcrl2::data::sort_real::plus
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
mcrl2::data::sort_real::times
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
mcrl2::data::sort_real::is_zero
bool is_zero(const atermpp::aterm &e)
Definition real_utilities.h:37
mcrl2::data::sort_real::divides
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
mcrl2::data::sort_real::real_one
data_expression & real_one()
Definition real_utilities.h:31
mcrl2::data::sort_real::is_one
bool is_one(const atermpp::aterm &e)
Definition real_utilities.h:42
mcrl2::data::sort_real::is_plus_application
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
mcrl2::data::sort_real::real_zero
data_expression & real_zero()
Definition real_utilities.h:25
mcrl2::data::sort_real::is_creal_application
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
mcrl2::data::sort_real::minus
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
mcrl2::data::sort_real::real_
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
mcrl2::data::sort_real::times
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1285
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:48
mcrl2::data::sort_real::abs
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
mcrl2::data::sort_real::is_times_application
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
mcrl2::data::sort_real::negate
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
mcrl2::data::sort_real::is_negate_application
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
mcrl2::data::sort_real::is_minus_application
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
mcrl2::data
Namespace for all data library functionality.
Definition data.cpp:22
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::assignment_vector
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
mcrl2::data::real_times
application real_times(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:42
mcrl2::data::real_one
data_expression & real_one()
Definition linear_inequalities.h:941
mcrl2::data::optimized_exists_no_empty_domain
void optimized_exists_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
Definition optimized_boolean_operators.h:624
mcrl2::data::optimized_exists
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
Definition optimized_boolean_operators.h:610
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:299
mcrl2::data::real_plus
application real_plus(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:49
mcrl2::data::function_symbol_list
atermpp::term_list< function_symbol > function_symbol_list
\brief list of function_symbols
Definition function_symbol.h:88
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:86
mcrl2::data::optimized_or
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
Definition optimized_boolean_operators.h:560
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:104
mcrl2::data::less_equal
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:295
mcrl2::data::pp
std::string pp(const data::variable &x)
Definition data.cpp:81
mcrl2::data::real_abs
application real_abs(const data_expression &arg)
Definition linear_inequalities.h:77
mcrl2::data::count_occurrences
void count_occurrences(const std::vector< linear_inequality > &inequalities, std::map< variable, std::size_t > &nr_positive_occurrences, std::map< variable, std::size_t > &nr_negative_occurrences, const rewriter &r)
Definition linear_inequalities.h:1048
mcrl2::data::less
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:258
mcrl2::data::substitution_variables
std::set< data::variable > substitution_variables(const map_substitution< AssociativeContainer > &sigma)
Definition map_substitution.h:75
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:26
mcrl2::data::variable_vector
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
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:219
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:1160
mcrl2::data::real_minus
application real_minus(const data_expression &arg0, const data_expression &arg1)
Definition linear_inequalities.h:63
mcrl2::data::sort_expression_list
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
Definition sort_expression.h:102
mcrl2::data::data_expression_vector
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
Definition data_expression.h:202
mcrl2::data::pivot_and_update
static void pivot_and_update(const variable &xi, const variable &xj, const data_expression &v, const data_expression &v_delta_correction, std::map< variable, data_expression > &beta, std::map< variable, data_expression > &beta_delta_correction, std::set< variable > &basic_variables, std::map< variable, detail::lhs_t > &working_equalities, const rewriter &r)
Definition linear_inequalities.h:1213
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:69
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:203
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:1944
mcrl2::data::optimized_imp
void optimized_imp(Term &result, const Term &p, const Term &q)
Make an implication.
Definition optimized_boolean_operators.h:571
mcrl2::data::structured_sort_constructor_vector
std::vector< structured_sort_constructor > structured_sort_constructor_vector
\brief vector of structured_sort_constructors
Definition structured_sort_constructor.h:202
mcrl2::data::is_zero
bool is_zero(const data_expression &e)
Definition linear_inequalities.h:1018
mcrl2::data::is_forall
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
Definition data_expression.h:38
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:68
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:28
mcrl2::data::data_expression_list
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
Definition data_expression.h:199
mcrl2::data::rewrite_with_memory
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
Definition linear_inequalities.h:2115
mcrl2::data::real_zero
data_expression & real_zero()
Definition linear_inequalities.h:935
mcrl2::data::is_a_redundant_inequality
bool is_a_redundant_inequality(const std::vector< linear_inequality > &inequalities, const std::vector< linear_inequality > ::iterator i, const rewriter &r)
Indicate whether an inequality from a set of inequalities is redundant.
Definition linear_inequalities.h:1092
mcrl2::data::greater
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:332
mcrl2::data::optimized_forall_no_empty_domain
void optimized_forall_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
Definition optimized_boolean_operators.h:597
mcrl2::data::variable_list
atermpp::term_list< variable > variable_list
\brief list of variables
Definition data_expression.h:278
mcrl2::data::is_exists
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
Definition data_expression.h:44
mcrl2::data::real_negate
application real_negate(const data_expression &arg)
Definition linear_inequalities.h:70
mcrl2::data::assignment_list
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
mcrl2::data::is_inconsistent
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in, const rewriter &r, const bool use_cache=true)
Determine whether a list of data expressions is inconsistent.
Definition linear_inequalities.h:1570
mcrl2::data::pp
std::string pp(const data::sort_expression &x)
Definition data.cpp:69
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:80
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:311
mcrl2::data::equal_to
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:144
mcrl2::data::optimized_not
void optimized_not(Term &result, const Term &arg)
Make a negation.
Definition optimized_boolean_operators.h:527
mcrl2::data::optimized_and
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
Definition optimized_boolean_operators.h:538
mcrl2::data::min
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
Definition linear_inequalities.h:953
mcrl2::data::function_symbol_vector
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
Definition function_symbol.h:91
mcrl2::data::structured_sort_constructor_argument_vector
std::vector< structured_sort_constructor_argument > structured_sort_constructor_argument_vector
\brief vector of structured_sort_constructor_arguments
Definition structured_sort_constructor_argument.h:96
mcrl2::data::optimized_forall
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
Definition optimized_boolean_operators.h:583
mcrl2::data::pp
std::string pp(const data::data_expression &x)
Definition data.cpp:52
mcrl2::data::is_variable
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
Definition data_expression.h:74
mcrl2::data::structured_sort_constructor_list
atermpp::term_list< structured_sort_constructor > structured_sort_constructor_list
\brief list of structured_sort_constructors
Definition structured_sort_constructor.h:199
mcrl2::log::warning
@ warning
Definition logger.h:34
mcrl2::log::verbose
@ verbose
Definition logger.h:37
mcrl2::log::mCRL2logEnabled
bool mCRL2logEnabled(const log_level_t level)
Definition logger.h:383
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:29
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:40
mcrl2::lps
The main namespace for the LPS library.
Definition constelm.h:21
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:104
mcrl2::lps::stochastic_action_summand_vector
std::vector< stochastic_action_summand > stochastic_action_summand_vector
\brief vector of stochastic_action_summands
Definition stochastic_action_summand.h:76
mcrl2::lps::replace_variables_capture_avoiding
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace_capture_avoiding.h:188
mcrl2::lps::occursinterm
bool occursinterm(const data::data_expression &t, const data::variable &var)
Definition linearise_utility.h:341
mcrl2::lps::deadlock_summand_vector
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
Definition deadlock_summand.h:84
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:190
mcrl2::lps::replace_variables_capture_avoiding
void replace_variables_capture_avoiding(T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace_capture_avoiding.h:219
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:271
mcrl2::lps::replace_variables_capture_avoiding
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace_capture_avoiding.h:203
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:247
mcrl2::lps::replace_variables_capture_avoiding
stochastic_distribution replace_variables_capture_avoiding(const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma, data::set_identifier_generator &id_generator)
Definition replace_capture_avoiding.h:259
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:211
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:229
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:10472
mcrl2::lps::rename
void rename(const process::rename_expression_list &renamings, lps::stochastic_action_summand_vector &action_summands)
Definition linearise_rename.h:98
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:199
mcrl2::lps::replace_variables_capture_avoiding
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace_capture_avoiding.h:237
mcrl2::lps::replace_variables_capture_avoiding
stochastic_distribution replace_variables_capture_avoiding(const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma)
Definition replace_capture_avoiding.h:277
mcrl2::process
The main namespace for the Process library.
Definition alphabet_reduce.h:19
mcrl2::process::is_at
bool is_at(const atermpp::aterm &x)
Definition process_expression.h:1062
mcrl2::process::is_process_instance
bool is_process_instance(const atermpp::aterm &x)
Definition process_expression.h:272
mcrl2::process::is_process_instance_assignment
bool is_process_instance_assignment(const atermpp::aterm &x)
Definition process_expression.h:348
mcrl2::process::is_tau
bool is_tau(const atermpp::aterm &x)
Definition process_expression.h:454
mcrl2::process::is_seq
bool is_seq(const atermpp::aterm &x)
Definition process_expression.h:1138
mcrl2::process::is_merge
bool is_merge(const atermpp::aterm &x)
Definition process_expression.h:1447
mcrl2::process::is_allow
bool is_allow(const atermpp::aterm &x)
Definition process_expression.h:910
mcrl2::process::pp
std::string pp(const process::process_identifier &x)
Definition process.cpp:53
mcrl2::process::is_bounded_init
bool is_bounded_init(const atermpp::aterm &x)
Definition process_expression.h:1371
mcrl2::process::is_delta
bool is_delta(const atermpp::aterm &x)
Definition process_expression.h:401
mcrl2::process::is_sum
bool is_sum(const atermpp::aterm &x)
Definition process_expression.h:530
mcrl2::process::is_process_identifier
bool is_process_identifier(const atermpp::aterm &x)
Definition process_identifier.h:91
mcrl2::process::is_block
bool is_block(const atermpp::aterm &x)
Definition process_expression.h:606
mcrl2::process::is_if_then_else
bool is_if_then_else(const atermpp::aterm &x)
Definition process_expression.h:1295
mcrl2::process::is_comm
bool is_comm(const atermpp::aterm &x)
Definition process_expression.h:834
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:83
mcrl2::process::is_action
bool is_action(const atermpp::aterm &x)
Definition process_expression.h:196
mcrl2::process::is_left_merge
bool is_left_merge(const atermpp::aterm &x)
Definition process_expression.h:1523
mcrl2::process::action_label_list
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
Definition action_label.h:77
mcrl2::process::action_vector
std::vector< action > action_vector
\brief vector of actions
Definition process_expression.h:190
mcrl2::process::action_list
atermpp::term_list< action > action_list
\brief list of actions
Definition process_expression.h:187
mcrl2::process::is_hide
bool is_hide(const atermpp::aterm &x)
Definition process_expression.h:682
mcrl2::process::pp
std::string pp(const process::process_expression &x)
Definition process.cpp:52
mcrl2::process::is_if_then
bool is_if_then(const atermpp::aterm &x)
Definition process_expression.h:1214
mcrl2::process::is_choice
bool is_choice(const atermpp::aterm &x)
Definition process_expression.h:1599
mcrl2::process::is_stochastic_operator
bool is_stochastic_operator(const atermpp::aterm &x)
Definition process_expression.h:1680
mcrl2::process::action_name_multiset_list
atermpp::term_list< action_name_multiset > action_name_multiset_list
\brief list of action_name_multisets
Definition action_name_multiset.h:67
mcrl2::process::is_rename
bool is_rename(const atermpp::aterm &x)
Definition process_expression.h:758
mcrl2::process::is_sync
bool is_sync(const atermpp::aterm &x)
Definition process_expression.h:986
mcrl2::process::pp
std::string pp(const process::action_label &x)
Definition process.cpp:36
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition shared_mutex.h:25
std::swap
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
Definition aterm.h:475
mcrl2::core::term_traits
Contains type information for terms.
Definition term_traits.h:24
mcrl2::data::detail::capture_avoiding_substitution_updater
Definition replace_capture_avoiding.h:28
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:317
mcrl2::data::fourier_motzkin_sigma::fourier_motzkin_sigma
fourier_motzkin_sigma(const rewriter &rewr_)
Definition fourier_motzkin.h:343
mcrl2::data::fourier_motzkin_sigma::operator()
const 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:320
mcrl2::data::fourier_motzkin_sigma::apply
const data_expression apply(const abstraction &d, bool negate) const
Definition fourier_motzkin.h:322
mcrl2::data::map_substitution
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
Definition map_substitution.h:26
mcrl2::data::map_substitution::to_string
std::string to_string() const
Definition map_substitution.h:53
mcrl2::data::map_substitution::operator()
const expression_type operator()(const variable_type &v) const
Definition map_substitution.h:38
mcrl2::data::map_substitution::m_map
const AssociativeContainer & m_map
Definition map_substitution.h:32
mcrl2::data::map_substitution::map_substitution
map_substitution(const AssociativeContainer &m)
Definition map_substitution.h:34
mcrl2::data::map_substitution::expression_type
AssociativeContainer::mapped_type expression_type
Definition map_substitution.h:28
mcrl2::data::map_substitution::variable_type
AssociativeContainer::key_type variable_type
Definition map_substitution.h:27
mcrl2::lps::action_compare
Definition linearise_utility.h:117
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_data_variable_builder_binding
Definition add_binding.h:142
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::detail::add_capture_avoiding_replacement
Definition replace_capture_avoiding.h:27
mcrl2::lps::detail::add_capture_avoiding_replacement::do_linear_process
void do_linear_process(LinearProcess &x)
Definition replace_capture_avoiding.h:91
mcrl2::lps::detail::add_capture_avoiding_replacement::operator()
void operator()(specification &x)
Definition replace_capture_avoiding.h:132
mcrl2::lps::detail::add_capture_avoiding_replacement::super
process::detail::add_capture_avoiding_replacement< Builder, Derived, Substitution > super
Definition replace_capture_avoiding.h:28
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:166
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(action_summand &x)
Definition replace_capture_avoiding.h:56
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:151
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(linear_process &x)
Definition replace_capture_avoiding.h:101
mcrl2::lps::detail::add_capture_avoiding_replacement::do_specification
void do_specification(Specification &x)
Definition replace_capture_avoiding.h:112
mcrl2::lps::detail::add_capture_avoiding_replacement::apply
void apply(T &, const stochastic_distribution &)
Definition replace_capture_avoiding.h:143
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:40
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(stochastic_linear_process &x)
Definition replace_capture_avoiding.h:106
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(deadlock_summand &x)
Definition replace_capture_avoiding.h:76
mcrl2::lps::detail::add_capture_avoiding_replacement::update
void update(stochastic_action_summand &x)
Definition replace_capture_avoiding.h:64
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:35
mcrl2::lps::detail::add_capture_avoiding_replacement::operator()
void operator()(stochastic_specification &x)
Definition replace_capture_avoiding.h:137
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:39
mcrl2::lps::detail::is_singleton_sort::is_singleton_sort
is_singleton_sort(const data::data_specification &data_spec)
Definition remove.h:42
mcrl2::lps::detail::is_singleton_sort::operator()
bool operator()(const data::sort_expression &s) const
Definition remove.h:46
mcrl2::lps::detail::is_singleton_sort::m_data_spec
const data::data_specification & m_data_spec
Definition remove.h:40
mcrl2::lps::detail::is_trivial_summand
Function object that checks if a summand has a false condition.
Definition remove.h:28
mcrl2::lps::detail::is_trivial_summand::operator()
bool operator()(const summand_base &s) const
Definition remove.h:29
mcrl2::lps::detail::remove_parameters_builder
Traverser for removing parameters from LPS data types. These parameters can be either process paramet...
Definition remove.h:61
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:104
mcrl2::lps::detail::remove_parameters_builder::apply
void apply(T &result, const stochastic_process_initializer &x)
Definition remove.h:159
mcrl2::lps::detail::remove_parameters_builder::apply
void apply(T &result, const process_initializer &x)
Definition remove.h:152
mcrl2::lps::detail::remove_parameters_builder::update
void update(std::set< data::variable > &x)
Removes parameters from a set container.
Definition remove.h:76
mcrl2::lps::detail::remove_parameters_builder::to_be_removed
const std::set< data::variable > & to_be_removed
Definition remove.h:68
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:86
mcrl2::lps::detail::remove_parameters_builder::update
void update(linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:114
mcrl2::lps::detail::remove_parameters_builder::super
data_expression_builder< remove_parameters_builder > super
Definition remove.h:62
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:133
mcrl2::lps::detail::remove_parameters_builder::process_parameters
data::variable_list process_parameters
Definition remove.h:69
mcrl2::lps::detail::remove_parameters_builder::update
void update(stochastic_specification &x)
Removes parameters from a linear process specification.
Definition remove.h:178
mcrl2::lps::detail::remove_parameters_builder::update
void update(specification &x)
Removes parameters from a linear process specification.
Definition remove.h:169
mcrl2::lps::detail::remove_parameters_builder::remove_parameters_builder
remove_parameters_builder(const std::set< data::variable > &to_be_removed_)
Definition remove.h:71
mcrl2::lps::detail::remove_parameters_builder::update
void update(stochastic_linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:124
mcrl2::lps::sort_expression_builder
\brief Builder class
Definition builder.h:187
mcrl2::lps::t_lin_options
Options for linearisation.
Definition linearise.h:28
mcrl2::lps::t_lin_options::lin_method
t_lin_method lin_method
Definition linearise.h:29
mcrl2::lps::t_lin_options::apply_alphabet_axioms
bool apply_alphabet_axioms
Definition linearise.h:41
mcrl2::lps::t_lin_options::balance_summands
bool balance_summands
Definition linearise.h:42
mcrl2::lps::variable_builder
\brief Builder class
Definition builder.h:491
specification_basic_type::make_substitution
Definition linearise.cpp:3965
specification_basic_type::make_substitution::make_substitution
make_substitution(const std::map< process_identifier, process_identifier > &map)
Definition linearise.cpp:3970
specification_basic_type::make_substitution::result_type
process_identifier result_type
Definition linearise.cpp:3966
specification_basic_type::make_substitution::argument_type
process_identifier argument_type
Definition linearise.cpp:3967
specification_basic_type::make_substitution::operator()
process_identifier operator()(const process_identifier &id) const
Definition linearise.cpp:3974
specification_basic_type::make_substitution::m_map
const std::map< process_identifier, process_identifier > & m_map
Definition linearise.cpp:3968
std::hash< atermpp::detail::reference_aterm< T > >::operator()
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
Definition aterm_container.h:495