Line data Source code
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 : //
9 : /// \file set_test.cpp
10 : /// \brief Basic regression test for set expressions.
11 :
12 : #define BOOST_TEST_MODULE set_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/parse.h"
16 : #include "mcrl2/data/rewriter.h"
17 : #include "mcrl2/data/set.h"
18 :
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::data;
22 : using namespace mcrl2::data::sort_set;
23 : using namespace mcrl2::data::sort_fset;
24 :
25 : template <typename Predicate>
26 11 : void test_data_expression(const std::string& s, const variable_vector& v, Predicate p)
27 : {
28 11 : std::cerr << "testing data expression " << s << std::endl;
29 11 : data_expression e = parse_data_expression(s, v);
30 11 : BOOST_CHECK(p(e));
31 11 : }
32 :
33 :
34 47 : void test_expression(const std::string& evaluate, const std::string& expected, data::rewriter r)
35 : {
36 47 : const data_expression d1 = parse_data_expression(evaluate);
37 47 : const data_expression rd1 =r(d1);
38 47 : const data_expression d2 = parse_data_expression(expected);
39 47 : const data_expression rd2 =r(d2);
40 :
41 47 : if (rd1!=rd2)
42 : {
43 0 : std::cerr << "------------------------------------------------------\n";
44 0 : std::cerr << "Evaluating: " << evaluate << "\n";
45 0 : std::cerr << "Result: " << rd1 << "\n";
46 0 : std::cerr << "Expected result: " << expected << "\n";
47 0 : std::cerr << "Evaluated expected result " << rd2 << "\n";
48 0 : BOOST_CHECK(rd1 == rd2);
49 0 : std::cerr << "------------------------------------------------------\n";
50 : }
51 47 : }
52 :
53 1 : void set_expression_test()
54 : {
55 1 : data::data_specification specification;
56 :
57 1 : specification.add_context_sort(sort_pos::pos());
58 1 : specification.add_context_sort(sort_set::set_(sort_pos::pos()));
59 1 : specification.add_context_sort(sort_set::set_(sort_bool::bool_()));
60 :
61 1 : data::rewriter normaliser(specification);
62 :
63 1 : variable_vector v;
64 1 : v.push_back(parse_variable("s:Set(Nat)"));
65 :
66 1 : test_data_expression("{x : Nat | x < 10}", v, sort_set::is_constructor_application);
67 1 : test_data_expression("!s", v, sort_set::is_complement_application);
68 1 : test_data_expression("s * {}", v, sort_set::is_intersection_application);
69 1 : test_data_expression("s * {1,2,3}", v, sort_set::is_intersection_application);
70 1 : test_data_expression("s - {3,1,2}", v, sort_set::is_difference_application);
71 1 : test_data_expression("1 in s", v, sort_set::is_in_application);
72 1 : test_data_expression("{} + s", v, sort_set::is_union_application);
73 1 : test_data_expression("(({} + s) - {20}) * {40}", v, sort_set::is_intersection_application);
74 1 : test_data_expression("{10} < s", v, is_less_application<data_expression>);
75 1 : test_data_expression("s <= {10}", v, is_less_equal_application<data_expression>);
76 1 : test_data_expression("{20} + {30}", v, sort_set::is_union_application);
77 :
78 1 : test_expression("{1,2}", "{2,1}", normaliser);
79 :
80 2 : data_expression t1d1a = parse_data_expression("{1,2,3}");
81 2 : data_expression t1d2a = parse_data_expression("{2,1}");
82 1 : BOOST_CHECK(normaliser(t1d1a) != normaliser(t1d2a));
83 :
84 2 : data_expression t2d1 = parse_data_expression("{1,2} == {1,2}");
85 2 : data_expression t2d2 = parse_data_expression("true");
86 1 : BOOST_CHECK(normaliser(t2d1) == normaliser(t2d2));
87 :
88 2 : data_expression t2d1a = parse_data_expression("{1,2,3} == {1,2,1}");
89 2 : data_expression t2d2a = parse_data_expression("false");
90 1 : BOOST_CHECK(normaliser(t2d1a) == normaliser(t2d2a));
91 :
92 2 : data_expression t3d1 = parse_data_expression("({1,2} != {2,3})");
93 2 : data_expression t3d2 = parse_data_expression("true");
94 1 : BOOST_CHECK(normaliser(t3d1) == normaliser(t3d2));
95 :
96 2 : data_expression t4d1 = parse_data_expression("(!{1,2}) == {1,2}");
97 2 : data_expression t4d2 = parse_data_expression("false");
98 1 : BOOST_CHECK(normaliser(t4d1) == normaliser(t4d2));
99 :
100 2 : data_expression t5d1 = parse_data_expression("(!!{1,2}) == {2,1}");
101 2 : data_expression t5d2 = parse_data_expression("true");
102 1 : BOOST_CHECK(normaliser(t5d1) == normaliser(t5d2));
103 :
104 :
105 2 : data_expression e = parse_data_expression("{20}", v);
106 1 : BOOST_CHECK(sort_fset::is_cons_application(normaliser(e)));
107 :
108 1 : e = parse_data_expression("{20, 30, 40}", v);
109 1 : BOOST_CHECK(sort_fset::is_cons_application(normaliser(e)));
110 :
111 1 : test_expression("{} == { b: Bool | true } - { true, false }","true",normaliser);
112 :
113 1 : test_expression("{ b: Bool | true } - { true, false } == {}","true", normaliser);
114 :
115 : // Check the operation == on sets.
116 1 : test_expression("{} == ({true} - {true})","true",normaliser); // {true}-{true} is a trick to type {} == {}.
117 1 : test_expression("{} == {false}", "false",normaliser);
118 1 : test_expression("{} == {true}", "false",normaliser);
119 1 : test_expression("{true} == {true}", "true",normaliser);
120 1 : test_expression("{false} == {false}", "true",normaliser);
121 1 : test_expression("{true} == {false, true}", "false",normaliser);
122 1 : test_expression("{false, true} == {false}", "false",normaliser);
123 1 : test_expression("{false, true} == {true, false}", "true",normaliser);
124 :
125 : // Check the operation < on sets.
126 1 : test_expression("{} < ({true} - {true})","false",normaliser); // {true}-{true} is a trick to type {} == {}.
127 1 : test_expression("{true} < {false}", "false",normaliser);
128 1 : test_expression("{false} < {true}", "false",normaliser);
129 1 : test_expression("{true} < {true}", "false",normaliser);
130 1 : test_expression("{false} < {false}", "false",normaliser);
131 1 : test_expression("{true} < {false, true}", "true",normaliser);
132 1 : test_expression("{false} < {false, true}", "true",normaliser);
133 1 : test_expression("{true} < {true, false}", "true",normaliser);
134 1 : test_expression("{false} < {true, false}", "true",normaliser);
135 1 : test_expression("{true, false} < {true}", "false",normaliser);
136 1 : test_expression("{true, false} < {false}", "false",normaliser);
137 1 : test_expression("{false, true} < {true}", "false",normaliser);
138 1 : test_expression("{false, true} < {false}", "false",normaliser);
139 1 : test_expression("{true, false} < {false, true}", "false",normaliser);
140 1 : test_expression("{true, false} < {true, false}", "false",normaliser);
141 1 : test_expression("{false, true} < {false, true}", "false",normaliser);
142 1 : test_expression("{false, true} < {true, false}", "false",normaliser);
143 1 : test_expression("{false, false} < {false}", "false",normaliser);
144 :
145 : // Check the operation <= on sets.
146 1 : test_expression("{} <= ({true}-{true})","true",normaliser); // {true} - {true} is a trick to type {} == {}.
147 1 : test_expression("{true} <= {false}", "false",normaliser);
148 1 : test_expression("{false} <= {true}", "false",normaliser);
149 1 : test_expression("{true} <= {true}", "true",normaliser);
150 1 : test_expression("{false} <= {false}", "true",normaliser);
151 1 : test_expression("{true} <= {false, true}", "true",normaliser);
152 1 : test_expression("{false} <= {false, true}", "true",normaliser);
153 1 : test_expression("{true} <= {true, false}", "true",normaliser);
154 1 : test_expression("{false} <= {true, false}", "true",normaliser);
155 1 : test_expression("{true, false} <= {true}", "false",normaliser);
156 1 : test_expression("{true, false} <= {false}", "false",normaliser);
157 1 : test_expression("{false, true} <= {true}", "false",normaliser);
158 1 : test_expression("{false, true} <= {false}", "false",normaliser);
159 1 : test_expression("{true, false} <= {false, true}", "true",normaliser);
160 1 : test_expression("{true, false} <= {true, false}", "true",normaliser);
161 1 : test_expression("{false, true} <= {false, true}", "true",normaliser);
162 1 : test_expression("{false, true} <= {true, false}", "true",normaliser);
163 1 : test_expression("{false, false} <= {false}", "true",normaliser);
164 :
165 :
166 :
167 1 : }
168 :
169 2 : BOOST_AUTO_TEST_CASE(test_main)
170 : {
171 1 : set_expression_test();
172 1 : }
173 :
|
