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 stochastic_specification_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE stochastic_specification_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/detail/test_input.h"
16 : #include "mcrl2/lps/is_stochastic.h"
17 : #include "mcrl2/lps/linearise.h"
18 : #include "mcrl2/lps/parelm.h"
19 : #include "mcrl2/lps/parse.h"
20 : #include "mcrl2/lps/print.h"
21 : #include "mcrl2/lps/is_well_typed.h"
22 :
23 : using namespace mcrl2;
24 : using namespace mcrl2::data;
25 : using namespace mcrl2::lps;
26 :
27 2 : BOOST_AUTO_TEST_CASE(test_empty_distribution)
28 : {
29 1 : stochastic_distribution dist;
30 1 : std::cout << "empty dist = " << dist << std::endl;
31 1 : BOOST_CHECK(!dist.is_defined());
32 1 : }
33 :
34 2 : BOOST_AUTO_TEST_CASE(test_remove_stochastic_operators)
35 : {
36 : std::string text =
37 : "act a;\n"
38 : "proc P = a.P;\n"
39 1 : "init P;"
40 : ;
41 :
42 1 : stochastic_specification src;
43 1 : parse_lps(text, src);
44 1 : BOOST_CHECK(!is_stochastic(src));
45 :
46 1 : specification dest = remove_stochastic_operators(src);
47 1 : std::cout << "dest = " << dest;
48 1 : BOOST_CHECK(lps::pp(src) == lps::pp(dest));
49 1 : }
50 :
51 2 : BOOST_AUTO_TEST_CASE(test_is_stochastic)
52 : {
53 : std::string text =
54 : "act throw: Bool; \n"
55 : " \n"
56 : "proc P = dist b:Bool[1/2].throw(b) . P; \n"
57 : " \n"
58 1 : "init P; \n"
59 : ;
60 1 : stochastic_specification spec;
61 1 : parse_lps(text, spec);
62 1 : BOOST_CHECK(is_stochastic(spec));
63 :
64 : text =
65 : "act throw: Bool; \n"
66 : " \n"
67 : "proc P = throw(true) . P; \n"
68 : " \n"
69 1 : "init dist b:Bool[1/2] . P;\n"
70 : ;
71 1 : parse_lps(text, spec);
72 1 : BOOST_CHECK(is_stochastic(spec));
73 1 : }
74 :
75 2 : BOOST_AUTO_TEST_CASE(test_print)
76 : {
77 : std::string text =
78 : "act a: Bool;\n"
79 : "\n"
80 : "proc P(s3: Pos, p: Bool) =\n"
81 : " (s3 == 1) ->\n"
82 : " a(p) .\n"
83 : " dist p: Bool[1 / 2] .\n"
84 : " P(s3 = 2, p = true)\n"
85 : " + delta;\n"
86 : "\n"
87 1 : "init dist p: Bool[1 / 2] . P(1, true);\n"
88 : ;
89 1 : stochastic_specification spec;
90 1 : parse_lps(text, spec);
91 1 : std::string result = lps::pp(spec);
92 1 : BOOST_CHECK_EQUAL(text, result);
93 1 : }
94 :
95 : // The following specification did not linearise, due to an infinite loop.
96 2 : BOOST_AUTO_TEST_CASE(test_linearisation)
97 : {
98 : std::string text =
99 : "act a:Bool;\n"
100 : "proc X=dist b:Bool[1/2].a(b).X;\n"
101 1 : "init X;\n"
102 : ;
103 :
104 : std::string result =
105 : "act a: Bool;\n"
106 : "\n"
107 : "proc P(b1_X: Bool) =\n"
108 : " a(b1_X) .\n"
109 : " dist b1_X1: Bool[1 / 2] .\n"
110 : " P(b1_X = b1_X1);\n"
111 : "\n"
112 1 : "init dist b1: Bool[1 / 2] . P(b1);\n"
113 : ;
114 :
115 1 : stochastic_specification spec=linearise(text);
116 1 : BOOST_CHECK_EQUAL(lps::pp(spec),result);
117 1 : }
118 :
119 : // This test checks whether multiple parameters in a stochastic operator are translated
120 : // correctely.
121 2 : BOOST_AUTO_TEST_CASE(test_multiple_stochastic_parameters)
122 : {
123 : std::string text =
124 : "act a:Bool#Bool;\n"
125 : "proc X=dist b1,b2:Bool[if(b1,1/8,3/8)].a(b1,b2).X;\n"
126 1 : "init X;\n"
127 : ;
128 :
129 : std::string result =
130 : "act a: Bool # Bool;\n"
131 : "\n"
132 : "proc P(b3_X,b4_X: Bool) =\n"
133 : " a(b3_X, b4_X) .\n"
134 : " dist b3_X1,b4_X1: Bool[if(b3_X1, 1 / 8, 3 / 8)] .\n"
135 : " P(b3_X = b3_X1, b4_X = b4_X1);\n"
136 : "\n"
137 1 : "init dist b3,b4: Bool[if(b3, 1 / 8, 3 / 8)] . P(b3, b4);\n"
138 : ;
139 :
140 1 : stochastic_specification spec=linearise(text);
141 1 : BOOST_CHECK_EQUAL(lps::pp(spec),result);
142 1 : }
143 :
144 : // This test checks whether a parameter in a stochastic operator are translated
145 : // correctely.
146 2 : BOOST_AUTO_TEST_CASE(test_properly_change_bound_variables)
147 : {
148 : std::string text =
149 : "map distribution: Bool#Pos#Pos->Real;\n"
150 : "\n"
151 : "act win, lose;\n"
152 : " hold:Bool;\n"
153 : "\n"
154 : "proc Play(round_: Nat, hold3:Bool, r3: Pos) = \n"
155 : " dist s3:Pos[distribution(hold3, r3, s3)].\n"
156 : " (\n"
157 : " (round_==1) -> lose.delta\n"
158 : " <> sum b3: Bool. hold(b3).Play(round_+1, b3, s3 )\n"
159 : " );\n"
160 : "\n"
161 1 : "init Play(0, false, 1);\n"
162 : ;
163 :
164 : std::string result1 =
165 : "map distribution: Bool # Pos # Pos -> Real;\n"
166 : "\n"
167 : "act win,lose;\n"
168 : " hold: Bool;\n"
169 : "\n"
170 : "glob dc: Pos;\n"
171 : " dc1: Nat;\n"
172 : "\n"
173 : "proc P(s4_Play,s1_Play: Pos, round__Play: Nat) =\n"
174 : " sum b1_Play: Bool.\n"
175 : " (s4_Play == 2 && !(round__Play == 1)) ->\n"
176 : " hold(b1_Play) .\n"
177 : " dist s2_Play: Pos[distribution(b1_Play, s1_Play, s2_Play)] .\n"
178 : " P(s4_Play = 2, s1_Play = s2_Play, round__Play = round__Play + 1)\n"
179 : " + (s4_Play == 2 && round__Play == 1) ->\n"
180 : " lose .\n"
181 : " P(s4_Play = 1, s1_Play = dc, round__Play = dc1)\n"
182 : " + delta;\n"
183 : "\n"
184 1 : "init dist s1: Pos[distribution(false, 1, s1)] . P(2, s1, 0);\n"
185 : ;
186 :
187 : std::string result2 =
188 : "map distribution: Bool # Pos # Pos -> Real;\n"
189 : "\n"
190 : "act win,lose;\n"
191 : " hold: Bool;\n"
192 : "\n"
193 : "glob dc: Pos;\n"
194 : " dc1: Nat;\n"
195 : "\n"
196 : "proc P(s4_Play,s1_Play: Pos, round__Play: Nat) =\n"
197 : " sum b1_Play: Bool.\n"
198 : " (s4_Play == 1 && !(round__Play == 1)) ->\n"
199 : " hold(b1_Play) .\n"
200 : " dist s2_Play: Pos[distribution(b1_Play, s1_Play, s2_Play)] .\n"
201 : " P(s4_Play = 1, s1_Play = s2_Play, round__Play = round__Play + 1)\n"
202 : " + (s4_Play == 1 && round__Play == 1) ->\n"
203 : " lose .\n"
204 : " P(s4_Play = 2, s1_Play = dc, round__Play = dc1)\n"
205 : " + delta;\n"
206 : "\n"
207 1 : "init dist s1: Pos[distribution(false, 1, s1)] . P(1, s1, 0);\n"
208 : ;
209 :
210 1 : stochastic_specification spec=linearise(text);
211 1 : BOOST_CHECK(lps::pp(spec)==result1 || // The lineariser can up with multiple results, depending on how terms are stored internally.
212 : lps::pp(spec)==result2);
213 1 : }
214 :
215 : // This test checks whether the outward distribution of dist operators is going
216 : // correctely.
217 2 : BOOST_AUTO_TEST_CASE(test_push_dist_outward)
218 : {
219 : std::string text =
220 : "sort Coin = struct head_ | tail_;\n"
221 : "\n"
222 : "act throw:Coin;\n"
223 : " success;\n"
224 : "\n"
225 : "proc X(head_seen:Bool) = dist c:Coin[1/2].throw(c).\n"
226 : " ((c==head_ && head_seen) -> success.delta+\n"
227 : " (c==head_ && !head_seen) -> X(true)+\n"
228 : " (c==tail_) -> X(false));\n"
229 : "\n"
230 1 : "init X(false);\n"
231 : ;
232 :
233 1 : stochastic_specification spec=linearise(text);
234 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
235 1 : }
236 :
237 :
238 2 : BOOST_AUTO_TEST_CASE(test_parelm)
239 : {
240 1 : stochastic_specification spec = linearise(lps::detail::ABP_SPECIFICATION());
241 1 : std::set<data::variable> v = lps::find_all_variables(spec);
242 1 : parelm(spec);
243 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
244 1 : }
245 :
246 : /* This test case caused the lineariser to incorrectly handle bound variables in the distribution operator */
247 2 : BOOST_AUTO_TEST_CASE(bound_variable)
248 : {
249 : std::string text =
250 : "act a;\n"
251 1 : "init dist x0: Bool[if(x0,1/3,2/3)].(x0 -> (a . dist x1: Bool[1/2].(x1 -> a)));\n";
252 1 : stochastic_specification spec=linearise(text);
253 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
254 1 : }
255 :
256 : /* The following test case requires that the sum operator is distributed over the dist operator.
257 : * This is only possible, as it stands for finite domains. */
258 2 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist1)
259 : {
260 : std::string text =
261 : "act\n"
262 : " c:Bool#Bool;\n"
263 : "\n"
264 : "proc\n"
265 : " Q = sum b1: Bool. dist x0: Bool[if(x0,1/4,3/4)].c(b1,x0).delta;\n"
266 : " \n"
267 1 : "init Q;\n";
268 1 : stochastic_specification spec=linearise(text);
269 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
270 1 : }
271 :
272 : /* A more elaborate example of the previous test case, where there are also distributions
273 : * inside the linear process. */
274 2 : BOOST_AUTO_TEST_CASE(distributed_sum_over_dist2)
275 : {
276 : std::string text =
277 : "act c: Bool # Bool;\n"
278 : " \n"
279 : "glob dc,dc1,dc2,dc3: Bool;\n"
280 : "\n"
281 : "proc P(s1_Q: Pos, x: Bool) = \n"
282 : " (s1_Q == 2) ->\n"
283 : " c(true, x) .\n"
284 : " P(s1_Q = 1, x = dc)\n"
285 : " + delta;\n"
286 : " \n"
287 1 : "init dist x: Bool[if(x, 1 / 4, 3 / 4)] . P(2, x);\n";
288 1 : stochastic_specification spec=linearise(text);
289 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
290 1 : }
291 :
292 : /* The following example shows an initial distribution with variables
293 : * that are not used in the body. */
294 2 : BOOST_AUTO_TEST_CASE(non_bound_initial_stochastic_variables)
295 : {
296 : std::string text =
297 : "act a;\n"
298 : "\n"
299 : "proc P = (true -> delta <> (dist x0: Bool[1 / 2] . x0 -> a)) . P;\n"
300 : "\n"
301 1 : "init P;\n";
302 1 : stochastic_specification spec=linearise(text);
303 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
304 1 : }
305 :
306 : /* The following example was not linearised correctly, as
307 : an expression sum x:D.a.P was returned
308 : unchanged when P had an initial distribution.
309 : */
310 2 : BOOST_AUTO_TEST_CASE(distribution_insided_sum_bug)
311 : {
312 : std::string text =
313 : "act a,b;\n"
314 : "\n"
315 : "proc Environment = \n"
316 : " sum realReading: Nat . (realReading<2) ->\n"
317 : " a . EnvironmentSensorProcess;\n"
318 : "\n"
319 : "proc EnvironmentSensorProcess =\n"
320 : " dist f:Bool[if(f, 1/4, 3/4)].f->b.delta;\n"
321 : "\n"
322 1 : "init Environment;\n";
323 1 : stochastic_specification spec=linearise(text);
324 1 : BOOST_CHECK(lps::detail::is_well_typed(spec));
325 1 : }
326 :
327 :
|