Line data Source code
1 : // Author(s): Wieger Wesselink, Jan Friso Groote
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 linearization_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE linearization_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #ifndef MCRL2_SKIP_LONG_TESTS
16 :
17 : #include "mcrl2/data/detail/rewrite_strategies.h"
18 : #include "mcrl2/lps/is_well_typed.h"
19 : #include "mcrl2/lps/linearise.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::lps;
23 :
24 : typedef data::rewriter::strategy rewrite_strategy;
25 : typedef std::vector<rewrite_strategy> rewrite_strategy_vector;
26 :
27 156 : void run_linearisation_instance(const std::string& spec, const t_lin_options& options, bool expect_success)
28 : {
29 156 : if (expect_success)
30 : {
31 144 : BOOST_CHECK(mcrl2::lps::detail::is_well_typed(linearise(spec, options)));
32 : }
33 : else
34 : {
35 24 : BOOST_CHECK_THROW(linearise(spec, options), mcrl2::runtime_error);
36 : }
37 156 : }
38 :
39 26 : void run_linearisation_test_case(const std::string& spec, const bool expect_success = true)
40 : {
41 : // Set various rewrite strategies
42 26 : rewrite_strategy_vector rewrite_strategies = data::detail::get_test_rewrite_strategies(false);
43 26 : std::clog << "Tested specification:\n" << spec << "\n------------------------------------\n";
44 :
45 52 : for (rewrite_strategy_vector::const_iterator i = rewrite_strategies.begin(); i != rewrite_strategies.end(); ++i)
46 : {
47 26 : std::clog << std::endl << "Testing with rewrite strategy " << *i << std::endl;
48 :
49 26 : t_lin_options options;
50 26 : options.rewrite_strategy=*i;
51 :
52 26 : std::clog << " Default options" << std::endl;
53 26 : run_linearisation_instance(spec, options, expect_success);
54 :
55 26 : std::clog << " Linearisation method regular2" << std::endl;
56 26 : options.lin_method=lmRegular2;
57 26 : run_linearisation_instance(spec, options, expect_success);
58 :
59 26 : std::clog << " Linearisation method stack" << std::endl;
60 26 : options.lin_method=lmStack;
61 26 : run_linearisation_instance(spec, options, expect_success);
62 :
63 26 : std::clog << " Linearisation method stack; binary enabled" << std::endl;
64 26 : options.binary=true;
65 26 : run_linearisation_instance(spec, options, expect_success);
66 :
67 26 : std::clog << " Linearisation method regular; binary enabled" << std::endl;
68 26 : options.lin_method=lmRegular;
69 26 : run_linearisation_instance(spec, options, expect_success);
70 :
71 26 : std::clog << " Linearisation method regular; no intermediate clustering" << std::endl;
72 26 : options.binary=false; // reset binary
73 26 : options.no_intermediate_cluster=true;
74 26 : run_linearisation_instance(spec, options, expect_success);
75 : }
76 26 : }
77 :
78 2 : BOOST_AUTO_TEST_CASE(various_case_27)
79 : {
80 : const std::string various_case_27=
81 : "act a:Pos;\n"
82 : "proc P(id,n:Pos)=(id<n) -> a(n).P(id,n);\n"
83 : " Q(n:Pos)=P(1,n)||P(2,n)||P(3,n);\n"
84 1 : "init Q(15);\n";
85 1 : run_linearisation_test_case(various_case_27);
86 1 : }
87 :
88 2 : BOOST_AUTO_TEST_CASE(various_case_28)
89 : {
90 : const std::string various_case_28=
91 : "sort A=List(Nat->Nat);"
92 : "T=struct f(Nat->Nat);"
93 : "act b:A;"
94 : "proc P(a:A)=b(a).P([]);"
95 1 : "init P([lambda n:Nat.n]);";
96 1 : run_linearisation_test_case(various_case_28);
97 1 : }
98 :
99 2 : BOOST_AUTO_TEST_CASE(various_case_29)
100 : {
101 : const std::string various_case_29=
102 : "sort Data = struct x;"
103 : "Coloured = struct flow(data : Data) | noflowG | noflowR;"
104 : "act A, B : Coloured;"
105 : "proc Sync = ( (A(noflowG) | B(noflowR)) + "
106 : " (A(noflowR) | B(noflowR)) + "
107 : " (sum d : Data.(A(flow(d)) | B(flow(d)))) "
108 : " ).Sync;"
109 1 : "init Sync;";
110 1 : run_linearisation_test_case(various_case_29);
111 1 : }
112 :
113 : // The test case below is to test whether the elements of a multi-action
114 : // are dealt with properly when they occur in a subexpression. The linearised
115 : // process below should have three and not two summand.
116 2 : BOOST_AUTO_TEST_CASE(various_case_30)
117 : {
118 : const std::string various_case_30=
119 : "act a;"
120 : " b,b':Nat;"
121 1 : "init a.(b(0)|b'(0))+a.(b(0)|b(0));";
122 1 : run_linearisation_test_case(various_case_30);
123 1 : }
124 :
125 2 : BOOST_AUTO_TEST_CASE(various_case_31)
126 : {
127 : const std::string various_case_31=
128 : "act a:List(List(Nat));"
129 : "proc X(x:List(List(Nat)))=a(x).delta;"
130 1 : "init X([[]]);";
131 1 : run_linearisation_test_case(various_case_31);
132 1 : }
133 :
134 : // Original name: LR2plus.mcrl2
135 : // This example can only be parsed unambiguously by an LR(k) parser generator
136 : // for the current grammar, where k > 1. Namely, process expression 'a + tau'
137 : // cannot be parsed unambiguously. After parsing the identifier 'a', it has to
138 : // be determined if 'a' is an action or process reference, or if 'a' is a data
139 : // expression, viz. part of the left hand side of a conditional process
140 : // expression. With a lookahead of 1, we may only use the '+' as extra
141 : // information, which is not enough, because this symbol is also ambiguous.
142 :
143 2 : BOOST_AUTO_TEST_CASE(various_case_LR2plus)
144 : {
145 : const std::string various_case_LR2plus=
146 : "act\n"
147 : " a;\n\n"
148 : "init\n"
149 1 : " a + tau;";
150 1 : run_linearisation_test_case(various_case_LR2plus);
151 1 : }
152 :
153 : // Original name: LR2par.mcrl2
154 : // This example can only be parsed unambiguously by an LR(k) parser generator
155 : // for the current grammar, where k > 1. Namely, process expression '(a)'
156 : // cannot be parsed unambiguously. After parsing the left parenthesis '(', it
157 : // has to be determined if it is part of a process or data expression, viz.
158 : // part of the left hand side of a conditional process expression. With a
159 : // lookahead of 1, we may only use the identifier 'a' as extra information,
160 : // which is not enough, because this symbol is also ambiguous.
161 :
162 2 : BOOST_AUTO_TEST_CASE(various_case_LR2par)
163 : {
164 : const std::string various_case_LR2par=
165 : "act\n"
166 : " a;\n\n"
167 : "init\n"
168 1 : " (a);";
169 1 : run_linearisation_test_case(various_case_LR2par);
170 1 : }
171 :
172 :
173 : // This test case is a simple test to test sort normalisation in the lineariser,
174 : // added because assertion failures in the domineering example were observed
175 2 : BOOST_AUTO_TEST_CASE(various_case_32)
176 : {
177 : const std::string various_case_32 =
178 : "sort Position = struct Full | Empty;\n"
179 : " Row = List(Position);\n"
180 : "\n"
181 : "proc P(r:Row) = delta;\n"
182 1 : "init P([Empty]);\n"
183 : ;
184 1 : run_linearisation_test_case(various_case_32);
185 1 : }
186 :
187 : // This test case is a test to check whether constant elimination in the
188 : // linearizer goes well. This testcase is inspired by an example by Chilo
189 : // van Best. The problem is that the constant x:Nat below may not be
190 : // recorded in the assignment list of process P, and therefore forgotten
191 2 : BOOST_AUTO_TEST_CASE(various_case_33)
192 : {
193 : const std::string various_case_33 =
194 : "act a:Nat; "
195 : "proc P(x:Nat,b:Bool,r:Real) = a(x).P(x,!b,r); "
196 : " P(x:Nat) = P(x,true,1); "
197 1 : "init P(1); "
198 : ;
199 1 : run_linearisation_test_case(various_case_33);
200 1 : }
201 :
202 : // The test case below checks whether the alphabet conversion does not accidentally
203 : // reverse the order of hide and sum operators. If this happens the linearizer will
204 : // not be able to linearize this process
205 2 : BOOST_AUTO_TEST_CASE(various_case_34)
206 : {
207 : const std::string various_case_34 =
208 : "act a; "
209 :
210 : "proc X = a.X;"
211 : "proc Y = sum n:Nat. X;"
212 :
213 1 : "init hide({a}, sum n:Nat. X);"
214 : ;
215 1 : run_linearisation_test_case(various_case_34);
216 1 : }
217 :
218 2 : BOOST_AUTO_TEST_CASE(various_case_par)
219 : {
220 : const std::string various_par =
221 : "act a;\n"
222 1 : "init a || a;\n"
223 : ;
224 1 : run_linearisation_test_case(various_par);
225 1 : }
226 :
227 2 : BOOST_AUTO_TEST_CASE(gpa_10_3)
228 : {
229 : const std::string various_gpa_10_3 =
230 : "act\n"
231 : " c,r_dup, s_dup1, s_dup2, r_inc, s_inc, r_mul1, r_mul2, s_mul: Int;\n"
232 : "proc\n"
233 : " Dup = sum x:Int. r_dup(x) | s_dup1(x) | s_dup2(x) . Dup;\n"
234 : " Inc = sum x:Int. r_inc(x) | s_inc(x+1) . Inc;\n"
235 : " Mul = sum x,y:Int. r_mul1(x) | r_mul2(y) | s_mul(x*y) . Mul;\n"
236 : " Dim = allow({r_dup | s_mul},\n"
237 : " hide({c},comm({s_dup1 | r_mul1 -> c , s_dup2 | r_inc -> c, s_inc | r_mul2 ->c},\n"
238 : " Dup || Inc || Mul\n"
239 : " ))\n"
240 : " );\n"
241 1 : "init Dim;\n"
242 : ;
243 1 : run_linearisation_test_case(various_gpa_10_3);
244 1 : }
245 :
246 : /* The following test cases fail because the n-parallel support in the alphabet reductions is broken
247 : * (Checked JK 31/8/2010)
248 : */
249 : /*
250 : BOOST_AUTO_TEST_CASE(philosophers)
251 : {
252 : const std::string various_philosophers =
253 : "map K: Pos;\n"
254 : "eqn K = 10;\n"
255 : "act get,_get,__get,put,_put,__put: Pos#Pos;\n"
256 : " eat: Pos;\n"
257 : "proc\n"
258 : " Phil(n:Pos) = _get(n,n)._get(n,if(n==K,1,n+1)).eat(n)._put(n,n)._put(n,if(n==K,1,n+1)).Phil(n);\n"
259 : " Fork(n:Pos) = sum m:Pos.get(m,n).put(m,n).Fork(n);\n"
260 : " ForkPhil(n:Pos) = Fork(n) || Phil(n);\n"
261 : " KForkPhil(p:Pos) =\n"
262 : " (p>1) -> (ForkPhil(p)||KForkPhil(max(p-1,1)))<>ForkPhil(1);\n"
263 : "init allow( { __get, __put, eat },\n"
264 : " comm( { get|_get->__get, put|_put->__put },\n"
265 : " KForkPhil(K)\n"
266 : " ));\n"
267 : ;
268 : run_linearisation_test_case(various_philosophers);
269 : }
270 :
271 : BOOST_AUTO_TEST_CASE(philosophers_nat)
272 : {
273 : const std::string various_philosophers_nat =
274 : "map K: Nat;\n"
275 : "eqn K = 10;\n"
276 : "act get,_get,__get,put,_put,__put: Nat#Nat;\n"
277 : " eat: Nat;\n"
278 : "proc\n"
279 : " Phil(n:Nat) = _get(n,n)._get(n,if(n==K,1,n+1)).eat(n)._put(n,n)._put(n,if(n==K,1,n+1)).Phil(n);\n"
280 : " Fork(n:Nat) = sum m:Nat.get(m,n).put(m,n).Fork(n);\n"
281 : " ForkPhil(n:Nat) = Fork(n) || Phil(n);\n"
282 : " KForkPhil(p:Nat) =\n"
283 : " (p>1) -> (ForkPhil(p)||KForkPhil(max(p-1,1)))<>ForkPhil(1);\n"
284 : "init allow( { __get, __put, eat },\n"
285 : " comm( { get|_get->__get, put|_put->__put },\n"
286 : " KForkPhil(K)\n"
287 : " ));\n"
288 : ;
289 : run_linearisation_test_case(various_philosophers_nat);
290 : }
291 : */
292 :
293 2 : BOOST_AUTO_TEST_CASE(sort_aliases)
294 : {
295 : const std::string various_sort_aliases =
296 : "sort Bits = struct b0|b1;\n"
297 : " t_sys_regset_fsm_state = Bits;\n"
298 : " t_timer_counter_fsm_state = Bits;\n"
299 : "map timer_counter_fsm_state_idle: t_timer_counter_fsm_state;\n"
300 : "act a:Bits;\n"
301 : "proc P(d:Bits)=a(d).delta;\n"
302 : "glob globd:Bits;\n"
303 1 : "init P(globd);\n"
304 : ;
305 1 : run_linearisation_test_case(various_sort_aliases);
306 1 : }
307 :
308 2 : BOOST_AUTO_TEST_CASE(test_aliases_complex)
309 : {
310 : const std::string spec =
311 : "sort\n"
312 : " Bits = struct singleBit (bit: Bool)?isSingleBit | bitVector (bitVec:List(Bool))?isBitVector;\n"
313 : " t_sys_regset_fsm_state = Bits;\n"
314 : " t_timer_counter_fsm_state = Bits;\n"
315 : "map\n"
316 : " repeat : Bool # Nat -> Bits;\n"
317 : " repeat_rec : Bool # Nat -> List(Bool);\n"
318 : "var\n"
319 : " b:Bool;\n"
320 : " n:Nat;\n"
321 : "eqn\n"
322 : " repeat(b,n) = if(n <= 1, singleBit(b), bitVector(repeat_rec(b,n)));\n"
323 : "act a:Bits;\n"
324 1 : "init a(repeat(true,32)).delta;\n";
325 1 : run_linearisation_test_case(spec);
326 1 : }
327 :
328 2 : BOOST_AUTO_TEST_CASE(test_bug_775a)
329 : {
330 : const std::string spec =
331 : "sort V = struct v1( l: Bool );\n"
332 : "act a: List( Bool );\n"
333 : "sort B = Bool -> List(Bool);\n"
334 : "proc X( M: B ) = \n"
335 : " sum v:V. a( [] ) \n"
336 : "+ sum v:V. a( M(l(v)))\n"
337 : ";\n"
338 1 : "init X( lambda i: Bool. [] );\n";
339 1 : run_linearisation_test_case(spec);
340 1 : }
341 :
342 2 : BOOST_AUTO_TEST_CASE(test_bug_775b)
343 : {
344 : const std::string spec =
345 : "sort V = struct v1( l: Bool );\n"
346 : "act a: List( Bool );\n"
347 : "sort B = Bool -> List(Bool);\n"
348 : "proc X( M: B ) = \n"
349 : " sum v:V. a( M(l(v)))\n"
350 : "+ sum v:V. a( [] ) \n"
351 : ";\n"
352 1 : "init X( lambda i: Bool. [] );\n";
353 1 : run_linearisation_test_case(spec);
354 1 : }
355 :
356 2 : BOOST_AUTO_TEST_CASE(test_bug_alphabet_reduction)
357 : {
358 : const std::string spec =
359 : "sort Variables = struct s;\n"
360 : "\n"
361 : "act send_c, recv_c, comm_c: Bool;\n"
362 : " chng: Set(Variables);\n"
363 : "\n"
364 : "init allow( { comm_c | chng | chng } ,\n"
365 : " comm( { send_c | recv_c -> comm_c,\n"
366 : " chng | chng -> chng},\n"
367 : " send_c(false) | chng( {} ) || recv_c(false) | chng( {s} )\n"
368 1 : " ) );\n";
369 1 : run_linearisation_test_case(spec);
370 1 : }
371 :
372 2 : BOOST_AUTO_TEST_CASE(test_bug_alphabet_reduction1)
373 : {
374 : const std::string spec =
375 : "act a: Bool;\n"
376 : " b: Nat;\n"
377 : "\n"
378 : "proc X = allow( {b | a | a },\n"
379 : " a(true)| b(5) | a(false) );\n"
380 : "\n"
381 1 : "init X;\n";
382 1 : run_linearisation_test_case(spec);
383 1 : }
384 :
385 : // The testcase below is added because the typechecker could not deal with this
386 : // case. The three options for the action a caused it to become confused.
387 2 : BOOST_AUTO_TEST_CASE(test_multiple_action_types)
388 : {
389 : const std::string spec =
390 : "sort Id = Pos;\n"
391 : "\n"
392 : "map FALSE: Id -> Bool;\n"
393 : "var n: Id;\n"
394 : "eqn FALSE(n) = false;\n"
395 : "\n"
396 : "act a: (Id -> Bool);\n"
397 : " a: Bool;\n"
398 : " a: Pos;\n"
399 : "\n"
400 : "proc P = a(FALSE) . delta;\n"
401 1 : "init P;\n";
402 :
403 1 : run_linearisation_test_case(spec);
404 1 : }
405 :
406 : // Test case for bug #1085
407 2 : BOOST_AUTO_TEST_CASE(bug_1085)
408 : {
409 : const std::string spec =
410 : "proc P = tau. a | b | c;\n"
411 : "act a,b,c;\n"
412 1 : "init P;\n";
413 :
414 1 : run_linearisation_test_case(spec);
415 1 : }
416 :
417 2 : BOOST_AUTO_TEST_CASE(bug_978)
418 : {
419 : const std::string spec =
420 : "act rd,wr:Bool;\n"
421 : "proc R(a,b : Bool) = \n"
422 : " rd(a) . R() +\n"
423 : " rd(b) . R() + \n"
424 : " sum b:Bool. wr(b) . R(a=b);\n"
425 1 : "init R(true,true);\n";
426 1 : run_linearisation_test_case(spec);
427 1 : }
428 :
429 2 : BOOST_AUTO_TEST_CASE(not_properly_ordered_assignments)
430 : {
431 : const std::string spec =
432 : "proc R(a,b : Bool) = \n"
433 : " tau . R(a=true,b=false) +\n"
434 : " tau . R(b=false,a=false); \n"
435 1 : "init R(true,true);\n";
436 1 : run_linearisation_test_case(spec);
437 1 : }
438 :
439 2 : BOOST_AUTO_TEST_CASE(the_bound_c_may_not_show_up_in_linear_process)
440 : {
441 : const std::string spec =
442 : "act \n"
443 : "rcv_req; \n"
444 : "snd_return : Bool; \n"
445 : "internal; \n"
446 : " \n"
447 : "proc \n"
448 : " \n"
449 : "test1 = \n"
450 : "( \n"
451 : " rcv_req. \n"
452 : " sum c:Bool. \n"
453 : " ( \n"
454 : " internal.snd_return(c) \n"
455 : " ). \n"
456 : " test1 \n"
457 : "); \n"
458 : " \n"
459 1 : "init test1; \n";
460 1 : run_linearisation_test_case(spec);
461 1 : }
462 :
463 2 : BOOST_AUTO_TEST_CASE(process_parameters_with_different_types_can_cause_problems)
464 : {
465 : const std::string spec =
466 : "proc P(x:Nat)=tau.Q(true); \n"
467 : " Q(x:Bool)=tau.P(1); \n"
468 1 : "init P(1);\n";
469 :
470 1 : run_linearisation_test_case(spec);
471 1 : }
472 :
473 2 : BOOST_AUTO_TEST_CASE(unguarded_recursion)
474 : {
475 : const std::string spec =
476 : "proc P=P; \n"
477 1 : "init P;\n";
478 :
479 1 : run_linearisation_test_case(spec,false);
480 1 : }
481 :
482 2 : BOOST_AUTO_TEST_CASE(unguarded_recursion_with_parallel_operator)
483 : {
484 : const std::string spec =
485 : "proc P=P||P; \n"
486 1 : "init P;\n";
487 :
488 1 : run_linearisation_test_case(spec,false);
489 1 : }
490 :
491 : #else // ndef MCRL2_SKIP_LONG_TESTS
492 :
493 : BOOST_AUTO_TEST_CASE(skip_linearization_test)
494 : {
495 : }
496 :
497 : #endif // ndef MCRL2_SKIP_LONG_TESTS
498 :
|
