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 process_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE process_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/process/balance_nesting_depth.h"
16 : #include "mcrl2/process/is_guarded.h"
17 : #include "mcrl2/process/is_linear.h"
18 : #include "mcrl2/process/parse.h"
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::process;
22 :
23 : const std::string SPEC1 =
24 : "act a; \n"
25 : "proc X = a; \n"
26 : "init X; \n"
27 : ;
28 :
29 : const std::string SPEC2 =
30 : "act a; \n"
31 : "proc X(i: Nat) = a.X(i);\n"
32 : "init X(2); \n"
33 : ;
34 :
35 : const std::string ABS_SPEC_LINEARIZED =
36 : "sort D = struct d1 | d2; \n"
37 : " Error = struct e; \n"
38 : " \n"
39 : "act r1,s4: D; \n"
40 : " s2,r2,c2,s3,r3,c3: D # Bool; \n"
41 : " s3,r3,c3: Error; \n"
42 : " s5,r5,c5,s6,r6,c6: Bool; \n"
43 : " s6,r6,c6: Error; \n"
44 : " i; \n"
45 : " \n"
46 : "proc P(s31_S: Pos, d_S: D, b_S: Bool, s32_K: Pos, d_K: D, b_K: Bool, s33_L: Pos, b_L: Bool, s34_R: Pos, d_R: D, b_R: Bool) = \n"
47 : " sum e1_S: Bool. \n"
48 : " ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) -> \n"
49 : " c6(if(e1_S, !b_S, b_S)) . \n"
50 : " P(if(e1_S, 2, 1), if(e1_S, d_S, d2), if(e1_S, b_S, !b_S), s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R) \n"
51 : " + (s31_S == 3 && s33_L == 4) -> \n"
52 : " c6(e) . \n"
53 : " P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R) \n"
54 : " + (s31_S == 2 && s32_K == 1) -> \n"
55 : " c2(d_S, b_S) . \n"
56 : " P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R) \n"
57 : " + sum e2_K: Bool. \n"
58 : " (s32_K == 2) -> \n"
59 : " i . \n"
60 : " P(s31_S, d_S, b_S, if(e2_K, 4, 3), if(e2_K, d2, d_K), if(e2_K, false, b_K), s33_L, b_L, s34_R, d_R, b_R) \n"
61 : " + sum e4_R: Bool. \n"
62 : " (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) -> \n"
63 : " c5(if(e4_R, !b_R, b_R)) . \n"
64 : " P(s31_S, d_S, b_S, s32_K, d_K, b_K, 2, if(e4_R, !b_R, b_R), 1, d2, if(e4_R, b_R, !b_R)) \n"
65 : " + (s34_R == 2) -> \n"
66 : " s4(d_R) . \n"
67 : " P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R) \n"
68 : " + sum e3_L: Bool. \n"
69 : " (s33_L == 2) -> \n"
70 : " i . \n"
71 : " P(s31_S, d_S, b_S, s32_K, d_K, b_K, if(e3_L, 4, 3), if(e3_L, false, b_L), s34_R, d_R, b_R) \n"
72 : " + (s32_K == 4 && s34_R == 1) -> \n"
73 : " c3(e) . \n"
74 : " P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R) \n"
75 : " + sum e5_R: Bool. \n"
76 : " ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) -> \n"
77 : " c3(d_K, if(e5_R, b_R, !b_R)) . \n"
78 : " P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, if(e5_R, 2, 4), if(e5_R, d_K, d2), b_R) \n"
79 : " + sum d3_S: D. \n"
80 : " (s31_S == 1) -> \n"
81 : " r1(d3_S) . \n"
82 : " P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R) \n"
83 : " + true -> \n"
84 : " delta; \n"
85 : " \n"
86 : "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true); \n"
87 : ;
88 :
89 : // CASE?? specifications were borrowed from sumelm_test.
90 :
91 : std::string CASE1 =
92 : "sort S = struct s1 | s2;\n"
93 : "map f : S -> Bool;\n"
94 : "act a : S # Bool;\n"
95 : "proc P = sum c : S, b : Bool . (b == f(c) && c == s2) -> a(c, b) . P;\n"
96 : "init P;\n"
97 : ;
98 :
99 : std::string CASE2 =
100 : "act a,b;\n"
101 : "proc P(s3_P: Pos) = sum y_P: Int. (s3_P == 1) -> a . P(2)\n"
102 : " + (s3_P == 2) -> b . P(1);\n"
103 : "init P(1);\n"
104 : ;
105 :
106 : std::string CASE3 =
107 : "act a;\n"
108 : "proc P = sum y:Int . (4 == y) -> a . P;\n"
109 : "init P;\n"
110 : ;
111 :
112 : std::string CASE4 =
113 : "act a;\n"
114 : "proc P = sum y:Int . (y == 4) -> a . P;\n"
115 : "init P;\n"
116 : ;
117 :
118 : std::string CASE5 =
119 : "act a,b:Int;\n"
120 : "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
121 : "init P;\n"
122 : ;
123 :
124 : std::string CASE6 =
125 : "act a;\n"
126 : "proc P = sum y:Int . (y == y + 1) -> a . P;\n"
127 : "init P;\n"
128 : ;
129 :
130 : std::string CASE7 =
131 : "sort D = struct d1 | d2 | d3;\n"
132 : "map g : D -> D;\n"
133 : "act a;\n"
134 : "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && e == g(e) && e == f) -> a . P(d);\n"
135 : "init P(d1);\n"
136 : ;
137 :
138 : std::string CASE8 =
139 : "sort D = struct d1 | d2 | d3;\n"
140 : "act a;\n"
141 : "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && d == f) -> a . P(d);\n"
142 : "init P(d1);\n"
143 : ;
144 :
145 : std::string CASE9 =
146 : "proc P = sum y:Bool . y -> delta;\n"
147 : "init P;\n"
148 : ;
149 :
150 : std::string CASE10 =
151 : "act a:Nat;\n"
152 : "proc P(n0: Nat) = sum n: Nat. (n == n0 && n == 1) -> a(n0) . P(n);\n"
153 : "init P(0);\n"
154 : ;
155 :
156 : // provided by Jeroen Keiren
157 : std::string CASE11 =
158 : "act a,b: Int; \n"
159 : "glob dc,dc0: Int; \n"
160 : "proc P(s3_P: Pos, y_P: Int) = \n"
161 : " sum y0_P: Int. \n"
162 : " (s3_P == 1 && y0_P == 4) -> \n"
163 : " a(y0_P) @ y0_P . \n"
164 : " P(s3_P = 2, y_P = y0_P) \n"
165 : " + (s3_P == 2) -> \n"
166 : " b(y_P * 2) @ (y_P + 1) . \n"
167 : " P(s3_P = 1, y_P = dc0); \n"
168 : "init P(1, dc); \n"
169 : ;
170 :
171 : // test case containing a global variable
172 : std::string CASE12 =
173 : " act a: Nat ; \n"
174 : " glob v: Nat ; \n"
175 : " proc P(i, j: Nat) = \n"
176 : " (i == j) -> a(i) . P(1, 1) \n"
177 : " ; \n"
178 : " \n"
179 : " init P(i = 1, j = v) ; \n"
180 : ;
181 :
182 : // this process is considered to be NOT linear
183 : std::string CASE13a =
184 : "proc X = tau; \n"
185 : " \n"
186 : "init delta; \n"
187 : ;
188 :
189 : // this process is considered to be NOT linear
190 : std::string CASE13b =
191 : "proc X = delta; \n"
192 : " \n"
193 : "init X; \n"
194 : ;
195 :
196 : // this process is considered to be NOT linear
197 : std::string CASE14 =
198 : "act a; \n"
199 : " \n"
200 : "proc X = tau; \n"
201 : " \n"
202 : "init a; \n"
203 : ;
204 :
205 : // This process is considered linear, although it cannot be directly represented as an LPS.
206 : const std::string CASE15 =
207 : "proc P = tau; \n"
208 : " \n"
209 : "init P; \n"
210 : ;
211 :
212 16 : void test_linear(const std::string& text, bool result = true)
213 : {
214 16 : process_specification p = parse_process_specification(text);
215 16 : if (is_linear(p) != result)
216 : {
217 0 : std::cerr << "--- Failed linearity test ---" << std::endl;
218 0 : std::cerr << text << std::endl;
219 : }
220 16 : bool verbose = true;
221 16 : BOOST_CHECK(is_linear(p, verbose) == result);
222 16 : }
223 :
224 : // Test case supplied by Frank Stappers. A segmentation fault is reported on Suse 64 bit.
225 1 : void test_data_spec()
226 : {
227 2 : process_specification spec = parse_process_specification("sort X; init tau;");
228 1 : data::pp(spec.data());
229 1 : }
230 :
231 1 : void test_guarded()
232 : {
233 : std::string PROCSPEC =
234 : "act a; \n"
235 : "proc P(n: Nat) = Q(n); \n"
236 : "proc Q(n: Nat) = a.P(n);\n"
237 : "proc R(n: Nat) = S(n); \n"
238 : "proc S(n: Nat) = R(n); \n"
239 1 : "init P(2); \n"
240 : ;
241 :
242 1 : std::string DATA_DECL = "act a;\n";
243 1 : std::string PROC_DECL = "proc P(n: Nat); proc Q(n: Nat); proc R(n: Nat); proc S(n: Nat);\n";
244 : process_specification procspec =
245 1 : parse_process_specification(PROCSPEC);
246 1 : process_expression x;
247 :
248 1 : x = parse_process_expression("delta", DATA_DECL, PROC_DECL);
249 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
250 :
251 1 : x = parse_process_expression("tau", DATA_DECL, PROC_DECL);
252 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
253 :
254 1 : x = parse_process_expression("a", DATA_DECL, PROC_DECL);
255 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
256 :
257 1 : x = parse_process_expression("P(0)", DATA_DECL, PROC_DECL);
258 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
259 :
260 1 : x = parse_process_expression("a.P(0) + P(1)", DATA_DECL, PROC_DECL);
261 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
262 :
263 1 : x = parse_process_expression("a.P(0) || P(1)", DATA_DECL, PROC_DECL);
264 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
265 :
266 1 : x = parse_process_expression("a.P(0) . P(1)", DATA_DECL, PROC_DECL);
267 1 : BOOST_CHECK(is_guarded(x, procspec.equations()));
268 :
269 1 : x = parse_process_expression("R(0)", DATA_DECL, PROC_DECL);
270 1 : BOOST_CHECK(!is_guarded(x, procspec.equations()));
271 1 : }
272 :
273 2 : BOOST_AUTO_TEST_CASE(balance_summands_test)
274 : {
275 1 : std::function<std::size_t(process_expression)> nesting_depth;
276 802 : nesting_depth = [&nesting_depth](const process_expression& x) -> std::size_t
277 : {
278 402 : if (is_choice(x))
279 : {
280 200 : const auto& x_ = atermpp::down_cast<choice>(x);
281 200 : return std::max(nesting_depth(x_.left()), nesting_depth(x_.right())) + 1;
282 : }
283 202 : return 0;
284 1 : };
285 :
286 1 : process_expression x = delta();
287 101 : for (int i = 0; i < 100; i++)
288 : {
289 100 : x = choice(x, delta());
290 : }
291 1 : auto depth1 = nesting_depth(x);
292 1 : x = balance_summands(x);
293 1 : auto depth2 = nesting_depth(x);
294 1 : BOOST_CHECK_EQUAL(depth1, 100);
295 1 : BOOST_CHECK_EQUAL(depth2, 7);
296 1 : }
297 :
298 2 : BOOST_AUTO_TEST_CASE(test_main)
299 : {
300 1 : test_linear(CASE1);
301 1 : test_linear(CASE2);
302 1 : test_linear(CASE3);
303 1 : test_linear(CASE4);
304 1 : test_linear(CASE5, false);
305 1 : test_linear(CASE6);
306 1 : test_linear(CASE7);
307 1 : test_linear(CASE8);
308 1 : test_linear(CASE9);
309 1 : test_linear(CASE10);
310 1 : test_linear(CASE11);
311 1 : test_linear(CASE12);
312 1 : test_linear(CASE13a, false);
313 1 : test_linear(CASE13b);
314 1 : test_linear(CASE14, false);
315 1 : test_linear(CASE15);
316 :
317 1 : test_data_spec();
318 :
319 1 : test_guarded();
320 1 : }
|
