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/modal_formula/action_formula.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
13 : #define MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
14 :
15 : #include "mcrl2/lps/multi_action.h"
16 : #include "mcrl2/process/untyped_multi_action.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace action_formulas
22 : {
23 :
24 : //--- start generated classes ---//
25 : /// \\brief An action formula
26 : class action_formula: public atermpp::aterm_appl
27 : {
28 : public:
29 : /// \\brief Default constructor.
30 14 : action_formula()
31 14 : : atermpp::aterm_appl(core::detail::default_values::ActFrm)
32 14 : {}
33 :
34 : /// \\brief Constructor.
35 : /// \\param term A term
36 7879 : explicit action_formula(const atermpp::aterm& term)
37 7879 : : atermpp::aterm_appl(term)
38 : {
39 7879 : assert(core::detail::check_rule_ActFrm(*this));
40 7879 : }
41 :
42 : /// \\brief Constructor.
43 0 : action_formula(const data::data_expression& x)
44 0 : : atermpp::aterm_appl(x)
45 0 : {}
46 :
47 : /// \\brief Constructor.
48 0 : action_formula(const data::untyped_data_parameter& x)
49 0 : : atermpp::aterm_appl(x)
50 0 : {}
51 :
52 : /// \\brief Constructor.
53 179 : action_formula(const process::untyped_multi_action& x)
54 179 : : atermpp::aterm_appl(x)
55 179 : {}
56 :
57 : /// Move semantics
58 : action_formula(const action_formula&) noexcept = default;
59 117 : action_formula(action_formula&&) noexcept = default;
60 0 : action_formula& operator=(const action_formula&) noexcept = default;
61 55 : action_formula& operator=(action_formula&&) noexcept = default;
62 : };
63 :
64 : /// \\brief list of action_formulas
65 : typedef atermpp::term_list<action_formula> action_formula_list;
66 :
67 : /// \\brief vector of action_formulas
68 : typedef std::vector<action_formula> action_formula_vector;
69 :
70 : // prototypes
71 : inline bool is_true(const atermpp::aterm_appl& x);
72 : inline bool is_false(const atermpp::aterm_appl& x);
73 : inline bool is_not(const atermpp::aterm_appl& x);
74 : inline bool is_and(const atermpp::aterm_appl& x);
75 : inline bool is_or(const atermpp::aterm_appl& x);
76 : inline bool is_imp(const atermpp::aterm_appl& x);
77 : inline bool is_forall(const atermpp::aterm_appl& x);
78 : inline bool is_exists(const atermpp::aterm_appl& x);
79 : inline bool is_at(const atermpp::aterm_appl& x);
80 : inline bool is_multi_action(const atermpp::aterm_appl& x);
81 :
82 : /// \\brief Test for a action_formula expression
83 : /// \\param x A term
84 : /// \\return True if \\a x is a action_formula expression
85 : inline
86 2836 : bool is_action_formula(const atermpp::aterm_appl& x)
87 : {
88 2836 : return data::is_data_expression(x) ||
89 2836 : data::is_untyped_data_parameter(x) ||
90 2836 : action_formulas::is_true(x) ||
91 2314 : action_formulas::is_false(x) ||
92 2271 : action_formulas::is_not(x) ||
93 1985 : action_formulas::is_and(x) ||
94 1897 : action_formulas::is_or(x) ||
95 1863 : action_formulas::is_imp(x) ||
96 1863 : action_formulas::is_forall(x) ||
97 1816 : action_formulas::is_exists(x) ||
98 1799 : action_formulas::is_at(x) ||
99 6086 : action_formulas::is_multi_action(x) ||
100 3250 : process::is_untyped_multi_action(x);
101 : }
102 :
103 : // prototype declaration
104 : std::string pp(const action_formula& x);
105 :
106 : /// \\brief Outputs the object to a stream
107 : /// \\param out An output stream
108 : /// \\param x Object x
109 : /// \\return The output stream
110 : inline
111 : std::ostream& operator<<(std::ostream& out, const action_formula& x)
112 : {
113 : return out << action_formulas::pp(x);
114 : }
115 :
116 : /// \\brief swap overload
117 : inline void swap(action_formula& t1, action_formula& t2)
118 : {
119 : t1.swap(t2);
120 : }
121 :
122 :
123 : /// \\brief The value true for action formulas
124 : class true_: public action_formula
125 : {
126 : public:
127 : /// \\brief Default constructor.
128 61 : true_()
129 61 : : action_formula(core::detail::default_values::ActTrue)
130 61 : {}
131 :
132 : /// \\brief Constructor.
133 : /// \\param term A term
134 791 : explicit true_(const atermpp::aterm& term)
135 791 : : action_formula(term)
136 : {
137 791 : assert(core::detail::check_term_ActTrue(*this));
138 791 : }
139 :
140 : /// Move semantics
141 : true_(const true_&) noexcept = default;
142 : true_(true_&&) noexcept = default;
143 : true_& operator=(const true_&) noexcept = default;
144 : true_& operator=(true_&&) noexcept = default;
145 : };
146 :
147 : /// \\brief Test for a true expression
148 : /// \\param x A term
149 : /// \\return True if \\a x is a true expression
150 : inline
151 7147 : bool is_true(const atermpp::aterm_appl& x)
152 : {
153 7147 : return x.function() == core::detail::function_symbols::ActTrue;
154 : }
155 :
156 : // prototype declaration
157 : std::string pp(const true_& x);
158 :
159 : /// \\brief Outputs the object to a stream
160 : /// \\param out An output stream
161 : /// \\param x Object x
162 : /// \\return The output stream
163 : inline
164 : std::ostream& operator<<(std::ostream& out, const true_& x)
165 : {
166 : return out << action_formulas::pp(x);
167 : }
168 :
169 : /// \\brief swap overload
170 : inline void swap(true_& t1, true_& t2)
171 : {
172 : t1.swap(t2);
173 : }
174 :
175 :
176 : /// \\brief The value false for action formulas
177 : class false_: public action_formula
178 : {
179 : public:
180 : /// \\brief Default constructor.
181 4 : false_()
182 4 : : action_formula(core::detail::default_values::ActFalse)
183 4 : {}
184 :
185 : /// \\brief Constructor.
186 : /// \\param term A term
187 49 : explicit false_(const atermpp::aterm& term)
188 49 : : action_formula(term)
189 : {
190 49 : assert(core::detail::check_term_ActFalse(*this));
191 49 : }
192 :
193 : /// Move semantics
194 : false_(const false_&) noexcept = default;
195 : false_(false_&&) noexcept = default;
196 : false_& operator=(const false_&) noexcept = default;
197 : false_& operator=(false_&&) noexcept = default;
198 : };
199 :
200 : /// \\brief Test for a false expression
201 : /// \\param x A term
202 : /// \\return True if \\a x is a false expression
203 : inline
204 5834 : bool is_false(const atermpp::aterm_appl& x)
205 : {
206 5834 : return x.function() == core::detail::function_symbols::ActFalse;
207 : }
208 :
209 : // prototype declaration
210 : std::string pp(const false_& x);
211 :
212 : /// \\brief Outputs the object to a stream
213 : /// \\param out An output stream
214 : /// \\param x Object x
215 : /// \\return The output stream
216 : inline
217 : std::ostream& operator<<(std::ostream& out, const false_& x)
218 : {
219 : return out << action_formulas::pp(x);
220 : }
221 :
222 : /// \\brief swap overload
223 : inline void swap(false_& t1, false_& t2)
224 : {
225 : t1.swap(t2);
226 : }
227 :
228 :
229 : /// \\brief The not operator for action formulas
230 : class not_: public action_formula
231 : {
232 : public:
233 : /// \\brief Default constructor.
234 : not_()
235 : : action_formula(core::detail::default_values::ActNot)
236 : {}
237 :
238 : /// \\brief Constructor.
239 : /// \\param term A term
240 456 : explicit not_(const atermpp::aterm& term)
241 456 : : action_formula(term)
242 : {
243 456 : assert(core::detail::check_term_ActNot(*this));
244 456 : }
245 :
246 : /// \\brief Constructor.
247 37 : explicit not_(const action_formula& operand)
248 37 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActNot(), operand))
249 37 : {}
250 :
251 : /// Move semantics
252 : not_(const not_&) noexcept = default;
253 : not_(not_&&) noexcept = default;
254 : not_& operator=(const not_&) noexcept = default;
255 : not_& operator=(not_&&) noexcept = default;
256 :
257 454 : const action_formula& operand() const
258 : {
259 454 : return atermpp::down_cast<action_formula>((*this)[0]);
260 : }
261 : };
262 :
263 : /// \\brief Make_not_ constructs a new term into a given address.
264 : /// \\ \param t The reference into which the new not_ is constructed.
265 : template <class... ARGUMENTS>
266 141 : inline void make_not_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
267 : {
268 141 : atermpp::make_term_appl(t, core::detail::function_symbol_ActNot(), args...);
269 141 : }
270 :
271 : /// \\brief Test for a not expression
272 : /// \\param x A term
273 : /// \\return True if \\a x is a not expression
274 : inline
275 5749 : bool is_not(const atermpp::aterm_appl& x)
276 : {
277 5749 : return x.function() == core::detail::function_symbols::ActNot;
278 : }
279 :
280 : // prototype declaration
281 : std::string pp(const not_& x);
282 :
283 : /// \\brief Outputs the object to a stream
284 : /// \\param out An output stream
285 : /// \\param x Object x
286 : /// \\return The output stream
287 : inline
288 : std::ostream& operator<<(std::ostream& out, const not_& x)
289 : {
290 : return out << action_formulas::pp(x);
291 : }
292 :
293 : /// \\brief swap overload
294 : inline void swap(not_& t1, not_& t2)
295 : {
296 : t1.swap(t2);
297 : }
298 :
299 :
300 : /// \\brief The and operator for action formulas
301 : class and_: public action_formula
302 : {
303 : public:
304 : /// \\brief Default constructor.
305 : and_()
306 : : action_formula(core::detail::default_values::ActAnd)
307 : {}
308 :
309 : /// \\brief Constructor.
310 : /// \\param term A term
311 148 : explicit and_(const atermpp::aterm& term)
312 148 : : action_formula(term)
313 : {
314 148 : assert(core::detail::check_term_ActAnd(*this));
315 148 : }
316 :
317 : /// \\brief Constructor.
318 9 : and_(const action_formula& left, const action_formula& right)
319 9 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActAnd(), left, right))
320 9 : {}
321 :
322 : /// Move semantics
323 : and_(const and_&) noexcept = default;
324 : and_(and_&&) noexcept = default;
325 : and_& operator=(const and_&) noexcept = default;
326 : and_& operator=(and_&&) noexcept = default;
327 :
328 148 : const action_formula& left() const
329 : {
330 148 : return atermpp::down_cast<action_formula>((*this)[0]);
331 : }
332 :
333 148 : const action_formula& right() const
334 : {
335 148 : return atermpp::down_cast<action_formula>((*this)[1]);
336 : }
337 : };
338 :
339 : /// \\brief Make_and_ constructs a new term into a given address.
340 : /// \\ \param t The reference into which the new and_ is constructed.
341 : template <class... ARGUMENTS>
342 40 : inline void make_and_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
343 : {
344 40 : atermpp::make_term_appl(t, core::detail::function_symbol_ActAnd(), args...);
345 40 : }
346 :
347 : /// \\brief Test for a and expression
348 : /// \\param x A term
349 : /// \\return True if \\a x is a and expression
350 : inline
351 5009 : bool is_and(const atermpp::aterm_appl& x)
352 : {
353 5009 : return x.function() == core::detail::function_symbols::ActAnd;
354 : }
355 :
356 : // prototype declaration
357 : std::string pp(const and_& x);
358 :
359 : /// \\brief Outputs the object to a stream
360 : /// \\param out An output stream
361 : /// \\param x Object x
362 : /// \\return The output stream
363 : inline
364 : std::ostream& operator<<(std::ostream& out, const and_& x)
365 : {
366 : return out << action_formulas::pp(x);
367 : }
368 :
369 : /// \\brief swap overload
370 : inline void swap(and_& t1, and_& t2)
371 : {
372 : t1.swap(t2);
373 : }
374 :
375 :
376 : /// \\brief The or operator for action formulas
377 : class or_: public action_formula
378 : {
379 : public:
380 : /// \\brief Default constructor.
381 : or_()
382 : : action_formula(core::detail::default_values::ActOr)
383 : {}
384 :
385 : /// \\brief Constructor.
386 : /// \\param term A term
387 57 : explicit or_(const atermpp::aterm& term)
388 57 : : action_formula(term)
389 : {
390 57 : assert(core::detail::check_term_ActOr(*this));
391 57 : }
392 :
393 : /// \\brief Constructor.
394 3 : or_(const action_formula& left, const action_formula& right)
395 3 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActOr(), left, right))
396 3 : {}
397 :
398 : /// Move semantics
399 : or_(const or_&) noexcept = default;
400 : or_(or_&&) noexcept = default;
401 : or_& operator=(const or_&) noexcept = default;
402 : or_& operator=(or_&&) noexcept = default;
403 :
404 57 : const action_formula& left() const
405 : {
406 57 : return atermpp::down_cast<action_formula>((*this)[0]);
407 : }
408 :
409 57 : const action_formula& right() const
410 : {
411 57 : return atermpp::down_cast<action_formula>((*this)[1]);
412 : }
413 : };
414 :
415 : /// \\brief Make_or_ constructs a new term into a given address.
416 : /// \\ \param t The reference into which the new or_ is constructed.
417 : template <class... ARGUMENTS>
418 15 : inline void make_or_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
419 : {
420 15 : atermpp::make_term_appl(t, core::detail::function_symbol_ActOr(), args...);
421 15 : }
422 :
423 : /// \\brief Test for a or expression
424 : /// \\param x A term
425 : /// \\return True if \\a x is a or expression
426 : inline
427 4773 : bool is_or(const atermpp::aterm_appl& x)
428 : {
429 4773 : return x.function() == core::detail::function_symbols::ActOr;
430 : }
431 :
432 : // prototype declaration
433 : std::string pp(const or_& x);
434 :
435 : /// \\brief Outputs the object to a stream
436 : /// \\param out An output stream
437 : /// \\param x Object x
438 : /// \\return The output stream
439 : inline
440 : std::ostream& operator<<(std::ostream& out, const or_& x)
441 : {
442 : return out << action_formulas::pp(x);
443 : }
444 :
445 : /// \\brief swap overload
446 : inline void swap(or_& t1, or_& t2)
447 : {
448 : t1.swap(t2);
449 : }
450 :
451 :
452 : /// \\brief The implication operator for action formulas
453 : class imp: public action_formula
454 : {
455 : public:
456 : /// \\brief Default constructor.
457 : imp()
458 : : action_formula(core::detail::default_values::ActImp)
459 : {}
460 :
461 : /// \\brief Constructor.
462 : /// \\param term A term
463 0 : explicit imp(const atermpp::aterm& term)
464 0 : : action_formula(term)
465 : {
466 0 : assert(core::detail::check_term_ActImp(*this));
467 0 : }
468 :
469 : /// \\brief Constructor.
470 0 : imp(const action_formula& left, const action_formula& right)
471 0 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActImp(), left, right))
472 0 : {}
473 :
474 : /// Move semantics
475 : imp(const imp&) noexcept = default;
476 : imp(imp&&) noexcept = default;
477 : imp& operator=(const imp&) noexcept = default;
478 : imp& operator=(imp&&) noexcept = default;
479 :
480 0 : const action_formula& left() const
481 : {
482 0 : return atermpp::down_cast<action_formula>((*this)[0]);
483 : }
484 :
485 0 : const action_formula& right() const
486 : {
487 0 : return atermpp::down_cast<action_formula>((*this)[1]);
488 : }
489 : };
490 :
491 : /// \\brief Make_imp constructs a new term into a given address.
492 : /// \\ \param t The reference into which the new imp is constructed.
493 : template <class... ARGUMENTS>
494 0 : inline void make_imp(atermpp::aterm_appl& t, const ARGUMENTS&... args)
495 : {
496 0 : atermpp::make_term_appl(t, core::detail::function_symbol_ActImp(), args...);
497 0 : }
498 :
499 : /// \\brief Test for a imp expression
500 : /// \\param x A term
501 : /// \\return True if \\a x is a imp expression
502 : inline
503 4682 : bool is_imp(const atermpp::aterm_appl& x)
504 : {
505 4682 : return x.function() == core::detail::function_symbols::ActImp;
506 : }
507 :
508 : // prototype declaration
509 : std::string pp(const imp& x);
510 :
511 : /// \\brief Outputs the object to a stream
512 : /// \\param out An output stream
513 : /// \\param x Object x
514 : /// \\return The output stream
515 : inline
516 : std::ostream& operator<<(std::ostream& out, const imp& x)
517 : {
518 : return out << action_formulas::pp(x);
519 : }
520 :
521 : /// \\brief swap overload
522 : inline void swap(imp& t1, imp& t2)
523 : {
524 : t1.swap(t2);
525 : }
526 :
527 :
528 : /// \\brief The universal quantification operator for action formulas
529 : class forall: public action_formula
530 : {
531 : public:
532 : /// \\brief Default constructor.
533 : forall()
534 : : action_formula(core::detail::default_values::ActForall)
535 : {}
536 :
537 : /// \\brief Constructor.
538 : /// \\param term A term
539 47 : explicit forall(const atermpp::aterm& term)
540 47 : : action_formula(term)
541 : {
542 47 : assert(core::detail::check_term_ActForall(*this));
543 47 : }
544 :
545 : /// \\brief Constructor.
546 6 : forall(const data::variable_list& variables, const action_formula& body)
547 6 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActForall(), variables, body))
548 6 : {}
549 :
550 : /// Move semantics
551 : forall(const forall&) noexcept = default;
552 : forall(forall&&) noexcept = default;
553 : forall& operator=(const forall&) noexcept = default;
554 : forall& operator=(forall&&) noexcept = default;
555 :
556 56 : const data::variable_list& variables() const
557 : {
558 56 : return atermpp::down_cast<data::variable_list>((*this)[0]);
559 : }
560 :
561 47 : const action_formula& body() const
562 : {
563 47 : return atermpp::down_cast<action_formula>((*this)[1]);
564 : }
565 : };
566 :
567 : /// \\brief Make_forall constructs a new term into a given address.
568 : /// \\ \param t The reference into which the new forall is constructed.
569 : template <class... ARGUMENTS>
570 12 : inline void make_forall(atermpp::aterm_appl& t, const ARGUMENTS&... args)
571 : {
572 12 : atermpp::make_term_appl(t, core::detail::function_symbol_ActForall(), args...);
573 12 : }
574 :
575 : /// \\brief Test for a forall expression
576 : /// \\param x A term
577 : /// \\return True if \\a x is a forall expression
578 : inline
579 4682 : bool is_forall(const atermpp::aterm_appl& x)
580 : {
581 4682 : return x.function() == core::detail::function_symbols::ActForall;
582 : }
583 :
584 : // prototype declaration
585 : std::string pp(const forall& x);
586 :
587 : /// \\brief Outputs the object to a stream
588 : /// \\param out An output stream
589 : /// \\param x Object x
590 : /// \\return The output stream
591 : inline
592 : std::ostream& operator<<(std::ostream& out, const forall& x)
593 : {
594 : return out << action_formulas::pp(x);
595 : }
596 :
597 : /// \\brief swap overload
598 : inline void swap(forall& t1, forall& t2)
599 : {
600 : t1.swap(t2);
601 : }
602 :
603 :
604 : /// \\brief The existential quantification operator for action formulas
605 : class exists: public action_formula
606 : {
607 : public:
608 : /// \\brief Default constructor.
609 : exists()
610 : : action_formula(core::detail::default_values::ActExists)
611 : {}
612 :
613 : /// \\brief Constructor.
614 : /// \\param term A term
615 28 : explicit exists(const atermpp::aterm& term)
616 28 : : action_formula(term)
617 : {
618 28 : assert(core::detail::check_term_ActExists(*this));
619 28 : }
620 :
621 : /// \\brief Constructor.
622 4 : exists(const data::variable_list& variables, const action_formula& body)
623 4 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActExists(), variables, body))
624 4 : {}
625 :
626 : /// Move semantics
627 : exists(const exists&) noexcept = default;
628 : exists(exists&&) noexcept = default;
629 : exists& operator=(const exists&) noexcept = default;
630 : exists& operator=(exists&&) noexcept = default;
631 :
632 33 : const data::variable_list& variables() const
633 : {
634 33 : return atermpp::down_cast<data::variable_list>((*this)[0]);
635 : }
636 :
637 28 : const action_formula& body() const
638 : {
639 28 : return atermpp::down_cast<action_formula>((*this)[1]);
640 : }
641 : };
642 :
643 : /// \\brief Make_exists constructs a new term into a given address.
644 : /// \\ \param t The reference into which the new exists is constructed.
645 : template <class... ARGUMENTS>
646 7 : inline void make_exists(atermpp::aterm_appl& t, const ARGUMENTS&... args)
647 : {
648 7 : atermpp::make_term_appl(t, core::detail::function_symbol_ActExists(), args...);
649 7 : }
650 :
651 : /// \\brief Test for a exists expression
652 : /// \\param x A term
653 : /// \\return True if \\a x is a exists expression
654 : inline
655 4588 : bool is_exists(const atermpp::aterm_appl& x)
656 : {
657 4588 : return x.function() == core::detail::function_symbols::ActExists;
658 : }
659 :
660 : // prototype declaration
661 : std::string pp(const exists& x);
662 :
663 : /// \\brief Outputs the object to a stream
664 : /// \\param out An output stream
665 : /// \\param x Object x
666 : /// \\return The output stream
667 : inline
668 : std::ostream& operator<<(std::ostream& out, const exists& x)
669 : {
670 : return out << action_formulas::pp(x);
671 : }
672 :
673 : /// \\brief swap overload
674 : inline void swap(exists& t1, exists& t2)
675 : {
676 : t1.swap(t2);
677 : }
678 :
679 :
680 : /// \\brief The at operator for action formulas
681 : class at: public action_formula
682 : {
683 : public:
684 : /// \\brief Default constructor.
685 : at()
686 : : action_formula(core::detail::default_values::ActAt)
687 : {}
688 :
689 : /// \\brief Constructor.
690 : /// \\param term A term
691 0 : explicit at(const atermpp::aterm& term)
692 0 : : action_formula(term)
693 : {
694 0 : assert(core::detail::check_term_ActAt(*this));
695 0 : }
696 :
697 : /// \\brief Constructor.
698 0 : at(const action_formula& operand, const data::data_expression& time_stamp)
699 0 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActAt(), operand, time_stamp))
700 0 : {}
701 :
702 : /// Move semantics
703 : at(const at&) noexcept = default;
704 : at(at&&) noexcept = default;
705 : at& operator=(const at&) noexcept = default;
706 : at& operator=(at&&) noexcept = default;
707 :
708 0 : const action_formula& operand() const
709 : {
710 0 : return atermpp::down_cast<action_formula>((*this)[0]);
711 : }
712 :
713 0 : const data::data_expression& time_stamp() const
714 : {
715 0 : return atermpp::down_cast<data::data_expression>((*this)[1]);
716 : }
717 : };
718 :
719 : /// \\brief Make_at constructs a new term into a given address.
720 : /// \\ \param t The reference into which the new at is constructed.
721 : template <class... ARGUMENTS>
722 0 : inline void make_at(atermpp::aterm_appl& t, const ARGUMENTS&... args)
723 : {
724 0 : atermpp::make_term_appl(t, core::detail::function_symbol_ActAt(), args...);
725 0 : }
726 :
727 : /// \\brief Test for a at expression
728 : /// \\param x A term
729 : /// \\return True if \\a x is a at expression
730 : inline
731 4543 : bool is_at(const atermpp::aterm_appl& x)
732 : {
733 4543 : return x.function() == core::detail::function_symbols::ActAt;
734 : }
735 :
736 : // prototype declaration
737 : std::string pp(const at& x);
738 :
739 : /// \\brief Outputs the object to a stream
740 : /// \\param out An output stream
741 : /// \\param x Object x
742 : /// \\return The output stream
743 : inline
744 : std::ostream& operator<<(std::ostream& out, const at& x)
745 : {
746 : return out << action_formulas::pp(x);
747 : }
748 :
749 : /// \\brief swap overload
750 : inline void swap(at& t1, at& t2)
751 : {
752 : t1.swap(t2);
753 : }
754 :
755 :
756 : /// \\brief The multi action for action formulas
757 : class multi_action: public action_formula
758 : {
759 : public:
760 : /// \\brief Default constructor.
761 0 : multi_action()
762 0 : : action_formula(core::detail::default_values::ActMultAct)
763 0 : {}
764 :
765 : /// \\brief Constructor.
766 : /// \\param term A term
767 2376 : explicit multi_action(const atermpp::aterm& term)
768 2376 : : action_formula(term)
769 : {
770 2376 : assert(core::detail::check_term_ActMultAct(*this));
771 2376 : }
772 :
773 : /// \\brief Constructor.
774 192 : explicit multi_action(const process::action_list& actions)
775 192 : : action_formula(atermpp::aterm_appl(core::detail::function_symbol_ActMultAct(), actions))
776 192 : {}
777 :
778 : /// Move semantics
779 : multi_action(const multi_action&) noexcept = default;
780 : multi_action(multi_action&&) noexcept = default;
781 : multi_action& operator=(const multi_action&) noexcept = default;
782 : multi_action& operator=(multi_action&&) noexcept = default;
783 :
784 2446 : const process::action_list& actions() const
785 : {
786 2446 : return atermpp::down_cast<process::action_list>((*this)[0]);
787 : }
788 : };
789 :
790 : /// \\brief Make_multi_action constructs a new term into a given address.
791 : /// \\ \param t The reference into which the new multi_action is constructed.
792 : template <class... ARGUMENTS>
793 403 : inline void make_multi_action(atermpp::aterm_appl& t, const ARGUMENTS&... args)
794 : {
795 403 : atermpp::make_term_appl(t, core::detail::function_symbol_ActMultAct(), args...);
796 403 : }
797 :
798 : /// \\brief Test for a multi_action expression
799 : /// \\param x A term
800 : /// \\return True if \\a x is a multi_action expression
801 : inline
802 4536 : bool is_multi_action(const atermpp::aterm_appl& x)
803 : {
804 4536 : return x.function() == core::detail::function_symbols::ActMultAct;
805 : }
806 :
807 : // prototype declaration
808 : std::string pp(const multi_action& x);
809 :
810 : /// \\brief Outputs the object to a stream
811 : /// \\param out An output stream
812 : /// \\param x Object x
813 : /// \\return The output stream
814 : inline
815 : std::ostream& operator<<(std::ostream& out, const multi_action& x)
816 : {
817 : return out << action_formulas::pp(x);
818 : }
819 :
820 : /// \\brief swap overload
821 : inline void swap(multi_action& t1, multi_action& t2)
822 : {
823 : t1.swap(t2);
824 : }
825 : //--- end generated classes ---//
826 :
827 : // template function overloads
828 : std::set<data::variable> find_all_variables(const action_formulas::action_formula& x);
829 :
830 : } // namespace action_formulas
831 :
832 : } // namespace mcrl2
833 :
834 : #endif // MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
|
