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 sort_traverser_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE sort_traverser_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 :
16 : #include "mcrl2/process/find.h"
17 : #include "mcrl2/process/parse.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::process;
21 :
22 : const std::string SPEC1 =
23 : "act a; \n"
24 : "proc X = a; \n"
25 : "init X; \n"
26 : ;
27 :
28 : const std::string SPEC2 =
29 : "act a; \n"
30 : "proc X(i: Nat) = a.X(i);\n"
31 : "init X(2); \n"
32 : ;
33 :
34 : const std::string ABS_SPEC_LINEARIZED =
35 : "sort D = struct d1 | d2; \n"
36 : " Error = struct e; \n"
37 : " \n"
38 : "act r1,s4: D; \n"
39 : " s2,r2,c2,s3,r3,c3: D # Bool; \n"
40 : " s3,r3,c3: Error; \n"
41 : " s5,r5,c5,s6,r6,c6: Bool; \n"
42 : " s6,r6,c6: Error; \n"
43 : " i; \n"
44 : " \n"
45 : "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"
46 : " sum e1_S: Bool. \n"
47 : " ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) -> \n"
48 : " c6(if(e1_S, !b_S, b_S)) . \n"
49 : " 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"
50 : " + (s31_S == 3 && s33_L == 4) -> \n"
51 : " c6(e) . \n"
52 : " P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R) \n"
53 : " + (s31_S == 2 && s32_K == 1) -> \n"
54 : " c2(d_S, b_S) . \n"
55 : " P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R) \n"
56 : " + sum e2_K: Bool. \n"
57 : " (s32_K == 2) -> \n"
58 : " i . \n"
59 : " 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"
60 : " + sum e4_R: Bool. \n"
61 : " (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) -> \n"
62 : " c5(if(e4_R, !b_R, b_R)) . \n"
63 : " 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"
64 : " + (s34_R == 2) -> \n"
65 : " s4(d_R) . \n"
66 : " P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R) \n"
67 : " + sum e3_L: Bool. \n"
68 : " (s33_L == 2) -> \n"
69 : " i . \n"
70 : " 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"
71 : " + (s32_K == 4 && s34_R == 1) -> \n"
72 : " c3(e) . \n"
73 : " P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R) \n"
74 : " + sum e5_R: Bool. \n"
75 : " ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) -> \n"
76 : " c3(d_K, if(e5_R, b_R, !b_R)) . \n"
77 : " 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"
78 : " + sum d3_S: D. \n"
79 : " (s31_S == 1) -> \n"
80 : " r1(d3_S) . \n"
81 : " P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R) \n"
82 : " + true -> \n"
83 : " delta; \n"
84 : " \n"
85 : "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true); \n"
86 : ;
87 :
88 : // CASE?? specifications were borrowed from sumelm_test.
89 :
90 : std::string CASE1 =
91 : "sort S = struct s1 | s2;\n"
92 : "map f : S -> Bool;\n"
93 : "act a : S # Bool;\n"
94 : "proc P = sum c : S, b : Bool . (b == f(c) && c == s2) -> a(c, b) . P;\n"
95 : "init P;\n"
96 : ;
97 :
98 : std::string CASE2 =
99 : "act a,b;\n"
100 : "proc P(s3_P: Pos) = sum y_P: Int. (s3_P == 1) -> a . P(2)\n"
101 : " + (s3_P == 2) -> b . P(1);\n"
102 : "init P(1);\n"
103 : ;
104 :
105 : std::string CASE3 =
106 : "act a;\n"
107 : "proc P = sum y:Int . (4 == y) -> a . P;\n"
108 : "init P;\n"
109 : ;
110 :
111 : std::string CASE4 =
112 : "act a;\n"
113 : "proc P = sum y:Int . (y == 4) -> a . P;\n"
114 : "init P;\n"
115 : ;
116 :
117 : std::string CASE5 =
118 : "act a,b:Int;\n"
119 : "proc P = sum y:Int . (y == 4) -> a(y)@y . b(y*2)@(y+1) . P;\n"
120 : "init P;\n"
121 : ;
122 :
123 : std::string CASE6 =
124 : "act a;\n"
125 : "proc P = sum y:Int . (y == y + 1) -> a . P;\n"
126 : "init P;\n"
127 : ;
128 :
129 : std::string CASE7 =
130 : "sort D = struct d1 | d2 | d3;\n"
131 : "map g : D -> D;\n"
132 : "act a;\n"
133 : "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && e == g(e) && e == f) -> a . P(d);\n"
134 : "init P(d1);\n"
135 : ;
136 :
137 : std::string CASE8 =
138 : "sort D = struct d1 | d2 | d3;\n"
139 : "act a;\n"
140 : "proc P(c:D) = sum d:D . sum e:D . sum f:D . (d == e && d == f) -> a . P(d);\n"
141 : "init P(d1);\n"
142 : ;
143 :
144 : std::string CASE9 =
145 : "proc P = sum y:Bool . y -> delta;\n"
146 : "init P;\n"
147 : ;
148 :
149 : std::string CASE10 =
150 : "act a:Nat;\n"
151 : "proc P(n0: Nat) = sum n: Nat. (n == n0 && n == 1) -> a(n0) . P(n);\n"
152 : "init P(0);\n"
153 : ;
154 :
155 13 : void test_process(const std::string& text)
156 : {
157 13 : process_specification spec = parse_process_specification(text);
158 13 : std::set<data::sort_expression> sorts;
159 13 : process::find_sort_expressions(spec, std::inserter(sorts, sorts.end()));
160 13 : std::cerr << "sorts: " << data::pp(data::sort_expression_list(sorts.begin(), sorts.end())) << std::endl;
161 13 : }
162 :
163 2 : BOOST_AUTO_TEST_CASE(test_main)
164 : {
165 1 : test_process(CASE1);
166 1 : test_process(CASE2);
167 1 : test_process(CASE3);
168 1 : test_process(CASE4);
169 1 : test_process(CASE5);
170 1 : test_process(CASE6);
171 1 : test_process(CASE7);
172 1 : test_process(CASE8);
173 1 : test_process(CASE9);
174 1 : test_process(CASE10);
175 1 : test_process(SPEC1);
176 1 : test_process(SPEC2);
177 1 : test_process(ABS_SPEC_LINEARIZED);
178 1 : }
179 :
|
