Line data Source code
1 : // Author(s): Wieger Wesselink, Jeroen van der Wulp
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 linear_process_conversion_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE linear_process_conversion_test
13 : #include "mcrl2/lps/parse.h"
14 :
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : using namespace mcrl2;
18 : using namespace mcrl2::process;
19 : using namespace mcrl2::lps;
20 :
21 : // Although this process is linear, the linear_process_conversion_traverser algorithm
22 : // is expected to generate an exception. The reason for this is that this process
23 : // cannot be directly represented as an LPS.
24 : const std::string SPEC1 =
25 : "act a; \n"
26 : "proc X = a; \n"
27 : "init X; \n"
28 : ;
29 :
30 : const std::string SPEC2 =
31 : "act a; \n"
32 : "proc X(i: Nat) = a.X(i);\n"
33 : "init X(2); \n"
34 : ;
35 :
36 : const std::string SPEC3 =
37 : "act a : Bool; \n"
38 : "proc X = sum b,c:Bool . (b && c) -> a(b).X; \n"
39 : "init X; \n"
40 : ;
41 :
42 : // Although this process is linear, the linear_process_conversion_traverser algorithm
43 : // is expected to generate an exception. The reason for this is that this process
44 : // cannot be directly represented as an LPS.
45 : const std::string SPEC4 =
46 : "proc P = tau; \n"
47 : " \n"
48 : "init P; \n"
49 : ;
50 :
51 : const std::string ABS_SPEC_LINEARIZED =
52 : // "sort D = struct d1 | d2; \n"
53 : // " Error = struct e; \n"
54 : // " \n"
55 : // "act r1,s4: D; \n"
56 : // " s2,r2,c2,s3,r3,c3: D # Bool; \n"
57 : // " s3,r3,c3: Error; \n"
58 : // " s5,r5,c5,s6,r6,c6: Bool; \n"
59 : // " s6,r6,c6: Error; \n"
60 : // " i; \n"
61 : // " \n"
62 : // "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"
63 : // " sum e1_S: Bool. \n"
64 : // " ((s31_S == 3 && s33_L == 3) && if(e1_S, !b_S, b_S) == b_L) -> \n"
65 : // " c6(if(e1_S, !b_S, b_S)) . \n"
66 : // " 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"
67 : // " + (s31_S == 3 && s33_L == 4) -> \n"
68 : // " c6(e) . \n"
69 : // " P(2, d_S, b_S, s32_K, d_K, b_K, 1, false, s34_R, d_R, b_R) \n"
70 : // " + (s31_S == 2 && s32_K == 1) -> \n"
71 : // " c2(d_S, b_S) . \n"
72 : // " P(3, d_S, b_S, 2, d_S, b_S, s33_L, b_L, s34_R, d_R, b_R) \n"
73 : // " + sum e2_K: Bool. \n"
74 : // " (s32_K == 2) -> \n"
75 : // " i . \n"
76 : // " 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"
77 : // " + sum e4_R: Bool. \n"
78 : // " (s33_L == 1 && if(e4_R, s34_R == 4, s34_R == 3)) -> \n"
79 : // " c5(if(e4_R, !b_R, b_R)) . \n"
80 : // " 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"
81 : // " + (s34_R == 2) -> \n"
82 : // " s4(d_R) . \n"
83 : // " P(s31_S, d_S, b_S, s32_K, d_K, b_K, s33_L, b_L, 3, d2, b_R) \n"
84 : // " + sum e3_L: Bool. \n"
85 : // " (s33_L == 2) -> \n"
86 : // " i . \n"
87 : // " 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"
88 : // " + (s32_K == 4 && s34_R == 1) -> \n"
89 : // " c3(e) . \n"
90 : // " P(s31_S, d_S, b_S, 1, d2, false, s33_L, b_L, 4, d2, b_R) \n"
91 : // " + sum e5_R: Bool. \n"
92 : // " ((s32_K == 3 && s34_R == 1) && if(e5_R, b_R, !b_R) == b_K) -> \n"
93 : // " c3(d_K, if(e5_R, b_R, !b_R)) . \n"
94 : // " 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"
95 : // " + sum d3_S: D. \n"
96 : // " (s31_S == 1) -> \n"
97 : // " r1(d3_S) . \n"
98 : // " P(2, d3_S, b_S, s32_K, d_K, b_K, s33_L, b_L, s34_R, d_R, b_R) \n"
99 : // " + true -> \n"
100 : // " delta; \n"
101 : // " \n"
102 : // "init P(1, d2, true, 1, d2, false, 1, false, 1, d2, true); \n"
103 : // ;
104 : "sort D = struct d1 | d2; \n"
105 : " Error = struct e; \n"
106 : " \n"
107 : "act r1,s4: D; \n"
108 : " s2,r2,c2,s3,r3,c3: D # Bool; \n"
109 : " s3,r3,c3: Error; \n"
110 : " s5,r5,c5,s6,r6,c6: Bool; \n"
111 : " s6,r6,c6: Error; \n"
112 : " i; \n"
113 : " \n"
114 : "glob dc,dc0,dc1,dc3,dc5,dc7,dc13,dc14,dc15,dc16,dc17,dc18: D; \n"
115 : " dc2,dc4,dc6,dc8,dc9,dc10,dc11,dc12: Bool; \n"
116 : " \n"
117 : "proc P(s30_S: Pos, d_S: D, b_S: Bool, s31_K: Pos, d_K: D, b_K: Bool, s32_L: Pos, b_L: Bool, s33_R: Pos, d_R: D, b_R: Bool) = \n"
118 : " sum e_S: Bool. \n"
119 : " ((s30_S == 3 && s32_L == 3) && if(e_S, b_S, !b_S) == b_L) -> \n"
120 : " c6(if(e_S, b_S, !b_S)) . \n"
121 : " P(s30_S = if(e_S, 1, 2), d_S = if(e_S, dc0, d_S), b_S = if(e_S, !b_S, b_S), s32_L = 1, b_L = dc11) \n"
122 : " + (s30_S == 3 && s32_L == 4) -> \n"
123 : " c6(e) . \n"
124 : " P(s30_S = 2, s32_L = 1, b_L = dc12) \n"
125 : " + (s30_S == 2 && s31_K == 1) -> \n"
126 : " c2(d_S, b_S) . \n"
127 : " P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S) \n"
128 : " + sum e3_R: Bool. \n"
129 : " ((s31_K == 3 && s33_R == 1) && if(e3_R, !b_R, b_R) == b_K) -> \n"
130 : " c3(d_K, if(e3_R, !b_R, b_R)) . \n"
131 : " P(s31_K = 1, d_K = dc5, b_K = dc6, s33_R = if(e3_R, 4, 2), d_R = if(e3_R, dc14, d_K)) \n"
132 : " + (s31_K == 4 && s33_R == 1) -> \n"
133 : " c3(e) . \n"
134 : " P(s31_K = 1, d_K = dc7, b_K = dc8, s33_R = 4, d_R = dc15) \n"
135 : " + sum e2_R: Bool. \n"
136 : " (s32_L == 1 && if(e2_R, s33_R == 4, s33_R == 3)) -> \n"
137 : " c5(if(e2_R, !b_R, b_R)) . \n"
138 : " P(s32_L = 2, b_L = if(e2_R, !b_R, b_R), s33_R = 1, d_R = if(e2_R, dc18, dc17), b_R = if(e2_R, b_R, !b_R)) \n"
139 : " + (s33_R == 2) -> \n"
140 : " s4(d_R) . \n"
141 : " P(s33_R = 3, d_R = dc16) \n"
142 : " + sum e1_L: Bool. \n"
143 : " (s32_L == 2) -> \n"
144 : " i . \n"
145 : " P(s32_L = if(e1_L, 4, 3), b_L = if(e1_L, dc10, b_L)) \n"
146 : " + sum e0_K: Bool. \n"
147 : " (s31_K == 2) -> \n"
148 : " i . \n"
149 : " P(s31_K = if(e0_K, 4, 3), d_K = if(e0_K, dc3, d_K), b_K = if(e0_K, dc4, b_K)) \n"
150 : " + sum d0_S: D. \n"
151 : " (s30_S == 1) -> \n"
152 : " r1(d0_S) . \n"
153 : " P(s30_S = 2, d_S = d0_S) \n"
154 : " + delta; \n"
155 : " \n"
156 : "init P(1, dc, true, 1, dc1, dc2, 1, dc9, 1, dc13, true); \n"
157 : ;
158 :
159 : // The flag expect_exception should be set for linear processes that cannot be represented by an LPS.
160 5 : void test_process(const std::string& text, bool expect_exception = false)
161 : {
162 5 : process_specification pspec = parse_process_specification(text);
163 5 : bool linear = is_linear(pspec, true);
164 5 : if (linear)
165 : {
166 : try
167 : {
168 5 : process::detail::linear_process_conversion_traverser visitor;
169 5 : specification spec = visitor.convert(pspec);
170 5 : }
171 2 : catch (mcrl2::runtime_error&)
172 : {
173 2 : BOOST_CHECK(expect_exception);
174 2 : return;
175 2 : }
176 3 : BOOST_CHECK(!expect_exception);
177 : }
178 : else
179 : {
180 : try
181 : {
182 0 : process::detail::linear_process_conversion_traverser visitor;
183 0 : specification spec = visitor.convert(pspec);
184 0 : BOOST_CHECK(false); // not supposed to arrive here
185 0 : }
186 0 : catch (...)
187 : {
188 : // skip
189 0 : }
190 : }
191 5 : }
192 :
193 2 : BOOST_AUTO_TEST_CASE(test_main)
194 : {
195 1 : std::clog << "SPEC1" << std::endl;
196 1 : test_process(SPEC1, true);
197 1 : std::clog << "SPEC2" << std::endl;
198 1 : test_process(SPEC2);
199 1 : std::clog << "SPEC3" << std::endl;
200 1 : test_process(SPEC3);
201 1 : std::clog << "SPEC4" << std::endl;
202 1 : test_process(SPEC4, true);
203 1 : std::clog << "ABS_SPEC_LINEARIZED" << std::endl;
204 1 : test_process(ABS_SPEC_LINEARIZED);
205 1 : }
206 :
|
