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/state_formula.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_STATE_FORMULA_H
13 : #define MCRL2_MODAL_FORMULA_STATE_FORMULA_H
14 :
15 : #include "mcrl2/modal_formula/regular_formula.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace state_formulas
21 : {
22 :
23 : //--- start generated classes ---//
24 : /// \\brief A state formula
25 : class state_formula: public atermpp::aterm_appl
26 : {
27 : public:
28 : /// \\brief Default constructor.
29 1951 : state_formula()
30 1951 : : atermpp::aterm_appl(core::detail::default_values::StateFrm)
31 1951 : {}
32 :
33 : /// \\brief Constructor.
34 : /// \\param term A term
35 62004 : explicit state_formula(const atermpp::aterm& term)
36 62004 : : atermpp::aterm_appl(term)
37 : {
38 62004 : assert(core::detail::check_rule_StateFrm(*this));
39 62004 : }
40 :
41 : /// \\brief Constructor.
42 127 : state_formula(const data::data_expression& x)
43 127 : : atermpp::aterm_appl(x)
44 127 : {}
45 :
46 : /// \\brief Constructor.
47 143 : state_formula(const data::untyped_data_parameter& x)
48 143 : : atermpp::aterm_appl(x)
49 143 : {}
50 :
51 : /// Move semantics
52 1710 : state_formula(const state_formula&) noexcept = default;
53 2001 : state_formula(state_formula&&) noexcept = default;
54 1483 : state_formula& operator=(const state_formula&) noexcept = default;
55 2448 : state_formula& operator=(state_formula&&) noexcept = default;
56 : //--- start user section state_formula ---//
57 : /// \brief Returns true if the formula is timed.
58 : /// \return True if the formula is timed.
59 : bool has_time() const;
60 : //--- end user section state_formula ---//
61 : };
62 :
63 : /// \\brief list of state_formulas
64 : typedef atermpp::term_list<state_formula> state_formula_list;
65 :
66 : /// \\brief vector of state_formulas
67 : typedef std::vector<state_formula> state_formula_vector;
68 :
69 : // prototypes
70 : inline bool is_true(const atermpp::aterm_appl& x);
71 : inline bool is_false(const atermpp::aterm_appl& x);
72 : inline bool is_not(const atermpp::aterm_appl& x);
73 : inline bool is_minus(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_plus(const atermpp::aterm_appl& x);
78 : inline bool is_const_multiply(const atermpp::aterm_appl& x);
79 : inline bool is_const_multiply_alt(const atermpp::aterm_appl& x);
80 : inline bool is_forall(const atermpp::aterm_appl& x);
81 : inline bool is_exists(const atermpp::aterm_appl& x);
82 : inline bool is_infimum(const atermpp::aterm_appl& x);
83 : inline bool is_supremum(const atermpp::aterm_appl& x);
84 : inline bool is_sum(const atermpp::aterm_appl& x);
85 : inline bool is_must(const atermpp::aterm_appl& x);
86 : inline bool is_may(const atermpp::aterm_appl& x);
87 : inline bool is_yaled(const atermpp::aterm_appl& x);
88 : inline bool is_yaled_timed(const atermpp::aterm_appl& x);
89 : inline bool is_delay(const atermpp::aterm_appl& x);
90 : inline bool is_delay_timed(const atermpp::aterm_appl& x);
91 : inline bool is_variable(const atermpp::aterm_appl& x);
92 : inline bool is_nu(const atermpp::aterm_appl& x);
93 : inline bool is_mu(const atermpp::aterm_appl& x);
94 :
95 : /// \\brief Test for a state_formula expression
96 : /// \\param x A term
97 : /// \\return True if \\a x is a state_formula expression
98 : inline
99 : bool is_state_formula(const atermpp::aterm_appl& x)
100 : {
101 : return data::is_data_expression(x) ||
102 : data::is_untyped_data_parameter(x) ||
103 : state_formulas::is_true(x) ||
104 : state_formulas::is_false(x) ||
105 : state_formulas::is_not(x) ||
106 : state_formulas::is_minus(x) ||
107 : state_formulas::is_and(x) ||
108 : state_formulas::is_or(x) ||
109 : state_formulas::is_imp(x) ||
110 : state_formulas::is_plus(x) ||
111 : state_formulas::is_const_multiply(x) ||
112 : state_formulas::is_const_multiply_alt(x) ||
113 : state_formulas::is_forall(x) ||
114 : state_formulas::is_exists(x) ||
115 : state_formulas::is_infimum(x) ||
116 : state_formulas::is_supremum(x) ||
117 : state_formulas::is_sum(x) ||
118 : state_formulas::is_must(x) ||
119 : state_formulas::is_may(x) ||
120 : state_formulas::is_yaled(x) ||
121 : state_formulas::is_yaled_timed(x) ||
122 : state_formulas::is_delay(x) ||
123 : state_formulas::is_delay_timed(x) ||
124 : state_formulas::is_variable(x) ||
125 : state_formulas::is_nu(x) ||
126 : state_formulas::is_mu(x);
127 : }
128 :
129 : // prototype declaration
130 : std::string pp(const state_formula& x);
131 :
132 : /// \\brief Outputs the object to a stream
133 : /// \\param out An output stream
134 : /// \\param x Object x
135 : /// \\return The output stream
136 : inline
137 82 : std::ostream& operator<<(std::ostream& out, const state_formula& x)
138 : {
139 82 : return out << state_formulas::pp(x);
140 : }
141 :
142 : /// \\brief swap overload
143 : inline void swap(state_formula& t1, state_formula& t2)
144 : {
145 : t1.swap(t2);
146 : }
147 :
148 :
149 : /// \\brief The value true for state formulas
150 : class true_: public state_formula
151 : {
152 : public:
153 : /// \\brief Default constructor.
154 128 : true_()
155 128 : : state_formula(core::detail::default_values::StateTrue)
156 128 : {}
157 :
158 : /// \\brief Constructor.
159 : /// \\param term A term
160 1966 : explicit true_(const atermpp::aterm& term)
161 1966 : : state_formula(term)
162 : {
163 1966 : assert(core::detail::check_term_StateTrue(*this));
164 1966 : }
165 :
166 : /// Move semantics
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 :
173 : /// \\brief Test for a true expression
174 : /// \\param x A term
175 : /// \\return True if \\a x is a true expression
176 : inline
177 31140 : bool is_true(const atermpp::aterm_appl& x)
178 : {
179 31140 : return x.function() == core::detail::function_symbols::StateTrue;
180 : }
181 :
182 : // prototype declaration
183 : std::string pp(const true_& x);
184 :
185 : /// \\brief Outputs the object to a stream
186 : /// \\param out An output stream
187 : /// \\param x Object x
188 : /// \\return The output stream
189 : inline
190 : std::ostream& operator<<(std::ostream& out, const true_& x)
191 : {
192 : return out << state_formulas::pp(x);
193 : }
194 :
195 : /// \\brief swap overload
196 : inline void swap(true_& t1, true_& t2)
197 : {
198 : t1.swap(t2);
199 : }
200 :
201 :
202 : /// \\brief The value false for state formulas
203 : class false_: public state_formula
204 : {
205 : public:
206 : /// \\brief Default constructor.
207 84 : false_()
208 84 : : state_formula(core::detail::default_values::StateFalse)
209 84 : {}
210 :
211 : /// \\brief Constructor.
212 : /// \\param term A term
213 1964 : explicit false_(const atermpp::aterm& term)
214 1964 : : state_formula(term)
215 : {
216 1964 : assert(core::detail::check_term_StateFalse(*this));
217 1964 : }
218 :
219 : /// Move semantics
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 :
226 : /// \\brief Test for a false expression
227 : /// \\param x A term
228 : /// \\return True if \\a x is a false expression
229 : inline
230 28896 : bool is_false(const atermpp::aterm_appl& x)
231 : {
232 28896 : return x.function() == core::detail::function_symbols::StateFalse;
233 : }
234 :
235 : // prototype declaration
236 : std::string pp(const false_& x);
237 :
238 : /// \\brief Outputs the object to a stream
239 : /// \\param out An output stream
240 : /// \\param x Object x
241 : /// \\return The output stream
242 : inline
243 : std::ostream& operator<<(std::ostream& out, const false_& x)
244 : {
245 : return out << state_formulas::pp(x);
246 : }
247 :
248 : /// \\brief swap overload
249 : inline void swap(false_& t1, false_& t2)
250 : {
251 : t1.swap(t2);
252 : }
253 :
254 :
255 : /// \\brief The not operator for state formulas
256 : class not_: public state_formula
257 : {
258 : public:
259 : /// \\brief Default constructor.
260 : not_()
261 : : state_formula(core::detail::default_values::StateNot)
262 : {}
263 :
264 : /// \\brief Constructor.
265 : /// \\param term A term
266 1023 : explicit not_(const atermpp::aterm& term)
267 1023 : : state_formula(term)
268 : {
269 1023 : assert(core::detail::check_term_StateNot(*this));
270 1023 : }
271 :
272 : /// \\brief Constructor.
273 144 : explicit not_(const state_formula& operand)
274 144 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateNot(), operand))
275 144 : {}
276 :
277 : /// Move semantics
278 36 : 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 1016 : const state_formula& operand() const
284 : {
285 1016 : return atermpp::down_cast<state_formula>((*this)[0]);
286 : }
287 : };
288 :
289 : /// \\brief Make_not_ constructs a new term into a given address.
290 : /// \\ \param t The reference into which the new not_ is constructed.
291 : template <class... ARGUMENTS>
292 302 : inline void make_not_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
293 : {
294 302 : atermpp::make_term_appl(t, core::detail::function_symbol_StateNot(), args...);
295 302 : }
296 :
297 : /// \\brief Test for a not expression
298 : /// \\param x A term
299 : /// \\return True if \\a x is a not expression
300 : inline
301 27113 : bool is_not(const atermpp::aterm_appl& x)
302 : {
303 27113 : return x.function() == core::detail::function_symbols::StateNot;
304 : }
305 :
306 : // prototype declaration
307 : std::string pp(const not_& x);
308 :
309 : /// \\brief Outputs the object to a stream
310 : /// \\param out An output stream
311 : /// \\param x Object x
312 : /// \\return The output stream
313 : inline
314 : std::ostream& operator<<(std::ostream& out, const not_& x)
315 : {
316 : return out << state_formulas::pp(x);
317 : }
318 :
319 : /// \\brief swap overload
320 : inline void swap(not_& t1, not_& t2)
321 : {
322 : t1.swap(t2);
323 : }
324 :
325 :
326 : /// \\brief The minus operator for state formulas
327 : class minus: public state_formula
328 : {
329 : public:
330 : /// \\brief Default constructor.
331 : minus()
332 : : state_formula(core::detail::default_values::StateMinus)
333 : {}
334 :
335 : /// \\brief Constructor.
336 : /// \\param term A term
337 0 : explicit minus(const atermpp::aterm& term)
338 0 : : state_formula(term)
339 : {
340 0 : assert(core::detail::check_term_StateMinus(*this));
341 0 : }
342 :
343 : /// \\brief Constructor.
344 0 : explicit minus(const state_formula& operand)
345 0 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateMinus(), operand))
346 0 : {}
347 :
348 : /// Move semantics
349 0 : 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 0 : const state_formula& operand() const
355 : {
356 0 : return atermpp::down_cast<state_formula>((*this)[0]);
357 : }
358 : };
359 :
360 : /// \\brief Make_minus constructs a new term into a given address.
361 : /// \\ \param t The reference into which the new minus is constructed.
362 : template <class... ARGUMENTS>
363 0 : inline void make_minus(atermpp::aterm_appl& t, const ARGUMENTS&... args)
364 : {
365 0 : atermpp::make_term_appl(t, core::detail::function_symbol_StateMinus(), args...);
366 0 : }
367 :
368 : /// \\brief Test for a minus expression
369 : /// \\param x A term
370 : /// \\return True if \\a x is a minus expression
371 : inline
372 26070 : bool is_minus(const atermpp::aterm_appl& x)
373 : {
374 26070 : return x.function() == core::detail::function_symbols::StateMinus;
375 : }
376 :
377 : // prototype declaration
378 : std::string pp(const minus& x);
379 :
380 : /// \\brief Outputs the object to a stream
381 : /// \\param out An output stream
382 : /// \\param x Object x
383 : /// \\return The output stream
384 : inline
385 : std::ostream& operator<<(std::ostream& out, const minus& x)
386 : {
387 : return out << state_formulas::pp(x);
388 : }
389 :
390 : /// \\brief swap overload
391 : inline void swap(minus& t1, minus& t2)
392 : {
393 : t1.swap(t2);
394 : }
395 :
396 :
397 : /// \\brief The and operator for state formulas
398 : class and_: public state_formula
399 : {
400 : public:
401 : /// \\brief Default constructor.
402 : and_()
403 : : state_formula(core::detail::default_values::StateAnd)
404 : {}
405 :
406 : /// \\brief Constructor.
407 : /// \\param term A term
408 3592 : explicit and_(const atermpp::aterm& term)
409 3592 : : state_formula(term)
410 : {
411 3592 : assert(core::detail::check_term_StateAnd(*this));
412 3592 : }
413 :
414 : /// \\brief Constructor.
415 165 : and_(const state_formula& left, const state_formula& right)
416 165 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateAnd(), left, right))
417 165 : {}
418 :
419 : /// Move semantics
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 3514 : const state_formula& left() const
426 : {
427 3514 : return atermpp::down_cast<state_formula>((*this)[0]);
428 : }
429 :
430 3514 : const state_formula& right() const
431 : {
432 3514 : return atermpp::down_cast<state_formula>((*this)[1]);
433 : }
434 : };
435 :
436 : /// \\brief Make_and_ constructs a new term into a given address.
437 : /// \\ \param t The reference into which the new and_ is constructed.
438 : template <class... ARGUMENTS>
439 430 : inline void make_and_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
440 : {
441 430 : atermpp::make_term_appl(t, core::detail::function_symbol_StateAnd(), args...);
442 429 : }
443 :
444 : /// \\brief Test for a and expression
445 : /// \\param x A term
446 : /// \\return True if \\a x is a and expression
447 : inline
448 25845 : bool is_and(const atermpp::aterm_appl& x)
449 : {
450 25845 : return x.function() == core::detail::function_symbols::StateAnd;
451 : }
452 :
453 : // prototype declaration
454 : std::string pp(const and_& x);
455 :
456 : /// \\brief Outputs the object to a stream
457 : /// \\param out An output stream
458 : /// \\param x Object x
459 : /// \\return The output stream
460 : inline
461 : std::ostream& operator<<(std::ostream& out, const and_& x)
462 : {
463 : return out << state_formulas::pp(x);
464 : }
465 :
466 : /// \\brief swap overload
467 : inline void swap(and_& t1, and_& t2)
468 : {
469 : t1.swap(t2);
470 : }
471 :
472 :
473 : /// \\brief The or operator for state formulas
474 : class or_: public state_formula
475 : {
476 : public:
477 : /// \\brief Default constructor.
478 : or_()
479 : : state_formula(core::detail::default_values::StateOr)
480 : {}
481 :
482 : /// \\brief Constructor.
483 : /// \\param term A term
484 2282 : explicit or_(const atermpp::aterm& term)
485 2282 : : state_formula(term)
486 : {
487 2282 : assert(core::detail::check_term_StateOr(*this));
488 2282 : }
489 :
490 : /// \\brief Constructor.
491 83 : or_(const state_formula& left, const state_formula& right)
492 83 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateOr(), left, right))
493 83 : {}
494 :
495 : /// Move semantics
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 2257 : const state_formula& left() const
502 : {
503 2257 : return atermpp::down_cast<state_formula>((*this)[0]);
504 : }
505 :
506 2257 : const state_formula& right() const
507 : {
508 2257 : return atermpp::down_cast<state_formula>((*this)[1]);
509 : }
510 : };
511 :
512 : /// \\brief Make_or_ constructs a new term into a given address.
513 : /// \\ \param t The reference into which the new or_ is constructed.
514 : template <class... ARGUMENTS>
515 242 : inline void make_or_(atermpp::aterm_appl& t, const ARGUMENTS&... args)
516 : {
517 242 : atermpp::make_term_appl(t, core::detail::function_symbol_StateOr(), args...);
518 242 : }
519 :
520 : /// \\brief Test for a or expression
521 : /// \\param x A term
522 : /// \\return True if \\a x is a or expression
523 : inline
524 22328 : bool is_or(const atermpp::aterm_appl& x)
525 : {
526 22328 : return x.function() == core::detail::function_symbols::StateOr;
527 : }
528 :
529 : // prototype declaration
530 : std::string pp(const or_& x);
531 :
532 : /// \\brief Outputs the object to a stream
533 : /// \\param out An output stream
534 : /// \\param x Object x
535 : /// \\return The output stream
536 : inline
537 : std::ostream& operator<<(std::ostream& out, const or_& x)
538 : {
539 : return out << state_formulas::pp(x);
540 : }
541 :
542 : /// \\brief swap overload
543 : inline void swap(or_& t1, or_& t2)
544 : {
545 : t1.swap(t2);
546 : }
547 :
548 :
549 : /// \\brief The implication operator for state formulas
550 : class imp: public state_formula
551 : {
552 : public:
553 : /// \\brief Default constructor.
554 : imp()
555 : : state_formula(core::detail::default_values::StateImp)
556 : {}
557 :
558 : /// \\brief Constructor.
559 : /// \\param term A term
560 352 : explicit imp(const atermpp::aterm& term)
561 352 : : state_formula(term)
562 : {
563 352 : assert(core::detail::check_term_StateImp(*this));
564 352 : }
565 :
566 : /// \\brief Constructor.
567 48 : imp(const state_formula& left, const state_formula& right)
568 48 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateImp(), left, right))
569 48 : {}
570 :
571 : /// Move semantics
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 329 : const state_formula& left() const
578 : {
579 329 : return atermpp::down_cast<state_formula>((*this)[0]);
580 : }
581 :
582 328 : const state_formula& right() const
583 : {
584 328 : return atermpp::down_cast<state_formula>((*this)[1]);
585 : }
586 : };
587 :
588 : /// \\brief Make_imp constructs a new term into a given address.
589 : /// \\ \param t The reference into which the new imp is constructed.
590 : template <class... ARGUMENTS>
591 101 : inline void make_imp(atermpp::aterm_appl& t, const ARGUMENTS&... args)
592 : {
593 101 : atermpp::make_term_appl(t, core::detail::function_symbol_StateImp(), args...);
594 101 : }
595 :
596 : /// \\brief Test for a imp expression
597 : /// \\param x A term
598 : /// \\return True if \\a x is a imp expression
599 : inline
600 20068 : bool is_imp(const atermpp::aterm_appl& x)
601 : {
602 20068 : return x.function() == core::detail::function_symbols::StateImp;
603 : }
604 :
605 : // prototype declaration
606 : std::string pp(const imp& x);
607 :
608 : /// \\brief Outputs the object to a stream
609 : /// \\param out An output stream
610 : /// \\param x Object x
611 : /// \\return The output stream
612 : inline
613 : std::ostream& operator<<(std::ostream& out, const imp& x)
614 : {
615 : return out << state_formulas::pp(x);
616 : }
617 :
618 : /// \\brief swap overload
619 : inline void swap(imp& t1, imp& t2)
620 : {
621 : t1.swap(t2);
622 : }
623 :
624 :
625 : /// \\brief The plus operator for state formulas with values
626 : class plus: public state_formula
627 : {
628 : public:
629 : /// \\brief Default constructor.
630 : plus()
631 : : state_formula(core::detail::default_values::StatePlus)
632 : {}
633 :
634 : /// \\brief Constructor.
635 : /// \\param term A term
636 0 : explicit plus(const atermpp::aterm& term)
637 0 : : state_formula(term)
638 : {
639 0 : assert(core::detail::check_term_StatePlus(*this));
640 0 : }
641 :
642 : /// \\brief Constructor.
643 0 : plus(const state_formula& left, const state_formula& right)
644 0 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StatePlus(), left, right))
645 0 : {}
646 :
647 : /// Move semantics
648 0 : 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 0 : const state_formula& left() const
654 : {
655 0 : return atermpp::down_cast<state_formula>((*this)[0]);
656 : }
657 :
658 0 : const state_formula& right() const
659 : {
660 0 : return atermpp::down_cast<state_formula>((*this)[1]);
661 : }
662 : };
663 :
664 : /// \\brief Make_plus constructs a new term into a given address.
665 : /// \\ \param t The reference into which the new plus is constructed.
666 : template <class... ARGUMENTS>
667 0 : inline void make_plus(atermpp::aterm_appl& t, const ARGUMENTS&... args)
668 : {
669 0 : atermpp::make_term_appl(t, core::detail::function_symbol_StatePlus(), args...);
670 0 : }
671 :
672 : /// \\brief Test for a plus expression
673 : /// \\param x A term
674 : /// \\return True if \\a x is a plus expression
675 : inline
676 19718 : bool is_plus(const atermpp::aterm_appl& x)
677 : {
678 19718 : return x.function() == core::detail::function_symbols::StatePlus;
679 : }
680 :
681 : // prototype declaration
682 : std::string pp(const plus& x);
683 :
684 : /// \\brief Outputs the object to a stream
685 : /// \\param out An output stream
686 : /// \\param x Object x
687 : /// \\return The output stream
688 : inline
689 : std::ostream& operator<<(std::ostream& out, const plus& x)
690 : {
691 : return out << state_formulas::pp(x);
692 : }
693 :
694 : /// \\brief swap overload
695 : inline void swap(plus& t1, plus& t2)
696 : {
697 : t1.swap(t2);
698 : }
699 :
700 :
701 : /// \\brief The multiply operator for state formulas with values
702 : class const_multiply: public state_formula
703 : {
704 : public:
705 : /// \\brief Default constructor.
706 : const_multiply()
707 : : state_formula(core::detail::default_values::StateConstantMultiply)
708 : {}
709 :
710 : /// \\brief Constructor.
711 : /// \\param term A term
712 11 : explicit const_multiply(const atermpp::aterm& term)
713 11 : : state_formula(term)
714 : {
715 11 : assert(core::detail::check_term_StateConstantMultiply(*this));
716 11 : }
717 :
718 : /// \\brief Constructor.
719 2 : const_multiply(const data::data_expression& left, const state_formula& right)
720 2 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateConstantMultiply(), left, right))
721 2 : {}
722 :
723 : /// Move semantics
724 2 : 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 8 : const data::data_expression& left() const
730 : {
731 8 : return atermpp::down_cast<data::data_expression>((*this)[0]);
732 : }
733 :
734 10 : const state_formula& right() const
735 : {
736 10 : return atermpp::down_cast<state_formula>((*this)[1]);
737 : }
738 : };
739 :
740 : /// \\brief Make_const_multiply constructs a new term into a given address.
741 : /// \\ \param t The reference into which the new const_multiply is constructed.
742 : template <class... ARGUMENTS>
743 3 : inline void make_const_multiply(atermpp::aterm_appl& t, const ARGUMENTS&... args)
744 : {
745 3 : atermpp::make_term_appl(t, core::detail::function_symbol_StateConstantMultiply(), args...);
746 3 : }
747 :
748 : /// \\brief Test for a const_multiply expression
749 : /// \\param x A term
750 : /// \\return True if \\a x is a const_multiply expression
751 : inline
752 19718 : bool is_const_multiply(const atermpp::aterm_appl& x)
753 : {
754 19718 : return x.function() == core::detail::function_symbols::StateConstantMultiply;
755 : }
756 :
757 : // prototype declaration
758 : std::string pp(const const_multiply& x);
759 :
760 : /// \\brief Outputs the object to a stream
761 : /// \\param out An output stream
762 : /// \\param x Object x
763 : /// \\return The output stream
764 : inline
765 : std::ostream& operator<<(std::ostream& out, const const_multiply& x)
766 : {
767 : return out << state_formulas::pp(x);
768 : }
769 :
770 : /// \\brief swap overload
771 : inline void swap(const_multiply& t1, const_multiply& t2)
772 : {
773 : t1.swap(t2);
774 : }
775 :
776 :
777 : /// \\brief The multiply operator for state formulas with values
778 : class const_multiply_alt: public state_formula
779 : {
780 : public:
781 : /// \\brief Default constructor.
782 : const_multiply_alt()
783 : : state_formula(core::detail::default_values::StateConstantMultiplyAlt)
784 : {}
785 :
786 : /// \\brief Constructor.
787 : /// \\param term A term
788 11 : explicit const_multiply_alt(const atermpp::aterm& term)
789 11 : : state_formula(term)
790 : {
791 11 : assert(core::detail::check_term_StateConstantMultiplyAlt(*this));
792 11 : }
793 :
794 : /// \\brief Constructor.
795 2 : const_multiply_alt(const state_formula& left, const data::data_expression& right)
796 2 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateConstantMultiplyAlt(), left, right))
797 2 : {}
798 :
799 : /// Move semantics
800 2 : const_multiply_alt(const const_multiply_alt&) noexcept = default;
801 : const_multiply_alt(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 10 : const state_formula& left() const
806 : {
807 10 : return atermpp::down_cast<state_formula>((*this)[0]);
808 : }
809 :
810 8 : const data::data_expression& right() const
811 : {
812 8 : return atermpp::down_cast<data::data_expression>((*this)[1]);
813 : }
814 : };
815 :
816 : /// \\brief Make_const_multiply_alt constructs a new term into a given address.
817 : /// \\ \param t The reference into which the new const_multiply_alt is constructed.
818 : template <class... ARGUMENTS>
819 3 : inline void make_const_multiply_alt(atermpp::aterm_appl& t, const ARGUMENTS&... args)
820 : {
821 3 : atermpp::make_term_appl(t, core::detail::function_symbol_StateConstantMultiplyAlt(), args...);
822 3 : }
823 :
824 : /// \\brief Test for a const_multiply_alt expression
825 : /// \\param x A term
826 : /// \\return True if \\a x is a const_multiply_alt expression
827 : inline
828 19708 : bool is_const_multiply_alt(const atermpp::aterm_appl& x)
829 : {
830 19708 : return x.function() == core::detail::function_symbols::StateConstantMultiplyAlt;
831 : }
832 :
833 : // prototype declaration
834 : std::string pp(const const_multiply_alt& x);
835 :
836 : /// \\brief Outputs the object to a stream
837 : /// \\param out An output stream
838 : /// \\param x Object x
839 : /// \\return The output stream
840 : inline
841 : std::ostream& operator<<(std::ostream& out, const const_multiply_alt& x)
842 : {
843 : return out << state_formulas::pp(x);
844 : }
845 :
846 : /// \\brief swap overload
847 : inline void swap(const_multiply_alt& t1, const_multiply_alt& t2)
848 : {
849 : t1.swap(t2);
850 : }
851 :
852 :
853 : /// \\brief The universal quantification operator for state formulas
854 : class forall: public state_formula
855 : {
856 : public:
857 : /// \\brief Default constructor.
858 : forall()
859 : : state_formula(core::detail::default_values::StateForall)
860 : {}
861 :
862 : /// \\brief Constructor.
863 : /// \\param term A term
864 324 : explicit forall(const atermpp::aterm& term)
865 324 : : state_formula(term)
866 : {
867 324 : assert(core::detail::check_term_StateForall(*this));
868 324 : }
869 :
870 : /// \\brief Constructor.
871 54 : forall(const data::variable_list& variables, const state_formula& body)
872 54 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateForall(), variables, body))
873 54 : {}
874 :
875 : /// Move semantics
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 264 : const data::variable_list& variables() const
882 : {
883 264 : return atermpp::down_cast<data::variable_list>((*this)[0]);
884 : }
885 :
886 306 : const state_formula& body() const
887 : {
888 306 : return atermpp::down_cast<state_formula>((*this)[1]);
889 : }
890 : };
891 :
892 : /// \\brief Make_forall constructs a new term into a given address.
893 : /// \\ \param t The reference into which the new forall is constructed.
894 : template <class... ARGUMENTS>
895 61 : inline void make_forall(atermpp::aterm_appl& t, const ARGUMENTS&... args)
896 : {
897 61 : atermpp::make_term_appl(t, core::detail::function_symbol_StateForall(), args...);
898 61 : }
899 :
900 : /// \\brief Test for a forall expression
901 : /// \\param x A term
902 : /// \\return True if \\a x is a forall expression
903 : inline
904 19722 : bool is_forall(const atermpp::aterm_appl& x)
905 : {
906 19722 : return x.function() == core::detail::function_symbols::StateForall;
907 : }
908 :
909 : // prototype declaration
910 : std::string pp(const forall& x);
911 :
912 : /// \\brief Outputs the object to a stream
913 : /// \\param out An output stream
914 : /// \\param x Object x
915 : /// \\return The output stream
916 : inline
917 : std::ostream& operator<<(std::ostream& out, const forall& x)
918 : {
919 : return out << state_formulas::pp(x);
920 : }
921 :
922 : /// \\brief swap overload
923 : inline void swap(forall& t1, forall& t2)
924 : {
925 : t1.swap(t2);
926 : }
927 :
928 :
929 : /// \\brief The existential quantification operator for state formulas
930 : class exists: public state_formula
931 : {
932 : public:
933 : /// \\brief Default constructor.
934 : exists()
935 : : state_formula(core::detail::default_values::StateExists)
936 : {}
937 :
938 : /// \\brief Constructor.
939 : /// \\param term A term
940 145 : explicit exists(const atermpp::aterm& term)
941 145 : : state_formula(term)
942 : {
943 145 : assert(core::detail::check_term_StateExists(*this));
944 145 : }
945 :
946 : /// \\brief Constructor.
947 22 : exists(const data::variable_list& variables, const state_formula& body)
948 22 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateExists(), variables, body))
949 22 : {}
950 :
951 : /// Move semantics
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 112 : const data::variable_list& variables() const
958 : {
959 112 : return atermpp::down_cast<data::variable_list>((*this)[0]);
960 : }
961 :
962 139 : const state_formula& body() const
963 : {
964 139 : return atermpp::down_cast<state_formula>((*this)[1]);
965 : }
966 : };
967 :
968 : /// \\brief Make_exists constructs a new term into a given address.
969 : /// \\ \param t The reference into which the new exists is constructed.
970 : template <class... ARGUMENTS>
971 29 : inline void make_exists(atermpp::aterm_appl& t, const ARGUMENTS&... args)
972 : {
973 29 : atermpp::make_term_appl(t, core::detail::function_symbol_StateExists(), args...);
974 29 : }
975 :
976 : /// \\brief Test for a exists expression
977 : /// \\param x A term
978 : /// \\return True if \\a x is a exists expression
979 : inline
980 19412 : bool is_exists(const atermpp::aterm_appl& x)
981 : {
982 19412 : return x.function() == core::detail::function_symbols::StateExists;
983 : }
984 :
985 : // prototype declaration
986 : std::string pp(const exists& x);
987 :
988 : /// \\brief Outputs the object to a stream
989 : /// \\param out An output stream
990 : /// \\param x Object x
991 : /// \\return The output stream
992 : inline
993 : std::ostream& operator<<(std::ostream& out, const exists& x)
994 : {
995 : return out << state_formulas::pp(x);
996 : }
997 :
998 : /// \\brief swap overload
999 : inline void swap(exists& t1, exists& t2)
1000 : {
1001 : t1.swap(t2);
1002 : }
1003 :
1004 :
1005 : /// \\brief The infimum over a data type for state formulas
1006 : class infimum: public state_formula
1007 : {
1008 : public:
1009 : /// \\brief Default constructor.
1010 : infimum()
1011 : : state_formula(core::detail::default_values::StateInfimum)
1012 : {}
1013 :
1014 : /// \\brief Constructor.
1015 : /// \\param term A term
1016 22 : explicit infimum(const atermpp::aterm& term)
1017 22 : : state_formula(term)
1018 : {
1019 22 : assert(core::detail::check_term_StateInfimum(*this));
1020 22 : }
1021 :
1022 : /// \\brief Constructor.
1023 6 : infimum(const data::variable_list& variables, const state_formula& body)
1024 6 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateInfimum(), variables, body))
1025 6 : {}
1026 :
1027 : /// Move semantics
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 18 : const data::variable_list& variables() const
1034 : {
1035 18 : return atermpp::down_cast<data::variable_list>((*this)[0]);
1036 : }
1037 :
1038 20 : const state_formula& body() const
1039 : {
1040 20 : return atermpp::down_cast<state_formula>((*this)[1]);
1041 : }
1042 : };
1043 :
1044 : /// \\brief Make_infimum constructs a new term into a given address.
1045 : /// \\ \param t The reference into which the new infimum is constructed.
1046 : template <class... ARGUMENTS>
1047 4 : inline void make_infimum(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1048 : {
1049 4 : atermpp::make_term_appl(t, core::detail::function_symbol_StateInfimum(), args...);
1050 4 : }
1051 :
1052 : /// \\brief Test for a infimum expression
1053 : /// \\param x A term
1054 : /// \\return True if \\a x is a infimum expression
1055 : inline
1056 19268 : bool is_infimum(const atermpp::aterm_appl& x)
1057 : {
1058 19268 : return x.function() == core::detail::function_symbols::StateInfimum;
1059 : }
1060 :
1061 : // prototype declaration
1062 : std::string pp(const infimum& x);
1063 :
1064 : /// \\brief Outputs the object to a stream
1065 : /// \\param out An output stream
1066 : /// \\param x Object x
1067 : /// \\return The output stream
1068 : inline
1069 : std::ostream& operator<<(std::ostream& out, const infimum& x)
1070 : {
1071 : return out << state_formulas::pp(x);
1072 : }
1073 :
1074 : /// \\brief swap overload
1075 : inline void swap(infimum& t1, infimum& t2)
1076 : {
1077 : t1.swap(t2);
1078 : }
1079 :
1080 :
1081 : /// \\brief The supremum over a data type for state formulas
1082 : class supremum: public state_formula
1083 : {
1084 : public:
1085 : /// \\brief Default constructor.
1086 : supremum()
1087 : : state_formula(core::detail::default_values::StateSupremum)
1088 : {}
1089 :
1090 : /// \\brief Constructor.
1091 : /// \\param term A term
1092 11 : explicit supremum(const atermpp::aterm& term)
1093 11 : : state_formula(term)
1094 : {
1095 11 : assert(core::detail::check_term_StateSupremum(*this));
1096 11 : }
1097 :
1098 : /// \\brief Constructor.
1099 3 : supremum(const data::variable_list& variables, const state_formula& body)
1100 3 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateSupremum(), variables, body))
1101 3 : {}
1102 :
1103 : /// Move semantics
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 9 : const data::variable_list& variables() const
1110 : {
1111 9 : return atermpp::down_cast<data::variable_list>((*this)[0]);
1112 : }
1113 :
1114 10 : const state_formula& body() const
1115 : {
1116 10 : return atermpp::down_cast<state_formula>((*this)[1]);
1117 : }
1118 : };
1119 :
1120 : /// \\brief Make_supremum constructs a new term into a given address.
1121 : /// \\ \param t The reference into which the new supremum is constructed.
1122 : template <class... ARGUMENTS>
1123 2 : inline void make_supremum(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1124 : {
1125 2 : atermpp::make_term_appl(t, core::detail::function_symbol_StateSupremum(), args...);
1126 2 : }
1127 :
1128 : /// \\brief Test for a supremum expression
1129 : /// \\param x A term
1130 : /// \\return True if \\a x is a supremum expression
1131 : inline
1132 19248 : bool is_supremum(const atermpp::aterm_appl& x)
1133 : {
1134 19248 : return x.function() == core::detail::function_symbols::StateSupremum;
1135 : }
1136 :
1137 : // prototype declaration
1138 : std::string pp(const supremum& x);
1139 :
1140 : /// \\brief Outputs the object to a stream
1141 : /// \\param out An output stream
1142 : /// \\param x Object x
1143 : /// \\return The output stream
1144 : inline
1145 : std::ostream& operator<<(std::ostream& out, const supremum& x)
1146 : {
1147 : return out << state_formulas::pp(x);
1148 : }
1149 :
1150 : /// \\brief swap overload
1151 : inline void swap(supremum& t1, supremum& t2)
1152 : {
1153 : t1.swap(t2);
1154 : }
1155 :
1156 :
1157 : /// \\brief The sum over a data type for state formulas
1158 : class sum: public state_formula
1159 : {
1160 : public:
1161 : /// \\brief Default constructor.
1162 : sum()
1163 : : state_formula(core::detail::default_values::StateSum)
1164 : {}
1165 :
1166 : /// \\brief Constructor.
1167 : /// \\param term A term
1168 11 : explicit sum(const atermpp::aterm& term)
1169 11 : : state_formula(term)
1170 : {
1171 11 : assert(core::detail::check_term_StateSum(*this));
1172 11 : }
1173 :
1174 : /// \\brief Constructor.
1175 3 : sum(const data::variable_list& variables, const state_formula& body)
1176 3 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateSum(), variables, body))
1177 3 : {}
1178 :
1179 : /// Move semantics
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 9 : const data::variable_list& variables() const
1186 : {
1187 9 : return atermpp::down_cast<data::variable_list>((*this)[0]);
1188 : }
1189 :
1190 10 : const state_formula& body() const
1191 : {
1192 10 : return atermpp::down_cast<state_formula>((*this)[1]);
1193 : }
1194 : };
1195 :
1196 : /// \\brief Make_sum constructs a new term into a given address.
1197 : /// \\ \param t The reference into which the new sum is constructed.
1198 : template <class... ARGUMENTS>
1199 2 : inline void make_sum(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1200 : {
1201 2 : atermpp::make_term_appl(t, core::detail::function_symbol_StateSum(), args...);
1202 2 : }
1203 :
1204 : /// \\brief Test for a sum expression
1205 : /// \\param x A term
1206 : /// \\return True if \\a x is a sum expression
1207 : inline
1208 19238 : bool is_sum(const atermpp::aterm_appl& x)
1209 : {
1210 19238 : return x.function() == core::detail::function_symbols::StateSum;
1211 : }
1212 :
1213 : // prototype declaration
1214 : std::string pp(const sum& x);
1215 :
1216 : /// \\brief Outputs the object to a stream
1217 : /// \\param out An output stream
1218 : /// \\param x Object x
1219 : /// \\return The output stream
1220 : inline
1221 : std::ostream& operator<<(std::ostream& out, const sum& x)
1222 : {
1223 : return out << state_formulas::pp(x);
1224 : }
1225 :
1226 : /// \\brief swap overload
1227 : inline void swap(sum& t1, sum& t2)
1228 : {
1229 : t1.swap(t2);
1230 : }
1231 :
1232 :
1233 : /// \\brief The must operator for state formulas
1234 : class must: public state_formula
1235 : {
1236 : public:
1237 : /// \\brief Default constructor.
1238 : must()
1239 : : state_formula(core::detail::default_values::StateMust)
1240 : {}
1241 :
1242 : /// \\brief Constructor.
1243 : /// \\param term A term
1244 4966 : explicit must(const atermpp::aterm& term)
1245 4966 : : state_formula(term)
1246 : {
1247 4966 : assert(core::detail::check_term_StateMust(*this));
1248 4966 : }
1249 :
1250 : /// \\brief Constructor.
1251 282 : must(const regular_formulas::regular_formula& formula, const state_formula& operand)
1252 282 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateMust(), formula, operand))
1253 282 : {}
1254 :
1255 : /// Move semantics
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 2044 : const regular_formulas::regular_formula& formula() const
1262 : {
1263 2044 : return atermpp::down_cast<regular_formulas::regular_formula>((*this)[0]);
1264 : }
1265 :
1266 4810 : const state_formula& operand() const
1267 : {
1268 4810 : return atermpp::down_cast<state_formula>((*this)[1]);
1269 : }
1270 : };
1271 :
1272 : /// \\brief Make_must constructs a new term into a given address.
1273 : /// \\ \param t The reference into which the new must is constructed.
1274 : template <class... ARGUMENTS>
1275 728 : inline void make_must(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1276 : {
1277 728 : atermpp::make_term_appl(t, core::detail::function_symbol_StateMust(), args...);
1278 728 : }
1279 :
1280 : /// \\brief Test for a must expression
1281 : /// \\param x A term
1282 : /// \\return True if \\a x is a must expression
1283 : inline
1284 19431 : bool is_must(const atermpp::aterm_appl& x)
1285 : {
1286 19431 : return x.function() == core::detail::function_symbols::StateMust;
1287 : }
1288 :
1289 : // prototype declaration
1290 : std::string pp(const must& x);
1291 :
1292 : /// \\brief Outputs the object to a stream
1293 : /// \\param out An output stream
1294 : /// \\param x Object x
1295 : /// \\return The output stream
1296 : inline
1297 : std::ostream& operator<<(std::ostream& out, const must& x)
1298 : {
1299 : return out << state_formulas::pp(x);
1300 : }
1301 :
1302 : /// \\brief swap overload
1303 : inline void swap(must& t1, must& t2)
1304 : {
1305 : t1.swap(t2);
1306 : }
1307 :
1308 :
1309 : /// \\brief The may operator for state formulas
1310 : class may: public state_formula
1311 : {
1312 : public:
1313 : /// \\brief Default constructor.
1314 : may()
1315 : : state_formula(core::detail::default_values::StateMay)
1316 : {}
1317 :
1318 : /// \\brief Constructor.
1319 : /// \\param term A term
1320 4071 : explicit may(const atermpp::aterm& term)
1321 4071 : : state_formula(term)
1322 : {
1323 4071 : assert(core::detail::check_term_StateMay(*this));
1324 4071 : }
1325 :
1326 : /// \\brief Constructor.
1327 215 : may(const regular_formulas::regular_formula& formula, const state_formula& operand)
1328 215 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateMay(), formula, operand))
1329 215 : {}
1330 :
1331 : /// Move semantics
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 1698 : const regular_formulas::regular_formula& formula() const
1338 : {
1339 1698 : return atermpp::down_cast<regular_formulas::regular_formula>((*this)[0]);
1340 : }
1341 :
1342 3932 : const state_formula& operand() const
1343 : {
1344 3932 : return atermpp::down_cast<state_formula>((*this)[1]);
1345 : }
1346 : };
1347 :
1348 : /// \\brief Make_may constructs a new term into a given address.
1349 : /// \\ \param t The reference into which the new may is constructed.
1350 : template <class... ARGUMENTS>
1351 611 : inline void make_may(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1352 : {
1353 611 : atermpp::make_term_appl(t, core::detail::function_symbol_StateMay(), args...);
1354 611 : }
1355 :
1356 : /// \\brief Test for a may expression
1357 : /// \\param x A term
1358 : /// \\return True if \\a x is a may expression
1359 : inline
1360 15063 : bool is_may(const atermpp::aterm_appl& x)
1361 : {
1362 15063 : return x.function() == core::detail::function_symbols::StateMay;
1363 : }
1364 :
1365 : // prototype declaration
1366 : std::string pp(const may& x);
1367 :
1368 : /// \\brief Outputs the object to a stream
1369 : /// \\param out An output stream
1370 : /// \\param x Object x
1371 : /// \\return The output stream
1372 : inline
1373 : std::ostream& operator<<(std::ostream& out, const may& x)
1374 : {
1375 : return out << state_formulas::pp(x);
1376 : }
1377 :
1378 : /// \\brief swap overload
1379 : inline void swap(may& t1, may& t2)
1380 : {
1381 : t1.swap(t2);
1382 : }
1383 :
1384 :
1385 : /// \\brief The yaled operator for state formulas
1386 : class yaled: public state_formula
1387 : {
1388 : public:
1389 : /// \\brief Default constructor.
1390 0 : yaled()
1391 0 : : state_formula(core::detail::default_values::StateYaled)
1392 0 : {}
1393 :
1394 : /// \\brief Constructor.
1395 : /// \\param term A term
1396 0 : explicit yaled(const atermpp::aterm& term)
1397 0 : : state_formula(term)
1398 : {
1399 0 : assert(core::detail::check_term_StateYaled(*this));
1400 0 : }
1401 :
1402 : /// Move semantics
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 :
1409 : /// \\brief Test for a yaled expression
1410 : /// \\param x A term
1411 : /// \\return True if \\a x is a yaled expression
1412 : inline
1413 10972 : bool is_yaled(const atermpp::aterm_appl& x)
1414 : {
1415 10972 : return x.function() == core::detail::function_symbols::StateYaled;
1416 : }
1417 :
1418 : // prototype declaration
1419 : std::string pp(const yaled& x);
1420 :
1421 : /// \\brief Outputs the object to a stream
1422 : /// \\param out An output stream
1423 : /// \\param x Object x
1424 : /// \\return The output stream
1425 : inline
1426 : std::ostream& operator<<(std::ostream& out, const yaled& x)
1427 : {
1428 : return out << state_formulas::pp(x);
1429 : }
1430 :
1431 : /// \\brief swap overload
1432 : inline void swap(yaled& t1, yaled& t2)
1433 : {
1434 : t1.swap(t2);
1435 : }
1436 :
1437 :
1438 : /// \\brief The timed yaled operator for state formulas
1439 : class yaled_timed: public state_formula
1440 : {
1441 : public:
1442 : /// \\brief Default constructor.
1443 : yaled_timed()
1444 : : state_formula(core::detail::default_values::StateYaledTimed)
1445 : {}
1446 :
1447 : /// \\brief Constructor.
1448 : /// \\param term A term
1449 36 : explicit yaled_timed(const atermpp::aterm& term)
1450 36 : : state_formula(term)
1451 : {
1452 36 : assert(core::detail::check_term_StateYaledTimed(*this));
1453 36 : }
1454 :
1455 : /// \\brief Constructor.
1456 1 : explicit yaled_timed(const data::data_expression& time_stamp)
1457 1 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateYaledTimed(), time_stamp))
1458 1 : {}
1459 :
1460 : /// Move semantics
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 20 : const data::data_expression& time_stamp() const
1467 : {
1468 20 : return atermpp::down_cast<data::data_expression>((*this)[0]);
1469 : }
1470 : };
1471 :
1472 : /// \\brief Make_yaled_timed constructs a new term into a given address.
1473 : /// \\ \param t The reference into which the new yaled_timed is constructed.
1474 : template <class... ARGUMENTS>
1475 6 : inline void make_yaled_timed(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1476 : {
1477 6 : atermpp::make_term_appl(t, core::detail::function_symbol_StateYaledTimed(), args...);
1478 6 : }
1479 :
1480 : /// \\brief Test for a yaled_timed expression
1481 : /// \\param x A term
1482 : /// \\return True if \\a x is a yaled_timed expression
1483 : inline
1484 10975 : bool is_yaled_timed(const atermpp::aterm_appl& x)
1485 : {
1486 10975 : return x.function() == core::detail::function_symbols::StateYaledTimed;
1487 : }
1488 :
1489 : // prototype declaration
1490 : std::string pp(const yaled_timed& x);
1491 :
1492 : /// \\brief Outputs the object to a stream
1493 : /// \\param out An output stream
1494 : /// \\param x Object x
1495 : /// \\return The output stream
1496 : inline
1497 : std::ostream& operator<<(std::ostream& out, const yaled_timed& x)
1498 : {
1499 : return out << state_formulas::pp(x);
1500 : }
1501 :
1502 : /// \\brief swap overload
1503 : inline void swap(yaled_timed& t1, yaled_timed& t2)
1504 : {
1505 : t1.swap(t2);
1506 : }
1507 :
1508 :
1509 : /// \\brief The delay operator for state formulas
1510 : class delay: public state_formula
1511 : {
1512 : public:
1513 : /// \\brief Default constructor.
1514 0 : delay()
1515 0 : : state_formula(core::detail::default_values::StateDelay)
1516 0 : {}
1517 :
1518 : /// \\brief Constructor.
1519 : /// \\param term A term
1520 0 : explicit delay(const atermpp::aterm& term)
1521 0 : : state_formula(term)
1522 : {
1523 0 : assert(core::detail::check_term_StateDelay(*this));
1524 0 : }
1525 :
1526 : /// Move semantics
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 :
1533 : /// \\brief Test for a delay expression
1534 : /// \\param x A term
1535 : /// \\return True if \\a x is a delay expression
1536 : inline
1537 10932 : bool is_delay(const atermpp::aterm_appl& x)
1538 : {
1539 10932 : return x.function() == core::detail::function_symbols::StateDelay;
1540 : }
1541 :
1542 : // prototype declaration
1543 : std::string pp(const delay& x);
1544 :
1545 : /// \\brief Outputs the object to a stream
1546 : /// \\param out An output stream
1547 : /// \\param x Object x
1548 : /// \\return The output stream
1549 : inline
1550 : std::ostream& operator<<(std::ostream& out, const delay& x)
1551 : {
1552 : return out << state_formulas::pp(x);
1553 : }
1554 :
1555 : /// \\brief swap overload
1556 : inline void swap(delay& t1, delay& t2)
1557 : {
1558 : t1.swap(t2);
1559 : }
1560 :
1561 :
1562 : /// \\brief The timed delay operator for state formulas
1563 : class delay_timed: public state_formula
1564 : {
1565 : public:
1566 : /// \\brief Default constructor.
1567 : delay_timed()
1568 : : state_formula(core::detail::default_values::StateDelayTimed)
1569 : {}
1570 :
1571 : /// \\brief Constructor.
1572 : /// \\param term A term
1573 46 : explicit delay_timed(const atermpp::aterm& term)
1574 46 : : state_formula(term)
1575 : {
1576 46 : assert(core::detail::check_term_StateDelayTimed(*this));
1577 46 : }
1578 :
1579 : /// \\brief Constructor.
1580 3 : explicit delay_timed(const data::data_expression& time_stamp)
1581 3 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateDelayTimed(), time_stamp))
1582 3 : {}
1583 :
1584 : /// Move semantics
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 32 : const data::data_expression& time_stamp() const
1591 : {
1592 32 : return atermpp::down_cast<data::data_expression>((*this)[0]);
1593 : }
1594 : };
1595 :
1596 : /// \\brief Make_delay_timed constructs a new term into a given address.
1597 : /// \\ \param t The reference into which the new delay_timed is constructed.
1598 : template <class... ARGUMENTS>
1599 12 : inline void make_delay_timed(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1600 : {
1601 12 : atermpp::make_term_appl(t, core::detail::function_symbol_StateDelayTimed(), args...);
1602 12 : }
1603 :
1604 : /// \\brief Test for a delay_timed expression
1605 : /// \\param x A term
1606 : /// \\return True if \\a x is a delay_timed expression
1607 : inline
1608 10935 : bool is_delay_timed(const atermpp::aterm_appl& x)
1609 : {
1610 10935 : return x.function() == core::detail::function_symbols::StateDelayTimed;
1611 : }
1612 :
1613 : // prototype declaration
1614 : std::string pp(const delay_timed& x);
1615 :
1616 : /// \\brief Outputs the object to a stream
1617 : /// \\param out An output stream
1618 : /// \\param x Object x
1619 : /// \\return The output stream
1620 : inline
1621 : std::ostream& operator<<(std::ostream& out, const delay_timed& x)
1622 : {
1623 : return out << state_formulas::pp(x);
1624 : }
1625 :
1626 : /// \\brief swap overload
1627 : inline void swap(delay_timed& t1, delay_timed& t2)
1628 : {
1629 : t1.swap(t2);
1630 : }
1631 :
1632 :
1633 : /// \\brief The state formula variable
1634 : class variable: public state_formula
1635 : {
1636 : public:
1637 : /// \\brief Default constructor.
1638 : variable()
1639 : : state_formula(core::detail::default_values::StateVar)
1640 : {}
1641 :
1642 : /// \\brief Constructor.
1643 : /// \\param term A term
1644 4342 : explicit variable(const atermpp::aterm& term)
1645 4342 : : state_formula(term)
1646 : {
1647 4342 : assert(core::detail::check_term_StateVar(*this));
1648 4342 : }
1649 :
1650 : /// \\brief Constructor.
1651 302 : variable(const core::identifier_string& name, const data::data_expression_list& arguments)
1652 302 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateVar(), name, arguments))
1653 302 : {}
1654 :
1655 : /// \\brief Constructor.
1656 9 : variable(const std::string& name, const data::data_expression_list& arguments)
1657 9 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateVar(), core::identifier_string(name), arguments))
1658 9 : {}
1659 :
1660 : /// Move semantics
1661 12 : 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 1600 : const core::identifier_string& name() const
1667 : {
1668 1600 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
1669 : }
1670 :
1671 1308 : const data::data_expression_list& arguments() const
1672 : {
1673 1308 : return atermpp::down_cast<data::data_expression_list>((*this)[1]);
1674 : }
1675 : };
1676 :
1677 : /// \\brief Make_variable constructs a new term into a given address.
1678 : /// \\ \param t The reference into which the new variable is constructed.
1679 : template <class... ARGUMENTS>
1680 282 : inline void make_variable(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1681 : {
1682 282 : atermpp::make_term_appl(t, core::detail::function_symbol_StateVar(), args...);
1683 282 : }
1684 :
1685 : /// \\brief Test for a variable expression
1686 : /// \\param x A term
1687 : /// \\return True if \\a x is a variable expression
1688 : inline
1689 11169 : bool is_variable(const atermpp::aterm_appl& x)
1690 : {
1691 11169 : return x.function() == core::detail::function_symbols::StateVar;
1692 : }
1693 :
1694 : // prototype declaration
1695 : std::string pp(const variable& x);
1696 :
1697 : /// \\brief Outputs the object to a stream
1698 : /// \\param out An output stream
1699 : /// \\param x Object x
1700 : /// \\return The output stream
1701 : inline
1702 : std::ostream& operator<<(std::ostream& out, const variable& x)
1703 : {
1704 : return out << state_formulas::pp(x);
1705 : }
1706 :
1707 : /// \\brief swap overload
1708 : inline void swap(variable& t1, variable& t2)
1709 : {
1710 : t1.swap(t2);
1711 : }
1712 :
1713 :
1714 : /// \\brief The nu operator for state formulas
1715 : class nu: public state_formula
1716 : {
1717 : public:
1718 : /// \\brief Default constructor.
1719 : nu()
1720 : : state_formula(core::detail::default_values::StateNu)
1721 : {}
1722 :
1723 : /// \\brief Constructor.
1724 : /// \\param term A term
1725 3682 : explicit nu(const atermpp::aterm& term)
1726 3682 : : state_formula(term)
1727 : {
1728 3682 : assert(core::detail::check_term_StateNu(*this));
1729 3682 : }
1730 :
1731 : /// \\brief Constructor.
1732 296 : nu(const core::identifier_string& name, const data::assignment_list& assignments, const state_formula& operand)
1733 296 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateNu(), name, assignments, operand))
1734 296 : {}
1735 :
1736 : /// \\brief Constructor.
1737 : nu(const std::string& name, const data::assignment_list& assignments, const state_formula& operand)
1738 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateNu(), core::identifier_string(name), assignments, operand))
1739 : {}
1740 :
1741 : /// Move semantics
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 2980 : const core::identifier_string& name() const
1748 : {
1749 2980 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
1750 : }
1751 :
1752 2583 : const data::assignment_list& assignments() const
1753 : {
1754 2583 : return atermpp::down_cast<data::assignment_list>((*this)[1]);
1755 : }
1756 :
1757 2620 : const state_formula& operand() const
1758 : {
1759 2620 : return atermpp::down_cast<state_formula>((*this)[2]);
1760 : }
1761 : };
1762 :
1763 : /// \\brief Make_nu constructs a new term into a given address.
1764 : /// \\ \param t The reference into which the new nu is constructed.
1765 : template <class... ARGUMENTS>
1766 288 : inline void make_nu(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1767 : {
1768 288 : atermpp::make_term_appl(t, core::detail::function_symbol_StateNu(), args...);
1769 288 : }
1770 :
1771 : /// \\brief Test for a nu expression
1772 : /// \\param x A term
1773 : /// \\return True if \\a x is a nu expression
1774 : inline
1775 6753 : bool is_nu(const atermpp::aterm_appl& x)
1776 : {
1777 6753 : return x.function() == core::detail::function_symbols::StateNu;
1778 : }
1779 :
1780 : // prototype declaration
1781 : std::string pp(const nu& x);
1782 :
1783 : /// \\brief Outputs the object to a stream
1784 : /// \\param out An output stream
1785 : /// \\param x Object x
1786 : /// \\return The output stream
1787 : inline
1788 0 : std::ostream& operator<<(std::ostream& out, const nu& x)
1789 : {
1790 0 : return out << state_formulas::pp(x);
1791 : }
1792 :
1793 : /// \\brief swap overload
1794 : inline void swap(nu& t1, nu& t2)
1795 : {
1796 : t1.swap(t2);
1797 : }
1798 :
1799 :
1800 : /// \\brief The mu operator for state formulas
1801 : class mu: public state_formula
1802 : {
1803 : public:
1804 : /// \\brief Default constructor.
1805 : mu()
1806 : : state_formula(core::detail::default_values::StateMu)
1807 : {}
1808 :
1809 : /// \\brief Constructor.
1810 : /// \\param term A term
1811 3111 : explicit mu(const atermpp::aterm& term)
1812 3111 : : state_formula(term)
1813 : {
1814 3111 : assert(core::detail::check_term_StateMu(*this));
1815 3111 : }
1816 :
1817 : /// \\brief Constructor.
1818 322 : mu(const core::identifier_string& name, const data::assignment_list& assignments, const state_formula& operand)
1819 322 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateMu(), name, assignments, operand))
1820 322 : {}
1821 :
1822 : /// \\brief Constructor.
1823 1 : mu(const std::string& name, const data::assignment_list& assignments, const state_formula& operand)
1824 1 : : state_formula(atermpp::aterm_appl(core::detail::function_symbol_StateMu(), core::identifier_string(name), assignments, operand))
1825 1 : {}
1826 :
1827 : /// Move semantics
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 2706 : const core::identifier_string& name() const
1834 : {
1835 2706 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
1836 : }
1837 :
1838 2311 : const data::assignment_list& assignments() const
1839 : {
1840 2311 : return atermpp::down_cast<data::assignment_list>((*this)[1]);
1841 : }
1842 :
1843 2623 : const state_formula& operand() const
1844 : {
1845 2623 : return atermpp::down_cast<state_formula>((*this)[2]);
1846 : }
1847 : };
1848 :
1849 : /// \\brief Make_mu constructs a new term into a given address.
1850 : /// \\ \param t The reference into which the new mu is constructed.
1851 : template <class... ARGUMENTS>
1852 389 : inline void make_mu(atermpp::aterm_appl& t, const ARGUMENTS&... args)
1853 : {
1854 389 : atermpp::make_term_appl(t, core::detail::function_symbol_StateMu(), args...);
1855 389 : }
1856 :
1857 : /// \\brief Test for a mu expression
1858 : /// \\param x A term
1859 : /// \\return True if \\a x is a mu expression
1860 : inline
1861 4701 : bool is_mu(const atermpp::aterm_appl& x)
1862 : {
1863 4701 : return x.function() == core::detail::function_symbols::StateMu;
1864 : }
1865 :
1866 : // prototype declaration
1867 : std::string pp(const mu& x);
1868 :
1869 : /// \\brief Outputs the object to a stream
1870 : /// \\param out An output stream
1871 : /// \\param x Object x
1872 : /// \\return The output stream
1873 : inline
1874 0 : std::ostream& operator<<(std::ostream& out, const mu& x)
1875 : {
1876 0 : return out << state_formulas::pp(x);
1877 : }
1878 :
1879 : /// \\brief swap overload
1880 : inline void swap(mu& t1, mu& t2)
1881 : {
1882 : t1.swap(t2);
1883 : }
1884 : //--- end generated classes ---//
1885 :
1886 : namespace algorithms {
1887 : bool is_timed(const state_formula& x);
1888 : } // namespace algorithms
1889 :
1890 : /// \brief Returns true if the formula is timed.
1891 : /// \return True if the formula is timed.
1892 : inline
1893 143 : bool state_formula::has_time() const
1894 : {
1895 143 : return algorithms::is_timed(*this);
1896 : }
1897 :
1898 : // template function overloads
1899 : state_formula normalize_sorts(const state_formula& x, const data::sort_specification& sortspec);
1900 : state_formulas::state_formula translate_user_notation(const state_formulas::state_formula& x);
1901 : std::set<data::sort_expression> find_sort_expressions(const state_formulas::state_formula& x);
1902 : std::set<data::variable> find_all_variables(const state_formulas::state_formula& x);
1903 : std::set<data::variable> find_free_variables(const state_formulas::state_formula& x);
1904 : std::set<core::identifier_string> find_identifiers(const state_formulas::state_formula& x);
1905 : std::set<process::action_label> find_action_labels(const state_formulas::state_formula& x);
1906 : bool find_nil(const state_formulas::state_formula& x);
1907 :
1908 : } // namespace state_formulas
1909 :
1910 : } // namespace mcrl2
1911 :
1912 : #endif // MCRL2_MODAL_FORMULA_STATE_FORMULA_H
|
