mCRL2
Loading...
Searching...
No Matches
action_formula.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
13#define MCRL2_MODAL_FORMULA_ACTION_FORMULA_H
14
17
18namespace mcrl2
19{
20
21namespace action_formulas
22{
23
24//--- start generated classes ---//
27{
28 public:
31 : atermpp::aterm(core::detail::default_values::ActFrm)
32 {}
33
36 explicit action_formula(const atermpp::aterm& term)
37 : atermpp::aterm(term)
38 {
40 }
41
44 : atermpp::aterm(x)
45 {}
46
49 : atermpp::aterm(x)
50 {}
51
54 : atermpp::aterm(x)
55 {}
56
58 action_formula(const action_formula&) noexcept = default;
59 action_formula(action_formula&&) noexcept = default;
60 action_formula& operator=(const action_formula&) noexcept = default;
61 action_formula& operator=(action_formula&&) noexcept = default;
62};
63
66
69
70// prototypes
71inline bool is_true(const atermpp::aterm& x);
72inline bool is_false(const atermpp::aterm& x);
73inline bool is_not(const atermpp::aterm& x);
74inline bool is_and(const atermpp::aterm& x);
75inline bool is_or(const atermpp::aterm& x);
76inline bool is_imp(const atermpp::aterm& x);
77inline bool is_forall(const atermpp::aterm& x);
78inline bool is_exists(const atermpp::aterm& x);
79inline bool is_at(const atermpp::aterm& x);
80inline bool is_multi_action(const atermpp::aterm& x);
81
85inline
87{
88 return data::is_data_expression(x) ||
101}
102
103// prototype declaration
104std::string pp(const action_formula& x);
105
110inline
111std::ostream& operator<<(std::ostream& out, const action_formula& x)
112{
113 return out << action_formulas::pp(x);
114}
115
117inline void swap(action_formula& t1, action_formula& t2)
118{
119 t1.swap(t2);
120}
121
122
125{
126 public:
129 : action_formula(core::detail::default_values::ActTrue)
130 {}
131
134 explicit true_(const atermpp::aterm& term)
135 : action_formula(term)
136 {
137 assert(core::detail::check_term_ActTrue(*this));
138 }
139
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
150inline
151bool is_true(const atermpp::aterm& x)
152{
153 return x.function() == core::detail::function_symbols::ActTrue;
154}
155
156// prototype declaration
157std::string pp(const true_& x);
158
163inline
164std::ostream& operator<<(std::ostream& out, const true_& x)
165{
166 return out << action_formulas::pp(x);
167}
168
170inline void swap(true_& t1, true_& t2)
171{
172 t1.swap(t2);
173}
174
175
178{
179 public:
182 : action_formula(core::detail::default_values::ActFalse)
183 {}
184
187 explicit false_(const atermpp::aterm& term)
188 : action_formula(term)
189 {
190 assert(core::detail::check_term_ActFalse(*this));
191 }
192
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
203inline
204bool is_false(const atermpp::aterm& x)
205{
206 return x.function() == core::detail::function_symbols::ActFalse;
207}
208
209// prototype declaration
210std::string pp(const false_& x);
211
216inline
217std::ostream& operator<<(std::ostream& out, const false_& x)
218{
219 return out << action_formulas::pp(x);
220}
221
223inline void swap(false_& t1, false_& t2)
224{
225 t1.swap(t2);
226}
227
228
230class not_: public action_formula
231{
232 public:
235 : action_formula(core::detail::default_values::ActNot)
236 {}
237
240 explicit not_(const atermpp::aterm& term)
241 : action_formula(term)
242 {
243 assert(core::detail::check_term_ActNot(*this));
244 }
245
247 explicit not_(const action_formula& operand)
248 : action_formula(atermpp::aterm(core::detail::function_symbol_ActNot(), operand))
249 {}
250
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 const action_formula& operand() const
258 {
259 return atermpp::down_cast<action_formula>((*this)[0]);
260 }
261};
262
265template <class... ARGUMENTS>
266inline void make_not_(atermpp::aterm& t, const ARGUMENTS&... args)
267{
268 atermpp::make_term_appl(t, core::detail::function_symbol_ActNot(), args...);
269}
270
274inline
275bool is_not(const atermpp::aterm& x)
276{
277 return x.function() == core::detail::function_symbols::ActNot;
278}
279
280// prototype declaration
281std::string pp(const not_& x);
282
287inline
288std::ostream& operator<<(std::ostream& out, const not_& x)
289{
290 return out << action_formulas::pp(x);
291}
292
294inline void swap(not_& t1, not_& t2)
295{
296 t1.swap(t2);
297}
298
299
301class and_: public action_formula
302{
303 public:
306 : action_formula(core::detail::default_values::ActAnd)
307 {}
308
311 explicit and_(const atermpp::aterm& term)
312 : action_formula(term)
313 {
314 assert(core::detail::check_term_ActAnd(*this));
315 }
316
318 and_(const action_formula& left, const action_formula& right)
319 : action_formula(atermpp::aterm(core::detail::function_symbol_ActAnd(), left, right))
320 {}
321
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 const action_formula& left() const
329 {
330 return atermpp::down_cast<action_formula>((*this)[0]);
331 }
332
333 const action_formula& right() const
334 {
335 return atermpp::down_cast<action_formula>((*this)[1]);
336 }
337};
338
341template <class... ARGUMENTS>
342inline void make_and_(atermpp::aterm& t, const ARGUMENTS&... args)
343{
344 atermpp::make_term_appl(t, core::detail::function_symbol_ActAnd(), args...);
345}
346
350inline
351bool is_and(const atermpp::aterm& x)
352{
353 return x.function() == core::detail::function_symbols::ActAnd;
354}
355
356// prototype declaration
357std::string pp(const and_& x);
358
363inline
364std::ostream& operator<<(std::ostream& out, const and_& x)
365{
366 return out << action_formulas::pp(x);
367}
368
370inline void swap(and_& t1, and_& t2)
371{
372 t1.swap(t2);
373}
374
375
377class or_: public action_formula
378{
379 public:
382 : action_formula(core::detail::default_values::ActOr)
383 {}
384
387 explicit or_(const atermpp::aterm& term)
388 : action_formula(term)
389 {
390 assert(core::detail::check_term_ActOr(*this));
391 }
392
394 or_(const action_formula& left, const action_formula& right)
395 : action_formula(atermpp::aterm(core::detail::function_symbol_ActOr(), left, right))
396 {}
397
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 const action_formula& left() const
405 {
406 return atermpp::down_cast<action_formula>((*this)[0]);
407 }
408
409 const action_formula& right() const
410 {
411 return atermpp::down_cast<action_formula>((*this)[1]);
412 }
413};
414
417template <class... ARGUMENTS>
418inline void make_or_(atermpp::aterm& t, const ARGUMENTS&... args)
419{
420 atermpp::make_term_appl(t, core::detail::function_symbol_ActOr(), args...);
421}
422
426inline
427bool is_or(const atermpp::aterm& x)
428{
429 return x.function() == core::detail::function_symbols::ActOr;
430}
431
432// prototype declaration
433std::string pp(const or_& x);
434
439inline
440std::ostream& operator<<(std::ostream& out, const or_& x)
441{
442 return out << action_formulas::pp(x);
443}
444
446inline void swap(or_& t1, or_& t2)
447{
448 t1.swap(t2);
449}
450
451
453class imp: public action_formula
454{
455 public:
458 : action_formula(core::detail::default_values::ActImp)
459 {}
460
463 explicit imp(const atermpp::aterm& term)
464 : action_formula(term)
465 {
466 assert(core::detail::check_term_ActImp(*this));
467 }
468
470 imp(const action_formula& left, const action_formula& right)
471 : action_formula(atermpp::aterm(core::detail::function_symbol_ActImp(), left, right))
472 {}
473
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 const action_formula& left() const
481 {
482 return atermpp::down_cast<action_formula>((*this)[0]);
483 }
484
485 const action_formula& right() const
486 {
487 return atermpp::down_cast<action_formula>((*this)[1]);
488 }
489};
490
493template <class... ARGUMENTS>
494inline void make_imp(atermpp::aterm& t, const ARGUMENTS&... args)
495{
496 atermpp::make_term_appl(t, core::detail::function_symbol_ActImp(), args...);
497}
498
502inline
503bool is_imp(const atermpp::aterm& x)
504{
505 return x.function() == core::detail::function_symbols::ActImp;
506}
507
508// prototype declaration
509std::string pp(const imp& x);
510
515inline
516std::ostream& operator<<(std::ostream& out, const imp& x)
517{
518 return out << action_formulas::pp(x);
519}
520
522inline void swap(imp& t1, imp& t2)
523{
524 t1.swap(t2);
525}
526
527
530{
531 public:
534 : action_formula(core::detail::default_values::ActForall)
535 {}
536
539 explicit forall(const atermpp::aterm& term)
540 : action_formula(term)
541 {
542 assert(core::detail::check_term_ActForall(*this));
543 }
544
546 forall(const data::variable_list& variables, const action_formula& body)
547 : action_formula(atermpp::aterm(core::detail::function_symbol_ActForall(), variables, body))
548 {}
549
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 const data::variable_list& variables() const
557 {
558 return atermpp::down_cast<data::variable_list>((*this)[0]);
559 }
560
561 const action_formula& body() const
562 {
563 return atermpp::down_cast<action_formula>((*this)[1]);
564 }
565};
566
569template <class... ARGUMENTS>
570inline void make_forall(atermpp::aterm& t, const ARGUMENTS&... args)
571{
572 atermpp::make_term_appl(t, core::detail::function_symbol_ActForall(), args...);
573}
574
578inline
579bool is_forall(const atermpp::aterm& x)
580{
581 return x.function() == core::detail::function_symbols::ActForall;
582}
583
584// prototype declaration
585std::string pp(const forall& x);
586
591inline
592std::ostream& operator<<(std::ostream& out, const forall& x)
593{
594 return out << action_formulas::pp(x);
595}
596
598inline void swap(forall& t1, forall& t2)
599{
600 t1.swap(t2);
601}
602
603
606{
607 public:
610 : action_formula(core::detail::default_values::ActExists)
611 {}
612
615 explicit exists(const atermpp::aterm& term)
616 : action_formula(term)
617 {
618 assert(core::detail::check_term_ActExists(*this));
619 }
620
622 exists(const data::variable_list& variables, const action_formula& body)
623 : action_formula(atermpp::aterm(core::detail::function_symbol_ActExists(), variables, body))
624 {}
625
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 const data::variable_list& variables() const
633 {
634 return atermpp::down_cast<data::variable_list>((*this)[0]);
635 }
636
637 const action_formula& body() const
638 {
639 return atermpp::down_cast<action_formula>((*this)[1]);
640 }
641};
642
645template <class... ARGUMENTS>
646inline void make_exists(atermpp::aterm& t, const ARGUMENTS&... args)
647{
648 atermpp::make_term_appl(t, core::detail::function_symbol_ActExists(), args...);
649}
650
654inline
655bool is_exists(const atermpp::aterm& x)
656{
657 return x.function() == core::detail::function_symbols::ActExists;
658}
659
660// prototype declaration
661std::string pp(const exists& x);
662
667inline
668std::ostream& operator<<(std::ostream& out, const exists& x)
669{
670 return out << action_formulas::pp(x);
671}
672
674inline void swap(exists& t1, exists& t2)
675{
676 t1.swap(t2);
677}
678
679
681class at: public action_formula
682{
683 public:
686 : action_formula(core::detail::default_values::ActAt)
687 {}
688
691 explicit at(const atermpp::aterm& term)
692 : action_formula(term)
693 {
694 assert(core::detail::check_term_ActAt(*this));
695 }
696
698 at(const action_formula& operand, const data::data_expression& time_stamp)
699 : action_formula(atermpp::aterm(core::detail::function_symbol_ActAt(), operand, time_stamp))
700 {}
701
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 const action_formula& operand() const
709 {
710 return atermpp::down_cast<action_formula>((*this)[0]);
711 }
712
714 {
715 return atermpp::down_cast<data::data_expression>((*this)[1]);
716 }
717};
718
721template <class... ARGUMENTS>
722inline void make_at(atermpp::aterm& t, const ARGUMENTS&... args)
723{
724 atermpp::make_term_appl(t, core::detail::function_symbol_ActAt(), args...);
725}
726
730inline
731bool is_at(const atermpp::aterm& x)
732{
733 return x.function() == core::detail::function_symbols::ActAt;
734}
735
736// prototype declaration
737std::string pp(const at& x);
738
743inline
744std::ostream& operator<<(std::ostream& out, const at& x)
745{
746 return out << action_formulas::pp(x);
747}
748
750inline void swap(at& t1, at& t2)
751{
752 t1.swap(t2);
753}
754
755
758{
759 public:
762 : action_formula(core::detail::default_values::ActMultAct)
763 {}
764
767 explicit multi_action(const atermpp::aterm& term)
768 : action_formula(term)
769 {
770 assert(core::detail::check_term_ActMultAct(*this));
771 }
772
774 explicit multi_action(const process::action_list& actions)
775 : action_formula(atermpp::aterm(core::detail::function_symbol_ActMultAct(), actions))
776 {}
777
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 const process::action_list& actions() const
785 {
786 return atermpp::down_cast<process::action_list>((*this)[0]);
787 }
788};
789
792template <class... ARGUMENTS>
793inline void make_multi_action(atermpp::aterm& t, const ARGUMENTS&... args)
794{
795 atermpp::make_term_appl(t, core::detail::function_symbol_ActMultAct(), args...);
796}
797
801inline
802bool is_multi_action(const atermpp::aterm& x)
803{
804 return x.function() == core::detail::function_symbols::ActMultAct;
805}
806
807// prototype declaration
808std::string pp(const multi_action& x);
809
814inline
815std::ostream& operator<<(std::ostream& out, const multi_action& x)
816{
817 return out << action_formulas::pp(x);
818}
819
821inline void swap(multi_action& t1, multi_action& t2)
822{
823 t1.swap(t2);
824}
825//--- end generated classes ---//
826
827// template function overloads
828std::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
void swap(StaticGraph &a, StaticGraph &b)
Definition Graph.h:297
aterm()
Default constructor.
Definition aterm.h:48
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
A list of aterm objects.
Definition aterm_list.h:24
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
action_formula(action_formula &&) noexcept=default
action_formula(const atermpp::aterm &term)
action_formula(const data::data_expression &x)
\brief Constructor Z6.
action_formula(const action_formula &) noexcept=default
Move semantics.
action_formula(const data::untyped_data_parameter &x)
\brief Constructor Z6.
action_formula()
\brief Default constructor X3.
action_formula(const process::untyped_multi_action &x)
\brief Constructor Z6.
\brief The and operator for action formulas
and_(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
and_()
\brief Default constructor X3.
and_(and_ &&) noexcept=default
and_(const atermpp::aterm &term)
and_(const and_ &) noexcept=default
Move semantics.
const action_formula & right() const
\brief The at operator for action formulas
at(const atermpp::aterm &term)
const data::data_expression & time_stamp() const
at(const at &) noexcept=default
Move semantics.
at(at &&) noexcept=default
at()
\brief Default constructor X3.
at(const action_formula &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
\brief The existential quantification operator for action formulas
exists(const atermpp::aterm &term)
exists(exists &&) noexcept=default
exists(const exists &) noexcept=default
Move semantics.
exists()
\brief Default constructor X3.
const action_formula & body() const
exists(const data::variable_list &variables, const action_formula &body)
\brief Constructor Z14.
\brief The value false for action formulas
false_(const atermpp::aterm &term)
false_()
\brief Default constructor X3.
false_(false_ &&) noexcept=default
false_(const false_ &) noexcept=default
Move semantics.
\brief The universal quantification operator for action formulas
const action_formula & body() const
forall(const atermpp::aterm &term)
forall()
\brief Default constructor X3.
forall(const data::variable_list &variables, const action_formula &body)
\brief Constructor Z14.
forall(const forall &) noexcept=default
Move semantics.
forall(forall &&) noexcept=default
\brief The implication operator for action formulas
imp(const imp &) noexcept=default
Move semantics.
imp(imp &&) noexcept=default
imp(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
imp()
\brief Default constructor X3.
imp(const atermpp::aterm &term)
const action_formula & right() const
\brief The multi action for action formulas
multi_action(const multi_action &) noexcept=default
Move semantics.
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions)
\brief Constructor Z14.
multi_action(const atermpp::aterm &term)
multi_action()
\brief Default constructor X3.
\brief The not operator for action formulas
not_(const action_formula &operand)
\brief Constructor Z14.
not_()
\brief Default constructor X3.
not_(const atermpp::aterm &term)
not_(not_ &&) noexcept=default
not_(const not_ &) noexcept=default
Move semantics.
\brief The or operator for action formulas
or_(or_ &&) noexcept=default
or_()
\brief Default constructor X3.
or_(const action_formula &left, const action_formula &right)
\brief Constructor Z14.
or_(const atermpp::aterm &term)
or_(const or_ &) noexcept=default
Move semantics.
const action_formula & right() const
\brief The value true for action formulas
true_(true_ &&) noexcept=default
true_()
\brief Default constructor X3.
true_(const true_ &) noexcept=default
Move semantics.
true_(const atermpp::aterm &term)
\brief An untyped multi action or data application
Multi-action class.
The main namespace for the aterm++ library.
Definition algorithm.h:21
void make_term_appl(Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor an aterm in a variable based on a function symbol and an forward iterator providing the a...
Definition aterm.h:213
std::vector< action_formula > action_formula_vector
\brief vector of action_formulas
bool is_at(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const action_formula &x)
void swap(action_formula &t1, action_formula &t2)
\brief swap overload
bool is_or(const atermpp::aterm &x)
bool is_true(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
std::string pp(const action_formula &x)
bool is_false(const atermpp::aterm &x)
bool is_not(const atermpp::aterm &x)
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_imp(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
bool is_multi_action(const atermpp::aterm &x)
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm &x)
bool is_action_formula(const atermpp::aterm &x)
bool check_rule_ActFrm(const Term &t)
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_untyped_data_parameter(const atermpp::aterm &x)
bool is_untyped_multi_action(const atermpp::aterm &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
add your file description here.