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_test1.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE linearization_test4
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 : #include "utility.h"
25 :
26 : // Here various testcases are checked, which have been used in
27 : // debugging the translation of the linearizer to the new data
28 : // library.
29 2 : BOOST_AUTO_TEST_CASE(various_case_1)
30 : {
31 1 : run_linearisation_test_case(
32 : "init delta;"
33 : );
34 1 : }
35 :
36 2 : BOOST_AUTO_TEST_CASE(various_case_2)
37 : {
38 : const std::string various_case_2=
39 : "act a;"
40 : "proc X=a.X;"
41 1 : "init X;";
42 1 : run_linearisation_test_case(various_case_2);
43 1 : }
44 :
45 2 : BOOST_AUTO_TEST_CASE(various_case_3)
46 : {
47 : const std::string various_case_3=
48 : "sort D = struct d1 | d2;"
49 : " Error = struct e;"
50 : "act r2: D # Bool;"
51 : " s3: D # Bool;"
52 : " s3: Error;"
53 : " i;"
54 : "proc K = sum d:D,b:Bool. r2(d,b).(i.s3(d,b)+i.s3(e)).K;"
55 1 : "init K;";
56 1 : run_linearisation_test_case(various_case_3);
57 1 : }
58 :
59 2 : BOOST_AUTO_TEST_CASE(various_case_4)
60 : {
61 : const std::string various_case_4=
62 : "act a:Nat;"
63 : "proc X=sum n:Nat. (n==0)->a(n).X;"
64 1 : "init X;";
65 1 : run_linearisation_test_case(various_case_4);
66 1 : }
67 :
68 2 : BOOST_AUTO_TEST_CASE(various_case_5)
69 : {
70 : const std::string various_case_5=
71 : "act a,b,c;"
72 : "proc X=a.X;"
73 : " Y=b.Y;"
74 1 : "init X||Y;";
75 1 : run_linearisation_test_case(various_case_5);
76 1 : }
77 :
78 2 : BOOST_AUTO_TEST_CASE(various_case_6)
79 : {
80 : const std::string various_case_6=
81 : "act a1,a2,b,c;"
82 : "proc X=a1.a2.X;"
83 : " Y=b.Y;"
84 1 : "init comm({a1|b->c},X||Y);";
85 1 : run_linearisation_test_case(various_case_6);
86 1 : }
87 :
88 2 : BOOST_AUTO_TEST_CASE(various_case_7)
89 : {
90 : const std::string various_case_7=
91 : "proc X=tau.X;"
92 1 : "init X;";
93 1 : run_linearisation_test_case(various_case_7);
94 1 : }
95 :
96 2 : BOOST_AUTO_TEST_CASE(various_case_8)
97 : {
98 : const std::string various_case_8=
99 : "act a,b;"
100 : "proc X= (a|b).X;"
101 1 : "init X;";
102 1 : run_linearisation_test_case(various_case_8);
103 1 : }
104 :
105 2 : BOOST_AUTO_TEST_CASE(various_case_9)
106 : {
107 : const std::string various_case_9=
108 : "act a;"
109 1 : "init allow({a},a.a.delta);";
110 1 : run_linearisation_test_case(various_case_9);
111 1 : }
112 :
113 2 : BOOST_AUTO_TEST_CASE(various_case_10)
114 : {
115 : const std::string various_case_10=
116 : "act a,b,c;"
117 1 : "init comm({a|b->c},(a|b).delta);";
118 1 : run_linearisation_test_case(various_case_10);
119 1 : }
120 :
121 2 : BOOST_AUTO_TEST_CASE(various_case_11)
122 : {
123 : const std::string various_case_11=
124 : "act a,b,c:Nat;"
125 : "map n:Nat;"
126 1 : "init comm({a|b->c},(a(3)|b(n)));";
127 1 : run_linearisation_test_case(various_case_11);
128 1 : }
129 :
130 2 : BOOST_AUTO_TEST_CASE(various_case_12)
131 : {
132 : const std::string various_case_12=
133 : "act c2:Nat#Nat;"
134 1 : "init allow({c2},c2(3,5));";
135 1 : run_linearisation_test_case(various_case_12);
136 1 : }
137 :
138 2 : BOOST_AUTO_TEST_CASE(various_case_13)
139 : {
140 : const std::string various_case_13=
141 : "sort D = struct d1 | d2;"
142 : "act r1,s4: D;"
143 : "proc S(b:Bool) = sum d:D. r1(d).S(true);"
144 1 : "init S(false);";
145 1 : run_linearisation_test_case(various_case_13);
146 1 : }
147 :
148 2 : BOOST_AUTO_TEST_CASE(various_case_14)
149 : {
150 : const std::string various_case_14=
151 : "act r1: Bool;"
152 : "proc S(d:Bool) = sum d:Bool. r1(d).S(true);"
153 1 : "init S(false);";
154 1 : run_linearisation_test_case(various_case_14);
155 1 : }
156 :
157 2 : BOOST_AUTO_TEST_CASE(various_case_15)
158 : {
159 : const std::string various_case_15=
160 : "act a;"
161 1 : "init (a+a.a+a.a.a+a.a.a.a).delta;";
162 1 : run_linearisation_test_case(various_case_15);
163 1 : }
164 :
165 2 : BOOST_AUTO_TEST_CASE(various_case_16)
166 : {
167 : const std::string various_case_16=
168 : "act s6,r6,c6, i;"
169 : "proc T = r6.T;"
170 : " K = i.K;"
171 : " L = s6.L;"
172 1 : "init comm({r6|s6->c6},T || K || L);";
173 1 : run_linearisation_test_case(various_case_16);
174 1 : }
175 :
176 2 : BOOST_AUTO_TEST_CASE(various_case_17)
177 : {
178 : const std::string various_case_17=
179 : "act s3,r3,c3,s6;"
180 : "proc R = r3.R;"
181 : " K = s3.K;"
182 : " L = s6.L;"
183 1 : "init comm({r3|s3->c3}, K || L || R);";
184 1 : run_linearisation_test_case(various_case_17);
185 1 : }
186 :
187 2 : BOOST_AUTO_TEST_CASE(various_case_18)
188 : {
189 : const std::string various_case_18=
190 : "act a,b,c,d,e;"
191 1 : "init comm({c|d->b},(a|b|c|d|e).delta);";
192 1 : run_linearisation_test_case(various_case_18);
193 1 : }
194 :
195 2 : BOOST_AUTO_TEST_CASE(various_case_19)
196 : {
197 : const std::string various_case_19=
198 : "act a,b,c,d,e;"
199 1 : "init comm({e|d->b},(a|b|c|d|e).delta);";
200 1 : run_linearisation_test_case(various_case_19);
201 1 : }
202 :
203 2 : BOOST_AUTO_TEST_CASE(various_case_20)
204 : {
205 : const std::string various_case_20=
206 : "act a:Nat;"
207 : "proc X(n:Nat)="
208 : " sum n:Nat.(n>25) -> a(n).X(n)+"
209 : " sum n:Nat.(n>25) -> a(n).X(n)+"
210 : " (n>25) -> a(n).X(n);"
211 1 : "init X(1);";
212 1 : run_linearisation_test_case(various_case_20);
213 1 : }
214 :
215 2 : BOOST_AUTO_TEST_CASE(various_case_21)
216 : {
217 : const std::string various_case_21=
218 : "act a,b:Pos;"
219 : "proc X(m:Pos)= sum n:Nat. (n<1) -> a(1)|b(1)@1.X(1)+"
220 : " sum n:Nat. (n<2) -> a(2)|b(2)@2.X(2)+"
221 : " sum n:Nat. (n<3) -> a(3)|b(3)@3.X(3)+"
222 : " sum n:Nat. (n<4) -> a(4)|b(4)@4.X(4)+"
223 : " sum n:Nat. (n<5) -> a(5)|b(5)@5.X(5);"
224 1 : "init X(1);";
225 1 : run_linearisation_test_case(various_case_21);
226 1 : }
227 :
228 2 : BOOST_AUTO_TEST_CASE(various_case_22)
229 : {
230 : const std::string various_case_22=
231 : "% This test is expected to fail with a proper error message.\n"
232 : "act a;\n"
233 : "proc P = (a || a) . P;\n"
234 1 : "init P;\n";
235 1 : run_linearisation_test_case(various_case_22, false);
236 1 : }
237 :
238 2 : BOOST_AUTO_TEST_CASE(various_case_23)
239 : {
240 : const std::string various_case_23=
241 : "act a,b;"
242 1 : "init a@1.b@2.delta||tau.tau;";
243 1 : run_linearisation_test_case(various_case_23);
244 1 : }
245 :
246 2 : BOOST_AUTO_TEST_CASE(various_case_24)
247 : {
248 : const std::string various_case_24=
249 : "act a: Pos;"
250 : "glob x: Pos;"
251 : "proc P = a(x).P;"
252 1 : "init P;";
253 1 : run_linearisation_test_case(various_case_24);
254 1 : }
255 :
256 : // The testcase below is designed to test the constant elimination in the lineariser.
257 : // Typically, x1 and x2 can be eliminated as they are always constant. Care must be
258 : // taken however that the variable y does not become unbound in the process.
259 2 : BOOST_AUTO_TEST_CASE(various_case_25)
260 : {
261 : const std::string various_case_25=
262 : "act a:Pos#Pos#Pos;"
263 : " b;"
264 : "proc Q(y:Pos)=P(y,1,1)||delta;"
265 : " P(x1,x2,x3:Pos)=a(x1,x2,x3).P(x1,x2,x3+1);"
266 1 : "init Q(2);";
267 1 : run_linearisation_test_case(various_case_25);
268 1 : }
269 :
270 : // The following testcase exhibits a problem that occurred in the lineariser in
271 : // August 2009. The variable m would only be partly renamed, and show up as an
272 : // undeclared variable in the resulting LPS. The LPS turned out to be not well
273 : // typed.
274 2 : BOOST_AUTO_TEST_CASE(various_case_26)
275 : {
276 : const std::string various_case_26=
277 : "act r,s1,s2:Nat;\n"
278 : "proc P=sum m:Nat.r(m).((m==1)->s1(m).P+(m==2)->P+P);\n"
279 1 : "init P;\n";
280 1 : run_linearisation_test_case(various_case_26);
281 1 : }
282 :
283 : #else // ndef MCRL2_SKIP_LONG_TESTS
284 :
285 : BOOST_AUTO_TEST_CASE(skip_linearization_test)
286 : {
287 : }
288 :
289 : #endif // ndef MCRL2_SKIP_LONG_TESTS
290 :
|
