Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/process/process_expression.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_PROCESS_EXPRESSION_H
13 : #define MCRL2_PROCESS_PROCESS_EXPRESSION_H
14 :
15 : #include "mcrl2/data/assignment.h"
16 : #include "mcrl2/data/untyped_data_parameter.h"
17 : #include "mcrl2/process/action_label.h"
18 : #include "mcrl2/process/communication_expression.h"
19 : #include "mcrl2/process/process_identifier.h"
20 : #include "mcrl2/process/rename_expression.h"
21 :
22 : namespace mcrl2
23 : {
24 :
25 : namespace process
26 : {
27 :
28 : //--- start generated classes ---//
29 : /// \\brief A process expression
30 : class process_expression: public atermpp::aterm_appl
31 : {
32 : public:
33 : /// \\brief Default constructor.
34 79063 : process_expression()
35 79063 : : atermpp::aterm_appl(core::detail::default_values::ProcExpr)
36 79063 : {}
37 :
38 : /// \\brief Constructor.
39 : /// \\param term A term
40 746823 : explicit process_expression(const atermpp::aterm& term)
41 746823 : : atermpp::aterm_appl(term)
42 : {
43 746823 : assert(core::detail::check_rule_ProcExpr(*this));
44 746823 : }
45 :
46 : /// \\brief Constructor.
47 5013 : process_expression(const data::untyped_data_parameter& x)
48 5013 : : atermpp::aterm_appl(x)
49 5013 : {}
50 :
51 : /// Move semantics
52 477478 : process_expression(const process_expression&) noexcept = default;
53 91264 : process_expression(process_expression&&) noexcept = default;
54 58232 : process_expression& operator=(const process_expression&) noexcept = default;
55 33031 : process_expression& operator=(process_expression&&) noexcept = default;
56 : };
57 :
58 : /// \\brief list of process_expressions
59 : typedef atermpp::term_list<process_expression> process_expression_list;
60 :
61 : /// \\brief vector of process_expressions
62 : typedef std::vector<process_expression> process_expression_vector;
63 :
64 : // prototypes
65 : inline bool is_action(const atermpp::aterm_appl& x);
66 : inline bool is_process_instance(const atermpp::aterm_appl& x);
67 : inline bool is_process_instance_assignment(const atermpp::aterm_appl& x);
68 : inline bool is_delta(const atermpp::aterm_appl& x);
69 : inline bool is_tau(const atermpp::aterm_appl& x);
70 : inline bool is_sum(const atermpp::aterm_appl& x);
71 : inline bool is_block(const atermpp::aterm_appl& x);
72 : inline bool is_hide(const atermpp::aterm_appl& x);
73 : inline bool is_rename(const atermpp::aterm_appl& x);
74 : inline bool is_comm(const atermpp::aterm_appl& x);
75 : inline bool is_allow(const atermpp::aterm_appl& x);
76 : inline bool is_sync(const atermpp::aterm_appl& x);
77 : inline bool is_at(const atermpp::aterm_appl& x);
78 : inline bool is_seq(const atermpp::aterm_appl& x);
79 : inline bool is_if_then(const atermpp::aterm_appl& x);
80 : inline bool is_if_then_else(const atermpp::aterm_appl& x);
81 : inline bool is_bounded_init(const atermpp::aterm_appl& x);
82 : inline bool is_merge(const atermpp::aterm_appl& x);
83 : inline bool is_left_merge(const atermpp::aterm_appl& x);
84 : inline bool is_choice(const atermpp::aterm_appl& x);
85 : inline bool is_stochastic_operator(const atermpp::aterm_appl& x);
86 : inline bool is_untyped_process_assignment(const atermpp::aterm_appl& x);
87 :
88 : /// \\brief Test for a process_expression expression
89 : /// \\param x A term
90 : /// \\return True if \\a x is a process_expression expression
91 : inline
92 : bool is_process_expression(const atermpp::aterm_appl& x)
93 : {
94 : return data::is_untyped_data_parameter(x) ||
95 : process::is_action(x) ||
96 : process::is_process_instance(x) ||
97 : process::is_process_instance_assignment(x) ||
98 : process::is_delta(x) ||
99 : process::is_tau(x) ||
100 : process::is_sum(x) ||
101 : process::is_block(x) ||
102 : process::is_hide(x) ||
103 : process::is_rename(x) ||
104 : process::is_comm(x) ||
105 : process::is_allow(x) ||
106 : process::is_sync(x) ||
107 : process::is_at(x) ||
108 : process::is_seq(x) ||
109 : process::is_if_then(x) ||
110 : process::is_if_then_else(x) ||
111 : process::is_bounded_init(x) ||
112 : process::is_merge(x) ||
113 : process::is_left_merge(x) ||
114 : process::is_choice(x) ||
115 : process::is_stochastic_operator(x) ||
116 : process::is_untyped_process_assignment(x);
117 : }
118 :
119 : // prototype declaration
120 : std::string pp(const process_expression& x);
121 :
122 : /// \\brief Outputs the object to a stream
123 : /// \\param out An output stream
124 : /// \\param x Object x
125 : /// \\return The output stream
126 : inline
127 3 : std::ostream& operator<<(std::ostream& out, const process_expression& x)
128 : {
129 3 : return out << process::pp(x);
130 : }
131 :
132 : /// \\brief swap overload
133 : inline void swap(process_expression& t1, process_expression& t2)
134 : {
135 : t1.swap(t2);
136 : }
137 :
138 :
139 : /// \\brief An action
140 : class action: public process_expression
141 : {
142 : public:
143 : /// \\brief Default constructor.
144 55211 : action()
145 55211 : : process_expression(core::detail::default_values::Action)
146 55211 : {}
147 :
148 : /// \\brief Constructor.
149 : /// \\param term A term
150 36442 : explicit action(const atermpp::aterm& term)
151 36442 : : process_expression(term)
152 : {
153 36442 : assert(core::detail::check_term_Action(*this));
154 36442 : }
155 :
156 : /// \\brief Constructor.
157 15727 : action(const action_label& label, const data::data_expression_list& arguments)
158 15727 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Action(), label, arguments))
159 15727 : {}
160 :
161 : /// Move semantics
162 409133 : action(const action&) noexcept = default;
163 63 : action(action&&) noexcept = default;
164 6 : action& operator=(const action&) noexcept = default;
165 964 : action& operator=(action&&) noexcept = default;
166 :
167 448463 : const action_label& label() const
168 : {
169 448463 : return atermpp::down_cast<action_label>((*this)[0]);
170 : }
171 :
172 170312 : const data::data_expression_list& arguments() const
173 : {
174 170312 : return atermpp::down_cast<data::data_expression_list>((*this)[1]);
175 : }
176 : };
177 :
178 : /// \\brief Make_action constructs a new term into a given address.
179 : /// \\ \param t The reference into which the new action is constructed.
180 : template <class... ARGUMENTS>
181 19210 : inline void make_action(atermpp::aterm_appl& t, const ARGUMENTS&... args)
182 : {
183 19210 : atermpp::make_term_appl(t, core::detail::function_symbol_Action(), args...);
184 19210 : }
185 :
186 : /// \\brief list of actions
187 : typedef atermpp::term_list<action> action_list;
188 :
189 : /// \\brief vector of actions
190 : typedef std::vector<action> action_vector;
191 :
192 : /// \\brief Test for a action expression
193 : /// \\param x A term
194 : /// \\return True if \\a x is a action expression
195 : inline
196 148349 : bool is_action(const atermpp::aterm_appl& x)
197 : {
198 148349 : return x.function() == core::detail::function_symbols::Action;
199 : }
200 :
201 : // prototype declaration
202 : std::string pp(const action& x);
203 :
204 : /// \\brief Outputs the object to a stream
205 : /// \\param out An output stream
206 : /// \\param x Object x
207 : /// \\return The output stream
208 : inline
209 0 : std::ostream& operator<<(std::ostream& out, const action& x)
210 : {
211 0 : return out << process::pp(x);
212 : }
213 :
214 : /// \\brief swap overload
215 14 : inline void swap(action& t1, action& t2)
216 : {
217 14 : t1.swap(t2);
218 14 : }
219 :
220 :
221 : /// \\brief A process
222 : class process_instance: public process_expression
223 : {
224 : public:
225 : /// \\brief Default constructor.
226 : process_instance()
227 : : process_expression(core::detail::default_values::Process)
228 : {}
229 :
230 : /// \\brief Constructor.
231 : /// \\param term A term
232 9550 : explicit process_instance(const atermpp::aterm& term)
233 9550 : : process_expression(term)
234 : {
235 9550 : assert(core::detail::check_term_Process(*this));
236 9550 : }
237 :
238 : /// \\brief Constructor.
239 2445 : process_instance(const process_identifier& identifier, const data::data_expression_list& actual_parameters)
240 2445 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Process(), identifier, actual_parameters))
241 2445 : {}
242 :
243 : /// Move semantics
244 1 : process_instance(const process_instance&) noexcept = default;
245 2 : process_instance(process_instance&&) noexcept = default;
246 : process_instance& operator=(const process_instance&) noexcept = default;
247 : process_instance& operator=(process_instance&&) noexcept = default;
248 :
249 13758 : const process_identifier& identifier() const
250 : {
251 13758 : return atermpp::down_cast<process_identifier>((*this)[0]);
252 : }
253 :
254 8362 : const data::data_expression_list& actual_parameters() const
255 : {
256 8362 : return atermpp::down_cast<data::data_expression_list>((*this)[1]);
257 : }
258 : };
259 :
260 : /// \\brief Make_process_instance constructs a new term into a given address.
261 : /// \\ \param t The reference into which the new process_instance is constructed.
262 : template <class... ARGUMENTS>
263 2138 : inline void make_process_instance(atermpp::aterm_appl& t, const ARGUMENTS&... args)
264 : {
265 2138 : atermpp::make_term_appl(t, core::detail::function_symbol_Process(), args...);
266 2138 : }
267 :
268 : /// \\brief Test for a process_instance expression
269 : /// \\param x A term
270 : /// \\return True if \\a x is a process_instance expression
271 : inline
272 54821 : bool is_process_instance(const atermpp::aterm_appl& x)
273 : {
274 54821 : return x.function() == core::detail::function_symbols::Process;
275 : }
276 :
277 : // prototype declaration
278 : std::string pp(const process_instance& x);
279 :
280 : /// \\brief Outputs the object to a stream
281 : /// \\param out An output stream
282 : /// \\param x Object x
283 : /// \\return The output stream
284 : inline
285 0 : std::ostream& operator<<(std::ostream& out, const process_instance& x)
286 : {
287 0 : return out << process::pp(x);
288 : }
289 :
290 : /// \\brief swap overload
291 : inline void swap(process_instance& t1, process_instance& t2)
292 : {
293 : t1.swap(t2);
294 : }
295 :
296 :
297 : /// \\brief A process assignment
298 : class process_instance_assignment: public process_expression
299 : {
300 : public:
301 : /// \\brief Default constructor.
302 : process_instance_assignment()
303 : : process_expression(core::detail::default_values::ProcessAssignment)
304 : {}
305 :
306 : /// \\brief Constructor.
307 : /// \\param term A term
308 65192 : explicit process_instance_assignment(const atermpp::aterm& term)
309 65192 : : process_expression(term)
310 : {
311 65192 : assert(core::detail::check_term_ProcessAssignment(*this));
312 65192 : }
313 :
314 : /// \\brief Constructor.
315 15077 : process_instance_assignment(const process_identifier& identifier, const data::assignment_list& assignments)
316 15077 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_ProcessAssignment(), identifier, assignments))
317 15077 : {}
318 :
319 : /// Move semantics
320 8039 : process_instance_assignment(const process_instance_assignment&) noexcept = default;
321 442 : process_instance_assignment(process_instance_assignment&&) noexcept = default;
322 : process_instance_assignment& operator=(const process_instance_assignment&) noexcept = default;
323 : process_instance_assignment& operator=(process_instance_assignment&&) noexcept = default;
324 :
325 74233 : const process_identifier& identifier() const
326 : {
327 74233 : return atermpp::down_cast<process_identifier>((*this)[0]);
328 : }
329 :
330 28096 : const data::assignment_list& assignments() const
331 : {
332 28096 : return atermpp::down_cast<data::assignment_list>((*this)[1]);
333 : }
334 : };
335 :
336 : /// \\brief Make_process_instance_assignment constructs a new term into a given address.
337 : /// \\ \param t The reference into which the new process_instance_assignment is constructed.
338 : template <class... ARGUMENTS>
339 1039 : inline void make_process_instance_assignment(atermpp::aterm_appl& t, const ARGUMENTS&... args)
340 : {
341 1039 : atermpp::make_term_appl(t, core::detail::function_symbol_ProcessAssignment(), args...);
342 1039 : }
343 :
344 : /// \\brief Test for a process_instance_assignment expression
345 : /// \\param x A term
346 : /// \\return True if \\a x is a process_instance_assignment expression
347 : inline
348 187527 : bool is_process_instance_assignment(const atermpp::aterm_appl& x)
349 : {
350 187527 : return x.function() == core::detail::function_symbols::ProcessAssignment;
351 : }
352 :
353 : // prototype declaration
354 : std::string pp(const process_instance_assignment& x);
355 :
356 : /// \\brief Outputs the object to a stream
357 : /// \\param out An output stream
358 : /// \\param x Object x
359 : /// \\return The output stream
360 : inline
361 : std::ostream& operator<<(std::ostream& out, const process_instance_assignment& x)
362 : {
363 : return out << process::pp(x);
364 : }
365 :
366 : /// \\brief swap overload
367 : inline void swap(process_instance_assignment& t1, process_instance_assignment& t2)
368 : {
369 : t1.swap(t2);
370 : }
371 :
372 :
373 : /// \\brief The value delta
374 : class delta: public process_expression
375 : {
376 : public:
377 : /// \\brief Default constructor.
378 13402 : delta()
379 13402 : : process_expression(core::detail::default_values::Delta)
380 13402 : {}
381 :
382 : /// \\brief Constructor.
383 : /// \\param term A term
384 2490 : explicit delta(const atermpp::aterm& term)
385 2490 : : process_expression(term)
386 : {
387 2490 : assert(core::detail::check_term_Delta(*this));
388 2490 : }
389 :
390 : /// Move semantics
391 : delta(const delta&) noexcept = default;
392 : delta(delta&&) noexcept = default;
393 : delta& operator=(const delta&) noexcept = default;
394 : delta& operator=(delta&&) noexcept = default;
395 : };
396 :
397 : /// \\brief Test for a delta expression
398 : /// \\param x A term
399 : /// \\return True if \\a x is a delta expression
400 : inline
401 61136 : bool is_delta(const atermpp::aterm_appl& x)
402 : {
403 61136 : return x.function() == core::detail::function_symbols::Delta;
404 : }
405 :
406 : // prototype declaration
407 : std::string pp(const delta& x);
408 :
409 : /// \\brief Outputs the object to a stream
410 : /// \\param out An output stream
411 : /// \\param x Object x
412 : /// \\return The output stream
413 : inline
414 : std::ostream& operator<<(std::ostream& out, const delta& x)
415 : {
416 : return out << process::pp(x);
417 : }
418 :
419 : /// \\brief swap overload
420 : inline void swap(delta& t1, delta& t2)
421 : {
422 : t1.swap(t2);
423 : }
424 :
425 :
426 : /// \\brief The value tau
427 : class tau: public process_expression
428 : {
429 : public:
430 : /// \\brief Default constructor.
431 9196 : tau()
432 9196 : : process_expression(core::detail::default_values::Tau)
433 9196 : {}
434 :
435 : /// \\brief Constructor.
436 : /// \\param term A term
437 784 : explicit tau(const atermpp::aterm& term)
438 784 : : process_expression(term)
439 : {
440 784 : assert(core::detail::check_term_Tau(*this));
441 784 : }
442 :
443 : /// Move semantics
444 : tau(const tau&) noexcept = default;
445 : tau(tau&&) noexcept = default;
446 : tau& operator=(const tau&) noexcept = default;
447 : tau& operator=(tau&&) noexcept = default;
448 : };
449 :
450 : /// \\brief Test for a tau expression
451 : /// \\param x A term
452 : /// \\return True if \\a x is a tau expression
453 : inline
454 59332 : bool is_tau(const atermpp::aterm_appl& x)
455 : {
456 59332 : return x.function() == core::detail::function_symbols::Tau;
457 : }
458 :
459 : // prototype declaration
460 : std::string pp(const tau& x);
461 :
462 : /// \\brief Outputs the object to a stream
463 : /// \\param out An output stream
464 : /// \\param x Object x
465 : /// \\return The output stream
466 : inline
467 : std::ostream& operator<<(std::ostream& out, const tau& x)
468 : {
469 : return out << process::pp(x);
470 : }
471 :
472 : /// \\brief swap overload
473 : inline void swap(tau& t1, tau& t2)
474 : {
475 : t1.swap(t2);
476 : }
477 :
478 :
479 : /// \\brief The sum operator
480 : class sum: public process_expression
481 : {
482 : public:
483 : /// \\brief Default constructor.
484 : sum()
485 : : process_expression(core::detail::default_values::Sum)
486 : {}
487 :
488 : /// \\brief Constructor.
489 : /// \\param term A term
490 16804 : explicit sum(const atermpp::aterm& term)
491 16804 : : process_expression(term)
492 : {
493 16804 : assert(core::detail::check_term_Sum(*this));
494 16804 : }
495 :
496 : /// \\brief Constructor.
497 4159 : sum(const data::variable_list& variables, const process_expression& operand)
498 4159 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Sum(), variables, operand))
499 4159 : {}
500 :
501 : /// Move semantics
502 : sum(const sum&) noexcept = default;
503 : sum(sum&&) noexcept = default;
504 : sum& operator=(const sum&) noexcept = default;
505 : sum& operator=(sum&&) noexcept = default;
506 :
507 9730 : const data::variable_list& variables() const
508 : {
509 9730 : return atermpp::down_cast<data::variable_list>((*this)[0]);
510 : }
511 :
512 12147 : const process_expression& operand() const
513 : {
514 12147 : return atermpp::down_cast<process_expression>((*this)[1]);
515 : }
516 : };
517 :
518 : /// \\brief Make_sum constructs a new term into a given address.
519 : /// \\ \param t The reference into which the new sum is constructed.
520 : template <class... ARGUMENTS>
521 1865 : inline void make_sum(atermpp::aterm_appl& t, const ARGUMENTS&... args)
522 : {
523 1865 : atermpp::make_term_appl(t, core::detail::function_symbol_Sum(), args...);
524 1865 : }
525 :
526 : /// \\brief Test for a sum expression
527 : /// \\param x A term
528 : /// \\return True if \\a x is a sum expression
529 : inline
530 148363 : bool is_sum(const atermpp::aterm_appl& x)
531 : {
532 148363 : return x.function() == core::detail::function_symbols::Sum;
533 : }
534 :
535 : // prototype declaration
536 : std::string pp(const sum& x);
537 :
538 : /// \\brief Outputs the object to a stream
539 : /// \\param out An output stream
540 : /// \\param x Object x
541 : /// \\return The output stream
542 : inline
543 : std::ostream& operator<<(std::ostream& out, const sum& x)
544 : {
545 : return out << process::pp(x);
546 : }
547 :
548 : /// \\brief swap overload
549 : inline void swap(sum& t1, sum& t2)
550 : {
551 : t1.swap(t2);
552 : }
553 :
554 :
555 : /// \\brief The block operator
556 : class block: public process_expression
557 : {
558 : public:
559 : /// \\brief Default constructor.
560 : block()
561 : : process_expression(core::detail::default_values::Block)
562 : {}
563 :
564 : /// \\brief Constructor.
565 : /// \\param term A term
566 0 : explicit block(const atermpp::aterm& term)
567 0 : : process_expression(term)
568 : {
569 0 : assert(core::detail::check_term_Block(*this));
570 0 : }
571 :
572 : /// \\brief Constructor.
573 0 : block(const core::identifier_string_list& block_set, const process_expression& operand)
574 0 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Block(), block_set, operand))
575 0 : {}
576 :
577 : /// Move semantics
578 : block(const block&) noexcept = default;
579 : block(block&&) noexcept = default;
580 : block& operator=(const block&) noexcept = default;
581 : block& operator=(block&&) noexcept = default;
582 :
583 0 : const core::identifier_string_list& block_set() const
584 : {
585 0 : return atermpp::down_cast<core::identifier_string_list>((*this)[0]);
586 : }
587 :
588 0 : const process_expression& operand() const
589 : {
590 0 : return atermpp::down_cast<process_expression>((*this)[1]);
591 : }
592 : };
593 :
594 : /// \\brief Make_block constructs a new term into a given address.
595 : /// \\ \param t The reference into which the new block is constructed.
596 : template <class... ARGUMENTS>
597 0 : inline void make_block(atermpp::aterm_appl& t, const ARGUMENTS&... args)
598 : {
599 0 : atermpp::make_term_appl(t, core::detail::function_symbol_Block(), args...);
600 0 : }
601 :
602 : /// \\brief Test for a block expression
603 : /// \\param x A term
604 : /// \\return True if \\a x is a block expression
605 : inline
606 82409 : bool is_block(const atermpp::aterm_appl& x)
607 : {
608 82409 : return x.function() == core::detail::function_symbols::Block;
609 : }
610 :
611 : // prototype declaration
612 : std::string pp(const block& x);
613 :
614 : /// \\brief Outputs the object to a stream
615 : /// \\param out An output stream
616 : /// \\param x Object x
617 : /// \\return The output stream
618 : inline
619 : std::ostream& operator<<(std::ostream& out, const block& x)
620 : {
621 : return out << process::pp(x);
622 : }
623 :
624 : /// \\brief swap overload
625 : inline void swap(block& t1, block& t2)
626 : {
627 : t1.swap(t2);
628 : }
629 :
630 :
631 : /// \\brief The hide operator
632 : class hide: public process_expression
633 : {
634 : public:
635 : /// \\brief Default constructor.
636 : hide()
637 : : process_expression(core::detail::default_values::Hide)
638 : {}
639 :
640 : /// \\brief Constructor.
641 : /// \\param term A term
642 444 : explicit hide(const atermpp::aterm& term)
643 444 : : process_expression(term)
644 : {
645 444 : assert(core::detail::check_term_Hide(*this));
646 444 : }
647 :
648 : /// \\brief Constructor.
649 96 : hide(const core::identifier_string_list& hide_set, const process_expression& operand)
650 96 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Hide(), hide_set, operand))
651 96 : {}
652 :
653 : /// Move semantics
654 : hide(const hide&) noexcept = default;
655 : hide(hide&&) noexcept = default;
656 : hide& operator=(const hide&) noexcept = default;
657 : hide& operator=(hide&&) noexcept = default;
658 :
659 240 : const core::identifier_string_list& hide_set() const
660 : {
661 240 : return atermpp::down_cast<core::identifier_string_list>((*this)[0]);
662 : }
663 :
664 348 : const process_expression& operand() const
665 : {
666 348 : return atermpp::down_cast<process_expression>((*this)[1]);
667 : }
668 : };
669 :
670 : /// \\brief Make_hide constructs a new term into a given address.
671 : /// \\ \param t The reference into which the new hide is constructed.
672 : template <class... ARGUMENTS>
673 72 : inline void make_hide(atermpp::aterm_appl& t, const ARGUMENTS&... args)
674 : {
675 72 : atermpp::make_term_appl(t, core::detail::function_symbol_Hide(), args...);
676 72 : }
677 :
678 : /// \\brief Test for a hide expression
679 : /// \\param x A term
680 : /// \\return True if \\a x is a hide expression
681 : inline
682 83271 : bool is_hide(const atermpp::aterm_appl& x)
683 : {
684 83271 : return x.function() == core::detail::function_symbols::Hide;
685 : }
686 :
687 : // prototype declaration
688 : std::string pp(const hide& x);
689 :
690 : /// \\brief Outputs the object to a stream
691 : /// \\param out An output stream
692 : /// \\param x Object x
693 : /// \\return The output stream
694 : inline
695 : std::ostream& operator<<(std::ostream& out, const hide& x)
696 : {
697 : return out << process::pp(x);
698 : }
699 :
700 : /// \\brief swap overload
701 : inline void swap(hide& t1, hide& t2)
702 : {
703 : t1.swap(t2);
704 : }
705 :
706 :
707 : /// \\brief The rename operator
708 : class rename: public process_expression
709 : {
710 : public:
711 : /// \\brief Default constructor.
712 : rename()
713 : : process_expression(core::detail::default_values::Rename)
714 : {}
715 :
716 : /// \\brief Constructor.
717 : /// \\param term A term
718 0 : explicit rename(const atermpp::aterm& term)
719 0 : : process_expression(term)
720 : {
721 0 : assert(core::detail::check_term_Rename(*this));
722 0 : }
723 :
724 : /// \\brief Constructor.
725 0 : rename(const rename_expression_list& rename_set, const process_expression& operand)
726 0 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Rename(), rename_set, operand))
727 0 : {}
728 :
729 : /// Move semantics
730 : rename(const rename&) noexcept = default;
731 : rename(rename&&) noexcept = default;
732 : rename& operator=(const rename&) noexcept = default;
733 : rename& operator=(rename&&) noexcept = default;
734 :
735 0 : const rename_expression_list& rename_set() const
736 : {
737 0 : return atermpp::down_cast<rename_expression_list>((*this)[0]);
738 : }
739 :
740 0 : const process_expression& operand() const
741 : {
742 0 : return atermpp::down_cast<process_expression>((*this)[1]);
743 : }
744 : };
745 :
746 : /// \\brief Make_rename constructs a new term into a given address.
747 : /// \\ \param t The reference into which the new rename is constructed.
748 : template <class... ARGUMENTS>
749 0 : inline void make_rename(atermpp::aterm_appl& t, const ARGUMENTS&... args)
750 : {
751 0 : atermpp::make_term_appl(t, core::detail::function_symbol_Rename(), args...);
752 0 : }
753 :
754 : /// \\brief Test for a rename expression
755 : /// \\param x A term
756 : /// \\return True if \\a x is a rename expression
757 : inline
758 82856 : bool is_rename(const atermpp::aterm_appl& x)
759 : {
760 82856 : return x.function() == core::detail::function_symbols::Rename;
761 : }
762 :
763 : // prototype declaration
764 : std::string pp(const rename& x);
765 :
766 : /// \\brief Outputs the object to a stream
767 : /// \\param out An output stream
768 : /// \\param x Object x
769 : /// \\return The output stream
770 : inline
771 : std::ostream& operator<<(std::ostream& out, const rename& x)
772 : {
773 : return out << process::pp(x);
774 : }
775 :
776 : /// \\brief swap overload
777 : inline void swap(rename& t1, rename& t2)
778 : {
779 : t1.swap(t2);
780 : }
781 :
782 :
783 : /// \\brief The communication operator
784 : class comm: public process_expression
785 : {
786 : public:
787 : /// \\brief Default constructor.
788 : comm()
789 : : process_expression(core::detail::default_values::Comm)
790 : {}
791 :
792 : /// \\brief Constructor.
793 : /// \\param term A term
794 2207 : explicit comm(const atermpp::aterm& term)
795 2207 : : process_expression(term)
796 : {
797 2207 : assert(core::detail::check_term_Comm(*this));
798 2207 : }
799 :
800 : /// \\brief Constructor.
801 485 : comm(const communication_expression_list& comm_set, const process_expression& operand)
802 485 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Comm(), comm_set, operand))
803 485 : {}
804 :
805 : /// Move semantics
806 : comm(const comm&) noexcept = default;
807 : comm(comm&&) noexcept = default;
808 : comm& operator=(const comm&) noexcept = default;
809 : comm& operator=(comm&&) noexcept = default;
810 :
811 1338 : const communication_expression_list& comm_set() const
812 : {
813 1338 : return atermpp::down_cast<communication_expression_list>((*this)[0]);
814 : }
815 :
816 1723 : const process_expression& operand() const
817 : {
818 1723 : return atermpp::down_cast<process_expression>((*this)[1]);
819 : }
820 : };
821 :
822 : /// \\brief Make_comm constructs a new term into a given address.
823 : /// \\ \param t The reference into which the new comm is constructed.
824 : template <class... ARGUMENTS>
825 366 : inline void make_comm(atermpp::aterm_appl& t, const ARGUMENTS&... args)
826 : {
827 366 : atermpp::make_term_appl(t, core::detail::function_symbol_Comm(), args...);
828 366 : }
829 :
830 : /// \\brief Test for a comm expression
831 : /// \\param x A term
832 : /// \\return True if \\a x is a comm expression
833 : inline
834 92892 : bool is_comm(const atermpp::aterm_appl& x)
835 : {
836 92892 : return x.function() == core::detail::function_symbols::Comm;
837 : }
838 :
839 : // prototype declaration
840 : std::string pp(const comm& x);
841 :
842 : /// \\brief Outputs the object to a stream
843 : /// \\param out An output stream
844 : /// \\param x Object x
845 : /// \\return The output stream
846 : inline
847 : std::ostream& operator<<(std::ostream& out, const comm& x)
848 : {
849 : return out << process::pp(x);
850 : }
851 :
852 : /// \\brief swap overload
853 : inline void swap(comm& t1, comm& t2)
854 : {
855 : t1.swap(t2);
856 : }
857 :
858 :
859 : /// \\brief The allow operator
860 : class allow: public process_expression
861 : {
862 : public:
863 : /// \\brief Default constructor.
864 : allow()
865 : : process_expression(core::detail::default_values::Allow)
866 : {}
867 :
868 : /// \\brief Constructor.
869 : /// \\param term A term
870 1256 : explicit allow(const atermpp::aterm& term)
871 1256 : : process_expression(term)
872 : {
873 1256 : assert(core::detail::check_term_Allow(*this));
874 1256 : }
875 :
876 : /// \\brief Constructor.
877 273 : allow(const action_name_multiset_list& allow_set, const process_expression& operand)
878 273 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Allow(), allow_set, operand))
879 273 : {}
880 :
881 : /// Move semantics
882 : allow(const allow&) noexcept = default;
883 : allow(allow&&) noexcept = default;
884 : allow& operator=(const allow&) noexcept = default;
885 : allow& operator=(allow&&) noexcept = default;
886 :
887 694 : const action_name_multiset_list& allow_set() const
888 : {
889 694 : return atermpp::down_cast<action_name_multiset_list>((*this)[0]);
890 : }
891 :
892 990 : const process_expression& operand() const
893 : {
894 990 : return atermpp::down_cast<process_expression>((*this)[1]);
895 : }
896 : };
897 :
898 : /// \\brief Make_allow constructs a new term into a given address.
899 : /// \\ \param t The reference into which the new allow is constructed.
900 : template <class... ARGUMENTS>
901 211 : inline void make_allow(atermpp::aterm_appl& t, const ARGUMENTS&... args)
902 : {
903 211 : atermpp::make_term_appl(t, core::detail::function_symbol_Allow(), args...);
904 211 : }
905 :
906 : /// \\brief Test for a allow expression
907 : /// \\param x A term
908 : /// \\return True if \\a x is a allow expression
909 : inline
910 82314 : bool is_allow(const atermpp::aterm_appl& x)
911 : {
912 82314 : return x.function() == core::detail::function_symbols::Allow;
913 : }
914 :
915 : // prototype declaration
916 : std::string pp(const allow& x);
917 :
918 : /// \\brief Outputs the object to a stream
919 : /// \\param out An output stream
920 : /// \\param x Object x
921 : /// \\return The output stream
922 : inline
923 0 : std::ostream& operator<<(std::ostream& out, const allow& x)
924 : {
925 0 : return out << process::pp(x);
926 : }
927 :
928 : /// \\brief swap overload
929 : inline void swap(allow& t1, allow& t2)
930 : {
931 : t1.swap(t2);
932 : }
933 :
934 :
935 : /// \\brief The synchronization operator
936 : class sync: public process_expression
937 : {
938 : public:
939 : /// \\brief Default constructor.
940 : sync()
941 : : process_expression(core::detail::default_values::Sync)
942 : {}
943 :
944 : /// \\brief Constructor.
945 : /// \\param term A term
946 11873 : explicit sync(const atermpp::aterm& term)
947 11873 : : process_expression(term)
948 : {
949 11873 : assert(core::detail::check_term_Sync(*this));
950 11873 : }
951 :
952 : /// \\brief Constructor.
953 2159 : sync(const process_expression& left, const process_expression& right)
954 2159 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Sync(), left, right))
955 2159 : {}
956 :
957 : /// Move semantics
958 : sync(const sync&) noexcept = default;
959 : sync(sync&&) noexcept = default;
960 : sync& operator=(const sync&) noexcept = default;
961 : sync& operator=(sync&&) noexcept = default;
962 :
963 6762 : const process_expression& left() const
964 : {
965 6762 : return atermpp::down_cast<process_expression>((*this)[0]);
966 : }
967 :
968 6738 : const process_expression& right() const
969 : {
970 6738 : return atermpp::down_cast<process_expression>((*this)[1]);
971 : }
972 : };
973 :
974 : /// \\brief Make_sync constructs a new term into a given address.
975 : /// \\ \param t The reference into which the new sync is constructed.
976 : template <class... ARGUMENTS>
977 975 : inline void make_sync(atermpp::aterm_appl& t, const ARGUMENTS&... args)
978 : {
979 975 : atermpp::make_term_appl(t, core::detail::function_symbol_Sync(), args...);
980 975 : }
981 :
982 : /// \\brief Test for a sync expression
983 : /// \\param x A term
984 : /// \\return True if \\a x is a sync expression
985 : inline
986 83655 : bool is_sync(const atermpp::aterm_appl& x)
987 : {
988 83655 : return x.function() == core::detail::function_symbols::Sync;
989 : }
990 :
991 : // prototype declaration
992 : std::string pp(const sync& x);
993 :
994 : /// \\brief Outputs the object to a stream
995 : /// \\param out An output stream
996 : /// \\param x Object x
997 : /// \\return The output stream
998 : inline
999 : std::ostream& operator<<(std::ostream& out, const sync& x)
1000 : {
1001 : return out << process::pp(x);
1002 : }
1003 :
1004 : /// \\brief swap overload
1005 : inline void swap(sync& t1, sync& t2)
1006 : {
1007 : t1.swap(t2);
1008 : }
1009 :
1010 :
1011 : /// \\brief The at operator
1012 : class at: public process_expression
1013 : {
1014 : public:
1015 : /// \\brief Default constructor.
1016 : at()
1017 : : process_expression(core::detail::default_values::AtTime)
1018 : {}
1019 :
1020 : /// \\brief Constructor.
1021 : /// \\param term A term
1022 9164 : explicit at(const atermpp::aterm& term)
1023 9164 : : process_expression(term)
1024 : {
1025 9164 : assert(core::detail::check_term_AtTime(*this));
1026 9164 : }
1027 :
1028 : /// \\brief Constructor.
1029 10973 : at(const process_expression& operand, const data::data_expression& time_stamp)
1030 10973 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_AtTime(), operand, time_stamp))
1031 10973 : {}
1032 :
1033 : /// Move semantics
1034 : at(const at&) noexcept = default;
1035 : at(at&&) noexcept = default;
1036 : at& operator=(const at&) noexcept = default;
1037 : at& operator=(at&&) noexcept = default;
1038 :
1039 6745 : const process_expression& operand() const
1040 : {
1041 6745 : return atermpp::down_cast<process_expression>((*this)[0]);
1042 : }
1043 :
1044 4128 : const data::data_expression& time_stamp() const
1045 : {
1046 4128 : return atermpp::down_cast<data::data_expression>((*this)[1]);
1047 : }
1048 : };
1049 :
1050 : /// \\brief Make_at constructs a new term into a given address.
1051 : /// \\ \param t The reference into which the new at is constructed.
1052 : template <class... ARGUMENTS>
1053 1027 : inline void make_at(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1054 : {
1055 1027 : atermpp::make_term_appl(t, core::detail::function_symbol_AtTime(), args...);
1056 1027 : }
1057 :
1058 : /// \\brief Test for a at expression
1059 : /// \\param x A term
1060 : /// \\return True if \\a x is a at expression
1061 : inline
1062 77986 : bool is_at(const atermpp::aterm_appl& x)
1063 : {
1064 77986 : return x.function() == core::detail::function_symbols::AtTime;
1065 : }
1066 :
1067 : // prototype declaration
1068 : std::string pp(const at& x);
1069 :
1070 : /// \\brief Outputs the object to a stream
1071 : /// \\param out An output stream
1072 : /// \\param x Object x
1073 : /// \\return The output stream
1074 : inline
1075 : std::ostream& operator<<(std::ostream& out, const at& x)
1076 : {
1077 : return out << process::pp(x);
1078 : }
1079 :
1080 : /// \\brief swap overload
1081 : inline void swap(at& t1, at& t2)
1082 : {
1083 : t1.swap(t2);
1084 : }
1085 :
1086 :
1087 : /// \\brief The sequential composition
1088 : class seq: public process_expression
1089 : {
1090 : public:
1091 : /// \\brief Default constructor.
1092 : seq()
1093 : : process_expression(core::detail::default_values::Seq)
1094 : {}
1095 :
1096 : /// \\brief Constructor.
1097 : /// \\param term A term
1098 103401 : explicit seq(const atermpp::aterm& term)
1099 103401 : : process_expression(term)
1100 : {
1101 103401 : assert(core::detail::check_term_Seq(*this));
1102 103401 : }
1103 :
1104 : /// \\brief Constructor.
1105 22797 : seq(const process_expression& left, const process_expression& right)
1106 22797 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Seq(), left, right))
1107 22797 : {}
1108 :
1109 : /// Move semantics
1110 : seq(const seq&) noexcept = default;
1111 : seq(seq&&) noexcept = default;
1112 : seq& operator=(const seq&) noexcept = default;
1113 : seq& operator=(seq&&) noexcept = default;
1114 :
1115 59178 : const process_expression& left() const
1116 : {
1117 59178 : return atermpp::down_cast<process_expression>((*this)[0]);
1118 : }
1119 :
1120 57424 : const process_expression& right() const
1121 : {
1122 57424 : return atermpp::down_cast<process_expression>((*this)[1]);
1123 : }
1124 : };
1125 :
1126 : /// \\brief Make_seq constructs a new term into a given address.
1127 : /// \\ \param t The reference into which the new seq is constructed.
1128 : template <class... ARGUMENTS>
1129 6823 : inline void make_seq(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1130 : {
1131 6823 : atermpp::make_term_appl(t, core::detail::function_symbol_Seq(), args...);
1132 6822 : }
1133 :
1134 : /// \\brief Test for a seq expression
1135 : /// \\param x A term
1136 : /// \\return True if \\a x is a seq expression
1137 : inline
1138 205975 : bool is_seq(const atermpp::aterm_appl& x)
1139 : {
1140 205975 : return x.function() == core::detail::function_symbols::Seq;
1141 : }
1142 :
1143 : // prototype declaration
1144 : std::string pp(const seq& x);
1145 :
1146 : /// \\brief Outputs the object to a stream
1147 : /// \\param out An output stream
1148 : /// \\param x Object x
1149 : /// \\return The output stream
1150 : inline
1151 : std::ostream& operator<<(std::ostream& out, const seq& x)
1152 : {
1153 : return out << process::pp(x);
1154 : }
1155 :
1156 : /// \\brief swap overload
1157 : inline void swap(seq& t1, seq& t2)
1158 : {
1159 : t1.swap(t2);
1160 : }
1161 :
1162 :
1163 : /// \\brief The if-then operator
1164 : class if_then: public process_expression
1165 : {
1166 : public:
1167 : /// \\brief Default constructor.
1168 : if_then()
1169 : : process_expression(core::detail::default_values::IfThen)
1170 : {}
1171 :
1172 : /// \\brief Constructor.
1173 : /// \\param term A term
1174 26699 : explicit if_then(const atermpp::aterm& term)
1175 26699 : : process_expression(term)
1176 : {
1177 26699 : assert(core::detail::check_term_IfThen(*this));
1178 26699 : }
1179 :
1180 : /// \\brief Constructor.
1181 5410 : if_then(const data::data_expression& condition, const process_expression& then_case)
1182 5410 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_IfThen(), condition, then_case))
1183 5410 : {}
1184 :
1185 : /// Move semantics
1186 : if_then(const if_then&) noexcept = default;
1187 : if_then(if_then&&) noexcept = default;
1188 : if_then& operator=(const if_then&) noexcept = default;
1189 : if_then& operator=(if_then&&) noexcept = default;
1190 :
1191 13924 : const data::data_expression& condition() const
1192 : {
1193 13924 : return atermpp::down_cast<data::data_expression>((*this)[0]);
1194 : }
1195 :
1196 16632 : const process_expression& then_case() const
1197 : {
1198 16632 : return atermpp::down_cast<process_expression>((*this)[1]);
1199 : }
1200 : };
1201 :
1202 : /// \\brief Make_if_then constructs a new term into a given address.
1203 : /// \\ \param t The reference into which the new if_then is constructed.
1204 : template <class... ARGUMENTS>
1205 2141 : inline void make_if_then(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1206 : {
1207 2141 : atermpp::make_term_appl(t, core::detail::function_symbol_IfThen(), args...);
1208 2141 : }
1209 :
1210 : /// \\brief Test for a if_then expression
1211 : /// \\param x A term
1212 : /// \\return True if \\a x is a if_then expression
1213 : inline
1214 153377 : bool is_if_then(const atermpp::aterm_appl& x)
1215 : {
1216 153377 : return x.function() == core::detail::function_symbols::IfThen;
1217 : }
1218 :
1219 : // prototype declaration
1220 : std::string pp(const if_then& x);
1221 :
1222 : /// \\brief Outputs the object to a stream
1223 : /// \\param out An output stream
1224 : /// \\param x Object x
1225 : /// \\return The output stream
1226 : inline
1227 : std::ostream& operator<<(std::ostream& out, const if_then& x)
1228 : {
1229 : return out << process::pp(x);
1230 : }
1231 :
1232 : /// \\brief swap overload
1233 : inline void swap(if_then& t1, if_then& t2)
1234 : {
1235 : t1.swap(t2);
1236 : }
1237 :
1238 :
1239 : /// \\brief The if-then-else operator
1240 : class if_then_else: public process_expression
1241 : {
1242 : public:
1243 : /// \\brief Default constructor.
1244 : if_then_else()
1245 : : process_expression(core::detail::default_values::IfThenElse)
1246 : {}
1247 :
1248 : /// \\brief Constructor.
1249 : /// \\param term A term
1250 3873 : explicit if_then_else(const atermpp::aterm& term)
1251 3873 : : process_expression(term)
1252 : {
1253 3873 : assert(core::detail::check_term_IfThenElse(*this));
1254 3873 : }
1255 :
1256 : /// \\brief Constructor.
1257 435 : if_then_else(const data::data_expression& condition, const process_expression& then_case, const process_expression& else_case)
1258 435 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_IfThenElse(), condition, then_case, else_case))
1259 435 : {}
1260 :
1261 : /// Move semantics
1262 : if_then_else(const if_then_else&) noexcept = default;
1263 : if_then_else(if_then_else&&) noexcept = default;
1264 : if_then_else& operator=(const if_then_else&) noexcept = default;
1265 : if_then_else& operator=(if_then_else&&) noexcept = default;
1266 :
1267 1167 : const data::data_expression& condition() const
1268 : {
1269 1167 : return atermpp::down_cast<data::data_expression>((*this)[0]);
1270 : }
1271 :
1272 1977 : const process_expression& then_case() const
1273 : {
1274 1977 : return atermpp::down_cast<process_expression>((*this)[1]);
1275 : }
1276 :
1277 1977 : const process_expression& else_case() const
1278 : {
1279 1977 : return atermpp::down_cast<process_expression>((*this)[2]);
1280 : }
1281 : };
1282 :
1283 : /// \\brief Make_if_then_else constructs a new term into a given address.
1284 : /// \\ \param t The reference into which the new if_then_else is constructed.
1285 : template <class... ARGUMENTS>
1286 375 : inline void make_if_then_else(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1287 : {
1288 375 : atermpp::make_term_appl(t, core::detail::function_symbol_IfThenElse(), args...);
1289 375 : }
1290 :
1291 : /// \\brief Test for a if_then_else expression
1292 : /// \\param x A term
1293 : /// \\return True if \\a x is a if_then_else expression
1294 : inline
1295 98727 : bool is_if_then_else(const atermpp::aterm_appl& x)
1296 : {
1297 98727 : return x.function() == core::detail::function_symbols::IfThenElse;
1298 : }
1299 :
1300 : // prototype declaration
1301 : std::string pp(const if_then_else& x);
1302 :
1303 : /// \\brief Outputs the object to a stream
1304 : /// \\param out An output stream
1305 : /// \\param x Object x
1306 : /// \\return The output stream
1307 : inline
1308 : std::ostream& operator<<(std::ostream& out, const if_then_else& x)
1309 : {
1310 : return out << process::pp(x);
1311 : }
1312 :
1313 : /// \\brief swap overload
1314 : inline void swap(if_then_else& t1, if_then_else& t2)
1315 : {
1316 : t1.swap(t2);
1317 : }
1318 :
1319 :
1320 : /// \\brief The bounded initialization
1321 : class bounded_init: public process_expression
1322 : {
1323 : public:
1324 : /// \\brief Default constructor.
1325 : bounded_init()
1326 : : process_expression(core::detail::default_values::BInit)
1327 : {}
1328 :
1329 : /// \\brief Constructor.
1330 : /// \\param term A term
1331 0 : explicit bounded_init(const atermpp::aterm& term)
1332 0 : : process_expression(term)
1333 : {
1334 0 : assert(core::detail::check_term_BInit(*this));
1335 0 : }
1336 :
1337 : /// \\brief Constructor.
1338 0 : bounded_init(const process_expression& left, const process_expression& right)
1339 0 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_BInit(), left, right))
1340 0 : {}
1341 :
1342 : /// Move semantics
1343 : bounded_init(const bounded_init&) noexcept = default;
1344 : bounded_init(bounded_init&&) noexcept = default;
1345 : bounded_init& operator=(const bounded_init&) noexcept = default;
1346 : bounded_init& operator=(bounded_init&&) noexcept = default;
1347 :
1348 0 : const process_expression& left() const
1349 : {
1350 0 : return atermpp::down_cast<process_expression>((*this)[0]);
1351 : }
1352 :
1353 0 : const process_expression& right() const
1354 : {
1355 0 : return atermpp::down_cast<process_expression>((*this)[1]);
1356 : }
1357 : };
1358 :
1359 : /// \\brief Make_bounded_init constructs a new term into a given address.
1360 : /// \\ \param t The reference into which the new bounded_init is constructed.
1361 : template <class... ARGUMENTS>
1362 0 : inline void make_bounded_init(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1363 : {
1364 0 : atermpp::make_term_appl(t, core::detail::function_symbol_BInit(), args...);
1365 0 : }
1366 :
1367 : /// \\brief Test for a bounded_init expression
1368 : /// \\param x A term
1369 : /// \\return True if \\a x is a bounded_init expression
1370 : inline
1371 17968 : bool is_bounded_init(const atermpp::aterm_appl& x)
1372 : {
1373 17968 : return x.function() == core::detail::function_symbols::BInit;
1374 : }
1375 :
1376 : // prototype declaration
1377 : std::string pp(const bounded_init& x);
1378 :
1379 : /// \\brief Outputs the object to a stream
1380 : /// \\param out An output stream
1381 : /// \\param x Object x
1382 : /// \\return The output stream
1383 : inline
1384 : std::ostream& operator<<(std::ostream& out, const bounded_init& x)
1385 : {
1386 : return out << process::pp(x);
1387 : }
1388 :
1389 : /// \\brief swap overload
1390 : inline void swap(bounded_init& t1, bounded_init& t2)
1391 : {
1392 : t1.swap(t2);
1393 : }
1394 :
1395 :
1396 : /// \\brief The merge operator
1397 : class merge: public process_expression
1398 : {
1399 : public:
1400 : /// \\brief Default constructor.
1401 : merge()
1402 : : process_expression(core::detail::default_values::Merge)
1403 : {}
1404 :
1405 : /// \\brief Constructor.
1406 : /// \\param term A term
1407 7632 : explicit merge(const atermpp::aterm& term)
1408 7632 : : process_expression(term)
1409 : {
1410 7632 : assert(core::detail::check_term_Merge(*this));
1411 7632 : }
1412 :
1413 : /// \\brief Constructor.
1414 1293 : merge(const process_expression& left, const process_expression& right)
1415 1293 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Merge(), left, right))
1416 1293 : {}
1417 :
1418 : /// Move semantics
1419 : merge(const merge&) noexcept = default;
1420 : merge(merge&&) noexcept = default;
1421 : merge& operator=(const merge&) noexcept = default;
1422 : merge& operator=(merge&&) noexcept = default;
1423 :
1424 4673 : const process_expression& left() const
1425 : {
1426 4673 : return atermpp::down_cast<process_expression>((*this)[0]);
1427 : }
1428 :
1429 4673 : const process_expression& right() const
1430 : {
1431 4673 : return atermpp::down_cast<process_expression>((*this)[1]);
1432 : }
1433 : };
1434 :
1435 : /// \\brief Make_merge constructs a new term into a given address.
1436 : /// \\ \param t The reference into which the new merge is constructed.
1437 : template <class... ARGUMENTS>
1438 1032 : inline void make_merge(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1439 : {
1440 1032 : atermpp::make_term_appl(t, core::detail::function_symbol_Merge(), args...);
1441 1032 : }
1442 :
1443 : /// \\brief Test for a merge expression
1444 : /// \\param x A term
1445 : /// \\return True if \\a x is a merge expression
1446 : inline
1447 92933 : bool is_merge(const atermpp::aterm_appl& x)
1448 : {
1449 92933 : return x.function() == core::detail::function_symbols::Merge;
1450 : }
1451 :
1452 : // prototype declaration
1453 : std::string pp(const merge& x);
1454 :
1455 : /// \\brief Outputs the object to a stream
1456 : /// \\param out An output stream
1457 : /// \\param x Object x
1458 : /// \\return The output stream
1459 : inline
1460 : std::ostream& operator<<(std::ostream& out, const merge& x)
1461 : {
1462 : return out << process::pp(x);
1463 : }
1464 :
1465 : /// \\brief swap overload
1466 : inline void swap(merge& t1, merge& t2)
1467 : {
1468 : t1.swap(t2);
1469 : }
1470 :
1471 :
1472 : /// \\brief The left merge operator
1473 : class left_merge: public process_expression
1474 : {
1475 : public:
1476 : /// \\brief Default constructor.
1477 : left_merge()
1478 : : process_expression(core::detail::default_values::LMerge)
1479 : {}
1480 :
1481 : /// \\brief Constructor.
1482 : /// \\param term A term
1483 0 : explicit left_merge(const atermpp::aterm& term)
1484 0 : : process_expression(term)
1485 : {
1486 0 : assert(core::detail::check_term_LMerge(*this));
1487 0 : }
1488 :
1489 : /// \\brief Constructor.
1490 0 : left_merge(const process_expression& left, const process_expression& right)
1491 0 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_LMerge(), left, right))
1492 0 : {}
1493 :
1494 : /// Move semantics
1495 : left_merge(const left_merge&) noexcept = default;
1496 : left_merge(left_merge&&) noexcept = default;
1497 : left_merge& operator=(const left_merge&) noexcept = default;
1498 : left_merge& operator=(left_merge&&) noexcept = default;
1499 :
1500 0 : const process_expression& left() const
1501 : {
1502 0 : return atermpp::down_cast<process_expression>((*this)[0]);
1503 : }
1504 :
1505 0 : const process_expression& right() const
1506 : {
1507 0 : return atermpp::down_cast<process_expression>((*this)[1]);
1508 : }
1509 : };
1510 :
1511 : /// \\brief Make_left_merge constructs a new term into a given address.
1512 : /// \\ \param t The reference into which the new left_merge is constructed.
1513 : template <class... ARGUMENTS>
1514 0 : inline void make_left_merge(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1515 : {
1516 0 : atermpp::make_term_appl(t, core::detail::function_symbol_LMerge(), args...);
1517 0 : }
1518 :
1519 : /// \\brief Test for a left_merge expression
1520 : /// \\param x A term
1521 : /// \\return True if \\a x is a left_merge expression
1522 : inline
1523 18884 : bool is_left_merge(const atermpp::aterm_appl& x)
1524 : {
1525 18884 : return x.function() == core::detail::function_symbols::LMerge;
1526 : }
1527 :
1528 : // prototype declaration
1529 : std::string pp(const left_merge& x);
1530 :
1531 : /// \\brief Outputs the object to a stream
1532 : /// \\param out An output stream
1533 : /// \\param x Object x
1534 : /// \\return The output stream
1535 : inline
1536 : std::ostream& operator<<(std::ostream& out, const left_merge& x)
1537 : {
1538 : return out << process::pp(x);
1539 : }
1540 :
1541 : /// \\brief swap overload
1542 : inline void swap(left_merge& t1, left_merge& t2)
1543 : {
1544 : t1.swap(t2);
1545 : }
1546 :
1547 :
1548 : /// \\brief The choice operator
1549 : class choice: public process_expression
1550 : {
1551 : public:
1552 : /// \\brief Default constructor.
1553 : choice()
1554 : : process_expression(core::detail::default_values::Choice)
1555 : {}
1556 :
1557 : /// \\brief Constructor.
1558 : /// \\param term A term
1559 39881 : explicit choice(const atermpp::aterm& term)
1560 39881 : : process_expression(term)
1561 : {
1562 39881 : assert(core::detail::check_term_Choice(*this));
1563 39881 : }
1564 :
1565 : /// \\brief Constructor.
1566 6574 : choice(const process_expression& left, const process_expression& right)
1567 6574 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_Choice(), left, right))
1568 6574 : {}
1569 :
1570 : /// Move semantics
1571 : choice(const choice&) noexcept = default;
1572 : choice(choice&&) noexcept = default;
1573 : choice& operator=(const choice&) noexcept = default;
1574 : choice& operator=(choice&&) noexcept = default;
1575 :
1576 23280 : const process_expression& left() const
1577 : {
1578 23280 : return atermpp::down_cast<process_expression>((*this)[0]);
1579 : }
1580 :
1581 21617 : const process_expression& right() const
1582 : {
1583 21617 : return atermpp::down_cast<process_expression>((*this)[1]);
1584 : }
1585 : };
1586 :
1587 : /// \\brief Make_choice constructs a new term into a given address.
1588 : /// \\ \param t The reference into which the new choice is constructed.
1589 : template <class... ARGUMENTS>
1590 2543 : inline void make_choice(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1591 : {
1592 2543 : atermpp::make_term_appl(t, core::detail::function_symbol_Choice(), args...);
1593 2543 : }
1594 :
1595 : /// \\brief Test for a choice expression
1596 : /// \\param x A term
1597 : /// \\return True if \\a x is a choice expression
1598 : inline
1599 203335 : bool is_choice(const atermpp::aterm_appl& x)
1600 : {
1601 203335 : return x.function() == core::detail::function_symbols::Choice;
1602 : }
1603 :
1604 : // prototype declaration
1605 : std::string pp(const choice& x);
1606 :
1607 : /// \\brief Outputs the object to a stream
1608 : /// \\param out An output stream
1609 : /// \\param x Object x
1610 : /// \\return The output stream
1611 : inline
1612 : std::ostream& operator<<(std::ostream& out, const choice& x)
1613 : {
1614 : return out << process::pp(x);
1615 : }
1616 :
1617 : /// \\brief swap overload
1618 : inline void swap(choice& t1, choice& t2)
1619 : {
1620 : t1.swap(t2);
1621 : }
1622 :
1623 :
1624 : /// \\brief The distribution operator
1625 : class stochastic_operator: public process_expression
1626 : {
1627 : public:
1628 : /// \\brief Default constructor.
1629 : stochastic_operator()
1630 : : process_expression(core::detail::default_values::StochasticOperator)
1631 : {}
1632 :
1633 : /// \\brief Constructor.
1634 : /// \\param term A term
1635 3514 : explicit stochastic_operator(const atermpp::aterm& term)
1636 3514 : : process_expression(term)
1637 : {
1638 3514 : assert(core::detail::check_term_StochasticOperator(*this));
1639 3514 : }
1640 :
1641 : /// \\brief Constructor.
1642 1624 : stochastic_operator(const data::variable_list& variables, const data::data_expression& distribution, const process_expression& operand)
1643 1624 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_StochasticOperator(), variables, distribution, operand))
1644 1624 : {}
1645 :
1646 : /// Move semantics
1647 50 : stochastic_operator(const stochastic_operator&) noexcept = default;
1648 : stochastic_operator(stochastic_operator&&) noexcept = default;
1649 : stochastic_operator& operator=(const stochastic_operator&) noexcept = default;
1650 : stochastic_operator& operator=(stochastic_operator&&) noexcept = default;
1651 :
1652 3251 : const data::variable_list& variables() const
1653 : {
1654 3251 : return atermpp::down_cast<data::variable_list>((*this)[0]);
1655 : }
1656 :
1657 2533 : const data::data_expression& distribution() const
1658 : {
1659 2533 : return atermpp::down_cast<data::data_expression>((*this)[1]);
1660 : }
1661 :
1662 3575 : const process_expression& operand() const
1663 : {
1664 3575 : return atermpp::down_cast<process_expression>((*this)[2]);
1665 : }
1666 : };
1667 :
1668 : /// \\brief Make_stochastic_operator constructs a new term into a given address.
1669 : /// \\ \param t The reference into which the new stochastic_operator is constructed.
1670 : template <class... ARGUMENTS>
1671 415 : inline void make_stochastic_operator(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1672 : {
1673 415 : atermpp::make_term_appl(t, core::detail::function_symbol_StochasticOperator(), args...);
1674 415 : }
1675 :
1676 : /// \\brief Test for a stochastic_operator expression
1677 : /// \\param x A term
1678 : /// \\return True if \\a x is a stochastic_operator expression
1679 : inline
1680 136311 : bool is_stochastic_operator(const atermpp::aterm_appl& x)
1681 : {
1682 136311 : return x.function() == core::detail::function_symbols::StochasticOperator;
1683 : }
1684 :
1685 : // prototype declaration
1686 : std::string pp(const stochastic_operator& x);
1687 :
1688 : /// \\brief Outputs the object to a stream
1689 : /// \\param out An output stream
1690 : /// \\param x Object x
1691 : /// \\return The output stream
1692 : inline
1693 : std::ostream& operator<<(std::ostream& out, const stochastic_operator& x)
1694 : {
1695 : return out << process::pp(x);
1696 : }
1697 :
1698 : /// \\brief swap overload
1699 : inline void swap(stochastic_operator& t1, stochastic_operator& t2)
1700 : {
1701 : t1.swap(t2);
1702 : }
1703 :
1704 :
1705 : /// \\brief An untyped process assginment
1706 : class untyped_process_assignment: public process_expression
1707 : {
1708 : public:
1709 : /// \\brief Default constructor.
1710 : untyped_process_assignment()
1711 : : process_expression(core::detail::default_values::UntypedProcessAssignment)
1712 : {}
1713 :
1714 : /// \\brief Constructor.
1715 : /// \\param term A term
1716 882 : explicit untyped_process_assignment(const atermpp::aterm& term)
1717 882 : : process_expression(term)
1718 : {
1719 882 : assert(core::detail::check_term_UntypedProcessAssignment(*this));
1720 882 : }
1721 :
1722 : /// \\brief Constructor.
1723 441 : untyped_process_assignment(const core::identifier_string& name, const data::untyped_identifier_assignment_list& assignments)
1724 441 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_UntypedProcessAssignment(), name, assignments))
1725 441 : {}
1726 :
1727 : /// \\brief Constructor.
1728 : untyped_process_assignment(const std::string& name, const data::untyped_identifier_assignment_list& assignments)
1729 : : process_expression(atermpp::aterm_appl(core::detail::function_symbol_UntypedProcessAssignment(), core::identifier_string(name), assignments))
1730 : {}
1731 :
1732 : /// Move semantics
1733 : untyped_process_assignment(const untyped_process_assignment&) noexcept = default;
1734 : untyped_process_assignment(untyped_process_assignment&&) noexcept = default;
1735 : untyped_process_assignment& operator=(const untyped_process_assignment&) noexcept = default;
1736 : untyped_process_assignment& operator=(untyped_process_assignment&&) noexcept = default;
1737 :
1738 1323 : const core::identifier_string& name() const
1739 : {
1740 1323 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
1741 : }
1742 :
1743 1763 : const data::untyped_identifier_assignment_list& assignments() const
1744 : {
1745 1763 : return atermpp::down_cast<data::untyped_identifier_assignment_list>((*this)[1]);
1746 : }
1747 : };
1748 :
1749 : /// \\brief Make_untyped_process_assignment constructs a new term into a given address.
1750 : /// \\ \param t The reference into which the new untyped_process_assignment is constructed.
1751 : template <class... ARGUMENTS>
1752 441 : inline void make_untyped_process_assignment(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1753 : {
1754 441 : atermpp::make_term_appl(t, core::detail::function_symbol_UntypedProcessAssignment(), args...);
1755 441 : }
1756 :
1757 : /// \\brief Test for a untyped_process_assignment expression
1758 : /// \\param x A term
1759 : /// \\return True if \\a x is a untyped_process_assignment expression
1760 : inline
1761 882 : bool is_untyped_process_assignment(const atermpp::aterm_appl& x)
1762 : {
1763 882 : return x.function() == core::detail::function_symbols::UntypedProcessAssignment;
1764 : }
1765 :
1766 : // prototype declaration
1767 : std::string pp(const untyped_process_assignment& x);
1768 :
1769 : /// \\brief Outputs the object to a stream
1770 : /// \\param out An output stream
1771 : /// \\param x Object x
1772 : /// \\return The output stream
1773 : inline
1774 0 : std::ostream& operator<<(std::ostream& out, const untyped_process_assignment& x)
1775 : {
1776 0 : return out << process::pp(x);
1777 : }
1778 :
1779 : /// \\brief swap overload
1780 : inline void swap(untyped_process_assignment& t1, untyped_process_assignment& t2)
1781 : {
1782 : t1.swap(t2);
1783 : }
1784 : //--- end generated classes ---//
1785 :
1786 : // template function overloads
1787 : std::string pp(const process_expression_list& x);
1788 : std::string pp(const process_expression_vector& x);
1789 : std::set<data::sort_expression> find_sort_expressions(const process::process_expression& x);
1790 : std::string pp(const action_list& x);
1791 : std::string pp(const action_vector& x);
1792 : action normalize_sorts(const action& x, const data::sort_specification& sortspec);
1793 : action translate_user_notation(const action& x);
1794 : process::process_expression translate_user_notation(const process::process_expression& x);
1795 : std::set<data::variable> find_all_variables(const action& x);
1796 : std::set<data::variable> find_free_variables(const action& x);
1797 :
1798 : /// \brief Compares the signatures of two actions
1799 : /// \param a An action
1800 : /// \param b An action
1801 : /// \return Returns true if the actions a and b have the same label, and
1802 : /// the sorts of the arguments of a and b are equal.
1803 : inline
1804 28 : bool equal_signatures(const action& a, const action& b)
1805 : {
1806 28 : if (a.label() != b.label())
1807 : {
1808 16 : return false;
1809 : }
1810 :
1811 12 : const data::data_expression_list& a_args = a.arguments();
1812 12 : const data::data_expression_list& b_args = b.arguments();
1813 :
1814 12 : if (a_args.size() != b_args.size())
1815 : {
1816 0 : return false;
1817 : }
1818 :
1819 26 : return std::equal(a_args.begin(), a_args.end(), b_args.begin(), [](const data::data_expression& x, const data::data_expression& y) { return x.sort() == y.sort(); });
1820 : }
1821 :
1822 : } // namespace process
1823 :
1824 : } // namespace mcrl2
1825 :
1826 : namespace std
1827 : {
1828 :
1829 : /// \brief Standard has function for actions.
1830 : template <>
1831 : struct hash<mcrl2::process::action>
1832 : {
1833 : std::size_t operator()(const mcrl2::process::action& t) const
1834 : {
1835 : return std::hash<atermpp::aterm>()(t);
1836 : }
1837 :
1838 : };
1839 :
1840 :
1841 : } // namespace std
1842 :
1843 : #endif // MCRL2_PROCESS_PROCESS_EXPRESSION_H
|
