Line data Source code
1 : // Author(s): mCRL2 team
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 lts_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_WITH_GARBAGE_COLLECTION
13 : #define MCRL2_WITH_GARBAGE_COLLECTION
14 : #endif
15 :
16 : #define BOOST_TEST_MODULE lps2lts_test
17 : #include <boost/test/included/unit_test.hpp>
18 :
19 : #include "mcrl2/data/detail/rewrite_strategies.h"
20 : #include "mcrl2/lps/is_stochastic.h"
21 : #include "mcrl2/lts/state_space_generator.h"
22 : #include "mcrl2/lts/stochastic_lts_builder.h"
23 : #include "mcrl2/utilities/test_utilities.h"
24 :
25 : using namespace mcrl2;
26 : using namespace mcrl2::lps;
27 :
28 : template <bool Stochastic, bool Timed, typename Specification, typename LTSBuilder>
29 174 : void generate_state_space(const Specification& lpsspec, LTSBuilder& builder, const std::string& output_filename, const lps::explorer_options& options)
30 : {
31 174 : lts::state_space_generator<Stochastic, Timed, Specification> generator(lpsspec, options);
32 174 : generator.explore(builder);
33 174 : builder.save(output_filename);
34 174 : }
35 :
36 174 : std::string file_extension(lts::lts_type output_format)
37 : {
38 174 : switch (output_format)
39 : {
40 58 : case lts::lts_lts: return ".lts";
41 58 : case lts::lts_aut: return ".aut";
42 58 : case lts::lts_fsm: return ".fsm";
43 0 : case lts::lts_dot: return ".dot";
44 0 : default: throw mcrl2::runtime_error("unsupported format");
45 : }
46 : }
47 :
48 174 : void run_generatelts(
49 : const lps::stochastic_specification& stochastic_lpsspec,
50 : data::rewrite_strategy rstrategy,
51 : lps::exploration_strategy estrategy,
52 : lts::lts_type output_format,
53 : const std::string& outputfile,
54 : const std::string& priority_action
55 : )
56 : {
57 174 : lps::explorer_options options;
58 174 : options.trace_prefix = "lps2lts_test";
59 174 : options.confluence_action = priority_action;
60 174 : options.rewrite_strategy = rstrategy;
61 174 : options.search_strategy = estrategy;
62 174 : options.save_at_end = true;
63 :
64 174 : bool is_timed = stochastic_lpsspec.process().has_time();
65 :
66 174 : if (lps::is_stochastic(stochastic_lpsspec))
67 : {
68 12 : auto builder = create_stochastic_lts_builder(stochastic_lpsspec, options, output_format);
69 12 : if (is_timed)
70 : {
71 0 : generate_state_space<true, true>(stochastic_lpsspec, *builder, outputfile, options);
72 : }
73 : else
74 : {
75 12 : generate_state_space<true, false>(stochastic_lpsspec, *builder, outputfile, options);
76 : }
77 12 : }
78 : else
79 : {
80 162 : lps::specification lpsspec = lps::remove_stochastic_operators(stochastic_lpsspec);
81 324 : auto builder = create_lts_builder(lpsspec, options, output_format);
82 162 : if (is_timed)
83 : {
84 6 : generate_state_space<false, true>(lpsspec, *builder, outputfile, options);
85 : }
86 : else
87 : {
88 156 : generate_state_space<false, false>(lpsspec, *builder, outputfile, options);
89 : }
90 162 : }
91 174 : }
92 :
93 : template <typename LTSType>
94 174 : void check_lts(
95 : const std::string& format,
96 : const lps::stochastic_specification& stochastic_lpsspec,
97 : data::rewrite_strategy rstrategy,
98 : lps::exploration_strategy estrategy,
99 : std::size_t expected_states,
100 : std::size_t expected_transitions,
101 : std::size_t expected_labels,
102 : const std::string& priority_action = ""
103 : )
104 : {
105 174 : std::cerr << "Translating LPS to LTS with exploration strategy " << estrategy << ", rewrite strategy " << rstrategy << "." << std::endl;
106 174 : std::cerr << format << " FORMAT\n";
107 174 : LTSType result;
108 174 : lts::lts_type output_format = result.type();
109 348 : std::string outputfile = static_cast<std::string>(boost::unit_test::framework::current_test_case().p_name) + ".generatelts" + file_extension(output_format);
110 174 : run_generatelts(stochastic_lpsspec, rstrategy, estrategy, output_format, outputfile, priority_action);
111 174 : result.load(outputfile);
112 :
113 174 : BOOST_CHECK_EQUAL(result.num_states(), expected_states);
114 174 : BOOST_CHECK_EQUAL(result.num_transitions(), expected_transitions);
115 174 : BOOST_CHECK_EQUAL(result.num_action_labels(), expected_labels);
116 :
117 174 : std::remove(outputfile.c_str());
118 174 : }
119 :
120 29 : static void check_lps2lts_specification(const std::string& specification,
121 : const std::size_t expected_states,
122 : const std::size_t expected_transitions,
123 : const std::size_t expected_labels,
124 : const std::string& priority_action = "")
125 : {
126 29 : std::cerr << "CHECK STATE SPACE GENERATION FOR:\n" << specification << "\n";
127 29 : lps::stochastic_specification lpsspec;
128 29 : parse_lps(specification, lpsspec);
129 29 : bool contains_probabilities = lps::is_stochastic(lpsspec);
130 :
131 58 : for (data::rewrite_strategy rstrategy: data::detail::get_test_rewrite_strategies(false))
132 : {
133 87 : for (lps::exploration_strategy estrategy: { lps::es_breadth, lps::es_depth })
134 : {
135 58 : if (contains_probabilities)
136 : {
137 4 : check_lts<lts::probabilistic_lts_aut_t>("PROBABILISTIC AUT", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
138 4 : check_lts<lts::probabilistic_lts_lts_t>("PROBABILISTIC LTS", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
139 4 : check_lts<lts::probabilistic_lts_fsm_t>("PROBABILISTIC FSM", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
140 : }
141 : else
142 : {
143 54 : check_lts<lts::lts_aut_t>("AUT", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
144 54 : check_lts<lts::lts_lts_t>("LTS", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
145 54 : check_lts<lts::lts_fsm_t>("FSM", lpsspec, rstrategy, estrategy, expected_states, expected_transitions, expected_labels, priority_action);
146 : }
147 : }
148 : }
149 29 : }
150 :
151 2 : BOOST_AUTO_TEST_CASE(test_a_delta)
152 : {
153 : std::string lps(
154 : "act a;\n"
155 : "proc P(b:Bool) = (b) -> a.P(!b)\n"
156 : " + delta;\n"
157 : "init P(true);\n"
158 1 : );
159 1 : check_lps2lts_specification(lps, 2, 1, 2);
160 1 : }
161 :
162 2 : BOOST_AUTO_TEST_CASE(test_abp)
163 : {
164 : std::string abp(
165 : "sort Error = struct e;\n"
166 : " D = struct d1 | d2;\n"
167 : "\n"
168 : "act i;\n"
169 : " c6,r6,s6: Error;\n"
170 : " c6,r6,s6,c5,r5,s5: Bool;\n"
171 : " c3,r3,s3: Error;\n"
172 : " c3,r3,s3,c2,r2,s2: D # Bool;\n"
173 : " s4,r1: D;\n"
174 : "\n"
175 : "glob dc,dc0,dc1,dc3,dc5,dc7,dc13,dc14,dc15,dc16,dc17,dc18: D;\n"
176 : " dc2,dc4,dc6,dc8,dc9,dc10,dc11,dc12: Bool;\n"
177 : "\n"
178 : "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"
179 : " sum d0_S: D.\n"
180 : " (s30_S == 1) ->\n"
181 : " r1(d0_S) .\n"
182 : " P(s30_S = 2, d_S = d0_S)\n"
183 : " + sum e0_K: Bool.\n"
184 : " (s31_K == 2) ->\n"
185 : " i .\n"
186 : " 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"
187 : " + sum e1_L: Bool.\n"
188 : " (s32_L == 2) ->\n"
189 : " i .\n"
190 : " P(s32_L = if(e1_L, 4, 3), b_L = if(e1_L, dc10, b_L))\n"
191 : " + (s33_R == 2) ->\n"
192 : " s4(d_R) .\n"
193 : " P(s33_R = 3, d_R = dc16)\n"
194 : " + sum e2_R: Bool.\n"
195 : " (s32_L == 1 && if(e2_R, s33_R == 4, s33_R == 3)) ->\n"
196 : " c5(if(e2_R, !b_R, b_R)) .\n"
197 : " 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"
198 : " + (s31_K == 4 && s33_R == 1) ->\n"
199 : " c3(e) .\n"
200 : " P(s31_K = 1, d_K = dc7, b_K = dc8, s33_R = 4, d_R = dc15)\n"
201 : " + sum e3_R: Bool.\n"
202 : " ((s31_K == 3 && s33_R == 1) && if(e3_R, !b_R, b_R) == b_K) ->\n"
203 : " c3(d_K, if(e3_R, !b_R, b_R)) .\n"
204 : " 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"
205 : " + (s30_S == 2 && s31_K == 1) ->\n"
206 : " c2(d_S, b_S) .\n"
207 : " P(s30_S = 3, s31_K = 2, d_K = d_S, b_K = b_S)\n"
208 : " + (s30_S == 3 && s32_L == 4) ->\n"
209 : " c6(e) .\n"
210 : " P(s30_S = 2, s32_L = 1, b_L = dc12)\n"
211 : " + sum e_S: Bool.\n"
212 : " ((s30_S == 3 && s32_L == 3) && if(e_S, b_S, !b_S) == b_L) ->\n"
213 : " c6(if(e_S, b_S, !b_S)) .\n"
214 : " 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"
215 : " + delta;\n"
216 : "\n"
217 : "init P(1, dc, true, 1, dc1, dc2, 1, dc9, 1, dc13, true);\n"
218 1 : );
219 1 : check_lps2lts_specification(abp, 74, 92, 20);
220 1 : check_lps2lts_specification(abp, 74, 92, 20, "tau");
221 1 : }
222 :
223 2 : BOOST_AUTO_TEST_CASE(test_confluence)
224 : {
225 : std::string spec(
226 : "sort State = struct S_FSM_UNINITIALIZED?isS_FSM_UNINITIALIZED | S_OFF?isS_OFF;\n"
227 : " IdList = List(Nat);\n"
228 : "\n"
229 : "act rs: State;\n"
230 : "\n"
231 : "proc P(s3_P: Pos, s1_P: State, ActPhaseArgs_pp2_P: IdList) =\n"
232 : " (s3_P == 1 && ActPhaseArgs_pp2_P == []) ->\n"
233 : " tau .\n"
234 : " P(s3_P = 1, s1_P = S_FSM_UNINITIALIZED, ActPhaseArgs_pp2_P = [12, 9])\n"
235 : " + sum s11_P: State.\n"
236 : " (s3_P == 1 && !(ActPhaseArgs_pp2_P == [])) ->\n"
237 : " rs(s11_P) .\n"
238 : " P(s3_P = 2, s1_P = s11_P)\n"
239 : " + delta;\n"
240 : "\n"
241 : "init P(1, S_FSM_UNINITIALIZED, []);\n"
242 1 : );
243 1 : check_lps2lts_specification(spec, 4, 3, 3);
244 1 : check_lps2lts_specification(spec, 3, 2, 3, "tau");
245 1 : }
246 :
247 2 : BOOST_AUTO_TEST_CASE(test_function_updates)
248 : {
249 : std::string spec(
250 : "act set,s: Pos;\n"
251 : "map f:Pos->Bool;\n"
252 : "var n:Pos;\n"
253 : "eqn f(n)=false;\n"
254 : "\n"
255 : "proc P(b_Sensor: Pos -> Bool) =\n"
256 : " sum n_Sensor: Pos.\n"
257 : " (n_Sensor <= 2) ->\n"
258 : " s(n_Sensor) .\n"
259 : " P(b_Sensor = b_Sensor[n_Sensor -> true])\n"
260 : " + sum n_Sensor0: Pos.\n"
261 : " (b_Sensor(n_Sensor0) && n_Sensor0 <= 2) ->\n"
262 : " set(n_Sensor0) .\n"
263 : " P(b_Sensor = b_Sensor[n_Sensor0 -> false])\n"
264 : " + delta;\n"
265 : "\n"
266 : "init P(f);\n"
267 1 : );
268 1 : check_lps2lts_specification(spec, 4, 12, 5);
269 1 : }
270 :
271 2 : BOOST_AUTO_TEST_CASE(test_timed) // For bug #756
272 : {
273 : std::string spec(
274 : "act a,Terminate;\n"
275 : "\n"
276 : "proc P(s3: Pos) =\n"
277 : " (s3 == 1) ->\n"
278 : " a @ 3 .\n"
279 : " P(s3 = 2)\n"
280 : " + (s3 == 2) ->\n"
281 : " Terminate .\n"
282 : " P(s3 = 3)\n"
283 : " + (s3 == 3) ->\n"
284 : " delta;\n"
285 : "\n"
286 : "init P(1);\n"
287 1 : );
288 1 : check_lps2lts_specification(spec, 3, 2, 3);
289 1 : }
290 :
291 2 : BOOST_AUTO_TEST_CASE(test_struct)
292 : {
293 : std::string spec(
294 : "sort Bits = struct b0 | b1;\n"
295 : " t_sys_regset_fsm_state = Bits;\n"
296 : " t_timer_counter_fsm_state = Bits;\n"
297 : "map timer_counter_fsm_state_idle: Bits;\n"
298 : "act a: t_sys_regset_fsm_state;\n"
299 : "glob globd: t_sys_regset_fsm_state;\n"
300 : "proc P(s3_P: Pos) =\n"
301 : " (s3_P == 1) ->\n"
302 : " a(globd) .\n"
303 : " P(s3_P = 2)\n"
304 : " + delta;\n"
305 : "init P(1);\n"
306 1 : );
307 1 : check_lps2lts_specification(spec, 2, 1, 2);
308 1 : }
309 :
310 2 : BOOST_AUTO_TEST_CASE(test_alias_complex)
311 : {
312 : std::string spec(
313 : "sort Bits = struct singleBit(bit: Bool)?isSingleBit | bitVector(bitVec: List(Bool))?isBitVector;\n"
314 : " t_sys_regset_fsm_state = Bits;\n"
315 : " t_timer_counter_fsm_state = Bits;\n"
316 : "\n"
317 : "map repeat_rec: Bool # Nat -> List(Bool);\n"
318 : " repeat: Bool # Nat -> Bits;\n"
319 : "\n"
320 : "var b: Bool;\n"
321 : " n: Nat;\n"
322 : "eqn repeat(b, n) = if(n <= 1, singleBit(b), bitVector(repeat_rec(b, n)));\n"
323 : "\n"
324 : "act a: t_sys_regset_fsm_state;\n"
325 : "\n"
326 : "proc P(s3: Pos) =\n"
327 : " (s3 == 1) ->\n"
328 : " a(repeat(true, 32)) .\n"
329 : " P(s3 = 2)\n"
330 : " + delta;\n"
331 : "\n"
332 : "init P(1);\n"
333 1 : );
334 1 : check_lps2lts_specification(spec, 2, 1, 2);
335 1 : }
336 :
337 2 : BOOST_AUTO_TEST_CASE(test_equality_with_empty_set)
338 : {
339 : std::string spec(
340 : "map emptyset:Set(Bool);\n"
341 : "eqn emptyset={};\n"
342 : "proc P=({ b: Bool | false } == emptyset) -> tau.P;\n"
343 : "init P;"
344 1 : );
345 1 : check_lps2lts_specification(spec, 1, 1, 1);
346 1 : }
347 :
348 2 : BOOST_AUTO_TEST_CASE(test_equality_of_finite_sets)
349 : {
350 : std::string spec(
351 : "sort R = struct r2 | r1 ;\n"
352 : "map All: Set(R);\n"
353 : "eqn All = { r: R | true };\n"
354 : "proc P=({r1, r2} == All) -> tau.P;\n"
355 : "init P;"
356 1 : );
357 1 : check_lps2lts_specification(spec, 1, 1, 1);
358 1 : }
359 :
360 : // Example from bug #832
361 2 : BOOST_AUTO_TEST_CASE(test_plus)
362 : {
363 : // This example provides two identical transitions between a state.
364 : // There is a discussion on whether this is desirable. Currently, for
365 : // efficiency reasons such extra transitions are not removed by lps2lts.
366 : std::string spec(
367 : "act a;\n"
368 : "proc P = a.P + a.P;\n"
369 : "init P;\n"
370 1 : );
371 1 : check_lps2lts_specification(spec, 1, 2, 2);
372 1 : }
373 :
374 : // The example below fails if #[0,1] does not have a decent
375 : // type. The tricky thing is that the type of the list can be List(Nat),
376 : // List(Int) or List(Real). Toolset version 10180 resolved this by
377 : // delivering the type List({Nat, Int, Real}), i.e. a set of possible
378 : // options. But this was not expected and understood by the other tools.
379 : // This is related to bug report #949.
380 2 : BOOST_AUTO_TEST_CASE(test_well_typedness_of_length_of_list_of_numbers)
381 : {
382 : std::string spec(
383 : "proc B (i:Int) = (i >= 2) -> tau. B();\n"
384 : "init B(#[0,1]);\n"
385 1 : );
386 1 : check_lps2lts_specification(spec, 1, 1, 1);
387 1 : }
388 :
389 : #if 0 // This test has been disabled; it was decided not to fix this issue.
390 : // The following example illustrates that enumeration can sometimes need
391 : // a large stack depth.
392 : // The example was attached to bug #1019, and fails with limited stack,
393 : // succeeds with unlimited stack.
394 : BOOST_AUTO_TEST_CASE(test_deep_stack)
395 : {
396 : std::string spec(
397 : "sort Packet = struct packet(d0: Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool, Bool);\n"
398 : "act Terminate;\n"
399 : "proc P(s3: Pos) =\n"
400 : " (s3 == 2) ->\n"
401 : " Terminate .\n"
402 : " P(s3 = 3)\n"
403 : " + sum p: Packet.\n"
404 : " (s3 == 1) ->\n"
405 : " tau .\n"
406 : " P(s3 = 2)\n"
407 : " + delta;\n"
408 : "init P(1);\n"
409 : );
410 : check_lps2lts_specification(spec, 3, 524289, 2);
411 : }
412 : #endif // false
413 :
414 :
415 2 : BOOST_AUTO_TEST_CASE(test_interaction_sum_and_assignment_notation1)
416 : {
417 : std::string spec(
418 : "proc B (i:Bool) = sum i:Bool.tau. B();\n"
419 : "init B(true);\n"
420 1 : );
421 1 : check_lps2lts_specification(spec, 1, 2, 1);
422 1 : }
423 :
424 2 : BOOST_AUTO_TEST_CASE(test_interaction_sum_and_assignment_notation2)
425 : {
426 : std::string spec(
427 : "proc B (i:Bool) = sum i:Bool.tau. B(i=i);\n"
428 : "init B(true);\n"
429 1 : );
430 1 : check_lps2lts_specification(spec, 2, 4, 1);
431 1 : }
432 :
433 2 : BOOST_AUTO_TEST_CASE(test_whether_function_update_is_declared)
434 : {
435 : std::string spec(
436 : "sort T = struct a|b;\n"
437 : "act int;\n"
438 : "map g: Bool -> T;\n"
439 : "var y: Bool;\n"
440 : "eqn g(y) = a;\n"
441 : "act d: Bool -> T;\n"
442 : "proc P(f: Bool -> T) = int . P(f[true->b]);\n"
443 : "init P(g) ;\n"
444 1 : );
445 1 : check_lps2lts_specification(spec, 2, 2, 2);
446 1 : }
447 :
448 2 : BOOST_AUTO_TEST_CASE(test_whether_bag_enumeration_with_similar_elements_is_allowed)
449 : {
450 : std::string spec(
451 : "sort S = struct s1 | s2;\n"
452 : "act int;\n"
453 : "proc P(b: Bag(S)) = (count(s1, b) < 3) -> int.P();\n"
454 : "init P({s1: 1, s1: 1});\n"
455 1 : );
456 1 : check_lps2lts_specification(spec, 1, 1, 2);
457 1 : }
458 :
459 2 : BOOST_AUTO_TEST_CASE(test_whether_functions_to_functions_are_causing_problems)
460 : {
461 : std::string spec(
462 : "map f:Nat->Nat->Nat->Nat;\n"
463 : " g:Nat->Nat;\n"
464 : "var x,y,z:Nat;"
465 : "eqn f(x)(y)(z)=x+y+z;\n"
466 : " f(x)(y)=g;\n"
467 : "act int:Nat;\n"
468 : "proc P = int(f(1)(2)(3)).P();\n"
469 : "init P;\n"
470 1 : );
471 1 : check_lps2lts_specification(spec, 1, 1, 2);
472 1 : }
473 :
474 2 : BOOST_AUTO_TEST_CASE(test_whether_functions_can_be_enumerated)
475 : {
476 : std::string spec(
477 : "act int:Bool->Bool;\n"
478 : "proc P = sum f:Bool->Bool.int(f).P;\n"
479 : "init P;\n"
480 1 : );
481 1 : check_lps2lts_specification(spec, 1, 4, 5);
482 1 : }
483 :
484 2 : BOOST_AUTO_TEST_CASE(test_whether_functions_with_more_arguments_can_be_enumerated)
485 : {
486 : std::string spec(
487 : "act int:Bool#Bool#Bool->Bool;\n"
488 : "proc P = sum f:Bool#Bool#Bool->Bool.f(true,true,true)->int(f).P;\n"
489 : "init P;\n"
490 1 : );
491 1 : check_lps2lts_specification(spec, 1, 128, 129);
492 1 : }
493 :
494 2 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_can_be_enumerated)
495 : {
496 : std::string spec(
497 : "act int:FSet(Bool);\n"
498 : "proc P = sum f:FSet(Bool).int(f).P;\n"
499 : "init P;\n"
500 1 : );
501 1 : check_lps2lts_specification(spec, 1, 4, 5);
502 1 : }
503 :
504 2 : BOOST_AUTO_TEST_CASE(test_whether_sets_can_be_enumerated)
505 : {
506 : std::string spec(
507 : "act int:FSet(Bool);\n"
508 : "proc P = sum f:FSet(Bool).int(f).P;\n"
509 : "init P;\n"
510 1 : );
511 1 : check_lps2lts_specification(spec, 1, 4, 5);
512 1 : }
513 :
514 2 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_with_conditions_can_be_enumerated)
515 : {
516 : std::string spec(
517 : "act int:FSet(Bool);\n"
518 : "proc P = sum f:FSet(Bool).(true in f) -> int(f).P;\n"
519 : "init P;\n"
520 1 : );
521 1 : check_lps2lts_specification(spec, 1, 2, 3);
522 1 : }
523 :
524 2 : BOOST_AUTO_TEST_CASE(test_whether_sets_with_conditions_can_be_enumerated)
525 : {
526 : std::string spec(
527 : "act int:Set(Bool);\n"
528 : "proc P = sum f:Set(Bool).(true in f) -> int(f).P;\n"
529 : "init P;\n"
530 1 : );
531 1 : check_lps2lts_specification(spec, 1, 2, 3);
532 1 : }
533 :
534 2 : BOOST_AUTO_TEST_CASE(test_whether_finite_sets_of_functions_can_be_enumerated)
535 : {
536 : std::string spec(
537 : "act int:FSet(Bool->Bool);\n"
538 : "proc P = sum f:FSet(Bool->Bool).((lambda x:Bool.true) in f) -> int(f).P;\n"
539 : "init P;\n"
540 1 : );
541 1 : check_lps2lts_specification(spec, 1, 8, 9);
542 1 : }
543 :
544 2 : BOOST_AUTO_TEST_CASE(test_whether_sets_of_functions_can_be_enumerated)
545 : {
546 : std::string spec(
547 : "act int:Set(Bool->Bool);\n"
548 : "proc P = sum f:Set(Bool->Bool).((lambda x:Bool.true) in f) -> int(f).P;\n"
549 : "init P;\n"
550 1 : );
551 1 : check_lps2lts_specification(spec, 1, 8, 9);
552 1 : }
553 :
554 2 : BOOST_AUTO_TEST_CASE(test_whether_probabilistic_state_spaces_are_generated_correctly) // Related to #1542
555 : {
556 : std::string spec(
557 : "act a;\n"
558 : "proc P(b:Bool) = b->a.P(false);\n"
559 : "init dist b: Bool[if(b, 1 / 4, 3 / 4)] . P(b);\n"
560 1 : );
561 1 : check_lps2lts_specification(spec, 2, 1, 2);
562 1 : }
563 :
564 2 : BOOST_AUTO_TEST_CASE(coins_simulate_dice) // Example from the probabilistic examples directory.
565 : {
566 : std::string spec(
567 : "act flip: Bool;\n"
568 : " dice: Nat;\n"
569 : "\n"
570 : "glob dc,dc3,dc4,dc5,dc6,dc7,dc8,dc9,dc10,dc11,dc12,dc13,dc14,dc15,dc16,dc17,dc18,dc19: Bool;\n"
571 : " dc1,dc2: Nat;\n"
572 : "\n"
573 : "proc P(s1: Pos, b3,b2: Bool, s,d: Nat) =\n"
574 : " (s1 == 1 && b2 && s == 0) ->\n"
575 : " flip(b2) .\n"
576 : " dist b2: Bool[1 / 2] .\n"
577 : " P(s1 = 1, b3 = dc3, b2 = b2, s = 1, d = 0)\n"
578 : " + (s1 == 1 && !b2 && s == 0) ->\n"
579 : " flip(b2) .\n"
580 : " dist b2: Bool[1 / 2] .\n"
581 : " P(s1 = 1, b3 = dc4, b2 = b2, s = 2, d = 0)\n"
582 : " + (s1 == 1 && b2 && s == 1 && !(s == 0)) ->\n"
583 : " flip(b2) .\n"
584 : " dist b2: Bool[1 / 2] .\n"
585 : " P(s1 = 1, b3 = dc5, b2 = b2, s = 3, d = 0)\n"
586 : " + (s1 == 1 && !b2 && s == 1 && !(s == 0)) ->\n"
587 : " flip(b2) .\n"
588 : " dist b2: Bool[1 / 2] .\n"
589 : " P(s1 = 1, b3 = dc6, b2 = b2, s = 4, d = 0)\n"
590 : " + (s1 == 1 && b2 && s == 2 && !(s == 1) && !(s == 0)) ->\n"
591 : " flip(b2) .\n"
592 : " dist b2: Bool[1 / 2] .\n"
593 : " P(s1 = 1, b3 = dc7, b2 = b2, s = 5, d = 0)\n"
594 : " + (s1 == 1 && !b2 && s == 2 && !(s == 1) && !(s == 0)) ->\n"
595 : " flip(b2) .\n"
596 : " dist b2: Bool[1 / 2] .\n"
597 : " P(s1 = 1, b3 = dc8, b2 = b2, s = 6, d = 0)\n"
598 : " + (s1 == 1 && b2 && s == 3 && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
599 : " flip(b2) .\n"
600 : " dist b2: Bool[1 / 2] .\n"
601 : " P(s1 = 1, b3 = dc9, b2 = b2, s = 1, d = 0)\n"
602 : " + (s1 == 1 && !b2 && s == 3 && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
603 : " flip(b2) .\n"
604 : " dist b2: Bool[1 / 2] .\n"
605 : " P(s1 = 1, b3 = dc10, b2 = b2, s = 7, d = 1)\n"
606 : " + (s1 == 1 && b2 && s == 4 && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
607 : " flip(b2) .\n"
608 : " dist b2: Bool[1 / 2] .\n"
609 : " P(s1 = 1, b3 = dc11, b2 = b2, s = 7, d = 2)\n"
610 : " + (s1 == 1 && !b2 && s == 4 && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
611 : " flip(b2) .\n"
612 : " dist b2: Bool[1 / 2] .\n"
613 : " P(s1 = 1, b3 = dc12, b2 = b2, s = 7, d = 3)\n"
614 : " + (s1 == 1 && b2 && s == 5 && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
615 : " flip(b2) .\n"
616 : " dist b2: Bool[1 / 2] .\n"
617 : " P(s1 = 1, b3 = dc13, b2 = b2, s = 7, d = 4)\n"
618 : " + (s1 == 1 && !b2 && s == 5 && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
619 : " flip(b2) .\n"
620 : " dist b2: Bool[1 / 2] .\n"
621 : " P(s1 = 1, b3 = dc14, b2 = b2, s = 7, d = 5)\n"
622 : " + (s1 == 1 && b2 && s == 6 && !(s == 5) && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
623 : " flip(b2) .\n"
624 : " dist b2: Bool[1 / 2] .\n"
625 : " P(s1 = 1, b3 = dc15, b2 = b2, s = 7, d = 6)\n"
626 : " + (s1 == 1 && !b2 && s == 6 && !(s == 5) && !(s == 4) && !(s == 3) && !(s == 2) && !(s == 1) && !(s == 0)) ->\n"
627 : " flip(b2) .\n"
628 : " dist b2: Bool[1 / 2] .\n"
629 : " P(s1 = 1, b3 = dc16, b2 = b2, s = 2, d = 0)\n"
630 : " + (s1 == 1 && s == 7) ->\n"
631 : " dice(d) .\n"
632 : " dist b2: Bool[1 / 2] .\n"
633 : " P(s1 = 1, b3 = dc17, b2 = b2)\n"
634 : " + (s1 == 2 && b3) ->\n"
635 : " flip(b3) .\n"
636 : " dist b2: Bool[1 / 2] .\n"
637 : " P(s1 = 1, b3 = dc18, b2 = b2, s = 1, d = 0)\n"
638 : " + (s1 == 2 && !b3) ->\n"
639 : " flip(b3) .\n"
640 : " dist b2: Bool[1 / 2] .\n"
641 : " P(s1 = 1, b3 = dc19, b2 = b2, s = 2, d = 0)\n"
642 : " + delta;\n"
643 : "\n"
644 : "init dist b3: Bool[1 / 2] . P(2, b3, dc, dc1, dc2);\n"
645 1 : );
646 1 : check_lps2lts_specification(spec, 26, 26, 9);
647 1 : }
648 :
649 2 : BOOST_AUTO_TEST_CASE(test_whether_action_a_b_and_b_a_are_the_same) // Related to #1595
650 : {
651 : std::string spec(
652 : "act a,b;\n"
653 : "proc P = a|b.P+\n"
654 : " b|a.P;\n"
655 : "init P;\n"
656 1 : );
657 1 : check_lps2lts_specification(spec, 1, 2, 2);
658 1 : }
659 :
660 :
|
