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 normalize_test.cpp
10 : /// \brief Test for normalization functions.
11 :
12 : #define BOOST_TEST_MODULE normalize_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/modal_formula/parse.h"
16 : #include "mcrl2/pbes/detail/normalize_and_or.h"
17 : #include "mcrl2/pbes/lps2pbes.h"
18 : #include "mcrl2/pbes/normalize.h"
19 : #include "mcrl2/pbes/detail/parse.h"
20 : #include "mcrl2/pbes/rewriter.h"
21 : #include "mcrl2/utilities/detail/test_operation.h"
22 :
23 : using namespace mcrl2;
24 : using namespace mcrl2::pbes_system;
25 :
26 2 : BOOST_AUTO_TEST_CASE(test_normalize1)
27 : {
28 2 : pbes_expression x = propositional_variable_instantiation{core::identifier_string("X"), data::data_expression_list()};
29 2 : pbes_expression y = propositional_variable_instantiation{core::identifier_string("Y"), data::data_expression_list()};
30 2 : pbes_expression z = propositional_variable_instantiation{core::identifier_string("Z"), data::data_expression_list()};
31 1 : pbes_expression f;
32 1 : pbes_expression f1;
33 1 : pbes_expression f2;
34 :
35 1 : f = not_(x);
36 1 : f = not_(f); // N.B. not_(not_(x)) does not work!
37 1 : f1 = pbes_system::normalize(f);
38 1 : f2 = x;
39 1 : std::cout << "f = " << f << std::endl;
40 1 : std::cout << "f1 = " << f1 << std::endl;
41 1 : std::cout << "f2 = " << f2 << std::endl;
42 1 : BOOST_CHECK(f1 == f2);
43 :
44 1 : f = imp(not_(x), y);
45 1 : f1 = pbes_system::normalize(f);
46 1 : f2 = or_(x, y);
47 1 : std::cout << "f = " << f << std::endl;
48 1 : std::cout << "f1 = " << f1 << std::endl;
49 1 : std::cout << "f2 = " << f2 << std::endl;
50 1 : BOOST_CHECK(f1 == f2);
51 :
52 1 : f = not_(and_(not_(x), not_(y)));
53 1 : f1 = pbes_system::normalize(f);
54 1 : f2 = or_(x, y);
55 1 : std::cout << "f = " << f << std::endl;
56 1 : std::cout << "f1 = " << f1 << std::endl;
57 1 : std::cout << "f2 = " << f2 << std::endl;
58 1 : BOOST_CHECK(f1 == f2);
59 :
60 1 : f = imp(and_(not_(x), not_(y)), z);
61 1 : f1 = pbes_system::normalize(f);
62 1 : f2 = or_(or_(x, y), z);
63 1 : std::cout << "f = " << f << std::endl;
64 1 : std::cout << "f1 = " << f1 << std::endl;
65 1 : std::cout << "f2 = " << f2 << std::endl;
66 1 : BOOST_CHECK(f1 == f2);
67 :
68 1 : x = data::variable("x", data::bool_());
69 1 : y = data::variable("y", data::bool_());
70 1 : z = data::variable("z", data::bool_());
71 1 : const data::data_expression& x1 = atermpp::down_cast<data::data_expression>(x);
72 1 : const data::data_expression& y1 = atermpp::down_cast<data::data_expression>(y);
73 :
74 1 : f = not_(x);
75 1 : f1 = pbes_system::normalize(f);
76 1 : f2 = data::not_(x1);
77 1 : std::cout << "f = " << f << std::endl;
78 1 : std::cout << "f1 = " << f1 << std::endl;
79 1 : std::cout << "f2 = " << f2 << std::endl;
80 1 : BOOST_CHECK(f1 == f2);
81 :
82 1 : f = imp(and_(x, y), z);
83 1 : f1 = pbes_system::normalize(f);
84 1 : f2 = or_(or_(data::not_(x1), data::not_(y1)), z);
85 1 : std::cout << "f = " << f << std::endl;
86 1 : std::cout << "f1 = " << f1 << std::endl;
87 1 : std::cout << "f2 = " << f2 << std::endl;
88 1 : BOOST_CHECK(f1 == f2);
89 :
90 1 : pbes_expression T = true_();
91 1 : pbes_expression F = false_();
92 1 : x = pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESImp(), T, F));
93 1 : y = pbes_system::normalize(x);
94 1 : std::cout << "x = " << x << std::endl;
95 1 : std::cout << "y = " << y << std::endl;
96 :
97 3 : data::variable_list ab = { data::variable("s", data::basic_sort("S")) };
98 1 : x = propositional_variable_instantiation{core::identifier_string("X"), data::data_expression_list()};
99 1 : y = and_(x, imp(pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESAnd(), false_(), false_())), false_()));
100 1 : z = pbes_system::normalize(y);
101 1 : std::cout << "y = " << y << std::endl;
102 1 : std::cout << "z = " << z << std::endl;
103 1 : }
104 :
105 2 : BOOST_AUTO_TEST_CASE(test_normalize2)
106 : {
107 : // test case from Aad Mathijssen, 2/11/2008
108 2 : lps::specification spec=remove_stochastic_operators(lps::linearise("init tau + tau;"));
109 2 : state_formulas::state_formula formula = state_formulas::parse_state_formula("nu X. [true]X", spec, false);
110 1 : bool timed = false;
111 1 : pbes_system::pbes p = pbes_system::lps2pbes(spec, formula, timed);
112 1 : pbes_system::normalize(p);
113 1 : }
114 :
115 2 : BOOST_AUTO_TEST_CASE(test_normalize3)
116 : {
117 : // test case from Aad Mathijssen, 1-4-2008
118 2 : lps::specification spec=remove_stochastic_operators(lps::linearise(
119 : "proc P = tau.P;\n"
120 1 : "init P; \n"));
121 2 : state_formulas::state_formula formula = state_formulas::parse_state_formula("![true*]<true>true", spec, false);
122 1 : bool timed = false;
123 1 : pbes_system::pbes p = pbes_system::lps2pbes(spec, formula, timed);
124 1 : pbes_system::normalize(p);
125 1 : }
126 :
127 : const std::string VARIABLE_SPECIFICATION =
128 : "datavar \n"
129 : " b: Bool; \n"
130 : " b1: Bool; \n"
131 : " b2: Bool; \n"
132 : " b3: Bool; \n"
133 : " \n"
134 : " n: Nat; \n"
135 : " n1: Nat; \n"
136 : " n2: Nat; \n"
137 : " n3: Nat; \n"
138 : " \n"
139 : " p: Pos; \n"
140 : " p1: Pos; \n"
141 : " p2: Pos; \n"
142 : " p3: Pos; \n"
143 : " \n"
144 : "predvar \n"
145 : " X; \n"
146 : " Y: Nat; \n"
147 : " Z: Bool, Pos; \n"
148 : ;
149 :
150 : inline
151 : pbes_system::pbes_expression expr(const std::string& text)
152 : {
153 : return pbes_system::parse_pbes_expression(text, VARIABLE_SPECIFICATION);
154 : }
155 :
156 : inline
157 6 : pbes_expression parse(const std::string& expr)
158 : {
159 : std::string var_decl =
160 : "datavar \n"
161 : " m: Nat; \n"
162 : " n: Nat; \n"
163 : " \n"
164 : "predvar \n"
165 : " X; \n"
166 : " Y; \n"
167 6 : " Z; \n"
168 : ;
169 :
170 6 : std::string data_spec = "";
171 12 : return pbes_system::parse_pbes_expression(expr, var_decl, data_spec);
172 6 : }
173 :
174 : inline
175 6 : pbes_expression norm(const pbes_expression& x)
176 : {
177 6 : return pbes_system::detail::normalize_and_or(x);
178 : }
179 :
180 : inline
181 3 : void test_normalize_and_or_equality(const std::string& expr1, const std::string& expr2)
182 : {
183 3 : BOOST_CHECK(utilities::detail::test_operation(
184 : expr1,
185 : expr2,
186 : parse,
187 : std::equal_to<pbes_expression>(),
188 : norm,
189 : "normalize_and_or",
190 : norm,
191 : "normalize_and_or"
192 : ));
193 3 : }
194 :
195 2 : BOOST_AUTO_TEST_CASE(test_normalize_and_or)
196 : {
197 1 : test_normalize_and_or_equality("X && Y", "Y && X");
198 1 : test_normalize_and_or_equality("X && X && Y", "X && Y && X");
199 1 : test_normalize_and_or_equality("X && X && Y", "Y && X && X");
200 1 : }
|
