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 constelm_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE constelm_test
13 : #include <boost/test/included/unit_test.hpp>
14 : #include "mcrl2/pbes/constelm.h"
15 : #include "mcrl2/pbes/detail/pbes_property_map.h"
16 : #include "mcrl2/pbes/remove_equations.h"
17 : #include "mcrl2/pbes/rewriter.h"
18 : #include "mcrl2/pbes/txt2pbes.h"
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::pbes_system;
22 :
23 : std::string t1 =
24 : "% simple test, n is constant \n"
25 : " \n"
26 : "pbes nu X(n: Nat) = \n"
27 : " X(n); \n"
28 : " \n"
29 : "init X(0); \n"
30 : ;
31 : std::string x1 = "binding_variables = X";
32 :
33 : std::string t2 =
34 : "% simple test, n is NOT constant \n"
35 : " \n"
36 : "pbes nu X(n: Nat) = \n"
37 : " X(n + 1); \n"
38 : " \n"
39 : "init X(0); \n"
40 : ;
41 : std::string x2 = "binding_variables = X(n: Nat)";
42 :
43 : std::string t3 =
44 : "% multiple parameters: n1 is constant, n2 is not \n"
45 : " \n"
46 : "pbes nu X(n1,n2: Nat) = \n"
47 : " X(n1, n2 + 1); \n"
48 : " \n"
49 : "init X(0, 1); \n"
50 : ;
51 : std::string x3 = "binding_variables = X(n2: Nat)";
52 :
53 : std::string t4 =
54 : "% conditions: n is not constant, even if conditions are enabled\n"
55 : " \n"
56 : "pbes nu X(n: Nat) = \n"
57 : " val(2 < n) || X(n + 1); \n"
58 : " \n"
59 : "init X(0); \n"
60 : ;
61 : std::string x4 = "binding_variables = X(n: Nat)";
62 :
63 : std::string t5 =
64 : "% conditions: n is constant if conditions are enabled \n"
65 : " \n"
66 : "pbes nu X(n: Nat) = \n"
67 : " val(2 < n) || X(n + 1); \n"
68 : " \n"
69 : "init X(5); \n"
70 : ;
71 : std::string x5 = "binding_variables = X";
72 :
73 : std::string t6 =
74 : "% reachability: n1 is not constant, equation Y is not reachable and should be removed \n"
75 : " \n"
76 : "pbes nu X(n1: Nat) = X(n1+1); \n"
77 : " mu Y(n2: Nat) = Y(n2+1); \n"
78 : " \n"
79 : "init X(5); \n"
80 : ;
81 : std::string x6 = "binding_variables = X(n1: Nat)";
82 :
83 : std::string t7 =
84 : "% multiple edges from one vertex, one edge invalidates the assertion of the other: no constants should be found \n"
85 : " \n"
86 : "pbes \n"
87 : " mu X1(n1,m1:Nat) = X2(n1) || X2(m1); \n"
88 : " mu X2(n2:Nat) = X1(n2,n2); \n"
89 : "init \n"
90 : " X1(2,1); \n"
91 : ;
92 : std::string x7 = "binding_variables = X1(n1,m1: Nat), X2(n2: Nat)";
93 :
94 : std::string t8 =
95 : "% conditions: parameters b,c and d will always be removed, with conditions on, parameter \n"
96 : "% n will NOT be removed. changing b,c or d to false or n to a bigger number \n"
97 : "% then 5 WILL result in the removal of n \n"
98 : " \n"
99 : "pbes nu X(b,c,d:Bool, n:Nat) = \n"
100 : " val(b) || ( val(c) && ( val(d) && (val(n > 5) || X(b,c,d,n+1)))); \n"
101 : " \n"
102 : "init \n"
103 : "X(false,true,true,5); \n"
104 : ;
105 : std::string x8 = "binding_variables = X(n: Nat)";
106 :
107 : std::string t9 =
108 : "% conditions: universal quantification which can be solved, n1 and n2 are \n"
109 : "% constants if conditions are enabled \n"
110 : " \n"
111 : "pbes mu X(n1,n2:Nat) = \n"
112 : " forall m:Nat. (val(n1>n2) && X(n1+1,n2+1)); \n"
113 : " \n"
114 : "init X(1,2); \n"
115 : ;
116 : std::string x9 = "binding_variables = X";
117 :
118 : std::string t10 =
119 : "% conditions: existential quantification which can be solved, n1 and n2 \n"
120 : "% are constants if conditions are enabled \n"
121 : " \n"
122 : "pbes mu X(n1,n2:Nat) = \n"
123 : " exists m:Nat. (val(n1>n2) && X(n1+1,n2+1)); \n"
124 : " \n"
125 : "init X(1,2); \n"
126 : ;
127 : std::string x10 = "binding_variables = X";
128 :
129 : std::string t11 =
130 : "pbes mu X(n1,n2:Nat) = \n"
131 : " forall m:Nat. (val(m>n2) && X(n1+1,n2+1)); \n"
132 : " \n"
133 : "init X(1,2); \n"
134 : ;
135 : std::string x11 = "binding_variables = X";
136 :
137 : std::string t12 =
138 : "% example 4.2.1 from \"Tools for PBES\" report \n"
139 : "% constants without conditions: o4, n2, n4, o4 \n"
140 : "% constants with conditions: everything (equations X1,X2,X3 and X4 are removed) \n"
141 : " \n"
142 : "pbes \n"
143 : " mu X1(n1,m1,o1,p1:Nat) = (val(n1<m1) || X2(o1,p1)) && X3(n1) && X1(n1,m1,4,p1); \n"
144 : " mu X2(n2,m2:Nat) = X5(n2,m2) || X5(m2,n2); \n"
145 : " nu X3(n3:Nat) = val(n3<3) || X1(n3,n3,4,n3+1); \n"
146 : " nu X4(n4,m4,o4:Nat) = val(n4 <= m4+o4) || (X3(n4) && X4(n4,m4+1,n4)); \n"
147 : " mu X5(n5,m5:Nat) = val(n5>m5) || X3(n5); \n"
148 : " \n"
149 : "init \n"
150 : " X4(0,0,0); \n"
151 : ;
152 : std::string x12 = "binding_variables = X1(n1,m1,p1: Nat), X2(m2: Nat), X3(n3: Nat), X4(m4: Nat), X5(n5,m5: Nat)";
153 :
154 : std::string t13 =
155 : "pbes nu X = \n"
156 : " Y(true); \n"
157 : " mu Y(b: Bool) = \n"
158 : " X; \n"
159 : " \n"
160 : "init X; \n"
161 : ;
162 : std::string x13 = "binding_variables = X, Y";
163 :
164 : std::string t14 =
165 : "pbes nu X(m:Nat) = \n"
166 : " forall n:Nat . X(n); \n"
167 : " \n"
168 : "init X(0); \n"
169 : ;
170 : std::string x14 = "binding_variables = X(m: Nat)";
171 :
172 : std::string t15 =
173 : "pbes \n"
174 : "nu X0(n:Nat) = X1; \n"
175 : "mu X1 = X0(0) || X1; \n"
176 : " \n"
177 : "init X0(0); \n"
178 : ;
179 : std::string x15 = "binding_variables = X0, X1";
180 :
181 : std::string t16 =
182 : "pbes \n"
183 : " nu X(n:Nat) = Y && X(n); \n"
184 : " mu Y = Z; \n"
185 : " nu Z = Y; \n"
186 : " \n"
187 : " init X(0); \n"
188 : ;
189 : std::string x16 = "binding_variables = X, Y, Z";
190 :
191 : std::string t17 =
192 : "sort D = struct d1 | d2 | d3 | d4;\n"
193 : "pbes nu X1 =\n"
194 : " X(2);\n"
195 : " mu X(s3_X: Pos) =\n"
196 : " val(s3_X == 4) || val(s3_X == 2) && X(3) || val(s3_X == 2) && X(4) || val(s3_X == 3) && X(1) || val(s3_X == 4) && X(1);\n"
197 : "init X1;\n";
198 :
199 : std::string x17 = "binding_variables = X1, X(s3_X: Pos)";
200 :
201 : std::string t18 =
202 : "% conditions: quantifications which cannot be solved, n1 and n2 are *not* \n"
203 : "% constants even if conditions are enabled. \n"
204 : " \n"
205 : "pbes mu X(n1,n2:Nat) = \n"
206 : " forall m1:Nat. exists m2:Nat. (val(m2 > n2 + m1) && X(n1+1,n2+1)); \n"
207 : " \n"
208 : "init X(1,2); \n"
209 : ;
210 :
211 : std::string x18 = "binding_variables = X(n1,n2: Nat)";
212 :
213 18 : void test_pbes(const std::string& pbes_spec, const std::string& expected_result, bool compute_conditions, bool remove_equations = true)
214 : {
215 : typedef simplify_data_rewriter<data::rewriter> my_pbes_rewriter;
216 :
217 18 : pbes p = txt2pbes(pbes_spec);
218 18 : pbes q = p;
219 :
220 : // data rewriter
221 18 : data::rewriter datar(q.data());
222 :
223 : // pbes rewriter
224 18 : my_pbes_rewriter pbesr(datar);
225 :
226 : // constelm algorithm
227 18 : pbes_constelm_algorithm<data::rewriter, my_pbes_rewriter> algorithm(datar, pbesr);
228 :
229 : // run the algorithm
230 18 : algorithm.run(q, compute_conditions);
231 18 : if (remove_equations)
232 : {
233 18 : remove_unreachable_variables(q);
234 : }
235 18 : BOOST_CHECK(q.is_well_typed());
236 18 : std::cout << "\n--- q ---\n" << pbes_system::pp(q) << std::endl;
237 :
238 18 : pbes_system::detail::pbes_property_map info1(q);
239 18 : pbes_system::detail::pbes_property_map info2(expected_result);
240 18 : std::string diff = info1.compare(info2);
241 18 : if (!diff.empty())
242 : {
243 0 : std::cerr << "\n------ FAILED TEST ------" << std::endl;
244 0 : std::cout << pbes_spec << std::endl;
245 0 : std::cerr << "--- expected result" << std::endl;
246 0 : std::cerr << expected_result << std::endl;
247 0 : std::cerr << "--- found result" << std::endl;
248 0 : std::cerr << info1.to_string() << std::endl;
249 0 : std::cerr << "--- differences" << std::endl;
250 0 : std::cerr << diff << std::endl;
251 : }
252 18 : BOOST_CHECK(diff.empty());
253 :
254 18 : }
255 :
256 2 : BOOST_AUTO_TEST_CASE(test_constelm)
257 : {
258 1 : test_pbes(t1 , x1 , false);
259 1 : test_pbes(t2 , x2 , false);
260 1 : test_pbes(t3 , x3 , false);
261 1 : test_pbes(t4 , x4 , true);
262 1 : test_pbes(t5 , x5 , true);
263 1 : test_pbes(t6 , x6 , false);
264 1 : test_pbes(t7 , x7 , false);
265 1 : test_pbes(t8 , x8 , true);
266 1 : test_pbes(t9 , x9 , true);
267 1 : test_pbes(t10, x10, true);
268 1 : test_pbes(t11, x11, true);
269 1 : test_pbes(t12, x12, false);
270 1 : test_pbes(t13, x13, false);
271 1 : test_pbes(t14, x14, false);
272 1 : test_pbes(t15, x15, false);
273 1 : test_pbes(t16, x16, true);
274 1 : test_pbes(t17, x17, false);
275 :
276 1 : data::detail::set_enumerator_iteration_limit(50); // This final test requires 50*50 enumerations and the default limit of 1000 takes too long.
277 1 : test_pbes(t18, x18, true);
278 1 : }
|
