mCRL2
Loading...
Searching...
No Matches
state_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_STATE_FORMULA_H
13#define MCRL2_MODAL_FORMULA_STATE_FORMULA_H
14
16
17namespace mcrl2
18{
19
20namespace state_formulas
21{
22
23//--- start generated classes ---//
26{
27 public:
30 : atermpp::aterm(core::detail::default_values::StateFrm)
31 {}
32
35 explicit state_formula(const atermpp::aterm& term)
36 : atermpp::aterm(term)
37 {
39 }
40
43 : atermpp::aterm(x)
44 {}
45
48 : atermpp::aterm(x)
49 {}
50
52 state_formula(const state_formula&) noexcept = default;
53 state_formula(state_formula&&) noexcept = default;
54 state_formula& operator=(const state_formula&) noexcept = default;
55 state_formula& operator=(state_formula&&) noexcept = default;
56//--- start user section state_formula ---//
59 bool has_time() const;
60//--- end user section state_formula ---//
61};
62
65
68
69// prototypes
70inline bool is_true(const atermpp::aterm& x);
71inline bool is_false(const atermpp::aterm& x);
72inline bool is_not(const atermpp::aterm& x);
73inline bool is_minus(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_plus(const atermpp::aterm& x);
78inline bool is_const_multiply(const atermpp::aterm& x);
79inline bool is_const_multiply_alt(const atermpp::aterm& x);
80inline bool is_forall(const atermpp::aterm& x);
81inline bool is_exists(const atermpp::aterm& x);
82inline bool is_infimum(const atermpp::aterm& x);
83inline bool is_supremum(const atermpp::aterm& x);
84inline bool is_sum(const atermpp::aterm& x);
85inline bool is_must(const atermpp::aterm& x);
86inline bool is_may(const atermpp::aterm& x);
87inline bool is_yaled(const atermpp::aterm& x);
88inline bool is_yaled_timed(const atermpp::aterm& x);
89inline bool is_delay(const atermpp::aterm& x);
90inline bool is_delay_timed(const atermpp::aterm& x);
91inline bool is_variable(const atermpp::aterm& x);
92inline bool is_nu(const atermpp::aterm& x);
93inline bool is_mu(const atermpp::aterm& x);
94
98inline
100{
101 return data::is_data_expression(x) ||
127}
128
129// prototype declaration
130std::string pp(const state_formula& x);
131
136inline
137std::ostream& operator<<(std::ostream& out, const state_formula& x)
138{
139 return out << state_formulas::pp(x);
140}
141
143inline void swap(state_formula& t1, state_formula& t2)
144{
145 t1.swap(t2);
146}
147
148
150class true_: public state_formula
151{
152 public:
155 : state_formula(core::detail::default_values::StateTrue)
156 {}
157
160 explicit true_(const atermpp::aterm& term)
161 : state_formula(term)
162 {
163 assert(core::detail::check_term_StateTrue(*this));
164 }
165
167 true_(const true_&) noexcept = default;
168 true_(true_&&) noexcept = default;
169 true_& operator=(const true_&) noexcept = default;
170 true_& operator=(true_&&) noexcept = default;
171};
172
176inline
177bool is_true(const atermpp::aterm& x)
178{
179 return x.function() == core::detail::function_symbols::StateTrue;
180}
181
182// prototype declaration
183std::string pp(const true_& x);
184
189inline
190std::ostream& operator<<(std::ostream& out, const true_& x)
191{
192 return out << state_formulas::pp(x);
193}
194
196inline void swap(true_& t1, true_& t2)
197{
198 t1.swap(t2);
199}
200
201
204{
205 public:
208 : state_formula(core::detail::default_values::StateFalse)
209 {}
210
213 explicit false_(const atermpp::aterm& term)
214 : state_formula(term)
215 {
216 assert(core::detail::check_term_StateFalse(*this));
217 }
218
220 false_(const false_&) noexcept = default;
221 false_(false_&&) noexcept = default;
222 false_& operator=(const false_&) noexcept = default;
223 false_& operator=(false_&&) noexcept = default;
224};
225
229inline
230bool is_false(const atermpp::aterm& x)
231{
232 return x.function() == core::detail::function_symbols::StateFalse;
233}
234
235// prototype declaration
236std::string pp(const false_& x);
237
242inline
243std::ostream& operator<<(std::ostream& out, const false_& x)
244{
245 return out << state_formulas::pp(x);
246}
247
249inline void swap(false_& t1, false_& t2)
250{
251 t1.swap(t2);
252}
253
254
256class not_: public state_formula
257{
258 public:
261 : state_formula(core::detail::default_values::StateNot)
262 {}
263
266 explicit not_(const atermpp::aterm& term)
267 : state_formula(term)
268 {
269 assert(core::detail::check_term_StateNot(*this));
270 }
271
273 explicit not_(const state_formula& operand)
274 : state_formula(atermpp::aterm(core::detail::function_symbol_StateNot(), operand))
275 {}
276
278 not_(const not_&) noexcept = default;
279 not_(not_&&) noexcept = default;
280 not_& operator=(const not_&) noexcept = default;
281 not_& operator=(not_&&) noexcept = default;
282
283 const state_formula& operand() const
284 {
285 return atermpp::down_cast<state_formula>((*this)[0]);
286 }
287};
288
291template <class... ARGUMENTS>
292inline void make_not_(atermpp::aterm& t, const ARGUMENTS&... args)
293{
294 atermpp::make_term_appl(t, core::detail::function_symbol_StateNot(), args...);
295}
296
300inline
301bool is_not(const atermpp::aterm& x)
302{
303 return x.function() == core::detail::function_symbols::StateNot;
304}
305
306// prototype declaration
307std::string pp(const not_& x);
308
313inline
314std::ostream& operator<<(std::ostream& out, const not_& x)
315{
316 return out << state_formulas::pp(x);
317}
318
320inline void swap(not_& t1, not_& t2)
321{
322 t1.swap(t2);
323}
324
325
327class minus: public state_formula
328{
329 public:
332 : state_formula(core::detail::default_values::StateMinus)
333 {}
334
337 explicit minus(const atermpp::aterm& term)
338 : state_formula(term)
339 {
340 assert(core::detail::check_term_StateMinus(*this));
341 }
342
344 explicit minus(const state_formula& operand)
345 : state_formula(atermpp::aterm(core::detail::function_symbol_StateMinus(), operand))
346 {}
347
349 minus(const minus&) noexcept = default;
350 minus(minus&&) noexcept = default;
351 minus& operator=(const minus&) noexcept = default;
352 minus& operator=(minus&&) noexcept = default;
353
354 const state_formula& operand() const
355 {
356 return atermpp::down_cast<state_formula>((*this)[0]);
357 }
358};
359
362template <class... ARGUMENTS>
363inline void make_minus(atermpp::aterm& t, const ARGUMENTS&... args)
364{
365 atermpp::make_term_appl(t, core::detail::function_symbol_StateMinus(), args...);
366}
367
371inline
372bool is_minus(const atermpp::aterm& x)
373{
374 return x.function() == core::detail::function_symbols::StateMinus;
375}
376
377// prototype declaration
378std::string pp(const minus& x);
379
384inline
385std::ostream& operator<<(std::ostream& out, const minus& x)
386{
387 return out << state_formulas::pp(x);
388}
389
391inline void swap(minus& t1, minus& t2)
392{
393 t1.swap(t2);
394}
395
396
398class and_: public state_formula
399{
400 public:
403 : state_formula(core::detail::default_values::StateAnd)
404 {}
405
408 explicit and_(const atermpp::aterm& term)
409 : state_formula(term)
410 {
411 assert(core::detail::check_term_StateAnd(*this));
412 }
413
415 and_(const state_formula& left, const state_formula& right)
416 : state_formula(atermpp::aterm(core::detail::function_symbol_StateAnd(), left, right))
417 {}
418
420 and_(const and_&) noexcept = default;
421 and_(and_&&) noexcept = default;
422 and_& operator=(const and_&) noexcept = default;
423 and_& operator=(and_&&) noexcept = default;
424
425 const state_formula& left() const
426 {
427 return atermpp::down_cast<state_formula>((*this)[0]);
428 }
429
430 const state_formula& right() const
431 {
432 return atermpp::down_cast<state_formula>((*this)[1]);
433 }
434};
435
438template <class... ARGUMENTS>
439inline void make_and_(atermpp::aterm& t, const ARGUMENTS&... args)
440{
441 atermpp::make_term_appl(t, core::detail::function_symbol_StateAnd(), args...);
442}
443
447inline
448bool is_and(const atermpp::aterm& x)
449{
450 return x.function() == core::detail::function_symbols::StateAnd;
451}
452
453// prototype declaration
454std::string pp(const and_& x);
455
460inline
461std::ostream& operator<<(std::ostream& out, const and_& x)
462{
463 return out << state_formulas::pp(x);
464}
465
467inline void swap(and_& t1, and_& t2)
468{
469 t1.swap(t2);
470}
471
472
474class or_: public state_formula
475{
476 public:
479 : state_formula(core::detail::default_values::StateOr)
480 {}
481
484 explicit or_(const atermpp::aterm& term)
485 : state_formula(term)
486 {
487 assert(core::detail::check_term_StateOr(*this));
488 }
489
491 or_(const state_formula& left, const state_formula& right)
492 : state_formula(atermpp::aterm(core::detail::function_symbol_StateOr(), left, right))
493 {}
494
496 or_(const or_&) noexcept = default;
497 or_(or_&&) noexcept = default;
498 or_& operator=(const or_&) noexcept = default;
499 or_& operator=(or_&&) noexcept = default;
500
501 const state_formula& left() const
502 {
503 return atermpp::down_cast<state_formula>((*this)[0]);
504 }
505
506 const state_formula& right() const
507 {
508 return atermpp::down_cast<state_formula>((*this)[1]);
509 }
510};
511
514template <class... ARGUMENTS>
515inline void make_or_(atermpp::aterm& t, const ARGUMENTS&... args)
516{
517 atermpp::make_term_appl(t, core::detail::function_symbol_StateOr(), args...);
518}
519
523inline
524bool is_or(const atermpp::aterm& x)
525{
526 return x.function() == core::detail::function_symbols::StateOr;
527}
528
529// prototype declaration
530std::string pp(const or_& x);
531
536inline
537std::ostream& operator<<(std::ostream& out, const or_& x)
538{
539 return out << state_formulas::pp(x);
540}
541
543inline void swap(or_& t1, or_& t2)
544{
545 t1.swap(t2);
546}
547
548
550class imp: public state_formula
551{
552 public:
555 : state_formula(core::detail::default_values::StateImp)
556 {}
557
560 explicit imp(const atermpp::aterm& term)
561 : state_formula(term)
562 {
563 assert(core::detail::check_term_StateImp(*this));
564 }
565
567 imp(const state_formula& left, const state_formula& right)
568 : state_formula(atermpp::aterm(core::detail::function_symbol_StateImp(), left, right))
569 {}
570
572 imp(const imp&) noexcept = default;
573 imp(imp&&) noexcept = default;
574 imp& operator=(const imp&) noexcept = default;
575 imp& operator=(imp&&) noexcept = default;
576
577 const state_formula& left() const
578 {
579 return atermpp::down_cast<state_formula>((*this)[0]);
580 }
581
582 const state_formula& right() const
583 {
584 return atermpp::down_cast<state_formula>((*this)[1]);
585 }
586};
587
590template <class... ARGUMENTS>
591inline void make_imp(atermpp::aterm& t, const ARGUMENTS&... args)
592{
593 atermpp::make_term_appl(t, core::detail::function_symbol_StateImp(), args...);
594}
595
599inline
600bool is_imp(const atermpp::aterm& x)
601{
602 return x.function() == core::detail::function_symbols::StateImp;
603}
604
605// prototype declaration
606std::string pp(const imp& x);
607
612inline
613std::ostream& operator<<(std::ostream& out, const imp& x)
614{
615 return out << state_formulas::pp(x);
616}
617
619inline void swap(imp& t1, imp& t2)
620{
621 t1.swap(t2);
622}
623
624
626class plus: public state_formula
627{
628 public:
631 : state_formula(core::detail::default_values::StatePlus)
632 {}
633
636 explicit plus(const atermpp::aterm& term)
637 : state_formula(term)
638 {
639 assert(core::detail::check_term_StatePlus(*this));
640 }
641
643 plus(const state_formula& left, const state_formula& right)
644 : state_formula(atermpp::aterm(core::detail::function_symbol_StatePlus(), left, right))
645 {}
646
648 plus(const plus&) noexcept = default;
649 plus(plus&&) noexcept = default;
650 plus& operator=(const plus&) noexcept = default;
651 plus& operator=(plus&&) noexcept = default;
652
653 const state_formula& left() const
654 {
655 return atermpp::down_cast<state_formula>((*this)[0]);
656 }
657
658 const state_formula& right() const
659 {
660 return atermpp::down_cast<state_formula>((*this)[1]);
661 }
662};
663
666template <class... ARGUMENTS>
667inline void make_plus(atermpp::aterm& t, const ARGUMENTS&... args)
668{
669 atermpp::make_term_appl(t, core::detail::function_symbol_StatePlus(), args...);
670}
671
675inline
676bool is_plus(const atermpp::aterm& x)
677{
678 return x.function() == core::detail::function_symbols::StatePlus;
679}
680
681// prototype declaration
682std::string pp(const plus& x);
683
688inline
689std::ostream& operator<<(std::ostream& out, const plus& x)
690{
691 return out << state_formulas::pp(x);
692}
693
695inline void swap(plus& t1, plus& t2)
696{
697 t1.swap(t2);
698}
699
700
703{
704 public:
707 : state_formula(core::detail::default_values::StateConstantMultiply)
708 {}
709
712 explicit const_multiply(const atermpp::aterm& term)
713 : state_formula(term)
714 {
715 assert(core::detail::check_term_StateConstantMultiply(*this));
716 }
717
720 : state_formula(atermpp::aterm(core::detail::function_symbol_StateConstantMultiply(), left, right))
721 {}
722
724 const_multiply(const const_multiply&) noexcept = default;
725 const_multiply(const_multiply&&) noexcept = default;
726 const_multiply& operator=(const const_multiply&) noexcept = default;
727 const_multiply& operator=(const_multiply&&) noexcept = default;
728
729 const data::data_expression& left() const
730 {
731 return atermpp::down_cast<data::data_expression>((*this)[0]);
732 }
733
734 const state_formula& right() const
735 {
736 return atermpp::down_cast<state_formula>((*this)[1]);
737 }
738};
739
742template <class... ARGUMENTS>
743inline void make_const_multiply(atermpp::aterm& t, const ARGUMENTS&... args)
744{
745 atermpp::make_term_appl(t, core::detail::function_symbol_StateConstantMultiply(), args...);
746}
747
751inline
753{
754 return x.function() == core::detail::function_symbols::StateConstantMultiply;
755}
756
757// prototype declaration
758std::string pp(const const_multiply& x);
759
764inline
765std::ostream& operator<<(std::ostream& out, const const_multiply& x)
766{
767 return out << state_formulas::pp(x);
768}
769
771inline void swap(const_multiply& t1, const_multiply& t2)
772{
773 t1.swap(t2);
774}
775
776
779{
780 public:
783 : state_formula(core::detail::default_values::StateConstantMultiplyAlt)
784 {}
785
788 explicit const_multiply_alt(const atermpp::aterm& term)
789 : state_formula(term)
790 {
791 assert(core::detail::check_term_StateConstantMultiplyAlt(*this));
792 }
793
796 : state_formula(atermpp::aterm(core::detail::function_symbol_StateConstantMultiplyAlt(), left, right))
797 {}
798
800 const_multiply_alt(const const_multiply_alt&) noexcept = default;
802 const_multiply_alt& operator=(const const_multiply_alt&) noexcept = default;
803 const_multiply_alt& operator=(const_multiply_alt&&) noexcept = default;
804
805 const state_formula& left() const
806 {
807 return atermpp::down_cast<state_formula>((*this)[0]);
808 }
809
811 {
812 return atermpp::down_cast<data::data_expression>((*this)[1]);
813 }
814};
815
818template <class... ARGUMENTS>
819inline void make_const_multiply_alt(atermpp::aterm& t, const ARGUMENTS&... args)
820{
821 atermpp::make_term_appl(t, core::detail::function_symbol_StateConstantMultiplyAlt(), args...);
822}
823
827inline
829{
830 return x.function() == core::detail::function_symbols::StateConstantMultiplyAlt;
831}
832
833// prototype declaration
834std::string pp(const const_multiply_alt& x);
835
840inline
841std::ostream& operator<<(std::ostream& out, const const_multiply_alt& x)
842{
843 return out << state_formulas::pp(x);
844}
845
848{
849 t1.swap(t2);
850}
851
852
855{
856 public:
859 : state_formula(core::detail::default_values::StateForall)
860 {}
861
864 explicit forall(const atermpp::aterm& term)
865 : state_formula(term)
866 {
867 assert(core::detail::check_term_StateForall(*this));
868 }
869
871 forall(const data::variable_list& variables, const state_formula& body)
872 : state_formula(atermpp::aterm(core::detail::function_symbol_StateForall(), variables, body))
873 {}
874
876 forall(const forall&) noexcept = default;
877 forall(forall&&) noexcept = default;
878 forall& operator=(const forall&) noexcept = default;
879 forall& operator=(forall&&) noexcept = default;
880
881 const data::variable_list& variables() const
882 {
883 return atermpp::down_cast<data::variable_list>((*this)[0]);
884 }
885
886 const state_formula& body() const
887 {
888 return atermpp::down_cast<state_formula>((*this)[1]);
889 }
890};
891
894template <class... ARGUMENTS>
895inline void make_forall(atermpp::aterm& t, const ARGUMENTS&... args)
896{
897 atermpp::make_term_appl(t, core::detail::function_symbol_StateForall(), args...);
898}
899
903inline
904bool is_forall(const atermpp::aterm& x)
905{
906 return x.function() == core::detail::function_symbols::StateForall;
907}
908
909// prototype declaration
910std::string pp(const forall& x);
911
916inline
917std::ostream& operator<<(std::ostream& out, const forall& x)
918{
919 return out << state_formulas::pp(x);
920}
921
923inline void swap(forall& t1, forall& t2)
924{
925 t1.swap(t2);
926}
927
928
931{
932 public:
935 : state_formula(core::detail::default_values::StateExists)
936 {}
937
940 explicit exists(const atermpp::aterm& term)
941 : state_formula(term)
942 {
943 assert(core::detail::check_term_StateExists(*this));
944 }
945
947 exists(const data::variable_list& variables, const state_formula& body)
948 : state_formula(atermpp::aterm(core::detail::function_symbol_StateExists(), variables, body))
949 {}
950
952 exists(const exists&) noexcept = default;
953 exists(exists&&) noexcept = default;
954 exists& operator=(const exists&) noexcept = default;
955 exists& operator=(exists&&) noexcept = default;
956
957 const data::variable_list& variables() const
958 {
959 return atermpp::down_cast<data::variable_list>((*this)[0]);
960 }
961
962 const state_formula& body() const
963 {
964 return atermpp::down_cast<state_formula>((*this)[1]);
965 }
966};
967
970template <class... ARGUMENTS>
971inline void make_exists(atermpp::aterm& t, const ARGUMENTS&... args)
972{
973 atermpp::make_term_appl(t, core::detail::function_symbol_StateExists(), args...);
974}
975
979inline
980bool is_exists(const atermpp::aterm& x)
981{
982 return x.function() == core::detail::function_symbols::StateExists;
983}
984
985// prototype declaration
986std::string pp(const exists& x);
987
992inline
993std::ostream& operator<<(std::ostream& out, const exists& x)
994{
995 return out << state_formulas::pp(x);
996}
997
999inline void swap(exists& t1, exists& t2)
1000{
1001 t1.swap(t2);
1002}
1003
1004
1007{
1008 public:
1011 : state_formula(core::detail::default_values::StateInfimum)
1012 {}
1013
1016 explicit infimum(const atermpp::aterm& term)
1017 : state_formula(term)
1018 {
1019 assert(core::detail::check_term_StateInfimum(*this));
1020 }
1021
1023 infimum(const data::variable_list& variables, const state_formula& body)
1024 : state_formula(atermpp::aterm(core::detail::function_symbol_StateInfimum(), variables, body))
1025 {}
1026
1028 infimum(const infimum&) noexcept = default;
1029 infimum(infimum&&) noexcept = default;
1030 infimum& operator=(const infimum&) noexcept = default;
1031 infimum& operator=(infimum&&) noexcept = default;
1032
1033 const data::variable_list& variables() const
1034 {
1035 return atermpp::down_cast<data::variable_list>((*this)[0]);
1036 }
1037
1038 const state_formula& body() const
1039 {
1040 return atermpp::down_cast<state_formula>((*this)[1]);
1041 }
1042};
1043
1046template <class... ARGUMENTS>
1047inline void make_infimum(atermpp::aterm& t, const ARGUMENTS&... args)
1048{
1049 atermpp::make_term_appl(t, core::detail::function_symbol_StateInfimum(), args...);
1050}
1051
1055inline
1057{
1058 return x.function() == core::detail::function_symbols::StateInfimum;
1059}
1060
1061// prototype declaration
1062std::string pp(const infimum& x);
1063
1068inline
1069std::ostream& operator<<(std::ostream& out, const infimum& x)
1070{
1071 return out << state_formulas::pp(x);
1072}
1073
1075inline void swap(infimum& t1, infimum& t2)
1076{
1077 t1.swap(t2);
1078}
1079
1080
1083{
1084 public:
1087 : state_formula(core::detail::default_values::StateSupremum)
1088 {}
1089
1092 explicit supremum(const atermpp::aterm& term)
1093 : state_formula(term)
1094 {
1095 assert(core::detail::check_term_StateSupremum(*this));
1096 }
1097
1099 supremum(const data::variable_list& variables, const state_formula& body)
1100 : state_formula(atermpp::aterm(core::detail::function_symbol_StateSupremum(), variables, body))
1101 {}
1102
1104 supremum(const supremum&) noexcept = default;
1105 supremum(supremum&&) noexcept = default;
1106 supremum& operator=(const supremum&) noexcept = default;
1107 supremum& operator=(supremum&&) noexcept = default;
1108
1109 const data::variable_list& variables() const
1110 {
1111 return atermpp::down_cast<data::variable_list>((*this)[0]);
1112 }
1113
1114 const state_formula& body() const
1115 {
1116 return atermpp::down_cast<state_formula>((*this)[1]);
1117 }
1118};
1119
1122template <class... ARGUMENTS>
1123inline void make_supremum(atermpp::aterm& t, const ARGUMENTS&... args)
1124{
1125 atermpp::make_term_appl(t, core::detail::function_symbol_StateSupremum(), args...);
1126}
1127
1131inline
1133{
1134 return x.function() == core::detail::function_symbols::StateSupremum;
1135}
1136
1137// prototype declaration
1138std::string pp(const supremum& x);
1139
1144inline
1145std::ostream& operator<<(std::ostream& out, const supremum& x)
1146{
1147 return out << state_formulas::pp(x);
1148}
1149
1151inline void swap(supremum& t1, supremum& t2)
1152{
1153 t1.swap(t2);
1154}
1155
1156
1158class sum: public state_formula
1159{
1160 public:
1163 : state_formula(core::detail::default_values::StateSum)
1164 {}
1165
1168 explicit sum(const atermpp::aterm& term)
1169 : state_formula(term)
1170 {
1171 assert(core::detail::check_term_StateSum(*this));
1172 }
1173
1175 sum(const data::variable_list& variables, const state_formula& body)
1176 : state_formula(atermpp::aterm(core::detail::function_symbol_StateSum(), variables, body))
1177 {}
1178
1180 sum(const sum&) noexcept = default;
1181 sum(sum&&) noexcept = default;
1182 sum& operator=(const sum&) noexcept = default;
1183 sum& operator=(sum&&) noexcept = default;
1184
1185 const data::variable_list& variables() const
1186 {
1187 return atermpp::down_cast<data::variable_list>((*this)[0]);
1188 }
1189
1190 const state_formula& body() const
1191 {
1192 return atermpp::down_cast<state_formula>((*this)[1]);
1193 }
1194};
1195
1198template <class... ARGUMENTS>
1199inline void make_sum(atermpp::aterm& t, const ARGUMENTS&... args)
1200{
1201 atermpp::make_term_appl(t, core::detail::function_symbol_StateSum(), args...);
1202}
1203
1207inline
1209{
1210 return x.function() == core::detail::function_symbols::StateSum;
1211}
1212
1213// prototype declaration
1214std::string pp(const sum& x);
1215
1220inline
1221std::ostream& operator<<(std::ostream& out, const sum& x)
1222{
1223 return out << state_formulas::pp(x);
1224}
1225
1227inline void swap(sum& t1, sum& t2)
1228{
1229 t1.swap(t2);
1230}
1231
1232
1234class must: public state_formula
1235{
1236 public:
1239 : state_formula(core::detail::default_values::StateMust)
1240 {}
1241
1244 explicit must(const atermpp::aterm& term)
1245 : state_formula(term)
1246 {
1247 assert(core::detail::check_term_StateMust(*this));
1248 }
1249
1252 : state_formula(atermpp::aterm(core::detail::function_symbol_StateMust(), formula, operand))
1253 {}
1254
1256 must(const must&) noexcept = default;
1257 must(must&&) noexcept = default;
1258 must& operator=(const must&) noexcept = default;
1259 must& operator=(must&&) noexcept = default;
1260
1261 const regular_formulas::regular_formula& formula() const
1262 {
1263 return atermpp::down_cast<regular_formulas::regular_formula>((*this)[0]);
1264 }
1265
1266 const state_formula& operand() const
1267 {
1268 return atermpp::down_cast<state_formula>((*this)[1]);
1269 }
1270};
1271
1274template <class... ARGUMENTS>
1275inline void make_must(atermpp::aterm& t, const ARGUMENTS&... args)
1276{
1277 atermpp::make_term_appl(t, core::detail::function_symbol_StateMust(), args...);
1278}
1279
1283inline
1285{
1286 return x.function() == core::detail::function_symbols::StateMust;
1287}
1288
1289// prototype declaration
1290std::string pp(const must& x);
1291
1296inline
1297std::ostream& operator<<(std::ostream& out, const must& x)
1298{
1299 return out << state_formulas::pp(x);
1300}
1301
1303inline void swap(must& t1, must& t2)
1304{
1305 t1.swap(t2);
1306}
1307
1308
1310class may: public state_formula
1311{
1312 public:
1315 : state_formula(core::detail::default_values::StateMay)
1316 {}
1317
1320 explicit may(const atermpp::aterm& term)
1321 : state_formula(term)
1322 {
1323 assert(core::detail::check_term_StateMay(*this));
1324 }
1325
1328 : state_formula(atermpp::aterm(core::detail::function_symbol_StateMay(), formula, operand))
1329 {}
1330
1332 may(const may&) noexcept = default;
1333 may(may&&) noexcept = default;
1334 may& operator=(const may&) noexcept = default;
1335 may& operator=(may&&) noexcept = default;
1336
1337 const regular_formulas::regular_formula& formula() const
1338 {
1339 return atermpp::down_cast<regular_formulas::regular_formula>((*this)[0]);
1340 }
1341
1342 const state_formula& operand() const
1343 {
1344 return atermpp::down_cast<state_formula>((*this)[1]);
1345 }
1346};
1347
1350template <class... ARGUMENTS>
1351inline void make_may(atermpp::aterm& t, const ARGUMENTS&... args)
1352{
1353 atermpp::make_term_appl(t, core::detail::function_symbol_StateMay(), args...);
1354}
1355
1359inline
1361{
1362 return x.function() == core::detail::function_symbols::StateMay;
1363}
1364
1365// prototype declaration
1366std::string pp(const may& x);
1367
1372inline
1373std::ostream& operator<<(std::ostream& out, const may& x)
1374{
1375 return out << state_formulas::pp(x);
1376}
1377
1379inline void swap(may& t1, may& t2)
1380{
1381 t1.swap(t2);
1382}
1383
1384
1387{
1388 public:
1391 : state_formula(core::detail::default_values::StateYaled)
1392 {}
1393
1396 explicit yaled(const atermpp::aterm& term)
1397 : state_formula(term)
1398 {
1399 assert(core::detail::check_term_StateYaled(*this));
1400 }
1401
1403 yaled(const yaled&) noexcept = default;
1404 yaled(yaled&&) noexcept = default;
1405 yaled& operator=(const yaled&) noexcept = default;
1406 yaled& operator=(yaled&&) noexcept = default;
1407};
1408
1412inline
1413bool is_yaled(const atermpp::aterm& x)
1414{
1415 return x.function() == core::detail::function_symbols::StateYaled;
1416}
1417
1418// prototype declaration
1419std::string pp(const yaled& x);
1420
1425inline
1426std::ostream& operator<<(std::ostream& out, const yaled& x)
1427{
1428 return out << state_formulas::pp(x);
1429}
1430
1432inline void swap(yaled& t1, yaled& t2)
1433{
1434 t1.swap(t2);
1435}
1436
1437
1440{
1441 public:
1444 : state_formula(core::detail::default_values::StateYaledTimed)
1445 {}
1446
1449 explicit yaled_timed(const atermpp::aterm& term)
1450 : state_formula(term)
1451 {
1452 assert(core::detail::check_term_StateYaledTimed(*this));
1453 }
1454
1456 explicit yaled_timed(const data::data_expression& time_stamp)
1457 : state_formula(atermpp::aterm(core::detail::function_symbol_StateYaledTimed(), time_stamp))
1458 {}
1459
1461 yaled_timed(const yaled_timed&) noexcept = default;
1462 yaled_timed(yaled_timed&&) noexcept = default;
1463 yaled_timed& operator=(const yaled_timed&) noexcept = default;
1464 yaled_timed& operator=(yaled_timed&&) noexcept = default;
1465
1466 const data::data_expression& time_stamp() const
1467 {
1468 return atermpp::down_cast<data::data_expression>((*this)[0]);
1469 }
1470};
1471
1474template <class... ARGUMENTS>
1475inline void make_yaled_timed(atermpp::aterm& t, const ARGUMENTS&... args)
1476{
1477 atermpp::make_term_appl(t, core::detail::function_symbol_StateYaledTimed(), args...);
1478}
1479
1483inline
1485{
1486 return x.function() == core::detail::function_symbols::StateYaledTimed;
1487}
1488
1489// prototype declaration
1490std::string pp(const yaled_timed& x);
1491
1496inline
1497std::ostream& operator<<(std::ostream& out, const yaled_timed& x)
1498{
1499 return out << state_formulas::pp(x);
1500}
1501
1503inline void swap(yaled_timed& t1, yaled_timed& t2)
1504{
1505 t1.swap(t2);
1506}
1507
1508
1511{
1512 public:
1515 : state_formula(core::detail::default_values::StateDelay)
1516 {}
1517
1520 explicit delay(const atermpp::aterm& term)
1521 : state_formula(term)
1522 {
1523 assert(core::detail::check_term_StateDelay(*this));
1524 }
1525
1527 delay(const delay&) noexcept = default;
1528 delay(delay&&) noexcept = default;
1529 delay& operator=(const delay&) noexcept = default;
1530 delay& operator=(delay&&) noexcept = default;
1531};
1532
1536inline
1537bool is_delay(const atermpp::aterm& x)
1538{
1539 return x.function() == core::detail::function_symbols::StateDelay;
1540}
1541
1542// prototype declaration
1543std::string pp(const delay& x);
1544
1549inline
1550std::ostream& operator<<(std::ostream& out, const delay& x)
1551{
1552 return out << state_formulas::pp(x);
1553}
1554
1556inline void swap(delay& t1, delay& t2)
1557{
1558 t1.swap(t2);
1559}
1560
1561
1564{
1565 public:
1568 : state_formula(core::detail::default_values::StateDelayTimed)
1569 {}
1570
1573 explicit delay_timed(const atermpp::aterm& term)
1574 : state_formula(term)
1575 {
1576 assert(core::detail::check_term_StateDelayTimed(*this));
1577 }
1578
1580 explicit delay_timed(const data::data_expression& time_stamp)
1581 : state_formula(atermpp::aterm(core::detail::function_symbol_StateDelayTimed(), time_stamp))
1582 {}
1583
1585 delay_timed(const delay_timed&) noexcept = default;
1586 delay_timed(delay_timed&&) noexcept = default;
1587 delay_timed& operator=(const delay_timed&) noexcept = default;
1588 delay_timed& operator=(delay_timed&&) noexcept = default;
1589
1590 const data::data_expression& time_stamp() const
1591 {
1592 return atermpp::down_cast<data::data_expression>((*this)[0]);
1593 }
1594};
1595
1598template <class... ARGUMENTS>
1599inline void make_delay_timed(atermpp::aterm& t, const ARGUMENTS&... args)
1600{
1601 atermpp::make_term_appl(t, core::detail::function_symbol_StateDelayTimed(), args...);
1602}
1603
1607inline
1609{
1610 return x.function() == core::detail::function_symbols::StateDelayTimed;
1611}
1612
1613// prototype declaration
1614std::string pp(const delay_timed& x);
1615
1620inline
1621std::ostream& operator<<(std::ostream& out, const delay_timed& x)
1622{
1623 return out << state_formulas::pp(x);
1624}
1625
1627inline void swap(delay_timed& t1, delay_timed& t2)
1628{
1629 t1.swap(t2);
1630}
1631
1632
1635{
1636 public:
1639 : state_formula(core::detail::default_values::StateVar)
1640 {}
1641
1644 explicit variable(const atermpp::aterm& term)
1645 : state_formula(term)
1646 {
1647 assert(core::detail::check_term_StateVar(*this));
1648 }
1649
1652 : state_formula(atermpp::aterm(core::detail::function_symbol_StateVar(), name, arguments))
1653 {}
1654
1656 variable(const std::string& name, const data::data_expression_list& arguments)
1657 : state_formula(atermpp::aterm(core::detail::function_symbol_StateVar(), core::identifier_string(name), arguments))
1658 {}
1659
1661 variable(const variable&) noexcept = default;
1662 variable(variable&&) noexcept = default;
1663 variable& operator=(const variable&) noexcept = default;
1664 variable& operator=(variable&&) noexcept = default;
1665
1666 const core::identifier_string& name() const
1667 {
1668 return atermpp::down_cast<core::identifier_string>((*this)[0]);
1669 }
1670
1672 {
1673 return atermpp::down_cast<data::data_expression_list>((*this)[1]);
1674 }
1675};
1676
1679template <class... ARGUMENTS>
1680inline void make_variable(atermpp::aterm& t, const ARGUMENTS&... args)
1681{
1682 atermpp::make_term_appl(t, core::detail::function_symbol_StateVar(), args...);
1683}
1684
1688inline
1689bool is_variable(const atermpp::aterm& x)
1690{
1691 return x.function() == core::detail::function_symbols::StateVar;
1692}
1693
1694// prototype declaration
1695std::string pp(const variable& x);
1696
1701inline
1702std::ostream& operator<<(std::ostream& out, const variable& x)
1703{
1704 return out << state_formulas::pp(x);
1705}
1706
1708inline void swap(variable& t1, variable& t2)
1709{
1710 t1.swap(t2);
1711}
1712
1713
1715class nu: public state_formula
1716{
1717 public:
1720 : state_formula(core::detail::default_values::StateNu)
1721 {}
1722
1725 explicit nu(const atermpp::aterm& term)
1726 : state_formula(term)
1727 {
1728 assert(core::detail::check_term_StateNu(*this));
1729 }
1730
1732 nu(const core::identifier_string& name, const data::assignment_list& assignments, const state_formula& operand)
1733 : state_formula(atermpp::aterm(core::detail::function_symbol_StateNu(), name, assignments, operand))
1734 {}
1735
1737 nu(const std::string& name, const data::assignment_list& assignments, const state_formula& operand)
1738 : state_formula(atermpp::aterm(core::detail::function_symbol_StateNu(), core::identifier_string(name), assignments, operand))
1739 {}
1740
1742 nu(const nu&) noexcept = default;
1743 nu(nu&&) noexcept = default;
1744 nu& operator=(const nu&) noexcept = default;
1745 nu& operator=(nu&&) noexcept = default;
1746
1747 const core::identifier_string& name() const
1748 {
1749 return atermpp::down_cast<core::identifier_string>((*this)[0]);
1750 }
1751
1753 {
1754 return atermpp::down_cast<data::assignment_list>((*this)[1]);
1755 }
1756
1757 const state_formula& operand() const
1758 {
1759 return atermpp::down_cast<state_formula>((*this)[2]);
1760 }
1761};
1762
1765template <class... ARGUMENTS>
1766inline void make_nu(atermpp::aterm& t, const ARGUMENTS&... args)
1767{
1768 atermpp::make_term_appl(t, core::detail::function_symbol_StateNu(), args...);
1769}
1770
1774inline
1775bool is_nu(const atermpp::aterm& x)
1776{
1777 return x.function() == core::detail::function_symbols::StateNu;
1778}
1779
1780// prototype declaration
1781std::string pp(const nu& x);
1782
1787inline
1788std::ostream& operator<<(std::ostream& out, const nu& x)
1789{
1790 return out << state_formulas::pp(x);
1791}
1792
1794inline void swap(nu& t1, nu& t2)
1795{
1796 t1.swap(t2);
1797}
1798
1799
1801class mu: public state_formula
1802{
1803 public:
1806 : state_formula(core::detail::default_values::StateMu)
1807 {}
1808
1811 explicit mu(const atermpp::aterm& term)
1812 : state_formula(term)
1813 {
1814 assert(core::detail::check_term_StateMu(*this));
1815 }
1816
1818 mu(const core::identifier_string& name, const data::assignment_list& assignments, const state_formula& operand)
1819 : state_formula(atermpp::aterm(core::detail::function_symbol_StateMu(), name, assignments, operand))
1820 {}
1821
1823 mu(const std::string& name, const data::assignment_list& assignments, const state_formula& operand)
1824 : state_formula(atermpp::aterm(core::detail::function_symbol_StateMu(), core::identifier_string(name), assignments, operand))
1825 {}
1826
1828 mu(const mu&) noexcept = default;
1829 mu(mu&&) noexcept = default;
1830 mu& operator=(const mu&) noexcept = default;
1831 mu& operator=(mu&&) noexcept = default;
1832
1833 const core::identifier_string& name() const
1834 {
1835 return atermpp::down_cast<core::identifier_string>((*this)[0]);
1836 }
1837
1839 {
1840 return atermpp::down_cast<data::assignment_list>((*this)[1]);
1841 }
1842
1843 const state_formula& operand() const
1844 {
1845 return atermpp::down_cast<state_formula>((*this)[2]);
1846 }
1847};
1848
1851template <class... ARGUMENTS>
1852inline void make_mu(atermpp::aterm& t, const ARGUMENTS&... args)
1853{
1854 atermpp::make_term_appl(t, core::detail::function_symbol_StateMu(), args...);
1855}
1856
1860inline
1861bool is_mu(const atermpp::aterm& x)
1862{
1863 return x.function() == core::detail::function_symbols::StateMu;
1864}
1865
1866// prototype declaration
1867std::string pp(const mu& x);
1868
1873inline
1874std::ostream& operator<<(std::ostream& out, const mu& x)
1875{
1876 return out << state_formulas::pp(x);
1877}
1878
1880inline void swap(mu& t1, mu& t2)
1881{
1882 t1.swap(t2);
1883}
1884//--- end generated classes ---//
1885
1886namespace algorithms {
1887 bool is_timed(const state_formula& x);
1888} // namespace algorithms
1889
1892inline
1893bool state_formula::has_time() const
1894{
1895 return algorithms::is_timed(*this);
1896}
1897
1898// template function overloads
1899state_formula normalize_sorts(const state_formula& x, const data::sort_specification& sortspec);
1900state_formulas::state_formula translate_user_notation(const state_formulas::state_formula& x);
1901std::set<data::sort_expression> find_sort_expressions(const state_formulas::state_formula& x);
1902std::set<data::variable> find_all_variables(const state_formulas::state_formula& x);
1903std::set<data::variable> find_free_variables(const state_formulas::state_formula& x);
1904std::set<core::identifier_string> find_identifiers(const state_formulas::state_formula& x);
1905std::set<process::action_label> find_action_labels(const state_formulas::state_formula& x);
1907
1908} // namespace state_formulas
1909
1910} // namespace mcrl2
1911
1912#endif // MCRL2_MODAL_FORMULA_STATE_FORMULA_H
void swap(StaticGraph &a, StaticGraph &b)
Definition Graph.h:297
Term containing a string.
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
\brief The and operator for state formulas
and_(and_ &&) noexcept=default
const state_formula & right() const
and_(const atermpp::aterm &term)
and_(const and_ &) noexcept=default
Move semantics.
and_(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
and_()
\brief Default constructor X3.
\brief The multiply operator for state formulas with values
const_multiply_alt(const state_formula &left, const data::data_expression &right)
\brief Constructor Z14.
const_multiply_alt(const const_multiply_alt &) noexcept=default
Move semantics.
const_multiply_alt(const_multiply_alt &&) noexcept=default
const data::data_expression & right() const
const_multiply_alt(const atermpp::aterm &term)
const_multiply_alt()
\brief Default constructor X3.
\brief The multiply operator for state formulas with values
const_multiply(const const_multiply &) noexcept=default
Move semantics.
const_multiply(const data::data_expression &left, const state_formula &right)
\brief Constructor Z14.
const_multiply()
\brief Default constructor X3.
const_multiply(const_multiply &&) noexcept=default
const_multiply(const atermpp::aterm &term)
const state_formula & right() const
\brief The timed delay operator for state formulas
delay_timed(const atermpp::aterm &term)
delay_timed()
\brief Default constructor X3.
delay_timed(const data::data_expression &time_stamp)
\brief Constructor Z14.
delay_timed(const delay_timed &) noexcept=default
Move semantics.
delay_timed(delay_timed &&) noexcept=default
\brief The delay operator for state formulas
delay()
\brief Default constructor X3.
delay(const delay &) noexcept=default
Move semantics.
delay(delay &&) noexcept=default
delay(const atermpp::aterm &term)
\brief The existential quantification operator for state formulas
exists(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
const state_formula & body() const
exists(const exists &) noexcept=default
Move semantics.
exists(exists &&) noexcept=default
exists()
\brief Default constructor X3.
exists(const atermpp::aterm &term)
\brief The value false for state formulas
false_(false_ &&) noexcept=default
false_(const atermpp::aterm &term)
false_(const false_ &) noexcept=default
Move semantics.
false_()
\brief Default constructor X3.
\brief The universal quantification operator for state formulas
const state_formula & body() const
forall(const atermpp::aterm &term)
forall(const forall &) noexcept=default
Move semantics.
forall(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
forall(forall &&) noexcept=default
forall()
\brief Default constructor X3.
\brief The implication operator for state formulas
imp()
\brief Default constructor X3.
imp(imp &&) noexcept=default
imp(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
const state_formula & right() const
imp(const atermpp::aterm &term)
imp(const imp &) noexcept=default
Move semantics.
\brief The infimum over a data type for state formulas
infimum(const infimum &) noexcept=default
Move semantics.
infimum()
\brief Default constructor X3.
infimum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
const state_formula & body() const
infimum(const atermpp::aterm &term)
infimum(infimum &&) noexcept=default
\brief The may operator for state formulas
const state_formula & operand() const
may()
\brief Default constructor X3.
may(const regular_formulas::regular_formula &formula, const state_formula &operand)
\brief Constructor Z14.
may(may &&) noexcept=default
may(const atermpp::aterm &term)
may(const may &) noexcept=default
Move semantics.
\brief The minus operator for state formulas
minus(minus &&) noexcept=default
minus(const minus &) noexcept=default
Move semantics.
minus(const atermpp::aterm &term)
minus(const state_formula &operand)
\brief Constructor Z14.
minus()
\brief Default constructor X3.
\brief The mu operator for state formulas
const data::assignment_list & assignments() const
mu(const mu &) noexcept=default
Move semantics.
mu(const std::string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z2.
mu(const core::identifier_string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z14.
mu(mu &&) noexcept=default
mu(const atermpp::aterm &term)
mu()
\brief Default constructor X3.
const state_formula & operand() const
\brief The must operator for state formulas
must(must &&) noexcept=default
must(const atermpp::aterm &term)
must(const regular_formulas::regular_formula &formula, const state_formula &operand)
\brief Constructor Z14.
must(const must &) noexcept=default
Move semantics.
const state_formula & operand() const
must()
\brief Default constructor X3.
\brief The not operator for state formulas
not_(not_ &&) noexcept=default
not_(const not_ &) noexcept=default
Move semantics.
not_()
\brief Default constructor X3.
not_(const atermpp::aterm &term)
not_(const state_formula &operand)
\brief Constructor Z14.
\brief The nu operator for state formulas
nu(const atermpp::aterm &term)
nu(nu &&) noexcept=default
nu(const core::identifier_string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z14.
nu()
\brief Default constructor X3.
nu(const std::string &name, const data::assignment_list &assignments, const state_formula &operand)
\brief Constructor Z2.
const state_formula & operand() const
nu(const nu &) noexcept=default
Move semantics.
const data::assignment_list & assignments() const
\brief The or operator for state formulas
or_(or_ &&) noexcept=default
or_()
\brief Default constructor X3.
or_(const or_ &) noexcept=default
Move semantics.
or_(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
const state_formula & right() const
or_(const atermpp::aterm &term)
\brief The plus operator for state formulas with values
plus(const plus &) noexcept=default
Move semantics.
plus(const atermpp::aterm &term)
plus()
\brief Default constructor X3.
const state_formula & right() const
plus(plus &&) noexcept=default
plus(const state_formula &left, const state_formula &right)
\brief Constructor Z14.
state_formula(const state_formula &) noexcept=default
Move semantics.
state_formula()
\brief Default constructor X3.
state_formula(state_formula &&) noexcept=default
bool has_time() const
Returns true if the formula is timed.
state_formula(const data::untyped_data_parameter &x)
\brief Constructor Z6.
state_formula(const data::data_expression &x)
\brief Constructor Z6.
state_formula(const atermpp::aterm &term)
\brief The sum over a data type for state formulas
sum(const sum &) noexcept=default
Move semantics.
sum(sum &&) noexcept=default
sum(const atermpp::aterm &term)
sum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
sum()
\brief Default constructor X3.
const state_formula & body() const
\brief The supremum over a data type for state formulas
supremum(supremum &&) noexcept=default
supremum(const atermpp::aterm &term)
supremum()
\brief Default constructor X3.
supremum(const supremum &) noexcept=default
Move semantics.
const state_formula & body() const
supremum(const data::variable_list &variables, const state_formula &body)
\brief Constructor Z14.
\brief The value true for state formulas
true_()
\brief Default constructor X3.
true_(true_ &&) noexcept=default
true_(const true_ &) noexcept=default
Move semantics.
true_(const atermpp::aterm &term)
\brief The state formula variable
variable(const core::identifier_string &name, const data::data_expression_list &arguments)
\brief Constructor Z14.
variable(const variable &) noexcept=default
Move semantics.
variable(const std::string &name, const data::data_expression_list &arguments)
\brief Constructor Z2.
variable()
\brief Default constructor X3.
const data::data_expression_list & arguments() const
variable(variable &&) noexcept=default
variable(const atermpp::aterm &term)
\brief The timed yaled operator for state formulas
yaled_timed(yaled_timed &&) noexcept=default
yaled_timed()
\brief Default constructor X3.
yaled_timed(const yaled_timed &) noexcept=default
Move semantics.
yaled_timed(const data::data_expression &time_stamp)
\brief Constructor Z14.
yaled_timed(const atermpp::aterm &term)
\brief The yaled operator for state formulas
yaled()
\brief Default constructor X3.
yaled(const atermpp::aterm &term)
yaled(const yaled &) noexcept=default
Move semantics.
yaled(yaled &&) noexcept=default
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
bool check_rule_StateFrm(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_infimum(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
bool is_delay_timed(const atermpp::aterm &x)
bool is_const_multiply(const atermpp::aterm &x)
bool is_minus(const atermpp::aterm &x)
bool is_exists(const atermpp::aterm &x)
bool is_not(const atermpp::aterm &x)
bool is_state_formula(const atermpp::aterm &x)
void make_const_multiply(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_supremum(const atermpp::aterm &x)
bool is_must(const atermpp::aterm &x)
bool is_yaled(const atermpp::aterm &x)
bool is_true(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const state_formula &x)
bool is_variable(const atermpp::aterm &x)
void make_infimum(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_may(const atermpp::aterm &x)
bool is_yaled_timed(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
void make_delay_timed(atermpp::aterm &t, const ARGUMENTS &... args)
std::vector< state_formula > state_formula_vector
\brief vector of state_formulas
void make_const_multiply_alt(atermpp::aterm &t, const ARGUMENTS &... args)
void pp(const T &t, std::ostream &out)
Prints the object t to a stream.
Definition print.h:668
void make_may(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_sum(const atermpp::aterm &x)
void make_must(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_nu(const atermpp::aterm &x)
bool is_delay(const atermpp::aterm &x)
bool is_false(const atermpp::aterm &x)
void make_nu(atermpp::aterm &t, const ARGUMENTS &... args)
void make_supremum(atermpp::aterm &t, const ARGUMENTS &... args)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_plus(const atermpp::aterm &x)
void swap(state_formula &t1, state_formula &t2)
\brief swap overload
bool is_mu(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
bool is_const_multiply_alt(const atermpp::aterm &x)
bool is_or(const atermpp::aterm &x)
void make_yaled_timed(atermpp::aterm &t, const ARGUMENTS &... args)
bool find_nil(const state_formulas::state_formula &x)
void make_mu(atermpp::aterm &t, const ARGUMENTS &... args)
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.