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 typecheck_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE typecheck_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/process/parse.h"
16 :
17 : using namespace mcrl2;
18 :
19 26 : void test_typechecker_case(std::string const& spec, bool const expected_result)
20 : {
21 26 : std::clog << std::endl
22 26 : << "<---- testing specification: ---->" << std::endl
23 26 : << spec << std::endl;
24 26 : if (expected_result)
25 : {
26 15 : std::clog << "expected result: success" << std::endl;
27 : try
28 : {
29 15 : process::parse_process_specification(spec);
30 : }
31 0 : catch (mcrl2::runtime_error& e) // Catch errors and print them, such that all cases are treated.
32 : {
33 0 : std::clog << "type checking failed with error: " << std::endl
34 0 : << e.what() << std::endl;
35 0 : BOOST_CHECK(false);
36 0 : }
37 : }
38 : else
39 : {
40 11 : std::clog << "expected result: failure" << std::endl;
41 22 : BOOST_CHECK_THROW(process::parse_process_specification(spec), mcrl2::runtime_error);
42 : }
43 26 : }
44 :
45 5 : void test_process_specification(const std::string& ps_in, bool const expected_result = true, bool const test_type_checker = true)
46 : {
47 5 : process::process_specification p = process::detail::parse_process_specification_new(ps_in);
48 5 : std::string ps_out;
49 5 : if (test_type_checker)
50 : {
51 5 : process::process_specification ps = p;
52 5 : if (expected_result)
53 : {
54 2 : process::typecheck_process_specification(ps);
55 2 : ps_out = process::pp(ps);
56 2 : if (ps_in != ps_out)
57 : {
58 0 : std::cerr << "--- failed test ---" << std::endl << "ps_in =\n" << ps_in << std::endl << std::endl << "ps_out =\n" << ps_out << std::endl;
59 0 : BOOST_CHECK_EQUAL(ps_in, ps_out);
60 : }
61 : }
62 : else
63 : {
64 6 : BOOST_CHECK_THROW(process::typecheck_process_specification(ps), mcrl2::runtime_error);
65 : }
66 5 : }
67 5 : }
68 :
69 2 : BOOST_AUTO_TEST_CASE(test_concat_element)
70 : {
71 : // Example provided by Tim Willemse, 7 Oct 2009
72 1 : test_typechecker_case(
73 : "map place : List(Nat) -> List(Nat); \n"
74 : " \n"
75 : "var l : List(Nat); \n"
76 : " \n"
77 : "eqn place (l) = head(l) ++ tail(l); \n"
78 : " \n"
79 : "init delta; \n",
80 : false
81 : );
82 1 : }
83 :
84 2 : BOOST_AUTO_TEST_CASE(test_concat_lists)
85 : {
86 1 : test_typechecker_case(
87 : "map place : List(Nat) -> List(Nat); \n"
88 : " \n"
89 : "var l : List(Nat); \n"
90 : " \n"
91 : "eqn place (l) = l ++ tail(l); \n"
92 : " \n"
93 : "init delta; \n",
94 : true
95 : );
96 1 : }
97 :
98 2 : BOOST_AUTO_TEST_CASE(test_bug_528a)
99 : {
100 1 : test_typechecker_case(
101 : "sort S = struct c; \n"
102 : "map succ_: S -> S; \n"
103 : "eqn succ_(c) = c; \n"
104 : "init delta; \n",
105 : true
106 : );
107 1 : }
108 :
109 2 : BOOST_AUTO_TEST_CASE(test_bug_528b)
110 : {
111 1 : test_typechecker_case(
112 : "sort S,T; \n"
113 : "map count_: S # T -> Nat; \n"
114 : "var x:S; \n"
115 : " y:T; \n"
116 : "eqn count_(x, y) = 0; \n"
117 : "init delta; \n",
118 : true
119 : );
120 1 : }
121 :
122 2 : BOOST_AUTO_TEST_CASE(test_bug_528c)
123 : {
124 1 : test_typechecker_case(
125 : "sort S; \n"
126 : "map count_: S -> Nat; \n"
127 : "var x:S; \n"
128 : "eqn count_(x) = 0; \n"
129 : "init delta; \n",
130 : true
131 : );
132 1 : }
133 :
134 2 : BOOST_AUTO_TEST_CASE(test_bug_528d)
135 : {
136 1 : test_typechecker_case(
137 : "map count: Pos#Bag(Pos)->Nat; \n"
138 : " f:Nat->Pos; \n"
139 : " \n"
140 : "act a:Nat; \n"
141 : " \n"
142 : "proc P1(i: Nat) = a(i); \n"
143 : " \n"
144 : "init P1(count(3,{3:4})); \n",
145 : false
146 : );
147 1 : }
148 :
149 :
150 2 : BOOST_AUTO_TEST_CASE(test_bug_663a)
151 : {
152 1 : test_typechecker_case(
153 : "map const: Pos; \n"
154 : "eqn const = 10; \n"
155 : " \n"
156 : "proc P1(i: Nat) = delta; \n"
157 : " \n"
158 : "init P1(const); \n",
159 : true
160 : );
161 1 : }
162 :
163 2 : BOOST_AUTO_TEST_CASE(test_bug_663b)
164 : {
165 1 : test_typechecker_case(
166 : "map const: Pos; \n"
167 : "eqn const = 10; \n"
168 : " \n"
169 : "proc P1(i: Nat) = delta; \n"
170 : " \n"
171 : "init P1(Nat2Pos(Pos2Nat(const)));\n",
172 : true
173 : );
174 1 : }
175 :
176 2 : BOOST_AUTO_TEST_CASE(test_bug_663c)
177 : {
178 1 : test_typechecker_case(
179 : "map const: Pos; \n"
180 : "eqn const = 10; \n"
181 : " \n"
182 : "proc P1(i: Nat) = delta; \n"
183 : " \n"
184 : "init P1(Pos2Nat(const));\n",
185 : true
186 : );
187 1 : }
188 :
189 2 : BOOST_AUTO_TEST_CASE(test_bug_644)
190 : {
191 1 : test_typechecker_case(
192 : "cons maybe: Bool; \n"
193 : "init delta; \n",
194 : false
195 : );
196 1 : }
197 :
198 2 : BOOST_AUTO_TEST_CASE(test_bug_626a)
199 : {
200 1 : test_typechecker_case(
201 : "sort S = struct c( proj: Int ); \n"
202 : " \n"
203 : "map f :(S -> Bool)#S -> S; \n"
204 : "var pre: S -> Bool; \n"
205 : " s: S; \n"
206 : "eqn f (pre, s) = s; \n"
207 : " \n"
208 : "act a: (S); \n"
209 : " \n"
210 : "init a( f( lambda x:S. proj(x) < 0 , c( 0 ) ) );\n",
211 : true
212 : );
213 1 : }
214 :
215 2 : BOOST_AUTO_TEST_CASE(test_bug_626b)
216 : {
217 1 : test_typechecker_case(
218 : "sort S = struct c( x: Int ); \n"
219 : " \n"
220 : "map f :(S -> Bool)#S -> S; \n"
221 : "var pre: S -> Bool; \n"
222 : " s: S; \n"
223 : "eqn f (pre, s) = s; \n"
224 : " \n"
225 : "act a: (S); \n"
226 : " \n"
227 : "init a( f( lambda i:S. x(i) < 0 , c( 0 ) ) );\n",
228 : true
229 : );
230 1 : }
231 :
232 : // First test case for issue #629, constructor domain is empty.
233 2 : BOOST_AUTO_TEST_CASE(test_bug_629a)
234 : {
235 1 : test_typechecker_case(
236 : "sort L_1=struct insert(L_1) ; \n"
237 : "init delta; \n",
238 : false
239 : );
240 1 : }
241 :
242 : // Second test case for issue #629, constructor domain is empty.
243 2 : BOOST_AUTO_TEST_CASE(test_bug_629b)
244 : {
245 1 : test_typechecker_case(
246 : "sort L_2=struct insert(L_3); \n"
247 : " L_3=struct insert(L_2); \n"
248 : "init delta; \n",
249 : false
250 : );
251 1 : }
252 :
253 : // Third test case for issue #629, constructor domain is empty.
254 2 : BOOST_AUTO_TEST_CASE(test_bug_629c)
255 : {
256 1 : test_typechecker_case(
257 : "sort D; \n"
258 : "cons f:D->D; \n"
259 : "init delta; \n",
260 : false
261 : );
262 1 : }
263 :
264 : // fourth test case for issue #629, constructor domain is empty.
265 2 : BOOST_AUTO_TEST_CASE(test_bug_629d)
266 : {
267 1 : test_typechecker_case(
268 : "sort D =struct f(struct g(D));"
269 : "init delta;",
270 : false
271 : );
272 1 : }
273 :
274 : // fifth test case for issue #629, constructor domain is NOT empty.
275 2 : BOOST_AUTO_TEST_CASE(test_bug_629e)
276 : {
277 1 : test_typechecker_case(
278 : "sort D =struct f(struct g(Nat));"
279 : "init delta;",
280 : true
281 : );
282 1 : }
283 :
284 : // Tricky test case that should succeed, as sorts are not recursively defined through sort containers.
285 2 : BOOST_AUTO_TEST_CASE(test_recursive_a)
286 : {
287 1 : test_typechecker_case(
288 : "sort MyRecType=struct f | g(MyRecType);"
289 : " D=List(MyRecType);"
290 : "init delta;",
291 : true
292 : );
293 1 : }
294 :
295 :
296 : // Tricky test case that should succeed, as recursive sorts are are defined through the list containers
297 : // are allowed.
298 2 : BOOST_AUTO_TEST_CASE(test_recursive_b)
299 : {
300 1 : test_typechecker_case(
301 : "sort MyRecType=struct f | g(List(MyRecType));"
302 : "init delta;",
303 : true
304 : );
305 1 : }
306 :
307 : // Tricky test case that should succeed, as sorts are not recursively defined through sort containers.
308 2 : BOOST_AUTO_TEST_CASE(test_recursive_c)
309 : {
310 1 : test_typechecker_case(
311 : "sort MyRecType=struct f | g(MyRecType);"
312 : " D=List(MyRecType)->MyRecType;"
313 : "init delta;",
314 : true
315 : );
316 1 : }
317 :
318 : // Tricky test case that should fail, as recursive sorts are are defined through sort containers
319 : // but in this case it is not that easy to see.
320 2 : BOOST_AUTO_TEST_CASE(test_recursive_d)
321 : {
322 1 : test_typechecker_case(
323 : "sort MyRecType=struct f | g(MyRecType->Nat);"
324 : "init delta;",
325 : false
326 : );
327 1 : }
328 :
329 : // Test case below went wrong, because sort expression was confused with a function symbol
330 2 : BOOST_AUTO_TEST_CASE(test_sort_expression_vs_function_symbol)
331 : {
332 1 : test_typechecker_case(
333 : "map const: Pos; \n"
334 : " f:Nat->Pos; \n"
335 : "eqn const = 10; \n"
336 : "proc P1(i: Nat) = delta; \n"
337 : "init P1(f(const)); \n",
338 : true
339 : );
340 1 : }
341 :
342 2 : BOOST_AUTO_TEST_CASE(test_real_zero)
343 : {
344 1 : test_typechecker_case(
345 : "sort T = Real;\n"
346 : "map x: List(T) -> List(T);\n"
347 : "var l: List(T);\n"
348 : " r: T;\n"
349 : "eqn x(r |> l) = (r+0) |> l;\n"
350 : "act a: List(T);\n"
351 : "init a(x([0]));\n",
352 : true
353 : );
354 1 : }
355 :
356 : // The following example tests whether a double assignment in a
357 : // process is properly caught by the typechecker.
358 2 : BOOST_AUTO_TEST_CASE(test_double_variable_assignment_in_process)
359 : {
360 1 : test_typechecker_case(
361 : "proc X( v :Bool ) = tau. X( v = true, v = false );\n"
362 : "init X(true);",
363 : false);
364 1 : }
365 :
366 2 : BOOST_AUTO_TEST_CASE(test_typecheck)
367 : {
368 : std::string text =
369 : "act a;\n"
370 : "glob d,c,b: Bool;\n"
371 : "n,m: Nat;\n"
372 : "p: Pos;\n"
373 : "proc P(b,c: Bool) = a . P(c = true);\n"
374 1 : "init delta;\n"
375 : ;
376 1 : process::process_specification procspec = process::detail::parse_process_specification_new(text);
377 1 : process::typecheck_process_specification(procspec);
378 1 : }
379 :
380 2 : BOOST_AUTO_TEST_CASE(test_process_reference_assignment)
381 : {
382 : //test process specification involving process reference assignments
383 1 : test_process_specification(
384 : "proc P(b: Bool) = tau . P() + tau . P(b = false);\n"
385 : "\n"
386 : "init P(b = true);\n"
387 : );
388 1 : }
389 :
390 2 : BOOST_AUTO_TEST_CASE(test_global_variables)
391 : {
392 : //test process specification involving global variables
393 1 : test_process_specification(
394 : "glob dc: Bool;\n"
395 : "\n"
396 : "proc P(b: Bool) = tau . P(dc);\n"
397 : "\n"
398 : "init P(dc);\n"
399 : );
400 1 : }
401 :
402 : // For bug #732
403 2 : BOOST_AUTO_TEST_CASE(test_function_condition)
404 : {
405 1 : test_process_specification(
406 : "map b: Nat -> Nat;\n\n"
407 : "init b -> tau;\n",
408 : false
409 : );
410 1 : }
411 :
412 : // For bug #732
413 2 : BOOST_AUTO_TEST_CASE(test_function_as_set_descriptor)
414 : {
415 1 : test_process_specification(
416 : "map b: Bool # Pos -> Nat;\n"
417 : " s: Set(Nat);\n\n"
418 : "eqn s = { n: Nat | b };\n\n"
419 : "init b -> tau;\n",
420 : false
421 : );
422 1 : }
423 :
424 : // For bug #732
425 2 : BOOST_AUTO_TEST_CASE(test_function_as_equation_condition)
426 : {
427 1 : test_process_specification(
428 : "map b: Bool # Pos -> Nat;\n"
429 : " n: Nat;\n\n"
430 : "eqn b -> n = 0;\n\n"
431 : "act a: Nat;\n\n"
432 : "init a(n);\n",
433 : false
434 : );
435 1 : }
436 :
437 : // Test case supplied by Johri van Eerd, 22-10-2019
438 2 : BOOST_AUTO_TEST_CASE(test_incomplete_assignments)
439 : {
440 1 : test_typechecker_case(
441 : "act F,T;\n"
442 : "proc P(b: Bool) = (b) -> T . Q() <> F . Q();\n"
443 : " Q(res: Bool) = P(b = !res);\n"
444 : "init P(true);",
445 : false
446 : );
447 1 : }
448 :
449 : // Test case induced by a problem found by Maarten Visscher
450 2 : BOOST_AUTO_TEST_CASE(test_incomplete_assignment_in_init_clause)
451 : {
452 1 : test_typechecker_case(
453 : "act a;\n"
454 : "proc P(x:Nat)=a.P();\n"
455 : "\n"
456 : "init P();\n", // here a value for x should be given.
457 : false
458 : );
459 1 : }
460 :
|
