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 stategraph_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE stategraph_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/pbes/detail/stategraph_global_reset_variables.h"
16 : #include "mcrl2/pbes/detail/stategraph_local_reset_variables.h"
17 : #include "mcrl2/pbes/significant_variables.h"
18 : #include "mcrl2/pbes/txt2pbes.h"
19 : #include "mcrl2/utilities/detail/split.h"
20 :
21 : using namespace mcrl2;
22 : using namespace pbes_system;
23 :
24 : // prints the names of the variables (sorted alphabetically)
25 4 : std::string print_set(const std::set<data::variable>& variables)
26 : {
27 4 : std::ostringstream out;
28 4 : std::set<std::string> s;
29 7 : for (const data::variable& v: variables)
30 : {
31 3 : s.insert(std::string(v.name()));
32 : }
33 4 : out << "{";
34 7 : for (auto i = s.begin(); i != s.end(); ++i)
35 : {
36 3 : if (i != s.begin())
37 : {
38 0 : out << ", ";
39 : }
40 3 : out << *i;
41 : }
42 4 : out << "}";
43 8 : return out.str();
44 4 : }
45 :
46 4 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
47 : {
48 4 : if (result != expected_result)
49 : {
50 0 : std::cout << "--- failure in " << title << " ---" << std::endl;
51 0 : std::cout << "expression = " << expression << std::endl;
52 0 : std::cout << "result = " << result << std::endl;
53 0 : std::cout << "expected result = " << expected_result << std::endl;
54 0 : BOOST_CHECK(result == expected_result);
55 : }
56 4 : }
57 :
58 : inline
59 31 : std::string print_connected_component(const std::set<std::size_t>& component, const pbes_system::detail::stategraph_algorithm& algorithm)
60 : {
61 31 : const std::vector<detail::GCFP_vertex>& V = algorithm.GCFP().vertices();
62 31 : std::ostringstream out;
63 31 : out << "{";
64 81 : for (auto i = component.begin(); i != component.end(); ++i)
65 : {
66 50 : if (!algorithm.is_valid_connected_component(component))
67 : {
68 0 : continue;
69 : }
70 50 : if (i != component.begin())
71 : {
72 19 : out << ", ";
73 : }
74 50 : out << algorithm.print(V[*i]);
75 : }
76 31 : out << "}";
77 62 : return out.str();
78 31 : }
79 :
80 : inline
81 26 : std::set<std::string> print_connected_components(const std::vector<std::set<std::size_t> >& components, const pbes_system::detail::stategraph_algorithm& algorithm)
82 : {
83 26 : std::set<std::string> result;
84 57 : for (const auto &component: components)
85 : {
86 31 : result.insert(print_connected_component(component, algorithm));
87 : }
88 26 : if (result.empty()) // Special handling of empty result to distinguish undefined/empty results
89 : {
90 4 : result.insert("{}");
91 : }
92 26 : return result;
93 0 : }
94 :
95 4 : void test_significant_variables(const pbes_expression& x, const std::string& expected_result)
96 : {
97 4 : std::set<data::variable> v = significant_variables(x);
98 4 : std::string result = print_set(v);
99 4 : check_result(pbes_system::pp(x), result, expected_result, "significant_variables");
100 4 : }
101 :
102 2 : BOOST_AUTO_TEST_CASE(test_significant_variables1)
103 : {
104 : std::string text =
105 : "pbes \n"
106 : " mu X0(b: Bool) = val(b); \n"
107 : " mu X1 = true; \n"
108 : " mu X2(b: Bool) = val(b) && forall b: Bool. val(b); \n"
109 : " mu X3(b: Bool) = val(b) && forall c: Bool. val(c); \n"
110 1 : "init X1; \n"
111 : ;
112 :
113 1 : bool normalize = false;
114 1 : pbes p = txt2pbes(text, normalize);
115 1 : const std::vector<pbes_equation>& eqn = p.equations();
116 1 : test_significant_variables(eqn[0].formula(), "{b}");
117 1 : test_significant_variables(eqn[1].formula(), "{}");
118 1 : test_significant_variables(eqn[2].formula(), "{b}");
119 1 : test_significant_variables(eqn[2].formula(), "{b}");
120 1 : }
121 :
122 : // find propositional variable instantiation with the given name
123 21 : propositional_variable_instantiation find_propvar(const std::string& name, const pbes_expression& x)
124 : {
125 46 : for (const propositional_variable_instantiation& v: find_propositional_variable_instantiations(x))
126 : {
127 46 : if (v.name() == core::identifier_string(name))
128 : {
129 42 : return v;
130 : }
131 21 : }
132 0 : throw mcrl2::runtime_error("propvar not found!");
133 : }
134 :
135 21 : void test_guard(const std::string& pbesspec, const std::string& X, const std::string& expected_result)
136 : {
137 21 : bool normalize = false;
138 21 : pbes p = txt2pbes(pbesspec, normalize);
139 21 : pbes_expression x1 = p.equations().front().formula();
140 21 : propositional_variable_instantiation X1 = find_propvar(X, x1);
141 21 : data::rewriter rewr(p.data());
142 21 : simplify_data_rewriter<data::rewriter> R(rewr);
143 :
144 21 : detail::guard_traverser f(rewr);
145 21 : f.apply(x1);
146 21 : BOOST_CHECK(f.expression_stack.back().check_guards(x1, R));
147 :
148 : // pbes_expression g = detail::guard(X1, x1);
149 : // std::string result = pbes_system::pp(g);
150 : // check_result(X, result, expected_result, "");
151 21 : }
152 :
153 2 : BOOST_AUTO_TEST_CASE(test_guard1)
154 : {
155 : std::string text =
156 : "pbes \n"
157 : " mu X1 = X1 || X2; \n"
158 : " mu X2 = true; \n"
159 1 : "init X2; \n"
160 : ;
161 1 : test_guard(text, "X1", "true");
162 :
163 : text =
164 : "pbes \n"
165 : " mu X1(b: Bool) = X1(true) && val(b); \n"
166 : " mu X2 = true; \n"
167 1 : "init X2; \n"
168 : ;
169 1 : test_guard(text, "X1", "b");
170 :
171 : text =
172 : "pbes \n"
173 : " mu X1(b: Bool) = X1(true) || val(b); \n"
174 : " mu X2 = true; \n"
175 1 : "init X2; \n"
176 : ;
177 1 : test_guard(text, "X1", "!val(b)");
178 :
179 : text =
180 : "pbes \n"
181 : " mu X1(b: Bool) = X1(true) || (val(b) && X2); \n"
182 : " mu X2 = true; \n"
183 1 : "init X2; \n"
184 : ;
185 1 : test_guard(text, "X1", "true");
186 :
187 : text =
188 : "pbes \n"
189 : " mu X1(b: Bool) = (forall c: Bool. val(c)) || X1(true); \n"
190 : " mu X2 = true; \n"
191 1 : "init X2; \n"
192 : ;
193 1 : test_guard(text, "X1", "!(forall c: Bool. val(c))");
194 :
195 : text =
196 : "pbes \n"
197 : " mu X1(b: Bool) = (forall c: Bool. val(c)) && X1(true); \n"
198 : " mu X2 = true; \n"
199 1 : "init X2; \n"
200 : ;
201 1 : test_guard(text, "X1", "forall c: Bool. val(c)");
202 :
203 : text =
204 : "pbes \n"
205 : " mu X1(b: Bool) = forall c: Bool. val(c) || X1(c); \n"
206 : " mu X2 = true; \n"
207 1 : "init X2; \n"
208 : ;
209 1 : test_guard(text, "X1", "!val(c)");
210 :
211 : text =
212 : "pbes \n"
213 : " mu X1(b: Bool) = val(b) || (forall c: Bool. val(c) || X1(c)); \n"
214 : " mu X2 = true; \n"
215 1 : "init X2; \n"
216 : ;
217 1 : test_guard(text, "X1", "!val(b) && !val(c)");
218 :
219 : text =
220 : "pbes \n"
221 : " mu X1(b: Bool) = (val(b) && X2) || (forall c: Bool. val(c) || X1(c)); \n"
222 : " mu X2 = true; \n"
223 1 : "init X2; \n"
224 : ;
225 1 : test_guard(text, "X1", "!val(c)");
226 :
227 : text =
228 : "pbes \n"
229 : " mu X1(b: Bool) = (val(b) || X2) || (forall c: Bool. val(c) || X1(c)); \n"
230 : " mu X2 = true; \n"
231 1 : "init X2; \n"
232 : ;
233 1 : test_guard(text, "X1", "!val(c)");
234 :
235 : text =
236 : "pbes \n"
237 : " mu X1(b: Bool) = (!val(b) || X2) || (forall c: Bool. val(c) || X1(c)); \n"
238 : " mu X2 = true; \n"
239 1 : "init X2; \n"
240 : ;
241 1 : test_guard(text, "X1", "!val(c)");
242 :
243 : text =
244 : "pbes \n"
245 : " mu X0(b, c, d, e: Bool) = (val(b) || X1) && (val(c) || X2) && (val(d) || X3); \n"
246 : " mu X1 = true; \n"
247 : " mu X2 = true; \n"
248 : " mu X3 = true; \n"
249 1 : "init X2; \n"
250 : ;
251 1 : test_guard(text, "X1", "!val(b)");
252 :
253 : text =
254 : "pbes \n"
255 : " mu X0(b, c, d, e: Bool) = (val(b) || val(e) && X1); \n"
256 : " mu X1 = true; \n"
257 1 : "init X1; \n"
258 : ;
259 1 : test_guard(text, "X1", "!val(b) && val(e)");
260 :
261 : text =
262 : "pbes \n"
263 : " mu X0(b, c, d, e: Bool) = (val(b) || val(e) && X1) && (val(c) || X2); \n"
264 : " mu X1 = true; \n"
265 : " mu X2 = true; \n"
266 1 : "init X1; \n"
267 : ;
268 1 : test_guard(text, "X1", "!val(b) && val(e)");
269 :
270 : text =
271 : "pbes nu X1(s,d: Nat) = (!val((s == 1)) || X1(2, d)) &&\n"
272 : " (!val((s == 2)) || X2(3, d)) &&\n"
273 : " (!val((s == 3)) || X3(4, d)) &&\n"
274 : " (!val((s == 4)) || (forall e: Nat. val(!(e < 10)) || X4(5, 2 * e))) &&\n"
275 : " (!val((s == 5)) || val(d mod 2 == 0) && X5(6, d)) &&\n"
276 : " (!val((s == 6)) || X6(7, d)) &&\n"
277 : " (!val((s == 7)) || X7(1, d));\n"
278 : " nu X2(s,d: Nat) = true;\n"
279 : " nu X3(s,d: Nat) = true;\n"
280 : " nu X4(s,d: Nat) = true;\n"
281 : " nu X5(s,d: Nat) = true;\n"
282 : " nu X6(s,d: Nat) = true;\n"
283 : " nu X7(s,d: Nat) = true;\n"
284 1 : "init X1(0, 0);\n"
285 : ;
286 1 : test_guard(text, "X1", "s == 1");
287 1 : test_guard(text, "X2", "s == 2");
288 1 : test_guard(text, "X3", "s == 3");
289 1 : test_guard(text, "X4", "val(s == 4) && !val(!(e < 10))");
290 1 : test_guard(text, "X5", "val(s == 5) && val(d mod 2 == 0)");
291 1 : test_guard(text, "X6", "s == 6");
292 1 : test_guard(text, "X7", "s == 7");
293 1 : }
294 :
295 2 : BOOST_AUTO_TEST_CASE(test_local_stategraph)
296 : {
297 1 : std::string text;
298 1 : bool normalize = false;
299 1 : pbes p;
300 :
301 : text =
302 : "sort D = struct d1 | d2;\n"
303 : "\n"
304 : "pbes nu X(s: Nat, d: D) = forall v: D. forall e1: D. val(!(e1 == v)) || val(!(s == 1)) || Y(2, e1, v);\n"
305 : " nu Y(s: Nat, d,v: D) = val(!(s == 2)) || Y(3, d, v);\n"
306 : "\n"
307 1 : "init X(1, d1);\n"
308 : ;
309 : // p = txt2pbes(text, normalize);
310 : // This fails because no suitable must graph is found
311 : // pbes_system::detail::local_reset_variables_algorithm(p).run();
312 :
313 : text =
314 : "pbes\n"
315 : "nu X(c:Pos, d:Nat) = val(c == 1) => Y(1,d+1) && (val(c == 1) => X(1,d+2));\n"
316 : "nu Y(c:Pos, d:Nat) = (val(c == 1) => Y(c,d+1)) && (val(d > 0));\n"
317 1 : "init X(1,0);\n"
318 : ;
319 1 : p = txt2pbes(text, normalize);
320 1 : pbesstategraph_options options;
321 1 : options.use_global_variant = false;
322 1 : pbes_system::detail::local_reset_variables_algorithm(p, options).run();
323 1 : }
324 :
325 : // Test cases provided by Tim Willemse, 28-06-2013
326 : // TODO: Some of the answers have been modified according to changes in the control flow graph
327 : // computation. These modifications have not been checked manually.
328 2 : BOOST_AUTO_TEST_CASE(test_cfp)
329 : {
330 : std::string text =
331 : "---------- \n"
332 : "pbes \n"
333 : "nu X(i,j,n,m:Nat) = \n"
334 : "(val(i == 1) => X(0,j+1,n+1,m+1)) && \n"
335 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
336 : " \n"
337 : "init \n"
338 : "X(0,0,0,0); \n"
339 : " \n"
340 : "expected_result \n"
341 : "{(X, i)} \n"
342 : "---------- \n"
343 : "pbes \n"
344 : "nu X(i,j,n,m:Nat) = \n"
345 : "(val(i == 1) => Y(0,j,n+1,m+1)) && \n"
346 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
347 : " \n"
348 : "nu Y(i,j,n,m:Nat) = \n"
349 : "(val(i == 1) => X(0,j,n,m) ) && \n"
350 : "(val(i == 0) => Y(1,n,j,m) ); \n"
351 : " \n"
352 : "init \n"
353 : "X(0,0,0,0); \n"
354 : " \n"
355 : "expected_result \n"
356 : "{(X, i)}, {(Y, i)} \n"
357 : "---------- \n"
358 : "pbes \n"
359 : "nu X(i,j,n,m:Nat) = \n"
360 : "(val(i == 1) => Y(0,j,n+1,m+1)) && \n"
361 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
362 : " \n"
363 : "nu Y(i,j,n,m:Nat) = \n"
364 : "(val(i == 1) => X(0,j,n,m) ) && \n"
365 : "(val(i == 0) => Y(1,j,n,m) ); \n"
366 : " \n"
367 : "init \n"
368 : "X(0,0,0,0); \n"
369 : " \n"
370 : "expected_result \n"
371 : "{(X, i)}, {(Y, i)} \n"
372 : "---------- \n"
373 : "pbes \n"
374 : "nu X(i,j,n,m:Nat) = \n"
375 : "(val(i == 1) => Y(i,j,n+1,m+1)) && \n"
376 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
377 : " \n"
378 : "nu Y(i,j,n,m:Nat) = \n"
379 : "(val(i == 1) => X(0,j,n,m) ) && \n"
380 : "(val(i == 0) => Y(1,j,n,m) ); \n"
381 : " \n"
382 : "init \n"
383 : "X(0,0,0,0); \n"
384 : " \n"
385 : "expected_result \n"
386 : "{(X, i), (Y, i)} \n"
387 : "---------- \n"
388 : "pbes \n"
389 : "nu X(i,j,n,m:Nat) = \n"
390 : "(val(i == 1) => Y(i,j,n+1,m+1)) && \n"
391 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
392 : " \n"
393 : "nu Y(i,j,n,m:Nat) = \n"
394 : "(val(i == 1) => X(0,j,n,m) ) && \n"
395 : "(val(i == 0) => Y(1,j,n,m) ) && \n"
396 : "(val(i == 1) => Y(0,j,n,m) ); \n"
397 : " \n"
398 : "init \n"
399 : "X(0,0,0,0); \n"
400 : " \n"
401 : "expected_result \n"
402 : "{(X, i), (Y, i)} \n"
403 : "---------- \n"
404 : "pbes \n"
405 : "nu X(i,j,n,m:Nat) = \n"
406 : "(val(i == 1) => Y(i,j,n+1,m+1)) && \n"
407 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
408 : " \n"
409 : "nu Y(i,j,n,m:Nat) = \n"
410 : "(val(i == 1) => X(0,j,n,m) ) && \n"
411 : "(val(i == 0) => Y(1,j,n,m) ) && \n"
412 : "(val(i == 1) => Y(0,j,n,m) ); \n"
413 : " \n"
414 : "init \n"
415 : "X(0,0,0,0); \n"
416 : " \n"
417 : "expected_result \n"
418 : "{(X, i), (Y, i)} \n"
419 : "---------- \n"
420 : "pbes \n"
421 : "nu X(i,j,n,m:Nat) = \n"
422 : "(val(i == 1) => Y(i,j,n+1,m+1)) && \n"
423 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
424 : " \n"
425 : "nu Y(i,j,n,m:Nat) = \n"
426 : "(val(i == 1) => X(j,j,n,m) ) && \n"
427 : "(val(i == 0) => X(i,j,n,m) ) && \n"
428 : "(val(i == 0) => Y(1,j,n,m) ) && \n"
429 : "(val(i == 1) => Y(0,j,n,m) ); \n"
430 : " \n"
431 : "init \n"
432 : "X(0,0,0,0); \n"
433 : " \n"
434 : "expected_result \n"
435 : "{(Y, i)} \n"
436 : "---------- \n"
437 : "pbes \n"
438 : "nu X(i,j,n,m:Nat) = \n"
439 : "(val(i == 1) => Y(i,j,n+1,m+1)) && \n"
440 : "(val(i == 0) => X(i+1,j+1,n+1,m+1)); \n"
441 : " \n"
442 : "nu Y(i,j,n,m:Nat) = \n"
443 : "(val(i == 1) => X(j,j,n,m) ) && \n"
444 : "(val(i == 0) => Z(i,j,n,m) ) && \n"
445 : "(val(i == 0) => Y(1,j,n,m) ) && \n"
446 : "(val(i == 1) => Y(0,j,n,m) ); \n"
447 : " \n"
448 : "nu Z(i,j,n,m:Nat) = \n"
449 : "(val(i== 0) => X(i,j,n,m)) && \n"
450 : "(val(i== 1) => Z(i,j,n,m)); \n"
451 : " \n"
452 : "init \n"
453 : "X(0,0,0,0); \n"
454 : " \n"
455 : "expected_result \n"
456 : "{(Y, i), (Z, i)} \n"
457 : "---------- \n"
458 : "pbes \n"
459 : "nu X(i,j,n:Nat) = \n"
460 : "(val(i == 1) => Y(i,j,n+1)) && \n"
461 : "(val(i == 0) => X(i+1,j+1,n+1)); \n"
462 : " \n"
463 : "nu Y(i,j,n:Nat) = \n"
464 : "(val(i == 1) => X(j,j,n) ) \n"
465 : "; \n"
466 : " \n"
467 : "init \n"
468 : "X(0,0,0); \n"
469 : " \n"
470 : "expected_result \n"
471 : "{(Y, i)} \n"
472 : "---------- \n"
473 : "pbes \n"
474 : "nu X(i,j,n:Nat) = \n"
475 : "(val(i == 1) => Y(i,j,n+1)) && \n"
476 : "(val(i == 0) => X(i+1,j+1,n+1)); \n"
477 : " \n"
478 : "nu Y(i,j,n:Nat) = \n"
479 : "(val(i == 1) => X(i,j,n) ) && \n"
480 : "(val(i == 1) => Z(i,j,n) ) \n"
481 : "; \n"
482 : " \n"
483 : "nu Z(i,j,n:Nat) = \n"
484 : "(val(j == 1) => X(i,j,n)) && \n"
485 : "(val(i == 1) => Z(0,j,n)) \n"
486 : "; \n"
487 : " \n"
488 : "init \n"
489 : "X(0,0,0); \n"
490 : " \n"
491 : "expected_result \n"
492 : "{(X, i), (Y, i), (Z, i)} \n"
493 : "---------- \n"
494 : "pbes \n"
495 : "nu X(i,j,n:Nat) = \n"
496 : "(val(i == 1) => Y(i,j,n+1)) && \n"
497 : "(val(i == 0) => X(i+1,j+1,n+1)); \n"
498 : " \n"
499 : "nu Y(i,j,n:Nat) = \n"
500 : "(val(i == 1) => X(i,j,n) ) && \n"
501 : "(val(i == 1) => Z(i,j,n) ) \n"
502 : "; \n"
503 : " \n"
504 : "nu Z(i,j,n:Nat) = \n"
505 : "(val(j == 1) => X(j,i,n)) && \n"
506 : "(val(i == 1) => Z(0,j,n)) \n"
507 : "; \n"
508 : " \n"
509 : "init \n"
510 : "X(0,0,0); \n"
511 : " \n"
512 : "expected_result \n"
513 : "{(X, i), (Y, i), (Z, i)} \n"
514 : "---------- \n"
515 : "pbes \n"
516 : "nu X(i,j,n:Nat) = \n"
517 : "(val(i == 1) => Y(i,j,n+1)) && \n"
518 : "(val(i == 0) => X(i+1,i+1,n+1)); \n"
519 : " \n"
520 : "nu Y(i,j,n:Nat) = \n"
521 : "(val(i == 1) => X(i,j,n) ) && \n"
522 : "(val(i == 1) => Z(i,j,n) ) \n"
523 : "; \n"
524 : " \n"
525 : "nu Z(i,j,n:Nat) = \n"
526 : "(val(j == 1) => X(i,j,n)) && \n"
527 : "(val(i == 1) => Z(0,j,n)) \n"
528 : "; \n"
529 : " \n"
530 : "init \n"
531 : "X(0,0,0); \n"
532 : " \n"
533 : "expected_result \n"
534 : "{(X, i), (Y, i), (Z, i)} \n"
535 : "---------- \n"
536 : "pbes \n"
537 : "nu X(i,j,n:Nat) = \n"
538 : "(val(i == 1) => Y(i,j,n+1)) && \n"
539 : "(val(i == 0) => X(1,1,n+1)); \n"
540 : " \n"
541 : "nu Y(i,j,n:Nat) = \n"
542 : "(val(i == 1) => X(i,j,n) ) && \n"
543 : "(val(i == 1) => Z(i,j,n) ) \n"
544 : "; \n"
545 : " \n"
546 : "nu Z(i,j,n:Nat) = \n"
547 : "(val(j == 1) => X(i,j,n)) && \n"
548 : "(val(i == 1) => Z(0,j,n)) \n"
549 : "; \n"
550 : " \n"
551 : "init \n"
552 : "X(0,0,0); \n"
553 : " \n"
554 : "expected_result \n"
555 : "{(X, i), (Y, i), (Z, i)} \n"
556 : "---------- \n"
557 : "pbes \n"
558 : "nu X(i,j,n:Nat) = \n"
559 : "(val(i == 0) => Y(i,j,n+1)); \n"
560 : " \n"
561 : "nu Y(i,j,n:Nat) = \n"
562 : "(val(i==0) => Z(i,j,n+1)); \n"
563 : " \n"
564 : "nu Z(i,j,n:Nat) = \n"
565 : "(val(i==0) => Z(1,j,n)) && \n"
566 : "(val(i==1) => (X(i,j,n) || Y(i,j,n))); \n"
567 : " \n"
568 : "init \n"
569 : "X(0,0,0); \n"
570 : " \n"
571 : "expected_result \n"
572 : "{(X, i), (Y, i), (Z, i)} \n"
573 : "---------- \n"
574 : "pbes \n"
575 : "nu X(i,n:Nat) = \n"
576 : "(val(i == 0) => Y(i,n+1)); \n"
577 : " \n"
578 : "nu Y(i,n:Nat) = \n"
579 : "(val(i==0) => Z(i,n+1)); \n"
580 : " \n"
581 : "nu Z(i,n:Nat) = \n"
582 : "(val(i==0) => X(i,n)); \n"
583 : " \n"
584 : "init \n"
585 : "X(0,0); \n"
586 : " \n"
587 : "expected_result \n"
588 : "{(X, i), (Y, i), (Z, i)} \n"
589 : "---------- \n"
590 : "pbes \n"
591 : "nu X(n:Nat) = Y(n+1); \n"
592 : "nu Y(n:Nat) = Z(n+1); \n"
593 : "nu Z(n:Nat) = X(n); \n"
594 : " \n"
595 : "init X(0); \n"
596 : " \n"
597 : "expected_result \n"
598 : "{} \n"
599 : "---------- \n"
600 : "pbes \n"
601 : "nu X(i,n:Nat) = \n"
602 : "(val(i == 0) => Y(i,n+1)); \n"
603 : " \n"
604 : "nu Y(i,n:Nat) = \n"
605 : "(val(i==0) => Z(i,0,n+1)) && \n"
606 : "(val(i==0) => X(i,n+1)); \n"
607 : " \n"
608 : "nu Z(i,j,n:Nat) = \n"
609 : "(val(i==0 && n == 1) => Z(1,j,n)) && \n"
610 : "(val(i==1) => X(n,j)); \n"
611 : " \n"
612 : "init \n"
613 : "X(0,0); \n"
614 : " \n"
615 : "expected_result \n"
616 : "{(Y, i), (Z, i)}, {(Z, j)} \n"
617 : "---------- \n"
618 : "pbes \n"
619 : "nu X(i,n:Nat) = \n"
620 : "(val(i == 0) => Y(i,n)); \n"
621 : " \n"
622 : "nu Y(i,n:Nat) = \n"
623 : "(val(i==0) => Z(i,0)) && \n"
624 : "(val(i==0) => X(i,2)); \n"
625 : " \n"
626 : "nu Z(i,n:Nat) = \n"
627 : "(val(i==0 && n == 1) => Z(1,n)) && \n"
628 : "(val(i==1) => X(n,i)); \n"
629 : " \n"
630 : "init \n"
631 : "X(0,0); \n"
632 : " \n"
633 : "expected_result \n"
634 : "{} \n"
635 : "---------- \n"
636 : "pbes \n"
637 : "nu X(i,n:Nat) = \n"
638 : "(val(i == 0) => Y(i,n)); \n"
639 : " \n"
640 : "nu Y(i,n:Nat) = \n"
641 : "(val(i==0) => X(i,0)) && \n"
642 : "(val(i==1) => X(n,2)); \n"
643 : " \n"
644 : "init \n"
645 : "X(0,0); \n"
646 : " \n"
647 : "expected_result \n"
648 : "{} \n"
649 : "---------- \n"
650 : "pbes \n"
651 : "nu X(i,n:Nat) = \n"
652 : "(val(i == 0) => Y(i,n+1)); \n"
653 : " \n"
654 : "nu Y(i,n:Nat) = \n"
655 : "(val(i==0) => X(i,0)) && \n"
656 : "(val(i==1) => X(n,2)); \n"
657 : " \n"
658 : "init \n"
659 : "X(0,0); \n"
660 : " \n"
661 : "expected_result \n"
662 : "{(X, n)}, {(Y, i)} \n"
663 : "---------- \n"
664 : "pbes \n"
665 : "nu X(n,i:Nat) = Y(n+1,0); \n"
666 : " \n"
667 : "nu Y(i,n:Nat) = X(0,n); \n"
668 : " \n"
669 : "init \n"
670 : "X(0,0); \n"
671 : " \n"
672 : "expected_result \n"
673 : "{(X, i), (Y, n)}, {(X, n)} \n"
674 : "---------- \n"
675 : "pbes \n"
676 : "nu X(i,n:Nat) = forall j:Nat.(val(i == 0) => Y(i,n+j)); \n"
677 : " \n"
678 : "nu Y(i,n:Nat) = (val(i==1) => X(n,2)); \n"
679 : " \n"
680 : " \n"
681 : "init \n"
682 : "X(0,0); \n"
683 : " \n"
684 : "expected_result \n"
685 : "{(X, n)}, {(Y, i)} \n"
686 : "---------- \n"
687 : "% \n"
688 : "% The below PBES should only have (Y,i) as a control flow parameter \n"
689 : "% \n"
690 : " \n"
691 : "pbes \n"
692 : "nu X(n:Nat) = forall j:Nat. Y(0,n+j); \n"
693 : " \n"
694 : "nu Y(i,n:Nat) = (val(i==1) => X(2)); \n"
695 : " \n"
696 : "init \n"
697 : "X(0); \n"
698 : " \n"
699 : "expected_result \n"
700 : "{(X, n)}, {(Y, i)} \n"
701 : "---------- \n"
702 : "pbes \n"
703 : "nu X(n:Nat) = forall j:Nat. Y(0,j); \n"
704 : " \n"
705 : "nu Y(i,n:Nat) = (val(i==1) => X(2)); \n"
706 : " \n"
707 : " \n"
708 : "init \n"
709 : "X(0); \n"
710 : " \n"
711 : "expected_result \n"
712 : "{(X, n)}, {(Y, i)} \n"
713 : "---------- \n"
714 : "pbes \n"
715 : " \n"
716 : "nu X(i,j:Nat) = \n"
717 : "(val(i==0) => X(0,i)) && \n"
718 : "(val(j==1) => X(j,1)); \n"
719 : " \n"
720 : "init X(0,0); \n"
721 : " \n"
722 : "expected_result \n"
723 : "{} \n"
724 : "---------- \n"
725 : "%This solution assumes strict separation between CFPs and DPs, if this assumption is \n"
726 : "%dropped, the following is the expected solution \n"
727 : "%{(X, n), (Y, n)} \n"
728 : "pbes \n"
729 : "nu X(i,n:Nat) = \n"
730 : "(val(i == 0) => Y(i,n)); \n"
731 : " \n"
732 : "nu Y(i,n:Nat) = \n"
733 : "(val(i==0) => X(i,0)) && \n"
734 : "(val(i==1) => X(n+1,2)); \n"
735 : " \n"
736 : "init \n"
737 : "X(0,0); \n"
738 : " \n"
739 : "expected_result \n"
740 1 : "{(X, n), (Y, n)}, {(Y, i)} \n"
741 : ;
742 :
743 2 : std::vector<std::string> test_cases = utilities::detail::split_text(text, "----------");
744 27 : for (const std::string& s: test_cases)
745 : {
746 130 : std::vector<std::string> keywords = { "pbes", "expected_result" };
747 26 : std::map<std::string, std::string> test_case = utilities::detail::split_text_using_keywords(s, keywords);
748 52 : pbes p = txt2pbes(test_case["pbes"], false);
749 52 : std::string expected_result = boost::trim_copy(test_case["expected_result"]);
750 26 : if (!expected_result.empty())
751 : {
752 26 : expected_result = boost::trim_copy(expected_result.substr(15));
753 : }
754 26 : std::vector<std::string> lines = utilities::detail::nonempty_lines(expected_result);
755 26 : std::set<std::string> lineset(lines.begin(), lines.end());
756 52 : std::string expected = utilities::string_join(lineset, ", ");
757 26 : pbesstategraph_options options;
758 26 : pbes_system::detail::stategraph_algorithm algorithm(p, options);
759 26 : algorithm.run();
760 52 : std::string result = utilities::string_join(print_connected_components(algorithm.connected_components(), algorithm), ", ");
761 :
762 26 : if (result != expected)
763 : {
764 0 : BOOST_CHECK(result == expected);
765 0 : std::cout << "--- Control flow test failed ---" << std::endl;
766 0 : std::cout << test_case["pbes"] << std::endl;
767 0 : std::cout << "result = " << result << std::endl;
768 0 : std::cout << "expected result = " << expected << std::endl;
769 : }
770 26 : }
771 1 : }
|
