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 rename_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define MCRL2_STATE_FORMULA_BUILDER_DEBUG
13 :
14 : #define BOOST_TEST_MODULE state_formula
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : #include "mcrl2/lps/linearise.h"
18 : #include "mcrl2/modal_formula/count_fixpoints.h"
19 : #include "mcrl2/modal_formula/maximal_closed_subformula.h"
20 : #include "mcrl2/modal_formula/parse.h"
21 : #include "mcrl2/modal_formula/preprocess_state_formula.h"
22 :
23 : using namespace mcrl2;
24 : using namespace mcrl2::core;
25 : using namespace mcrl2::lps;
26 : using namespace mcrl2::lps::detail;
27 : using namespace mcrl2::state_formulas;
28 :
29 2 : BOOST_AUTO_TEST_CASE(test_rename)
30 : {
31 : const std::string SPECIFICATION =
32 : "act a:Nat; \n"
33 : " \n"
34 : "map smaller: Nat#Nat -> Bool; \n"
35 : " \n"
36 : "var x,y : Nat; \n"
37 : " \n"
38 : "eqn smaller(x,y) = x < y; \n"
39 : " \n"
40 : "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n"
41 : " \n"
42 1 : "init P(0); \n"
43 : ;
44 :
45 : using mcrl2::state_formulas::pp;
46 1 : specification lpsspec = remove_stochastic_operators(linearise(SPECIFICATION));
47 :
48 2 : state_formula formula = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec, false);
49 :
50 1 : data::set_identifier_generator generator;
51 1 : generator.add_identifiers(lps::find_identifiers(lpsspec));
52 1 : formula = rename_predicate_variables(formula, generator);
53 :
54 1 : std::cout << "pp(formula) == " << pp(formula) << std::endl;
55 1 : BOOST_CHECK(pp(formula) == "(mu X1. X1) && (mu X. X)" || pp(formula) == "(mu X. X) && (mu X1. X1)");
56 :
57 1 : generator = data::set_identifier_generator();
58 1 : generator.add_identifiers(lps::find_identifiers(lpsspec));
59 1 : parse_state_formula_options options;
60 1 : options.check_monotonicity = false;
61 1 : options.resolve_name_clashes = false;
62 1 : formula = parse_state_formula("mu X. mu X. X", lpsspec, false, options);
63 1 : std::cout << "formula: " << pp(formula) << std::endl;
64 1 : formula = rename_predicate_variables(formula, generator);
65 1 : std::cout << "formula: " << pp(formula) << std::endl;
66 1 : BOOST_CHECK_EQUAL(pp(formula), "mu X. mu X1. X1");
67 1 : }
68 :
69 2 : BOOST_AUTO_TEST_CASE(test_normalize)
70 : {
71 2 : state_formula x = state_formulas::variable(identifier_string("X"), data::data_expression_list());
72 2 : state_formula y = state_formulas::variable(identifier_string("Y"), data::data_expression_list());
73 1 : state_formula f;
74 1 : state_formula f1;
75 1 : state_formula f2;
76 :
77 1 : f = imp(not_(x), y);
78 1 : f1 = normalize(f);
79 1 : f2 = or_(x, y);
80 1 : std::cout << "f = " << state_formulas::pp(f) << std::endl;
81 1 : std::cout << "f1 = " << state_formulas::pp(f1) << std::endl;
82 1 : std::cout << "f2 = " << state_formulas::pp(f2) << std::endl;
83 1 : BOOST_CHECK_EQUAL(f1, f2);
84 :
85 1 : f = not_(and_(not_(x), not_(y)));
86 1 : f1 = normalize(f);
87 1 : f2 = or_(x, y);
88 1 : std::cout << "f = " << state_formulas::pp(f) << std::endl;
89 1 : std::cout << "f1 = " << state_formulas::pp(f1) << std::endl;
90 1 : std::cout << "f2 = " << state_formulas::pp(f2) << std::endl;
91 1 : BOOST_CHECK_EQUAL(f1, f2);
92 1 : }
93 :
94 2 : BOOST_AUTO_TEST_CASE(test_type_checking)
95 : {
96 2 : specification lpsspec = remove_stochastic_operators(linearise(
97 : "sort CPU = struct p1;"
98 : "sort CPUs = Set(CPU);"
99 1 : "init delta;"));
100 :
101 2 : state_formula formula = parse_state_formula("nu X (P : CPUs = {p1}) . val(P != {})", lpsspec, false);
102 1 : }
103 :
104 2 : BOOST_AUTO_TEST_CASE(test_type_checking_conversion_of_arguments)
105 : {
106 2 : specification lpsspec = remove_stochastic_operators(linearise(
107 : "sort B = struct d;"
108 : "act a: List(B);"
109 : "init a([d]);"
110 1 : ));
111 :
112 2 : state_formula formula = parse_state_formula("<a([d])>true", lpsspec, false);
113 :
114 1 : BOOST_CHECK(is_may(formula));
115 1 : const state_formulas::may& f = atermpp::down_cast<state_formulas::may>(formula);
116 1 : BOOST_CHECK(is_regular_formula(f.formula()));
117 1 : }
118 :
119 :
120 : static inline
121 1 : state_formula negate_variable(const variable& x)
122 : {
123 1 : return state_formulas::not_(x);
124 : }
125 :
126 2 : BOOST_AUTO_TEST_CASE(test_not)
127 : {
128 1 : data::data_expression_list args;
129 2 : variable v(core::identifier_string("v"), args);
130 2 : state_formula s = not_(v);
131 1 : BOOST_CHECK(is_not(s));
132 :
133 1 : state_formula t = negate_variable(v);
134 1 : BOOST_CHECK_EQUAL(s, t);
135 :
136 : // The following is expected to trigger an assertion failure
137 : // aterm_appl a = v;
138 : // state_formula t = not_(a);
139 1 : }
140 :
141 : // test case supplied by Jan Friso, 4-1-2011
142 2 : BOOST_AUTO_TEST_CASE(test_parse)
143 : {
144 : std::string spec_text =
145 : "act a:Nat; \n"
146 1 : "init a(1); \n"
147 : ;
148 :
149 1 : std::string formula_text = "<a(1)>true";
150 :
151 1 : lps::specification lpsspec = remove_stochastic_operators(lps::linearise(spec_text));
152 1 : state_formulas::state_formula f = state_formulas::parse_state_formula(formula_text, lpsspec, false);
153 :
154 1 : std::cerr << "--- f ---\n" << state_formulas::pp(f) << std::endl;
155 1 : std::set<core::identifier_string> ids = state_formulas::find_identifiers(f);
156 1 : BOOST_CHECK(ids.find(core::identifier_string("1")) == ids.end());
157 1 : BOOST_CHECK(ids.find(core::identifier_string("@c1")) != ids.end());
158 1 : }
159 :
160 2 : BOOST_AUTO_TEST_CASE(test_count_fixpoints)
161 : {
162 1 : state_formula formula;
163 1 : specification lpsspec;
164 :
165 1 : formula = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec, false);
166 1 : BOOST_CHECK_EQUAL(count_fixpoints(formula), 2u);
167 :
168 1 : formula = parse_state_formula("exists b:Bool. (mu X. X) || forall b:Bool. (nu X. mu Y. (X || Y))", lpsspec, false);
169 1 : BOOST_CHECK_EQUAL(count_fixpoints(formula), 3u);
170 1 : }
171 :
172 : // Test case for bug #1094.
173 : // This is expected to fail, due to the occurrence of an unbound variable Y
174 : // in the formula.
175 2 : BOOST_AUTO_TEST_CASE(test_1094)
176 : {
177 : const std::string SPEC =
178 : "act a,b,c,d;\n"
179 : "\n"
180 : "proc P(s3_X: Pos) =\n"
181 : " (s3_X == 1) ->\n"
182 : " a .\n"
183 : " P(s3_X = 2)\n"
184 : " + (s3_X == 2) ->\n"
185 : " b .\n"
186 : " P(s3_X = 3)\n"
187 : " + (s3_X == 3) ->\n"
188 : " a .\n"
189 : " P(s3_X = 4)\n"
190 : " + (s3_X == 3) ->\n"
191 : " a .\n"
192 : " P(s3_X = 5)\n"
193 : " + (s3_X == 4) ->\n"
194 : " c .\n"
195 : " P(s3_X = 1)\n"
196 : " + (s3_X == 5) ->\n"
197 : " d .\n"
198 : " P(s3_X = 1)\n"
199 : " + delta;\n"
200 : "\n"
201 1 : "init P(1);\n"
202 : ;
203 1 : specification s(parse_linear_process_specification(SPEC));
204 :
205 2 : const std::string FORMULA = "[true*]([b] nu X. mu X.( [!c]X && [!c]Y))";
206 :
207 2 : BOOST_CHECK_THROW(parse_state_formula(FORMULA, s, false), mcrl2::runtime_error);
208 1 : }
209 :
210 : inline
211 5 : state_formula sigma(const state_formula& x)
212 : {
213 10 : variable X("X", data::data_expression_list());
214 15 : return x == X ? false_() : x;
215 5 : }
216 :
217 2 : BOOST_AUTO_TEST_CASE(test_replace_state_formulas)
218 : {
219 1 : specification lpsspec;
220 2 : state_formula f = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec, false);
221 1 : state_formula result = replace_state_formulas(f, sigma);
222 2 : state_formula expected_result = parse_state_formula("(mu X. false) && (mu X. false)", lpsspec, false);
223 1 : if (!(result == expected_result))
224 : {
225 0 : std::cout << "error: " << state_formulas::pp(result) << " != " << state_formulas::pp(expected_result) << std::endl;
226 : }
227 1 : BOOST_CHECK(result == expected_result);
228 1 : }
229 :
230 2 : BOOST_AUTO_TEST_CASE(test_find_state_variables)
231 : {
232 1 : specification lpsspec;
233 :
234 2 : state_formula f = parse_state_formula("(mu X. nu Y. true && mu Z. X && Z)", lpsspec, false);
235 1 : std::set<state_formulas::variable> v = state_formulas::find_state_variables(f);
236 1 : BOOST_CHECK(v.size() == 2);
237 :
238 1 : f = parse_state_formula("mu X. nu Y. (true && mu Z. (X && Y || Z))", lpsspec, false);
239 1 : v = find_state_variables(f);
240 1 : BOOST_CHECK(v.size() == 3);
241 :
242 2 : state_formulas::variable X("X", data::data_expression_list());
243 2 : state_formulas::variable Y("Y", data::data_expression_list());
244 2 : state_formulas::variable Z("Z", data::data_expression_list());
245 1 : state_formula phi = state_formulas::and_(X, Y);
246 1 : v = find_state_variables(phi);
247 1 : BOOST_CHECK(v.size() == 2);
248 1 : v = find_free_state_variables(phi);
249 1 : BOOST_CHECK(v.size() == 2);
250 2 : state_formula psi = state_formulas::mu("X", data::assignment_list(), phi);
251 1 : v = find_state_variables(psi);
252 1 : BOOST_CHECK(v.size() == 2);
253 1 : v = find_free_state_variables(psi);
254 1 : BOOST_CHECK(v.size() == 1);
255 1 : }
256 :
257 : inline
258 4 : bool contains(const std::set<state_formulas::state_formula>& v, const std::string& s)
259 : {
260 6 : for (const state_formulas::state_formula& f: v)
261 : {
262 6 : if (state_formulas::pp(f) == s)
263 : {
264 4 : return true;
265 : }
266 : }
267 0 : return false;
268 : }
269 :
270 2 : BOOST_AUTO_TEST_CASE(test_maximal_closed_subformulas)
271 : {
272 1 : mcrl2::log::logger::set_reporting_level(mcrl2::log::debug);
273 :
274 1 : specification lpsspec;
275 2 : state_formula f = parse_state_formula("(mu X. nu Y. true && mu Z. X && Z)", lpsspec, false);
276 1 : std::set<state_formulas::state_formula> v = maximal_closed_subformulas(f);
277 1 : BOOST_CHECK(v.size() == 1);
278 :
279 1 : f = parse_state_formula("exists b: Bool. forall c: Bool. val(b) && (val(c) || true) && false", lpsspec, false);
280 1 : v = maximal_closed_subformulas(f);
281 1 : BOOST_CHECK(v.size() == 1);
282 :
283 1 : state_formula g = exists(f).body();
284 1 : std::cout << "g = " << state_formulas::pp(g) << std::endl;
285 1 : v = maximal_closed_subformulas(g);
286 3 : for (const state_formula& f: v)
287 : {
288 2 : std::cout << "element " << f << std::endl;
289 : }
290 1 : BOOST_CHECK(v.size() == 2);
291 1 : BOOST_CHECK(contains(v, "true"));
292 1 : BOOST_CHECK(contains(v, "false"));
293 :
294 1 : state_formula h = forall(g).body();
295 1 : v = maximal_closed_subformulas(h);
296 1 : std::cout << "h = " << state_formulas::pp(h) << std::endl;
297 3 : for (const state_formula& f: v)
298 : {
299 2 : std::cout << "element " << f << std::endl;
300 : }
301 1 : BOOST_CHECK(v.size() == 2);
302 1 : BOOST_CHECK(contains(v, "true"));
303 1 : BOOST_CHECK(contains(v, "false"));
304 1 : }
305 :
306 4 : void test_has_unscoped_modal_formulas(const std::string& text, lps::specification& lpsspec, bool expected_result)
307 : {
308 4 : state_formula x = parse_state_formula(text, lpsspec, false);
309 4 : bool result = state_formulas::detail::has_unscoped_modal_formulas(x);
310 4 : if (result != expected_result)
311 : {
312 0 : std::cout << "--- has_unscoped_modal_formulas failure ---" << std::endl;
313 0 : std::cout << "formula = " << text << std::endl;
314 0 : std::cout << "result = " << result << std::endl;
315 : }
316 4 : BOOST_CHECK_EQUAL(result, expected_result);
317 4 : }
318 :
319 2 : BOOST_AUTO_TEST_CASE(has_unscoped_modal_formulas_test)
320 : {
321 : const std::string text =
322 : "act a, b, c; \n"
323 : " \n"
324 : "proc P = delta; \n"
325 : " \n"
326 1 : "init P; \n"
327 : ;
328 1 : lps::specification lpsspec = lps::parse_linear_process_specification(text);
329 :
330 1 : test_has_unscoped_modal_formulas("[a]true", lpsspec, true);
331 1 : test_has_unscoped_modal_formulas("mu X. X", lpsspec, false);
332 1 : test_has_unscoped_modal_formulas("true => [a]true", lpsspec, true);
333 1 : test_has_unscoped_modal_formulas("true => mu X. [a]<b>true", lpsspec, false);
334 1 : }
335 :
336 4 : void test_preprocess_nested_modal_operators(const std::string& text, lps::specification& lpsspec, const std::string& expected_result_text)
337 : {
338 4 : state_formula x = parse_state_formula(text, lpsspec, false);
339 4 : state_formula expected_result = parse_state_formula(expected_result_text, lpsspec, false);
340 4 : state_formula result = state_formulas::preprocess_nested_modal_operators(x);
341 4 : if (result != expected_result)
342 : {
343 0 : std::cout << "--- preprocess_nested_modal_operators failure ---" << std::endl;
344 0 : std::cout << "formula = " << text << std::endl;
345 0 : std::cout << "result = " << state_formulas::pp(result) << std::endl;
346 0 : std::cout << "expected result = " << expected_result_text << std::endl;
347 : }
348 4 : BOOST_CHECK_EQUAL(result, expected_result);
349 4 : }
350 :
351 2 : BOOST_AUTO_TEST_CASE(preprocess_nested_modal_operators_test)
352 : {
353 : const std::string text =
354 : "act a, b, c; \n"
355 : " \n"
356 : "proc P = delta; \n"
357 : " \n"
358 1 : "init P; \n"
359 : ;
360 1 : lps::specification lpsspec = lps::parse_linear_process_specification(text);
361 :
362 1 : test_preprocess_nested_modal_operators("[a]true", lpsspec, "[a]true");
363 1 : test_preprocess_nested_modal_operators("[a]<b>true", lpsspec, "[a]mu X. <b>true");
364 1 : test_preprocess_nested_modal_operators("true && <a><a>true", lpsspec, "true && <a>mu X. <a>true");
365 1 : test_preprocess_nested_modal_operators("true => mu X. [a]<b>true", lpsspec, "true => mu X. [a]mu X1. <b>true");
366 1 : }
367 :
368 2 : BOOST_AUTO_TEST_CASE(parse_modal_formula_test)
369 : {
370 : const std::string text =
371 : "act a, b, c; \n"
372 : " \n"
373 : "proc P = delta; \n"
374 : " \n"
375 1 : "init P; \n"
376 : ;
377 1 : lps::specification lpsspec = lps::parse_linear_process_specification(text);
378 :
379 1 : const std::string formula_text = "nu X(n: Nat = 0, b: Bool = false). X(n, b)";
380 1 : state_formula x = parse_state_formula(formula_text, lpsspec, false);
381 1 : std::string s = state_formulas::pp(x);
382 1 : BOOST_CHECK_EQUAL(s, formula_text);
383 1 : }
384 :
385 2 : BOOST_AUTO_TEST_CASE(check_parameter_name_clashes_test)
386 : {
387 : const std::string text =
388 : "act a, b, c; \n"
389 : " \n"
390 : "proc P = delta; \n"
391 : " \n"
392 1 : "init P; \n"
393 : ;
394 1 : lps::specification lpsspec = lps::parse_linear_process_specification(text);
395 :
396 1 : BOOST_CHECK(has_data_variable_name_clashes(parse_state_formula("nu X(n: Nat = 0). mu Y(n: Nat = 1). val(n == 0)", lpsspec, false)));
397 1 : BOOST_CHECK(!has_data_variable_name_clashes(parse_state_formula("nu X(n: Nat = 0). mu Y(m: Nat = 1). val(n == 0)", lpsspec, false)));
398 1 : }
399 :
400 2 : BOOST_AUTO_TEST_CASE(parse_state_formula_specification_test)
401 : {
402 : const std::string text =
403 : "sort S; \n"
404 : "cons s0: S; \n"
405 : "act a: S; \n"
406 1 : "form forall s: S. [a(s)]true; \n"
407 : ;
408 1 : state_formula_specification x = parse_state_formula_specification(text, false);
409 1 : std::string text1 = state_formulas::pp(x);
410 1 : std::cout << text1 << std::endl;
411 1 : BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
412 1 : }
413 :
414 2 : BOOST_AUTO_TEST_CASE(parse_state_formula_with_supremum_specification_test)
415 : {
416 : const std::string text =
417 : "sort S; \n"
418 : "cons s0: S; \n"
419 : "act a: S; \n"
420 1 : "form sup s: S. [a(s)]true; \n"
421 : ;
422 1 : state_formula_specification x = parse_state_formula_specification(text, true);
423 1 : std::string text1 = state_formulas::pp(x);
424 1 : std::cout << text1 << std::endl;
425 1 : BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
426 1 : }
427 :
428 2 : BOOST_AUTO_TEST_CASE(parse_state_formula_with_sum_specification_test)
429 : {
430 : const std::string text =
431 : "sort S; \n"
432 : "cons s0: S; \n"
433 : "act a: S; \n"
434 1 : "form sum s: S. val(1 / 2) * [a(s)]false; \n"
435 : ;
436 1 : state_formula_specification x = parse_state_formula_specification(text, true);
437 1 : std::string text1 = state_formulas::pp(x);
438 1 : std::cout << text1 << std::endl;
439 1 : BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
440 1 : }
441 :
442 2 : BOOST_AUTO_TEST_CASE(parse_state_formula_with_const_multiply_alt_specification_test)
443 : {
444 : const std::string text =
445 : "sort S; \n"
446 : "cons s0: S; \n"
447 : "act a: S; \n"
448 1 : "form inf s: S. [a(s)]false * val(1/5); \n"
449 : ;
450 1 : state_formula_specification x = parse_state_formula_specification(text, true);
451 1 : std::string text1 = state_formulas::pp(x);
452 1 : std::cout << text1 << std::endl;
453 1 : BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
454 1 : }
455 :
456 2 : BOOST_AUTO_TEST_CASE(parse_state_formula_with_infimum_specification_test)
457 : {
458 : const std::string text =
459 1 : "form inf n: Nat. val(n); \n"
460 : ;
461 1 : state_formula_specification x = parse_state_formula_specification(text, true);
462 1 : std::string text1 = state_formulas::pp(x);
463 1 : std::cout << text1 << std::endl;
464 1 : BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
465 1 : }
|
