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 pbesinst_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE pbesinst_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/detail/test_input.h"
16 : #include "mcrl2/modal_formula/detail/test_input.h"
17 : #include "mcrl2/modal_formula/parse.h"
18 : #include "mcrl2/pbes/is_bes.h"
19 : #include "mcrl2/pbes/lps2pbes.h"
20 : #include "mcrl2/pbes/pbesinst_finite_algorithm.h"
21 : #include "mcrl2/pbes/pbesinst_symbolic.h"
22 : #include "mcrl2/pbes/rewriter.h"
23 : #include "mcrl2/pbes/txt2pbes.h"
24 :
25 : using namespace mcrl2;
26 : using namespace mcrl2::pbes_system;
27 :
28 : inline
29 7 : pbes pbesinst_lazy(const pbes& p)
30 : {
31 7 : pbes q = p;
32 7 : pbesinst_algorithm algorithm(q.data());
33 7 : algorithm.run(q);
34 14 : return algorithm.get_result();
35 7 : }
36 :
37 : inline
38 9 : pbes pbesinst_finite(const pbes& p)
39 : {
40 9 : pbes q = p;
41 9 : pbesinst_finite_algorithm algorithm(data::jitty);
42 9 : algorithm.run(q);
43 18 : return q;
44 9 : }
45 :
46 : std::string test1 =
47 : "pbes \n"
48 : " \n"
49 : "nu X(b:Bool, n:Nat) = (val(b) => X(!b, n)) && (val(!b) => X(!b, n+1)); \n"
50 : " \n"
51 : "init X(true,0); \n"
52 : ;
53 :
54 : std::string test2 =
55 : "pbes \n"
56 : " \n"
57 : "nu X(b:Bool, n:Nat) = forall c:Bool. X(c,n); \n"
58 : " \n"
59 : "init X(true,0); \n"
60 : ;
61 :
62 : std::string test3 =
63 : "pbes \n"
64 : " \n"
65 : "nu X(b:Bool, n:Nat) = exists c:Bool. X(c,n+1); \n"
66 : " \n"
67 : "init X(true,0); \n"
68 : ;
69 :
70 : std::string test4 =
71 : "pbes \n"
72 : " \n"
73 : "nu X(b:Bool, n:Nat) = val(b && n < 10) => X(!b,n+1); \n"
74 : " \n"
75 : "init X(true,0); \n"
76 : ;
77 :
78 : std::string test5 =
79 : "sort D = struct d1 | d2; \n"
80 : " \n"
81 : "pbes \n"
82 : " \n"
83 : "nu X(d:D, n:Nat) = val(d == d1 && n < 10) => X(d2,n+1); \n"
84 : " \n"
85 : "init X(d1,0); \n"
86 : ;
87 :
88 : std::string test6 =
89 : "pbes \n"
90 : "nu X(b:Bool) = forall c:Bool. X(if (c,!c,c)); \n"
91 : " \n"
92 : "init X(true); \n"
93 : ;
94 :
95 : std::string test7 =
96 : "sort Enum2 = struct e1_5 | e0_5; \n"
97 : " \n"
98 : "map \n"
99 : " \n"
100 : " C5_fun2: Enum2 # Enum2 # Enum2 -> Enum2; \n"
101 : " C5_fun1: Enum2 # Nat # Nat -> Nat; \n"
102 : " \n"
103 : "var y23,y22,y21,x5,y14,y13,y12,y11,y10,x2,e3,e2,e1: Enum2; \n"
104 : " y20,y19,y18,x4,y9,y8,y7,y6,y5,x1: Nat; \n"
105 : " y17,y16,y15,x3,y4,y3,y2,y1,y,x: Bool; \n"
106 : "eqn \n"
107 : " C5_fun2(e0_5, y14, y13) = y14; \n"
108 : " C5_fun2(e1_5, y14, y13) = y13; \n"
109 : " C5_fun2(e3, x2, x2) = x2; \n"
110 : " C5_fun1(e0_5, y6, y5) = y5; \n"
111 : " C5_fun1(e1_5, y6, y5) = y6; \n"
112 : " C5_fun1(e2, x1, x1) = x1; \n"
113 : " \n"
114 : "pbes nu X(s3_P: Enum2, n_P: Nat) = \n"
115 : " \n"
116 : "(forall e: Enum2. X(C5_fun2(e, e, e1_5), C5_fun1(e, 0, n_P)) \n"
117 : " \n"
118 : ") \n"
119 : " \n"
120 : " \n"
121 : "; \n"
122 : " \n"
123 : "init X(e1_5, 0); \n"
124 : ;
125 :
126 : std::string test8 =
127 : "pbes \n"
128 : " \n"
129 : "nu X(b:Bool) = val(b) && Y(!b); \n"
130 : " \n"
131 : "mu Y(c:Bool) = forall d:Bool. X(d && c) || Y(d); \n"
132 : " \n"
133 : "init X(true); \n"
134 : ;
135 :
136 : // This pbes triggered a garbage collection problem, that has been solved.
137 : std::string random1 =
138 : "pbes \n"
139 : "nu X0(c:Bool, n:Nat) = (forall n:Nat.((val(n < 3)) && (((val(n < 3)) || (exists m:Nat.((val(m < 3)) || (X3(m + 1, m > 0))))) && ((forall m:Nat.((val(m < 3)) && (!X2(m + 1, 1)))) => ((val(c)) || (val(n < 3))))))) || ((val(false)) || (X0(false, n + 1))); \n"
140 : "nu X1(b:Bool) = (!(!(forall k:Nat.((val(k < 3)) && ((forall k:Nat.((val(k < 3)) && ((X2(1, k + 1)) && (val(false))))) || ((X4(k > 0, k + 1)) && (X1(k > 1)))))))) && (!(forall m:Nat.((val(m < 3)) && (((val(m < 2)) && (val(m > 0))) && (val(true)))))); \n"
141 : "mu X2(m:Nat, n:Nat) = (((val(m < 2)) && (X4(m == n, n + 1))) || ((val(false)) || ((val(true)) => (X0(n == m, 0))))) || (forall k:Nat.((val(k < 3)) && (exists m:Nat.((val(m < 3)) || ((val(n < 2)) && (X2(m + 1, m + 1))))))); \n"
142 : "nu X3(n:Nat, c:Bool) = ((forall k:Nat.((val(k < 3)) && (!((forall m:Nat.((val(m < 3)) && (val(n > 0)))) => (val(c)))))) && ((X3(0, n < 3)) && (exists m:Nat.((val(m < 3)) || ((!(exists n:Nat.((val(n < 3)) || (val(m < 2))))) && (X2(n + 1, m + 1))))))) || ((!(!X1(n > 0))) || (val(false))); \n"
143 : "nu X4(c:Bool, n:Nat) = (((exists m:Nat.((val(m < 3)) || (val(m > 0)))) && ((!(!X0(n < 3, 0))) || (!((val(n > 0)) => (!X2(0, 0)))))) => (forall k:Nat.((val(k < 3)) && (!(forall n:Nat.((val(n < 3)) && (val(n < 2)))))))) => (!(forall m:Nat.((val(m < 3)) && ((val(c)) && (forall m:Nat.((val(m < 3)) && (!X3(n + 1, false)))))))); \n"
144 : " \n"
145 : "init X0(true, 0); \n"
146 : ;
147 :
148 : // This pbes triggered a garbage collection problem, that has been solved.
149 : std::string random2 =
150 : "pbes \n"
151 : "mu X0(m:Nat, b:Bool) = (X0(m + 1, m > 0)) && (((forall m:Nat.((val(m < 3)) && (forall k:Nat.((val(k < 3)) && (!((val(k > 1)) && (val(false)))))))) && (exists n:Nat.((val(n < 3)) || (!(!(val(n > 1))))))) || (exists n:Nat.((val(n < 3)) || (forall n:Nat.((val(n < 3)) && (exists n:Nat.((val(n < 3)) || (((forall m:Nat.((val(m < 3)) && (val(m == n)))) => (X3(0, n > 1))) && (!(!X2(n == m))))))))))); \n"
152 : "mu X1(c:Bool, b:Bool) = (((!X1(c, true)) || ((!X2(b)) || (val(b)))) && (forall k:Nat.((val(k < 3)) && (((val(c)) => (X4(c, 1))) => (val(true)))))) => (val(true)); \n"
153 : "nu X2(b:Bool) = (!(!(((exists m:Nat.((val(m < 3)) || (val(m < 3)))) => ((X0(1, true)) => (!(val(false))))) && ((!((!X1(b, true)) && (!X3(0, false)))) => (val(false)))))) => (exists m:Nat.((val(m < 3)) || (forall k:Nat.((val(k < 3)) && (exists n:Nat.((val(n < 3)) || (forall n:Nat.((val(n < 3)) && (exists n:Nat.((val(n < 3)) || (forall n:Nat.((val(n < 3)) && (val(false)))))))))))))); \n"
154 : "mu X3(m:Nat, c:Bool) = (exists m:Nat.((val(m < 3)) || ((!(val(c))) && (forall k:Nat.((val(k < 3)) && (exists m:Nat.((val(m < 3)) || (forall k:Nat.((val(k < 3)) && (val(false))))))))))) || (exists m:Nat.((val(m < 3)) || (exists n:Nat.((val(n < 3)) || ((!((exists k:Nat.((val(k < 3)) || (!X4(false, k + 1)))) && ((!X1(m > 0, n < 2)) || ((val(n > 0)) || (val(c)))))) && (exists k:Nat.((val(k < 3)) || (exists n:Nat.((val(n < 3)) || (exists k:Nat.((val(k < 3)) || (X3(k + 1, k == n))))))))))))); \n"
155 : "nu X4(b:Bool, n:Nat) = (exists m:Nat.((val(m < 3)) || ((val(b)) || ((val(n > 1)) && ((X1(m > 1, n == m)) || (val(m > 0))))))) && ((exists k:Nat.((val(k < 3)) || (!(!((!X3(1, n > 0)) && (!(val(k == n)))))))) => (forall n:Nat.((val(n < 3)) && (exists k:Nat.((val(k < 3)) || (!(!(X4(n > 1, 0))))))))); \n"
156 : " \n"
157 : "init X0(0, true); \n"
158 : ;
159 :
160 : // This pbes triggered an error with pbesinst finite
161 : std::string random3 =
162 : "pbes \n"
163 : "mu X0(n:Nat, c:Bool) = ((!(((val(n < 2)) && (!X1)) && (exists k:Nat.((val(k < 3)) || (val(c)))))) && (((forall n:Nat.((val(n < 3)) && (!X4(n > 1)))) || (!(val(n > 1)))) => (val(true)))) && (exists n:Nat.((val(n < 3)) || (exists k:Nat.((val(k < 3)) || (forall m:Nat.((val(m < 3)) && (X0(k + 1, n < 3)))))))); \n"
164 : "mu X1 = (((!((val(true)) => (X2))) => (!(!(!(!X1))))) && (((val(false)) || (X3(1))) && (forall n:Nat.((val(n < 3)) && (val(true)))))) || (forall k:Nat.((val(k < 3)) && (!(forall k:Nat.((val(k < 3)) && (exists m:Nat.((val(m < 3)) || (val(k < 2))))))))); \n"
165 : "mu X2 = ((exists k:Nat.((val(k < 3)) || (exists k:Nat.((val(k < 3)) || (exists m:Nat.((val(m < 3)) || ((val(m == k)) => (X1)))))))) => (((val(true)) => (!X2)) || (exists k:Nat.((val(k < 3)) || (val(false)))))) => (!((val(false)) => (!(X3(0))))); \n"
166 : "mu X3(n:Nat) = ((exists n:Nat.((val(n < 3)) || (exists n:Nat.((val(n < 3)) || (forall n:Nat.((val(n < 3)) && (val(false)))))))) && (forall m:Nat.((val(m < 3)) && (((forall m:Nat.((val(m < 3)) && (exists m:Nat.((val(m < 3)) || (exists m:Nat.((val(m < 3)) || (!(val(n > 0))))))))) && ((!X4(m > 1)) || (!X2))) || (val(n < 2)))))) => ((val(n < 2)) => (X1)); \n"
167 : "nu X4(b:Bool) = ((val(true)) => ((forall m:Nat.((val(m < 3)) && (val(false)))) => ((X1) || ((!X3(0)) => (forall n:Nat.((val(n < 3)) && (val(n > 1)))))))) && (forall m:Nat.((val(m < 3)) && (forall n:Nat.((val(n < 3)) && ((X2) && (val(false))))))); \n"
168 : " \n"
169 : "init X0(0, true); \n"
170 : ;
171 :
172 9 : void test_pbes(const std::string& pbes_spec, bool test_finite, bool test_lazy)
173 : {
174 9 : pbes p = txt2pbes(pbes_spec);
175 9 : std::cout << "------------------------------\n" << pbes_system::pp(p) << std::endl;
176 9 : if (!p.is_closed())
177 : {
178 0 : std::cout << "ERROR: the pbes is not closed!" << std::endl;
179 0 : return;
180 : }
181 :
182 9 : if (test_finite)
183 : {
184 8 : std::cout << "FINITE" << std::endl;
185 : try
186 : {
187 : using namespace pbes_system;
188 8 : pbes q1 = ::pbesinst_finite(p);
189 8 : std::cout << pbes_system::pp(q1) << std::endl;
190 8 : }
191 0 : catch (mcrl2::runtime_error& e)
192 : {
193 0 : std::cout << "pbesinst failed: " << e.what() << std::endl;
194 0 : }
195 : }
196 :
197 9 : if (test_lazy)
198 : {
199 7 : std::cout << "LAZY" << std::endl;
200 : try
201 : {
202 : using namespace pbes_system;
203 7 : pbes q1 = pbesinst_lazy(p);
204 7 : std::cout << pbes_system::pp(q1) << std::endl;
205 7 : }
206 0 : catch (mcrl2::runtime_error& e)
207 : {
208 0 : std::cout << "pbesinst failed: " << e.what() << std::endl;
209 0 : }
210 : }
211 9 : }
212 :
213 2 : BOOST_AUTO_TEST_CASE(test_pbesinst)
214 : {
215 1 : test_pbes(test1, true, false);
216 1 : test_pbes(test2, true, true);
217 1 : test_pbes(test3, true, false);
218 1 : test_pbes(test4, true, true);
219 1 : test_pbes(test5, true, true);
220 1 : test_pbes(test6, true, true);
221 1 : test_pbes(test7, true, true);
222 1 : test_pbes(test8, true, true);
223 1 : test_pbes(random3, false, true);
224 1 : }
225 :
226 2 : BOOST_AUTO_TEST_CASE(test_pbesinst_finite)
227 : {
228 1 : pbes p = txt2pbes(random3);
229 1 : pbes q = pbesinst_finite(p);
230 1 : std::cerr << pbes_system::pp(q) << std::endl;
231 :
232 : std::string text =
233 : "sort D = struct d1 | d2; \n"
234 : " \n"
235 : "pbes \n"
236 : " \n"
237 : "nu X(d:D) = (val(d == d1) && X(d2)) || (val(d == d2) && X(d1)); \n"
238 : " \n"
239 1 : "init X(d1); \n"
240 : ;
241 1 : pbes p1 = txt2pbes(text);
242 1 : pbesinst_finite_algorithm algorithm(data::jitty);
243 2 : pbesinst_variable_map variable_map = mcrl2::pbes_system::detail::parse_pbes_parameter_map(p1, "X(*:D)");
244 1 : algorithm.run(p1, variable_map);
245 1 : }
246 :
247 2 : BOOST_AUTO_TEST_CASE(test_abp_no_deadlock)
248 : {
249 2 : lps::specification spec=remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
250 1 : state_formulas::state_formula formula = state_formulas::parse_state_formula(lps::detail::NO_DEADLOCK(), spec, false);
251 1 : bool timed = false;
252 1 : pbes p = lps2pbes(spec, formula, timed);
253 1 : data::rewriter::strategy rewriter_strategy = data::jitty;
254 1 : bool print_equations = true;
255 1 : pbes_system::pbesinst_algorithm algorithm(p.data(), rewriter_strategy, print_equations);
256 1 : algorithm.run(p);
257 1 : pbes q = algorithm.get_result();
258 1 : std::cout << "--- ABP ---" << std::endl;
259 1 : std::cout << pbes_system::pp(q) << std::endl;
260 1 : BOOST_CHECK(is_bes(q));
261 1 : }
262 :
263 : // Example supplied by Tim Willemse, 23-05-2011
264 2 : BOOST_AUTO_TEST_CASE(test_functions)
265 : {
266 : std::string text =
267 : "sort D = struct one | two; \n"
268 : " \n"
269 : "map f: D -> D; \n"
270 : " \n"
271 : "eqn f = lambda x: D. one; \n"
272 : " \n"
273 : "pbes nu X(d: D, g: D -> D) = \n"
274 : " forall e: D. X(e, g[e -> e]); \n"
275 : " \n"
276 1 : "init X(one, f); \n"
277 : ;
278 1 : pbes p = txt2pbes(text);
279 1 : data::rewriter::strategy rewrite_strategy = data::jitty;
280 1 : pbesinst_finite_algorithm algorithm(rewrite_strategy);
281 2 : mcrl2::pbes_system::detail::pbes_parameter_map parameter_map = mcrl2::pbes_system::detail::parse_pbes_parameter_map(p, "X(*:D)");
282 1 : algorithm.run(p, parameter_map);
283 1 : }
284 :
285 4 : void test_pbesinst_symbolic(const std::string& text)
286 : {
287 4 : pbes p;
288 4 : p = txt2pbes(text);
289 4 : pbesinst_symbolic_algorithm algorithm(p);
290 4 : algorithm.run();
291 4 : }
292 :
293 2 : BOOST_AUTO_TEST_CASE(test_pbesinst_symbolic1)
294 : {
295 1 : test_pbesinst_symbolic(test2);
296 1 : test_pbesinst_symbolic(test4);
297 1 : test_pbesinst_symbolic(test5);
298 1 : test_pbesinst_symbolic(test6);
299 1 : }
300 :
301 : #ifdef MCRL2_EXTENDED_TESTS
302 : BOOST_AUTO_TEST_CASE(test_pbesinst_slow)
303 : {
304 : test_pbes(random1, false, true);
305 : test_pbes(random2, false, true);
306 : }
307 :
308 : // Note: this test takes a lot of time!
309 : BOOST_AUTO_TEST_CASE(test_cabp)
310 : {
311 : std::string CABP_SPECIFICATION =
312 : "% This file contains the cabp protocol as described in section 3.5 of \n"
313 : "% S. Mauw and G.J. Veltink, editors, Algebraic Specification of Communication \n"
314 : "% Protocols, Cambridge tracts in theoretical computer science 36, Cambridge \n"
315 : "% University Press, Cambridge 1993. \n"
316 : "% \n"
317 : "% With two data elements, the generated transition system has 464 states. \n"
318 : "% \n"
319 : "% It is interesting to see the clustering of this statespace in ltsgraph. \n"
320 : "% The statespace after branching bisimulation contains 3 states and is \n"
321 : "% exactly the same as the reduced statespace of the alternating bit protocol. \n"
322 : "% \n"
323 : "% Note that it is interesting to compare the differences of the alternating \n"
324 : "% bit protocol (abp), concurrent alternating bit protocol (cabp), one bit \n"
325 : "% sliding window protocol (onebit) and the alternating bit protocol with \n"
326 : "% independent acknowledgements (par), regarding the implementation, the \n"
327 : "% the number of states and the external behaviour. \n"
328 : " \n"
329 : "%------------------------------- DATA ---------------------------------- \n"
330 : " \n"
331 : "sort DATA = struct d1 | d2; \n"
332 : " \n"
333 : "%------------------------------- error ---------------------------------- \n"
334 : " \n"
335 : "sort error = struct ce | ae; \n"
336 : " \n"
337 : "%------------------------------- bit ------------------------------------ \n"
338 : " \n"
339 : "sort bit = struct bit0 | bit1; \n"
340 : " \n"
341 : "map invert:bit -> bit; \n"
342 : "eqn invert(bit1)=bit0; \n"
343 : " invert(bit0)=bit1; \n"
344 : " \n"
345 : "%------------------------------- Frame ---------------------------------- \n"
346 : " \n"
347 : "sort Frame = struct frame(getd : DATA, getb: bit); \n"
348 : " \n"
349 : "%------------------------------ ACK ----------------------------------- \n"
350 : " \n"
351 : "sort ACK = struct ac; \n"
352 : " \n"
353 : "%------------------------------ act ----------------------------------- \n"
354 : " \n"
355 : "act r1,s2 : DATA; \n"
356 : " c3,r3,s3,c4,r4,s4 : Frame; \n"
357 : " c4,r4,s4,c7,r7,s7 : error; \n"
358 : " c5,r5,s5,c8,r8,s8 : ACK; \n"
359 : " c6,r6,s6,c7,r7,s7 : bit; \n"
360 : " skip; \n"
361 : " \n"
362 : "%------------------------------ proc ----------------------------------- \n"
363 : " \n"
364 : " \n"
365 : "proc S = RM(bit0); \n"
366 : " RM(b:bit) = sum d:DATA.r1(d).SF(frame(d,b)); \n"
367 : " SF(f:Frame) = s3(f).SF(f) + r8(ac).RM(invert(getb(f))); \n"
368 : " \n"
369 : " K = sum f:Frame.r3(f).K(f); \n"
370 : " K(f:Frame) = (skip.s4(f)+skip.s4(ce)+skip).K; \n"
371 : " \n"
372 : " R = RF(bit0); \n"
373 : " RF(b:bit) = sum d:DATA.r4(frame(d,b)).s2(d).s5(ac).RF(invert(b)) \n"
374 : " + sum d:DATA. r4(frame(d,invert(b))).RF(b) \n"
375 : " + r4(ce).RF(b); \n"
376 : " \n"
377 : " AS = AS(bit1); \n"
378 : " AS(b:bit) = r5(ac).AS(invert(b)) + s6(b).AS(b); \n"
379 : " \n"
380 : " L = sum b:bit.r6(b) . L(b); \n"
381 : " L(b:bit) = ( skip.s7(b) + skip.s7(ae) + skip ).L; \n"
382 : " \n"
383 : " AR = AR(bit0); \n"
384 : " AR(b:bit) = ( r7(ae) + r7(invert(b))) . AR(b) \n"
385 : " + r7(b).s8(ac).AR(invert(b)); \n"
386 : " \n"
387 : "init \n"
388 : " hide({c3,c4,c5,c6,c7,c8,skip}, \n"
389 : " allow({c3,c4,c5,c6,c7,c8,skip,r1,s2}, \n"
390 : " comm({r3|s3->c3, r4|s4->c4, r5|s5->c5, r6|s6->c6, \n"
391 : " r7|s7->c7, r8|s8->c8}, \n"
392 : " S || K || R || AS || L || AR ))); \n"
393 : ;
394 :
395 : std::string INFINITELY_OFTEN_SEND = "nu X. mu Y. (<r1(d1)>X || <!r1(d1)>Y)";
396 :
397 : // create a pbes p
398 : lps::specification spec = remove_stochastic_operators(lps::linearise(CABP_SPECIFICATION));
399 : state_formulas::state_formula formula = state_formulas::parse_state_formula(INFINITELY_OFTEN_SEND, spec, false);
400 : bool timed = false;
401 : pbes p = lps2pbes(spec, formula, timed);
402 : pbes_system::detail::instantiate_global_variables(p);
403 :
404 : std::string expr = "(exists d_RM_00: DATA. (val(d_RM_00 == d1) && val(s31_RM == 1)) && X(2, bit0, frame(d_RM_00, b_RM), s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1)) || (((((((((((exists d_RM_00: DATA. (val(!(d_RM_00 == d1)) && val(s31_RM == 1)) && Y(2, bit0, frame(d_RM_00, b_RM), s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1)) || (exists e4_RF1_00: Bool, d4_RF1_00: DATA. val((s32_K == 3 && s33_RF1 == 1) && if(e4_RF1_00, frame(d4_RF1_00, invert(b_RF1)), frame(d4_RF1_00, b_RF1)) == f_K) && Y(s31_RM, b_RM, f_RM, 1, frame(d1, bit0), if(e4_RF1_00, 1, 2), if(e4_RF1_00, d1, d4_RF1_00), b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1))) || val(s32_K == 4 && s33_RF1 == 1) && Y(s31_RM, b_RM, f_RM, 1, frame(d1, bit0), 1, d1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1)) || val(s33_RF1 == 2) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, 3, d1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1)) || val(s35_L == 1) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, 2, b_AS1, s36_AR1, b_AR1)) || (exists e5_L_00: Enum3. val(C3_fun2(e5_L_00, true, true, true) && s35_L == 2) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, C3_fun(e5_L_00, 1, 3, 4), C3_fun3(e5_L_00, bit0, b_L, bit0), s36_AR1, b_AR1))) || val(s35_L == 4 && s36_AR1 == 1) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, 1, bit0, 1, b_AR1)) || (exists e7_AR1_00: Bool. val((s35_L == 3 && s36_AR1 == 1) && if(e7_AR1_00, b_AR1, invert(b_AR1)) == b_L) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, 1, bit0, if(e7_AR1_00, 2, 1), b_AR1))) || val(s33_RF1 == 3) && Y(s31_RM, b_RM, f_RM, s32_K, f_K, 1, d1, invert(b_RF1), invert(b_AS1), s35_L, b_L, s36_AR1, b_AR1)) || (exists e_K_00: Enum3. val(C3_fun2(e_K_00, true, true, true) && s32_K == 2) && Y(s31_RM, b_RM, f_RM, C3_fun(e_K_00, 1, 3, 4), C3_fun1(e_K_00, frame(d1, bit0), f_K, frame(d1, bit0)), s33_RF1, d_RF1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1))) || val(s31_RM == 2 && s32_K == 1) && Y(2, bit0, f_RM, 2, f_RM, s33_RF1, d_RF1, b_RF1, b_AS1, s35_L, b_L, s36_AR1, b_AR1)) || val(s31_RM == 2 && s36_AR1 == 2) && Y(1, invert(getb(f_RM)), frame(d1, bit0), s32_K, f_K, s33_RF1, d_RF1, b_RF1, b_AS1, s35_L, b_L, 1, invert(b_AR1))";
405 : std::string subst = "s31_RM:Pos := 2; b_RM:bit := bit0; f_RM:Frame := frame(d2, bit0); s32_K:Pos := 3; f_K:Frame := frame(d2, bit0); s33_RF1:Pos := 1; d_RF1:DATA := d1; b_RF1:bit := bit0; b_AS1:bit := bit1; s35_L:Pos := 1; b_L:bit := bit0; s36_AR1:Pos := 1; b_AR1:bit := bit0";
406 :
407 : data::mutable_map_substitution<> sigma;
408 : pbes_expression t = parse_pbes_expression(expr, subst, p, sigma);
409 : pbesinst_algorithm algorithm(p.data());
410 : enumerate_quantifiers_rewriter& R = algorithm.rewriter();
411 : data::mutable_indexed_substitution<> sigma1;
412 : for (const auto& i: sigma)
413 : {
414 : sigma1[i.first] = i.second;
415 : }
416 : pbes_expression z = R(t, sigma1);
417 : }
418 :
419 : // Note: this test takes a lot of time!
420 : BOOST_AUTO_TEST_CASE(test_balancing_plat)
421 : {
422 : using namespace pbes_system;
423 :
424 : const std::string BALANCE_PLAT_SPECIFICATION =
425 : " % Specification of balancing coins to determine the single coin with \n"
426 : " % different weight. \n"
427 : " \n"
428 : " % C: Total number of coins \n"
429 : " map C: Nat; \n"
430 : " eqn C = 12; \n"
431 : " \n"
432 : " % Every coin can be in one of four categories: NHL, NH, NL, and N, \n"
433 : " % where: \n"
434 : " % N: possibly normal weight \n"
435 : " % H: possibly heavy weight \n"
436 : " % L: possibly light weight \n"
437 : " % We count the number of coins in every category, but we do not count \n"
438 : " % the number of coins in N explicitly, because: \n"
439 : " % |N| = C - ( |NHL| + |NH| + |NL| ) \n"
440 : " \n"
441 : " map \n"
442 : " lexleq: Nat # Nat # Nat # Nat # Nat # Nat -> Bool; \n"
443 : " is_better: Nat # Nat # Nat # Nat # Nat # Nat -> Bool; \n"
444 : " is_useful: Nat # Nat # Nat # Nat # Nat # Nat # Nat # Nat # Nat -> Bool; \n"
445 : " is_possible: Nat # Nat # Nat # Nat # Nat # Nat # Nat # Nat # Nat -> Bool; \n"
446 : " \n"
447 : " var d1,d2,d3,e1,e2,e3,f1,f2,f3: Nat; \n"
448 : " \n"
449 : " eqn \n"
450 : " % lexicographical ordening on distributions; this is needed to \n"
451 : " % eliminate half of the possibilities for balancing: only consider \n"
452 : " % X vs. Y and not Y vs. X, if X <= Y. \n"
453 : " lexleq(d1,d2,d3,e1,e2,e3) = \n"
454 : " d1<e1 || (d1==e1 && d2<e2) || (d1==e1 && d2==e2 && d3<=e3); \n"
455 : " \n"
456 : " % determines whether a distribution d is 'better than' a \n"
457 : " % distribution e, in the sense that in d we have more certainty (or \n"
458 : " % less uncertainty) about a larger number of coins \n"
459 : " is_better(d1,d2,d3,e1,e2,e3) = d1+d2+d3 < e1+e2+e3 || d1 < e1; \n"
460 : " \n"
461 : " % determines whether weighing e against f is useful in situation d: \n"
462 : " % all possible outcomes should be an improvement \n"
463 : " is_useful(d1,d2,d3,e1,e2,e3,f1,f2,f3) = \n"
464 : " is_better(Int2Nat(d1-e1-f1),Int2Nat(d2-e2-f2),Int2Nat(d3-e3-f3),d1,d2,d3) && \n"
465 : " is_better(0,e1+e2,f1+f3,d1,d2,d3) && \n"
466 : " is_better(0,f1+f2,e1+e3,d1,d2,d3); \n"
467 : " \n"
468 : " % determines whether weighing e against f is possible in situation \n"
469 : " % d: \n"
470 : " % - for every category X: X(e) + X(f) <= X(d) \n"
471 : " % - if total(e) < total(f) then N 'normal' coins are added to e \n"
472 : " % such that N = total(f) - total(e), so N 'normal' coins must \n"
473 : " % be available in situation d, i.e. N <= C - total(d). \n"
474 : " % - analogously if total(e) > total(f). \n"
475 : " is_possible(d1,d2,d3,e1,e2,e3,f1,f2,f3) = \n"
476 : " e1+f1 <= d1 && e2+f2 <= d2 && e3+f3 <= d3 && \n"
477 : " ( e1+e2+e3 == f1+f2+f3 || \n"
478 : " (e1+e2+e3 < f1+f2+f3 && f1+f2+f3 - e1-e2-e3 <= C - d1-d2-d3) || \n"
479 : " (f1+f2+f3 < e1+e2+e3 && e1+e2+e3 - f1-f2-f3 <= C - d1-d2-d3) \n"
480 : " ); \n"
481 : " \n"
482 : " act weigh, equal, greater, smaller: Nat # Nat # Nat # Nat # Nat # Nat; \n"
483 : " done; \n"
484 : " \n"
485 : " proc BalancingAct(NHL,NH,NL:Nat) = \n"
486 : " % we're done if |NHL| + |NH| + |NL| == 1 \n"
487 : " (NHL+NH+NL == 1) -> done . BalancingAct(NHL,NH,NL) \n"
488 : " \n"
489 : " + (NHL+NH+NL > 1) -> \n"
490 : " ( \n"
491 : " sum nhl_l,nh_l,nl_l:Nat, nhl_r,nh_r,nl_r:Nat . \n"
492 : " \n"
493 : " (lexleq(nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) && \n"
494 : " is_possible(NHL,NH,NL,nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) && \n"
495 : " is_useful(NHL,NH,NL,nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r)) -> \n"
496 : " \n"
497 : " weigh(nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) . \n"
498 : " ( \n"
499 : " % left and right have equal weight \n"
500 : " ((NHL-nhl_l-nhl_r + NH-nh_l-nh_r + NL-nl_l-nl_r > 0) -> \n"
501 : " equal(nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) . \n"
502 : " BalancingAct(Int2Nat(NHL-nhl_l-nhl_r), \n"
503 : " Int2Nat(NH-nh_l-nh_r), \n"
504 : " Int2Nat(NL-nl_l-nl_r))) \n"
505 : " + \n"
506 : " % left is heavier than right \n"
507 : " ((nhl_l+nh_l + nhl_r+nl_r > 0) -> \n"
508 : " greater(nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) . \n"
509 : " BalancingAct(0,nhl_l+nh_l,nhl_r+nl_r)) \n"
510 : " + \n"
511 : " % left is lighter than right \n"
512 : " ((nhl_r+nh_r + nhl_l+nl_l > 0) -> \n"
513 : " smaller(nhl_l,nh_l,nl_l,nhl_r,nh_r,nl_r) . \n"
514 : " BalancingAct(0,nhl_r+nh_r,nhl_l+nl_l)) \n"
515 : " ) \n"
516 : " ); \n"
517 : " \n"
518 : " init BalancingAct(C,0,0); \n"
519 : ;
520 :
521 : lps::specification spec = remove_stochastic_operators(lps::linearise(BALANCE_PLAT_SPECIFICATION));
522 : state_formulas::state_formula formula = state_formulas::parse_state_formula(lps::detail::NO_DEADLOCK(), spec, false);
523 : bool timed = false;
524 : pbes p = lps2pbes(spec, formula, timed);
525 : pbes_system::pbesinst_algorithm algorithm(p.data());
526 : algorithm.run(p);
527 : pbes q = algorithm.get_result();
528 : }
529 : #endif // MCRL2_EXTENDED_TESTS
|
