mCRL2
Loading...
Searching...
No Matches
regular_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_REGULAR_FORMULA_H
13#define MCRL2_MODAL_FORMULA_REGULAR_FORMULA_H
14
16
17namespace mcrl2
18{
19
20namespace regular_formulas
21{
22
23//--- start generated classes ---//
26{
27 public:
30 : atermpp::aterm(core::detail::default_values::RegFrm)
31 {}
32
35 explicit regular_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 regular_formula(const regular_formula&) noexcept = default;
53 regular_formula(regular_formula&&) noexcept = default;
54 regular_formula& operator=(const regular_formula&) noexcept = default;
55 regular_formula& operator=(regular_formula&&) noexcept = default;
56};
57
60
63
64// prototypes
65inline bool is_seq(const atermpp::aterm& x);
66inline bool is_alt(const atermpp::aterm& x);
67inline bool is_trans(const atermpp::aterm& x);
68inline bool is_trans_or_nil(const atermpp::aterm& x);
69inline bool is_untyped_regular_formula(const atermpp::aterm& x);
70
74inline
76{
77 return data::is_data_expression(x) ||
84}
85
86// prototype declaration
87std::string pp(const regular_formula& x);
88
93inline
94std::ostream& operator<<(std::ostream& out, const regular_formula& x)
95{
96 return out << regular_formulas::pp(x);
97}
98
101{
102 t1.swap(t2);
103}
104
105
107class seq: public regular_formula
108{
109 public:
112 : regular_formula(core::detail::default_values::RegSeq)
113 {}
114
117 explicit seq(const atermpp::aterm& term)
118 : regular_formula(term)
119 {
120 assert(core::detail::check_term_RegSeq(*this));
121 }
122
124 seq(const regular_formula& left, const regular_formula& right)
125 : regular_formula(atermpp::aterm(core::detail::function_symbol_RegSeq(), left, right))
126 {}
127
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 const regular_formula& left() const
135 {
136 return atermpp::down_cast<regular_formula>((*this)[0]);
137 }
138
139 const regular_formula& right() const
140 {
141 return atermpp::down_cast<regular_formula>((*this)[1]);
142 }
143};
144
147template <class... ARGUMENTS>
148inline void make_seq(atermpp::aterm& t, const ARGUMENTS&... args)
149{
151}
152
156inline
157bool is_seq(const atermpp::aterm& x)
158{
160}
161
162// prototype declaration
163std::string pp(const seq& x);
164
169inline
170std::ostream& operator<<(std::ostream& out, const seq& x)
171{
172 return out << regular_formulas::pp(x);
173}
174
176inline void swap(seq& t1, seq& t2)
177{
178 t1.swap(t2);
179}
180
181
183class alt: public regular_formula
184{
185 public:
188 : regular_formula(core::detail::default_values::RegAlt)
189 {}
190
193 explicit alt(const atermpp::aterm& term)
194 : regular_formula(term)
195 {
196 assert(core::detail::check_term_RegAlt(*this));
197 }
198
200 alt(const regular_formula& left, const regular_formula& right)
201 : regular_formula(atermpp::aterm(core::detail::function_symbol_RegAlt(), left, right))
202 {}
203
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 const regular_formula& left() const
211 {
212 return atermpp::down_cast<regular_formula>((*this)[0]);
213 }
214
215 const regular_formula& right() const
216 {
217 return atermpp::down_cast<regular_formula>((*this)[1]);
218 }
219};
220
223template <class... ARGUMENTS>
224inline void make_alt(atermpp::aterm& t, const ARGUMENTS&... args)
225{
227}
228
232inline
233bool is_alt(const atermpp::aterm& x)
234{
236}
237
238// prototype declaration
239std::string pp(const alt& x);
240
245inline
246std::ostream& operator<<(std::ostream& out, const alt& x)
247{
248 return out << regular_formulas::pp(x);
249}
250
252inline void swap(alt& t1, alt& t2)
253{
254 t1.swap(t2);
255}
256
257
260{
261 public:
264 : regular_formula(core::detail::default_values::RegTrans)
265 {}
266
269 explicit trans(const atermpp::aterm& term)
270 : regular_formula(term)
271 {
272 assert(core::detail::check_term_RegTrans(*this));
273 }
274
276 explicit trans(const regular_formula& operand)
277 : regular_formula(atermpp::aterm(core::detail::function_symbol_RegTrans(), operand))
278 {}
279
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 const regular_formula& operand() const
287 {
288 return atermpp::down_cast<regular_formula>((*this)[0]);
289 }
290};
291
294template <class... ARGUMENTS>
295inline void make_trans(atermpp::aterm& t, const ARGUMENTS&... args)
296{
298}
299
303inline
305{
307}
308
309// prototype declaration
310std::string pp(const trans& x);
311
316inline
317std::ostream& operator<<(std::ostream& out, const trans& x)
318{
319 return out << regular_formulas::pp(x);
320}
321
323inline void swap(trans& t1, trans& t2)
324{
325 t1.swap(t2);
326}
327
328
331{
332 public:
335 : regular_formula(core::detail::default_values::RegTransOrNil)
336 {}
337
340 explicit trans_or_nil(const atermpp::aterm& term)
341 : regular_formula(term)
342 {
343 assert(core::detail::check_term_RegTransOrNil(*this));
344 }
345
347 explicit trans_or_nil(const regular_formula& operand)
348 : regular_formula(atermpp::aterm(core::detail::function_symbol_RegTransOrNil(), operand))
349 {}
350
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 const regular_formula& operand() const
358 {
359 return atermpp::down_cast<regular_formula>((*this)[0]);
360 }
361};
362
365template <class... ARGUMENTS>
366inline void make_trans_or_nil(atermpp::aterm& t, const ARGUMENTS&... args)
367{
369}
370
374inline
376{
378}
379
380// prototype declaration
381std::string pp(const trans_or_nil& x);
382
387inline
388std::ostream& operator<<(std::ostream& out, const trans_or_nil& x)
389{
390 return out << regular_formulas::pp(x);
391}
392
394inline void swap(trans_or_nil& t1, trans_or_nil& t2)
395{
396 t1.swap(t2);
397}
398
399
402{
403 public:
406 : regular_formula(core::detail::default_values::UntypedRegFrm)
407 {}
408
412 : regular_formula(term)
413 {
414 assert(core::detail::check_term_UntypedRegFrm(*this));
415 }
416
419 : regular_formula(atermpp::aterm(core::detail::function_symbol_UntypedRegFrm(), name, left, right))
420 {}
421
423 untyped_regular_formula(const std::string& name, const regular_formula& left, const regular_formula& right)
424 : regular_formula(atermpp::aterm(core::detail::function_symbol_UntypedRegFrm(), core::identifier_string(name), left, right))
425 {}
426
430 untyped_regular_formula& operator=(const untyped_regular_formula&) noexcept = default;
431 untyped_regular_formula& operator=(untyped_regular_formula&&) noexcept = default;
432
433 const core::identifier_string& name() const
434 {
435 return atermpp::down_cast<core::identifier_string>((*this)[0]);
436 }
437
438 const regular_formula& left() const
439 {
440 return atermpp::down_cast<regular_formula>((*this)[1]);
441 }
442
443 const regular_formula& right() const
444 {
445 return atermpp::down_cast<regular_formula>((*this)[2]);
446 }
447};
448
451template <class... ARGUMENTS>
452inline void make_untyped_regular_formula(atermpp::aterm& t, const ARGUMENTS&... args)
453{
455}
456
460inline
462{
464}
465
466// prototype declaration
467std::string pp(const untyped_regular_formula& x);
468
473inline
474std::ostream& operator<<(std::ostream& out, const untyped_regular_formula& x)
475{
476 return out << regular_formulas::pp(x);
477}
478
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
Add your file description here.
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 alt operator for regular formulas
alt(const atermpp::aterm &term)
alt()
\brief Default constructor X3.
const regular_formula & right() const
alt(const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
alt(const alt &) noexcept=default
Move semantics.
alt(alt &&) noexcept=default
regular_formula()
\brief Default constructor X3.
regular_formula(const action_formulas::action_formula &x)
\brief Constructor Z6.
regular_formula(const atermpp::aterm &term)
regular_formula(const regular_formula &) noexcept=default
Move semantics.
regular_formula(const data::data_expression &x)
\brief Constructor Z6.
regular_formula(regular_formula &&) noexcept=default
\brief The seq operator for regular formulas
seq(const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
const regular_formula & right() const
seq(const seq &) noexcept=default
Move semantics.
seq(seq &&) noexcept=default
seq()
\brief Default constructor X3.
seq(const atermpp::aterm &term)
\brief The 'trans or nil' operator for regular formulas
trans_or_nil(const trans_or_nil &) noexcept=default
Move semantics.
trans_or_nil(const regular_formula &operand)
\brief Constructor Z14.
trans_or_nil()
\brief Default constructor X3.
trans_or_nil(trans_or_nil &&) noexcept=default
trans_or_nil(const atermpp::aterm &term)
\brief The trans operator for regular formulas
trans(const atermpp::aterm &term)
trans(trans &&) noexcept=default
trans()
\brief Default constructor X3.
trans(const trans &) noexcept=default
Move semantics.
trans(const regular_formula &operand)
\brief Constructor Z14.
\brief An untyped regular formula or action formula
untyped_regular_formula()
\brief Default constructor X3.
untyped_regular_formula(const std::string &name, const regular_formula &left, const regular_formula &right)
\brief Constructor Z2.
untyped_regular_formula(const core::identifier_string &name, const regular_formula &left, const regular_formula &right)
\brief Constructor Z14.
untyped_regular_formula(const untyped_regular_formula &) noexcept=default
Move semantics.
untyped_regular_formula(untyped_regular_formula &&) 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 is_action_formula(const atermpp::aterm &x)
const atermpp::function_symbol & function_symbol_RegSeq()
const atermpp::function_symbol & function_symbol_RegTransOrNil()
const atermpp::function_symbol & function_symbol_RegTrans()
const atermpp::function_symbol & function_symbol_RegAlt()
bool check_rule_RegFrm(const Term &t)
const atermpp::function_symbol & function_symbol_UntypedRegFrm()
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_alt(const atermpp::aterm &x)
bool is_untyped_regular_formula(const atermpp::aterm &x)
void make_trans(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const regular_formula &x)
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
void make_trans_or_nil(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_trans(const atermpp::aterm &x)
void make_alt(atermpp::aterm &t, const ARGUMENTS &... args)
void make_untyped_regular_formula(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_trans_or_nil(const atermpp::aterm &x)
bool is_regular_formula(const atermpp::aterm &x)
bool is_seq(const atermpp::aterm &x)
std::vector< regular_formula > regular_formula_vector
\brief vector of regular_formulas
void swap(regular_formula &t1, regular_formula &t2)
\brief swap overload
void pp(const T &t, std::ostream &out)
Prints the object t to a stream.
Definition print.h:279
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.
static const atermpp::function_symbol UntypedRegFrm
static const atermpp::function_symbol RegSeq
static const atermpp::function_symbol RegTransOrNil
static const atermpp::function_symbol RegAlt
static const atermpp::function_symbol RegTrans