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/regular_formula.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
13 : #define MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
14 :
15 : #include "mcrl2/modal_formula/action_formula.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace regular_formulas
21 : {
22 :
23 : //--- start generated classes ---//
24 : /// \\brief A regular formula
25 : class regular_formula: public atermpp::aterm_appl
26 : {
27 : public:
28 : /// \\brief Default constructor.
29 235 : regular_formula()
30 235 : : atermpp::aterm_appl(core::detail::default_values::RegFrm)
31 235 : {}
32 :
33 : /// \\brief Constructor.
34 : /// \\param term A term
35 4231 : explicit regular_formula(const atermpp::aterm& term)
36 4231 : : atermpp::aterm_appl(term)
37 : {
38 4231 : assert(core::detail::check_rule_RegFrm(*this));
39 4231 : }
40 :
41 : /// \\brief Constructor.
42 842 : regular_formula(const action_formulas::action_formula& x)
43 842 : : atermpp::aterm_appl(x)
44 842 : {}
45 :
46 : /// \\brief Constructor.
47 0 : regular_formula(const data::data_expression& x)
48 0 : : atermpp::aterm_appl(x)
49 0 : {}
50 :
51 : /// Move semantics
52 297 : regular_formula(const regular_formula&) noexcept = default;
53 40 : regular_formula(regular_formula&&) noexcept = default;
54 : regular_formula& operator=(const regular_formula&) noexcept = default;
55 604 : regular_formula& operator=(regular_formula&&) noexcept = default;
56 : };
57 :
58 : /// \\brief list of regular_formulas
59 : typedef atermpp::term_list<regular_formula> regular_formula_list;
60 :
61 : /// \\brief vector of regular_formulas
62 : typedef std::vector<regular_formula> regular_formula_vector;
63 :
64 : // prototypes
65 : inline bool is_seq(const atermpp::aterm_appl& x);
66 : inline bool is_alt(const atermpp::aterm_appl& x);
67 : inline bool is_trans(const atermpp::aterm_appl& x);
68 : inline bool is_trans_or_nil(const atermpp::aterm_appl& x);
69 : inline bool is_untyped_regular_formula(const atermpp::aterm_appl& x);
70 :
71 : /// \\brief Test for a regular_formula expression
72 : /// \\param x A term
73 : /// \\return True if \\a x is a regular_formula expression
74 : inline
75 1 : bool is_regular_formula(const atermpp::aterm_appl& x)
76 : {
77 1 : return data::is_data_expression(x) ||
78 1 : action_formulas::is_action_formula(x) ||
79 0 : regular_formulas::is_seq(x) ||
80 0 : regular_formulas::is_alt(x) ||
81 0 : regular_formulas::is_trans(x) ||
82 2 : regular_formulas::is_trans_or_nil(x) ||
83 1 : regular_formulas::is_untyped_regular_formula(x);
84 : }
85 :
86 : // prototype declaration
87 : std::string pp(const regular_formula& x);
88 :
89 : /// \\brief Outputs the object to a stream
90 : /// \\param out An output stream
91 : /// \\param x Object x
92 : /// \\return The output stream
93 : inline
94 : std::ostream& operator<<(std::ostream& out, const regular_formula& x)
95 : {
96 : return out << regular_formulas::pp(x);
97 : }
98 :
99 : /// \\brief swap overload
100 : inline void swap(regular_formula& t1, regular_formula& t2)
101 : {
102 : t1.swap(t2);
103 : }
104 :
105 :
106 : /// \\brief The seq operator for regular formulas
107 : class seq: public regular_formula
108 : {
109 : public:
110 : /// \\brief Default constructor.
111 : seq()
112 : : regular_formula(core::detail::default_values::RegSeq)
113 : {}
114 :
115 : /// \\brief Constructor.
116 : /// \\param term A term
117 12 : explicit seq(const atermpp::aterm& term)
118 12 : : regular_formula(term)
119 : {
120 12 : assert(core::detail::check_term_RegSeq(*this));
121 12 : }
122 :
123 : /// \\brief Constructor.
124 3 : seq(const regular_formula& left, const regular_formula& right)
125 3 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_RegSeq(), left, right))
126 3 : {}
127 :
128 : /// Move semantics
129 : seq(const seq&) noexcept = default;
130 : seq(seq&&) noexcept = default;
131 : seq& operator=(const seq&) noexcept = default;
132 : seq& operator=(seq&&) noexcept = default;
133 :
134 9 : const regular_formula& left() const
135 : {
136 9 : return atermpp::down_cast<regular_formula>((*this)[0]);
137 : }
138 :
139 9 : const regular_formula& right() const
140 : {
141 9 : return atermpp::down_cast<regular_formula>((*this)[1]);
142 : }
143 : };
144 :
145 : /// \\brief Make_seq constructs a new term into a given address.
146 : /// \\ \param t The reference into which the new seq is constructed.
147 : template <class... ARGUMENTS>
148 0 : inline void make_seq(atermpp::aterm_appl& t, const ARGUMENTS&... args)
149 : {
150 0 : atermpp::make_term_appl(t, core::detail::function_symbol_RegSeq(), args...);
151 0 : }
152 :
153 : /// \\brief Test for a seq expression
154 : /// \\param x A term
155 : /// \\return True if \\a x is a seq expression
156 : inline
157 432 : bool is_seq(const atermpp::aterm_appl& x)
158 : {
159 432 : return x.function() == core::detail::function_symbols::RegSeq;
160 : }
161 :
162 : // prototype declaration
163 : std::string pp(const seq& x);
164 :
165 : /// \\brief Outputs the object to a stream
166 : /// \\param out An output stream
167 : /// \\param x Object x
168 : /// \\return The output stream
169 : inline
170 : std::ostream& operator<<(std::ostream& out, const seq& x)
171 : {
172 : return out << regular_formulas::pp(x);
173 : }
174 :
175 : /// \\brief swap overload
176 : inline void swap(seq& t1, seq& t2)
177 : {
178 : t1.swap(t2);
179 : }
180 :
181 :
182 : /// \\brief The alt operator for regular formulas
183 : class alt: public regular_formula
184 : {
185 : public:
186 : /// \\brief Default constructor.
187 : alt()
188 : : regular_formula(core::detail::default_values::RegAlt)
189 : {}
190 :
191 : /// \\brief Constructor.
192 : /// \\param term A term
193 10 : explicit alt(const atermpp::aterm& term)
194 10 : : regular_formula(term)
195 : {
196 10 : assert(core::detail::check_term_RegAlt(*this));
197 10 : }
198 :
199 : /// \\brief Constructor.
200 4 : alt(const regular_formula& left, const regular_formula& right)
201 4 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_RegAlt(), left, right))
202 4 : {}
203 :
204 : /// Move semantics
205 : alt(const alt&) noexcept = default;
206 : alt(alt&&) noexcept = default;
207 : alt& operator=(const alt&) noexcept = default;
208 : alt& operator=(alt&&) noexcept = default;
209 :
210 8 : const regular_formula& left() const
211 : {
212 8 : return atermpp::down_cast<regular_formula>((*this)[0]);
213 : }
214 :
215 8 : const regular_formula& right() const
216 : {
217 8 : return atermpp::down_cast<regular_formula>((*this)[1]);
218 : }
219 : };
220 :
221 : /// \\brief Make_alt constructs a new term into a given address.
222 : /// \\ \param t The reference into which the new alt is constructed.
223 : template <class... ARGUMENTS>
224 0 : inline void make_alt(atermpp::aterm_appl& t, const ARGUMENTS&... args)
225 : {
226 0 : atermpp::make_term_appl(t, core::detail::function_symbol_RegAlt(), args...);
227 0 : }
228 :
229 : /// \\brief Test for a alt expression
230 : /// \\param x A term
231 : /// \\return True if \\a x is a alt expression
232 : inline
233 423 : bool is_alt(const atermpp::aterm_appl& x)
234 : {
235 423 : return x.function() == core::detail::function_symbols::RegAlt;
236 : }
237 :
238 : // prototype declaration
239 : std::string pp(const alt& x);
240 :
241 : /// \\brief Outputs the object to a stream
242 : /// \\param out An output stream
243 : /// \\param x Object x
244 : /// \\return The output stream
245 : inline
246 : std::ostream& operator<<(std::ostream& out, const alt& x)
247 : {
248 : return out << regular_formulas::pp(x);
249 : }
250 :
251 : /// \\brief swap overload
252 : inline void swap(alt& t1, alt& t2)
253 : {
254 : t1.swap(t2);
255 : }
256 :
257 :
258 : /// \\brief The trans operator for regular formulas
259 : class trans: public regular_formula
260 : {
261 : public:
262 : /// \\brief Default constructor.
263 : trans()
264 : : regular_formula(core::detail::default_values::RegTrans)
265 : {}
266 :
267 : /// \\brief Constructor.
268 : /// \\param term A term
269 0 : explicit trans(const atermpp::aterm& term)
270 0 : : regular_formula(term)
271 : {
272 0 : assert(core::detail::check_term_RegTrans(*this));
273 0 : }
274 :
275 : /// \\brief Constructor.
276 0 : explicit trans(const regular_formula& operand)
277 0 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_RegTrans(), operand))
278 0 : {}
279 :
280 : /// Move semantics
281 : trans(const trans&) noexcept = default;
282 : trans(trans&&) noexcept = default;
283 : trans& operator=(const trans&) noexcept = default;
284 : trans& operator=(trans&&) noexcept = default;
285 :
286 0 : const regular_formula& operand() const
287 : {
288 0 : return atermpp::down_cast<regular_formula>((*this)[0]);
289 : }
290 : };
291 :
292 : /// \\brief Make_trans constructs a new term into a given address.
293 : /// \\ \param t The reference into which the new trans is constructed.
294 : template <class... ARGUMENTS>
295 0 : inline void make_trans(atermpp::aterm_appl& t, const ARGUMENTS&... args)
296 : {
297 0 : atermpp::make_term_appl(t, core::detail::function_symbol_RegTrans(), args...);
298 0 : }
299 :
300 : /// \\brief Test for a trans expression
301 : /// \\param x A term
302 : /// \\return True if \\a x is a trans expression
303 : inline
304 415 : bool is_trans(const atermpp::aterm_appl& x)
305 : {
306 415 : return x.function() == core::detail::function_symbols::RegTrans;
307 : }
308 :
309 : // prototype declaration
310 : std::string pp(const trans& x);
311 :
312 : /// \\brief Outputs the object to a stream
313 : /// \\param out An output stream
314 : /// \\param x Object x
315 : /// \\return The output stream
316 : inline
317 : std::ostream& operator<<(std::ostream& out, const trans& x)
318 : {
319 : return out << regular_formulas::pp(x);
320 : }
321 :
322 : /// \\brief swap overload
323 : inline void swap(trans& t1, trans& t2)
324 : {
325 : t1.swap(t2);
326 : }
327 :
328 :
329 : /// \\brief The 'trans or nil' operator for regular formulas
330 : class trans_or_nil: public regular_formula
331 : {
332 : public:
333 : /// \\brief Default constructor.
334 : trans_or_nil()
335 : : regular_formula(core::detail::default_values::RegTransOrNil)
336 : {}
337 :
338 : /// \\brief Constructor.
339 : /// \\param term A term
340 176 : explicit trans_or_nil(const atermpp::aterm& term)
341 176 : : regular_formula(term)
342 : {
343 176 : assert(core::detail::check_term_RegTransOrNil(*this));
344 176 : }
345 :
346 : /// \\brief Constructor.
347 41 : explicit trans_or_nil(const regular_formula& operand)
348 41 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_RegTransOrNil(), operand))
349 41 : {}
350 :
351 : /// Move semantics
352 : trans_or_nil(const trans_or_nil&) noexcept = default;
353 : trans_or_nil(trans_or_nil&&) noexcept = default;
354 : trans_or_nil& operator=(const trans_or_nil&) noexcept = default;
355 : trans_or_nil& operator=(trans_or_nil&&) noexcept = default;
356 :
357 174 : const regular_formula& operand() const
358 : {
359 174 : return atermpp::down_cast<regular_formula>((*this)[0]);
360 : }
361 : };
362 :
363 : /// \\brief Make_trans_or_nil constructs a new term into a given address.
364 : /// \\ \param t The reference into which the new trans_or_nil is constructed.
365 : template <class... ARGUMENTS>
366 68 : inline void make_trans_or_nil(atermpp::aterm_appl& t, const ARGUMENTS&... args)
367 : {
368 68 : atermpp::make_term_appl(t, core::detail::function_symbol_RegTransOrNil(), args...);
369 68 : }
370 :
371 : /// \\brief Test for a trans_or_nil expression
372 : /// \\param x A term
373 : /// \\return True if \\a x is a trans_or_nil expression
374 : inline
375 415 : bool is_trans_or_nil(const atermpp::aterm_appl& x)
376 : {
377 415 : return x.function() == core::detail::function_symbols::RegTransOrNil;
378 : }
379 :
380 : // prototype declaration
381 : std::string pp(const trans_or_nil& x);
382 :
383 : /// \\brief Outputs the object to a stream
384 : /// \\param out An output stream
385 : /// \\param x Object x
386 : /// \\return The output stream
387 : inline
388 : std::ostream& operator<<(std::ostream& out, const trans_or_nil& x)
389 : {
390 : return out << regular_formulas::pp(x);
391 : }
392 :
393 : /// \\brief swap overload
394 : inline void swap(trans_or_nil& t1, trans_or_nil& t2)
395 : {
396 : t1.swap(t2);
397 : }
398 :
399 :
400 : /// \\brief An untyped regular formula or action formula
401 : class untyped_regular_formula: public regular_formula
402 : {
403 : public:
404 : /// \\brief Default constructor.
405 : untyped_regular_formula()
406 : : regular_formula(core::detail::default_values::UntypedRegFrm)
407 : {}
408 :
409 : /// \\brief Constructor.
410 : /// \\param term A term
411 10 : explicit untyped_regular_formula(const atermpp::aterm& term)
412 10 : : regular_formula(term)
413 : {
414 10 : assert(core::detail::check_term_UntypedRegFrm(*this));
415 10 : }
416 :
417 : /// \\brief Constructor.
418 5 : untyped_regular_formula(const core::identifier_string& name, const regular_formula& left, const regular_formula& right)
419 5 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_UntypedRegFrm(), name, left, right))
420 5 : {}
421 :
422 : /// \\brief Constructor.
423 : untyped_regular_formula(const std::string& name, const regular_formula& left, const regular_formula& right)
424 : : regular_formula(atermpp::aterm_appl(core::detail::function_symbol_UntypedRegFrm(), core::identifier_string(name), left, right))
425 : {}
426 :
427 : /// Move semantics
428 : untyped_regular_formula(const untyped_regular_formula&) noexcept = default;
429 : untyped_regular_formula(untyped_regular_formula&&) noexcept = default;
430 : untyped_regular_formula& operator=(const untyped_regular_formula&) noexcept = default;
431 : untyped_regular_formula& operator=(untyped_regular_formula&&) noexcept = default;
432 :
433 10 : const core::identifier_string& name() const
434 : {
435 10 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
436 : }
437 :
438 10 : const regular_formula& left() const
439 : {
440 10 : return atermpp::down_cast<regular_formula>((*this)[1]);
441 : }
442 :
443 10 : const regular_formula& right() const
444 : {
445 10 : return atermpp::down_cast<regular_formula>((*this)[2]);
446 : }
447 : };
448 :
449 : /// \\brief Make_untyped_regular_formula constructs a new term into a given address.
450 : /// \\ \param t The reference into which the new untyped_regular_formula is constructed.
451 : template <class... ARGUMENTS>
452 5 : inline void make_untyped_regular_formula(atermpp::aterm_appl& t, const ARGUMENTS&... args)
453 : {
454 5 : atermpp::make_term_appl(t, core::detail::function_symbol_UntypedRegFrm(), args...);
455 5 : }
456 :
457 : /// \\brief Test for a untyped_regular_formula expression
458 : /// \\param x A term
459 : /// \\return True if \\a x is a untyped_regular_formula expression
460 : inline
461 10 : bool is_untyped_regular_formula(const atermpp::aterm_appl& x)
462 : {
463 10 : return x.function() == core::detail::function_symbols::UntypedRegFrm;
464 : }
465 :
466 : // prototype declaration
467 : std::string pp(const untyped_regular_formula& x);
468 :
469 : /// \\brief Outputs the object to a stream
470 : /// \\param out An output stream
471 : /// \\param x Object x
472 : /// \\return The output stream
473 : inline
474 : std::ostream& operator<<(std::ostream& out, const untyped_regular_formula& x)
475 : {
476 : return out << regular_formulas::pp(x);
477 : }
478 :
479 : /// \\brief swap overload
480 : inline void swap(untyped_regular_formula& t1, untyped_regular_formula& t2)
481 : {
482 : t1.swap(t2);
483 : }
484 : //--- end generated classes ---//
485 :
486 : } // namespace regular_formulas
487 :
488 : } // namespace mcrl2
489 :
490 : #endif // MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
|
