Line data Source code
1 : // Author(s): Jan Friso Groote
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 linear_inequalities_test.cpp
10 : /// \brief Test the linear_inequality functionality.
11 :
12 : #define BOOST_TEST_MODULE linear_inequalities_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/fourier_motzkin.h"
16 : #include "mcrl2/data/join.h"
17 : #include "mcrl2/data/parse.h"
18 :
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::core;
22 : using namespace mcrl2::data;
23 :
24 12 : void check(bool result, std::string message)
25 : {
26 12 : if(!result) {
27 0 : std::cout << message << std::endl;
28 : }
29 12 : BOOST_CHECK(result);
30 12 : }
31 :
32 1 : void test_linear_inequality()
33 : {
34 1 : data_specification data_spec;
35 1 : data_spec.add_context_sort(sort_real::real_());
36 1 : rewriter rewr(data_spec);
37 :
38 2 : variable vx("x", sort_real::real_());
39 2 : variable vy("y", sort_real::real_());
40 1 : linear_inequality li;
41 1 : data_expression expr;
42 :
43 1 : expr = less(real_zero(), real_zero());
44 1 : li = linear_inequality(expr, rewr);
45 1 : check(li.is_false(rewr), "Expected " + pp(expr) + "' to be false");
46 1 : check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty " + pp(li.lhs()));
47 :
48 1 : expr = less_equal(real_zero(), real_zero());
49 1 : li = linear_inequality(expr, rewr);
50 1 : check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
51 1 : check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
52 :
53 1 : expr = less_equal(sort_real::minus(vx, vx), real_one());
54 1 : li = linear_inequality(expr, rewr);
55 1 : check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
56 1 : check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
57 :
58 1 : expr = less_equal(sort_real::minus(vx, vx), real_one());
59 1 : li = linear_inequality(expr, rewr);
60 1 : check(li.is_true(rewr), "Expected '" + pp(expr) + "' to be true");
61 1 : check(li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' to be empty");
62 :
63 1 : expr = less_equal(sort_real::plus(vx, vy), vx);
64 1 : li = linear_inequality(expr, rewr);
65 1 : check(!li.is_true(rewr), "Expected '" + pp(expr) + "' to not be true");
66 1 : check(!li.lhs().empty(), "Expected left hand side of '" + pp(expr) + "' not to be empty");
67 1 : check(li.transform_to_data_expression() == less_equal(sort_real::times(real_one(), vy), real_zero()),
68 2 : "Expression '" + pp(expr) + "' parsing/output problem " + pp(li.transform_to_data_expression()));
69 :
70 1 : bool got_exception = false;
71 : try
72 : {
73 1 : expr = not_equal_to(vx, vy);
74 1 : li = linear_inequality(expr, rewr);
75 : }
76 1 : catch(const mcrl2::runtime_error&)
77 : {
78 1 : got_exception = true;
79 1 : }
80 1 : check(got_exception, "Expected an exception while parsing x != y.");
81 1 : }
82 :
83 47 : void split_conjunction_of_inequalities_set(const data_expression& e, std::vector < linear_inequality >& v, const rewriter& r)
84 : {
85 47 : if (sort_bool::is_and_application(e))
86 : {
87 19 : split_conjunction_of_inequalities_set(application(e)[0],v,r);
88 19 : split_conjunction_of_inequalities_set(application(e)[1],v,r);
89 : }
90 : else
91 : {
92 28 : v.push_back(linear_inequality(e,r));
93 : }
94 47 : }
95 :
96 7 : bool test_consistency_of_inequalities(const std::string& vars,
97 : const std::string& inequalities,
98 : const bool expect_consistent)
99 : {
100 : // Take care that reals are part of the data type.
101 7 : data_specification data_spec;
102 7 : variable_list variables=parse_variables(vars);
103 7 : data_spec.add_context_sort(sort_real::real_());
104 7 : const data_expression e=parse_data_expression(inequalities,variables,data_spec);
105 :
106 7 : rewriter r(data_spec);
107 7 : std::vector < linear_inequality > v_inequalities;
108 7 : split_conjunction_of_inequalities_set(e,v_inequalities,r);
109 :
110 7 : if (is_inconsistent(v_inequalities,r))
111 : {
112 2 : if (expect_consistent)
113 : {
114 0 : std::cout << "Expected consistent, found inconsistent\n";
115 0 : std::cout << variables << ": " << inequalities << "\n";
116 0 : std::cout << "Internal inequalities: " << pp_vector(v_inequalities) << "\n";
117 0 : return false;
118 : }
119 : }
120 : else
121 : {
122 5 : if (!expect_consistent)
123 : {
124 0 : std::cout << "Expected inconsistent, found consistent\n";
125 0 : std::cout << variables << ": " << inequalities << "\n";
126 0 : std::cout << "Internal inequalities: " << pp_vector(v_inequalities) << "\n";
127 0 : return false;
128 : }
129 : }
130 7 : return true;
131 7 : }
132 :
133 2 : bool test_application_of_Fourier_Motzkin(const std::string& vars,
134 : const std::string& variables_to_be_eliminated,
135 : const std::string& inequalities,
136 : const std::string& inconsistent_with,
137 : bool check_consistent = false)
138 : {
139 : // Take care that reals are part of the data type.
140 2 : data_specification data_spec;
141 2 : data_spec.add_context_sort(sort_real::real_());
142 2 : const variable_list variables=parse_variables(vars);
143 2 : const data_expression e_in=parse_data_expression(inequalities,variables,data_spec);
144 2 : const variable_list v_elim= data::detail::parse_variables(variables_to_be_eliminated);
145 :
146 2 : rewriter r(data_spec);
147 2 : std::vector < linear_inequality > v_inequalities;
148 2 : split_conjunction_of_inequalities_set(e_in,v_inequalities,r);
149 :
150 2 : std::vector < linear_inequality> resulting_inequalities;
151 2 : fourier_motzkin(v_inequalities, v_elim.begin(), v_elim.end(), resulting_inequalities, r);
152 :
153 2 : std::vector < linear_inequality> inconsistent_inequalities=resulting_inequalities;
154 2 : inconsistent_inequalities.push_back(linear_inequality(parse_data_expression(inconsistent_with,variables,data_spec),r));
155 2 : if (!(check_consistent ^ is_inconsistent(inconsistent_inequalities,r, false)))
156 : {
157 0 : std::cout << "Expected set of inequations to be " << (check_consistent ? "" : "in") << "consistent with given inequality after applying Fourier-Motzkin elimination\n";
158 0 : std::cout << "Input: " << variables << ": " << inequalities << "\n";
159 0 : std::cout << "Parsed input : " << pp_vector(v_inequalities) << "\n";
160 0 : std::cout << "Variables to be eliminated: " << v_elim << "\n";
161 0 : std::cout << "Input after applying Fourier Motzkin: " << pp_vector(resulting_inequalities) << "\n";
162 0 : std::cout << "Should be " << (check_consistent ? "" : "in") << "consistent with " << inconsistent_with << "\n";
163 0 : std::cout << (check_consistent ? "Consistent" : "Inconsistent") << " inequality after parsing " << pp(linear_inequality(parse_data_expression(inconsistent_with,variables,data_spec),r)) << "\n";
164 0 : return false;
165 : }
166 2 : return true;
167 2 : }
168 :
169 1 : void test_high_level_fourier_motzkin()
170 : {
171 1 : data_specification data_spec;
172 1 : data_spec.add_context_sort(sort_real::real_());
173 1 : rewriter rewr(data_spec);
174 2 : variable vx("x", sort_real::real_());
175 2 : variable vy("y", sort_real::real_());
176 :
177 2 : data_expression expr = sort_bool::and_(equal_to(vx, vy), less(vy, sort_real::real_(2)));
178 3 : variable_list elim_vars({variable("y", sort_real::real_())});
179 1 : data_expression out;
180 1 : variable_list vars_out;
181 1 : fourier_motzkin(expr, elim_vars, out, vars_out, rewr);
182 :
183 1 : BOOST_CHECK(vars_out.empty());
184 1 : BOOST_CHECK(out == less(sort_real::times(real_one(), vx), sort_real::real_(2)));
185 1 : }
186 :
187 1 : void test_high_level_fourier_motzkin_non_linear()
188 : {
189 1 : data_specification data_spec;
190 1 : data_spec.add_context_sort(sort_real::real_());
191 1 : rewriter rewr(data_spec);
192 2 : variable vx("x", sort_real::real_());
193 :
194 2 : data_expression expr = less(sort_real::times(vx,vx), sort_real::real_(0));
195 2 : variable_list elim_vars({vx});
196 1 : data_expression out;
197 1 : variable_list vars_out;
198 1 : fourier_motzkin(expr, elim_vars, out, vars_out, rewr);
199 :
200 : // Fourier Motzkin should fail, because the expression is not linear
201 : // Original result should be returned
202 1 : BOOST_CHECK(vars_out == elim_vars);
203 1 : BOOST_CHECK(out == expr);
204 1 : }
205 :
206 6 : void split_conditions_helper(const std::string& vars,
207 : const std::string& expr,
208 : std::vector< data_expression_list >& real_conditions,
209 : std::vector< data_expression >& non_real_conditions)
210 : {
211 6 : data_specification data_spec;
212 6 : data_spec.add_context_sort(sort_real::real_());
213 6 : const variable_list variables=parse_variables(vars);
214 6 : const data_expression e_in=parse_data_expression(expr,variables,data_spec);
215 :
216 6 : data::detail::split_condition(e_in, real_conditions, non_real_conditions);
217 6 : }
218 :
219 1 : void test_split_conditions()
220 : {
221 1 : std::vector < data_expression_list > real_conditions;
222 1 : std::vector < data_expression > non_real_conditions;
223 :
224 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "a && b", real_conditions, non_real_conditions);
225 1 : BOOST_CHECK(real_conditions.size() == 1);
226 1 : BOOST_CHECK(non_real_conditions.size() == 1);
227 1 : BOOST_CHECK(real_conditions[0].size() == 0);
228 1 : BOOST_CHECK(sort_bool::is_and_application(non_real_conditions[0]));
229 1 : real_conditions.clear(); non_real_conditions.clear();
230 :
231 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && c", real_conditions, non_real_conditions);
232 1 : BOOST_CHECK(real_conditions.size() == 1);
233 1 : BOOST_CHECK(non_real_conditions.size() == 1);
234 1 : BOOST_CHECK(real_conditions[0].size() == 0);
235 1 : BOOST_CHECK(sort_bool::is_and_application(non_real_conditions[0]));
236 1 : BOOST_CHECK(sort_bool::is_or_application(sort_bool::left(non_real_conditions[0])));
237 1 : real_conditions.clear(); non_real_conditions.clear();
238 :
239 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && x < 5", real_conditions, non_real_conditions);
240 1 : BOOST_CHECK(real_conditions.size() == 1);
241 1 : BOOST_CHECK(non_real_conditions.size() == 1);
242 1 : BOOST_CHECK(real_conditions[0].size() == 1);
243 1 : BOOST_CHECK(is_less_application(real_conditions[0].front()));
244 1 : BOOST_CHECK(sort_bool::is_or_application(non_real_conditions[0]));
245 1 : real_conditions.clear(); non_real_conditions.clear();
246 :
247 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "(a || b) && (x == 3 || y > 4)", real_conditions, non_real_conditions);
248 1 : BOOST_CHECK(real_conditions.size() == 2);
249 1 : BOOST_CHECK(non_real_conditions.size() == 2);
250 1 : BOOST_CHECK(real_conditions[0].size() == 1);
251 1 : BOOST_CHECK(real_conditions[1].size() == 1);
252 1 : BOOST_CHECK((is_equal_to_application(real_conditions[0].front()) && is_greater_application(real_conditions[1].front())) ||
253 : (is_equal_to_application(real_conditions[1].front()) && is_greater_application(real_conditions[0].front())));
254 1 : BOOST_CHECK(non_real_conditions[0] == non_real_conditions[1]);
255 1 : real_conditions.clear(); non_real_conditions.clear();
256 :
257 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "(x == y || y < 0) && (x == 3 || y > 4)", real_conditions, non_real_conditions);
258 1 : BOOST_CHECK(real_conditions.size() == 4);
259 1 : BOOST_CHECK(non_real_conditions.size() == 4);
260 5 : for(int i = 0; i < 4; i++)
261 : {
262 4 : BOOST_CHECK(real_conditions[i].size() == 2);
263 4 : BOOST_CHECK(non_real_conditions[i] == sort_bool::true_());
264 : }
265 1 : real_conditions.clear(); non_real_conditions.clear();
266 :
267 1 : split_conditions_helper("x,y:Real, a,b,c:Bool;", "(x == y || a) && (x == 3 || b)", real_conditions, non_real_conditions);
268 1 : BOOST_CHECK(real_conditions.size() == 4);
269 1 : BOOST_CHECK(non_real_conditions.size() == 4);
270 5 : for(int i = 0; i < 4; i++)
271 : {
272 4 : std::set< data_expression > split_without_true = split_and(non_real_conditions[i]);
273 4 : split_without_true.erase(sort_bool::true_());
274 4 : BOOST_CHECK(real_conditions[i].size() + split_without_true.size() == 2);
275 4 : }
276 1 : real_conditions.clear(); non_real_conditions.clear();
277 1 : }
278 :
279 2 : BOOST_AUTO_TEST_CASE(test_main)
280 : {
281 1 : test_linear_inequality();
282 1 : test_split_conditions();
283 :
284 1 : BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3 && x>=4", false));
285 1 : BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3 && x>=2", true));
286 1 : BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<3 && x>=3", false));
287 1 : BOOST_CHECK(test_consistency_of_inequalities("x:Real;", "x<=3 && x>=3", true));
288 1 : BOOST_CHECK(test_consistency_of_inequalities("u:Real;","0 <= u && -u <= -4 && -u < 0",true));
289 1 : BOOST_CHECK(test_consistency_of_inequalities("u,t:Real;","u + -t <= 1 && -u <= -4 && t < u && -u < 0 && -t <= 0 ",true));
290 1 : BOOST_CHECK(test_consistency_of_inequalities("u,t,l:Real;","u + -t <= 1 && -u <= -4 && -u + l < 0 && -u < 0 && -t <= 0 && -l + t <= 0",true));
291 :
292 1 : BOOST_CHECK(test_application_of_Fourier_Motzkin("x,y:Real;", "y:Real;", "-y + x < 0 && y < 2", "x>=2"));
293 1 : BOOST_CHECK(test_application_of_Fourier_Motzkin("cup1,cup2,add:Real;", "add:Real;", "add <= 2 && 0 <= add && cup2 + 2 - add <= cup1 + add && 3 < cup1 + add - 2", "cup2 - cup1 >= 2", true));
294 1 : test_high_level_fourier_motzkin();
295 1 : test_high_level_fourier_motzkin_non_linear();
296 1 : }
|