mCRL2
Loading...
Searching...
No Matches
standard.h
Go to the documentation of this file.
1// Author(s): Jeroen Keiren
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_DATA_STANDARD_H
13#define MCRL2_DATA_STANDARD_H
14
18
19
20namespace mcrl2
21{
22
23namespace data
24{
25
26// predeclare
27namespace sort_bool
28{
29const basic_sort& bool_();
30const function_symbol& false_();
31const function_symbol& true_();
32application and_(const data_expression&,const data_expression&);
33application not_(const data_expression&);
34bool is_bool(const sort_expression&);
35} // namespace sort_bool
36
38namespace detail
39{
40
42template < typename Derived >
43struct symbol : public core::detail::singleton_identifier< Derived >
44{
45 static bool is_symbol(const core::identifier_string& e)
46 {
47 return e == core::detail::singleton_identifier< Derived >::instance();
48 }
49
50 static bool is_application(const data_expression& e)
51 {
52 return data::is_application(e) ? is_application(atermpp::down_cast<application>(e)) : false;
53 }
54
55 static bool is_application(const application& e)
56 {
57 return is_function_symbol(e.head());
58 }
59
60 static bool is_function_symbol(const data_expression& e)
61 {
62 return data::is_function_symbol(e) ? is_function_symbol(atermpp::down_cast<function_symbol>(e)) : false;
63 }
64
65 static bool is_function_symbol(const function_symbol& e)
66 {
67 return is_symbol(e.name());
68 }
69};
70
71struct equal_symbol : public symbol< equal_symbol >
72{
73 static char const* initialise()
74 {
75 return "==";
76 }
77};
78struct not_equal_symbol : public symbol< not_equal_symbol >
79{
80 static char const* initialise()
81 {
82 return "!=";
83 }
84};
85struct if_symbol : public symbol< if_symbol >
86{
87 static char const* initialise()
88 {
89 return "if";
90 }
91};
92struct less_symbol : public symbol< less_symbol >
93{
94 static char const* initialise()
95 {
96 return "<";
97 }
98};
99struct less_equal_symbol : public symbol< less_equal_symbol >
100{
101 static char const* initialise()
102 {
103 return "<=";
104 }
105};
106struct greater_symbol : public symbol< greater_symbol >
107{
108 static char const* initialise()
109 {
110 return ">";
111 }
112};
113struct greater_equal_symbol : public symbol< greater_equal_symbol >
114{
115 static char const* initialise()
116 {
117 return ">=";
118 }
119};
120} // namespace detail
122
127{
128 return function_symbol(detail::equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
129}
130
134template < typename DataExpression >
135inline bool is_equal_to_function_symbol(const DataExpression& e)
136{
137 return detail::equal_symbol::is_function_symbol(e);
138}
139
145{
146 assert(arg0.sort() == arg1.sort());
147 return equal_to(arg0.sort())(arg0, arg1);
148}
149
154template < typename DataExpression >
155inline bool is_equal_to_application(const DataExpression& e)
156{
157 return detail::equal_symbol::is_application(e);
158}
159
164{
165 return function_symbol(detail::not_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
166}
167
171template < typename DataExpression >
172inline bool is_not_equal_to_function_symbol(const DataExpression& e)
173{
174 return detail::not_equal_symbol::is_function_symbol(e);
175}
176
182{
183 assert(arg0.sort() == arg1.sort());
184 return not_equal_to(arg0.sort())(arg0, arg1);
185}
186
191template < typename DataExpression >
192inline bool is_not_equal_to_application(const DataExpression& e)
193{
194 return detail::not_equal_symbol::is_application(e);
195}
196
201{
202 return function_symbol(detail::if_symbol::instance(), make_function_sort_(sort_bool::bool_(), s, s, s));
203}
204
208template < typename DataExpression >
209inline bool is_if_function_symbol(const DataExpression& e)
210{
211 return detail::if_symbol::is_function_symbol(e);
212}
213
220{
221 assert(sort_bool::is_bool(arg0.sort()));
222 assert(arg1.sort() == arg2.sort());
223
224 return if_(arg1.sort())(arg0, arg1, arg2);
225}
226
231template < typename DataExpression >
232inline bool is_if_application(const DataExpression& e)
233{
234 return detail::if_symbol::is_application(e);
235}
236
241{
242 return function_symbol(detail::less_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
243}
244
248template < typename DataExpression >
249inline bool is_less_function_symbol(const DataExpression& e)
250{
251 return detail::less_symbol::is_function_symbol(e);
252}
253
259{
260 assert(arg0.sort() == arg1.sort());
261 return less(arg0.sort())(arg0, arg1);
262}
263
268template < typename DataExpression >
269inline bool is_less_application(const DataExpression& e)
270{
271 return detail::less_symbol::is_application(e);
272}
273
278{
279 return function_symbol(detail::less_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
280}
281
285template < typename DataExpression >
286inline bool is_less_equal_function_symbol(const DataExpression& e)
287{
288 return detail::less_equal_symbol::is_function_symbol(e);
289}
290
296{
297 assert(arg0.sort() == arg1.sort());
298 return less_equal(arg0.sort())(arg0, arg1);
299}
300
305template < typename DataExpression >
306inline bool is_less_equal_application(const DataExpression& e)
307{
308 return detail::less_equal_symbol::is_application(e);
309}
310
315{
316 return function_symbol(detail::greater_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
317}
318
322template < typename DataExpression >
323inline bool is_greater_function_symbol(const DataExpression& e)
324{
325 return detail::greater_symbol::is_function_symbol(e);
326}
327
333{
334 assert(arg0.sort() == arg1.sort());
335 return greater(arg0.sort())(arg0, arg1);
336}
337
342template < typename DataExpression >
343inline bool is_greater_application(const DataExpression& e)
344{
345 return detail::greater_symbol::is_application(e);
346}
347
352{
353 return function_symbol(detail::greater_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
354}
355
359template < typename DataExpression >
360inline bool is_greater_equal_function_symbol(const DataExpression& e)
361{
362 return detail::greater_equal_symbol::is_function_symbol(e);
363}
364
370{
371 assert(arg0.sort() == arg1.sort());
372 return greater_equal(arg0.sort())(arg0, arg1);
373}
374
379template < typename DataExpression >
380inline bool is_greater_equal_application(const DataExpression& e)
381{
382 return detail::greater_equal_symbol::is_application(e);
383}
384
389{
391 result.push_back(equal_to(s));
392 result.push_back(not_equal_to(s));
393 result.push_back(if_(s));
394 result.push_back(less(s));
395 result.push_back(less_equal(s));
396 result.push_back(greater_equal(s));
397 result.push_back(greater(s));
398
399 return result;
400}
401
406{
408 variable b("b", sort_bool::bool_());
409 variable x("x", s);
410 variable y("y", s);
411 result.push_back(data_equation(variable_list({x}), equal_to(x, x), sort_bool::true_()));
412 result.push_back(data_equation(variable_list({x, y}), not_equal_to(x, y), sort_bool::not_(equal_to(x, y))));
413 result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::true_(), x, y), x));
414 result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::false_(), x, y), y));
415 result.push_back(data_equation(variable_list({b, x}), if_(b, x, x), x));
416 result.push_back(data_equation(variable_list({x}), less(x,x), sort_bool::false_()));
417 result.push_back(data_equation(variable_list({x}), less_equal(x,x), sort_bool::true_()));
418 result.push_back(data_equation(variable_list({x, y}), greater_equal(x,y), less_equal(y,x)));
419 result.push_back(data_equation(variable_list({x, y}), greater(x,y), less(y,x)));
420
421 // For a function sort, add the equation f==g iff forall x.f(x)==g(x). This equation is not in the Specification and Analysis of Communicating Systems of 2014.
422 if (is_function_sort(s))
423 {
424 const function_sort& fs = atermpp::down_cast<function_sort>(s);
425 variable_vector xvars,yvars;
426 std::size_t index=0;
427 for(const sort_expression& sort: fs.domain())
428 {
429 std::stringstream xs;
430 xs << "x" << index;
431 ++index;
432 variable x(xs.str(),sort);
433 xvars.push_back(x);
434 }
435 variable f("f",s);
436 variable g("g",s);
437 variable_list xvar_list=variable_list(xvars.begin(),xvars.end());
438 result.push_back(data_equation(variable_list({ f, g }) + xvar_list,
439 equal_to(f,g),
440 abstraction(forall_binder(),xvar_list,
441 equal_to(
442 application(f,xvars.begin(),xvars.end()),
443 application(g,xvars.begin(),xvars.end())))));
444 }
445
446 return result;
447}
448
449} // namespace data
450} // namespace mcrl2
451
452#endif // MCRL2_DATA_STANDARD_H
The class abstraction.
An abstraction expression.
Definition abstraction.h:26
An application of a data expression to a number of arguments.
\brief A data equation
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
const_iterator begin() const
\brief Binder for universal quantification
\brief A function sort
const sort_expression_list & domain() const
\brief A function symbol
\brief A sort expression
\brief A data variable
Definition variable.h:28
The class data_equation.
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:343
bool is_greater_function_symbol(const DataExpression &e)
Recogniser for function >
Definition standard.h:323
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:388
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
bool is_equal_to_function_symbol(const DataExpression &e)
Recogniser for function ==.
Definition standard.h:135
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
bool is_not_equal_to_application(const DataExpression &e)
Recogniser for application of !=.
Definition standard.h:192
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:380
bool is_function_symbol(const atermpp::aterm_appl &x)
Returns true if the term t is a function symbol.
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
Definition standard.h:405
bool is_not_equal_to_function_symbol(const DataExpression &e)
Recogniser for function !=.
Definition standard.h:172
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
bool is_application(const atermpp::aterm_appl &x)
Returns true if the term t is an application.
bool is_less_function_symbol(const DataExpression &e)
Recogniser for function <.
Definition standard.h:249
bool is_if_function_symbol(const DataExpression &e)
Recogniser for function if.
Definition standard.h:209
atermpp::term_list< variable > variable_list
\brief list of variables
bool is_less_equal_function_symbol(const DataExpression &e)
Recogniser for function <=.
Definition standard.h:286
bool is_greater_equal_function_symbol(const DataExpression &e)
Recogniser for function >=.
Definition standard.h:360
bool is_function_sort(const atermpp::aterm_appl &x)
Returns true if the term t is a function sort.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:269
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:306
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72