Line data Source code
1 : // Author(s): anonymous
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 : #define BOOST_TEST_MODULE lts_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lts/lts_algorithm.h"
16 :
17 : using namespace mcrl2;
18 :
19 : class expected_sizes
20 : {
21 : public:
22 : std::size_t states_plain, transitions_plain, labels_plain;
23 : std::size_t states_bisimulation, transitions_bisimulation, labels_bisimulation;
24 : std::size_t states_branching_bisimulation, transitions_branching_bisimulation, labels_branching_bisimulation;
25 : std::size_t states_divergence_preserving_branching_bisimulation, transitions_divergence_preserving_branching_bisimulation, labels_divergence_preserving_branching_bisimulation;
26 : std::size_t states_weak_bisimulation, transitions_weak_bisimulation, labels_weak_bisimulation;
27 : std::size_t states_divergence_preserving_weak_bisimulation, transitions_divergence_preserving_weak_bisimulation, labels_divergence_preserving_weak_bisimulation;
28 : std::size_t states_simulation, transitions_simulation, labels_simulation;
29 : std::size_t states_trace_equivalence, transitions_trace_equivalence, labels_trace_equivalence;
30 : std::size_t states_weak_trace_equivalence, transitions_weak_trace_equivalence, labels_weak_trace_equivalence;
31 : std::size_t states_determinisation, transitions_determinisation, labels_determinisation;
32 : bool is_deterministic;
33 : };
34 :
35 118 : static void test_lts(const std::string& test_description,
36 : const lts::lts_aut_t& l,
37 : std::size_t expected_label_count,
38 : std::size_t expected_state_count,
39 : std::size_t expected_transition_count
40 : )
41 : {
42 118 : std::cerr << "LPS test: " << test_description << " -----------------------------------------------\n";
43 118 : BOOST_CHECK(l.num_action_labels() == expected_label_count);
44 118 : if (l.num_action_labels() != expected_label_count)
45 : {
46 0 : std::cerr << "Expected # of labels " << expected_label_count << " Actual # " << l.num_action_labels() << "\n";
47 : }
48 118 : BOOST_CHECK(l.num_states() == expected_state_count);
49 118 : if (l.num_states() != expected_state_count)
50 : {
51 0 : std::cerr << "Expected # of states " << expected_state_count << " Actual # " << l.num_states() << "\n";
52 : }
53 118 : BOOST_CHECK(l.num_transitions() == expected_transition_count);
54 118 : if (l.num_transitions() != expected_transition_count)
55 : {
56 0 : std::cerr << "Expected # of transitions " << expected_transition_count << " Actual # " << l.num_transitions() << "\n";
57 : }
58 118 : }
59 :
60 5 : static void reduce_lts_in_various_ways(const std::string& test_description,
61 : const std::string& lts,
62 : const expected_sizes& expected)
63 : {
64 5 : std::istringstream is(lts);
65 5 : lts::lts_aut_t l_in;
66 5 : l_in.load(is);
67 5 : test_lts(test_description + " (plain input)",l_in, expected.labels_plain,expected.states_plain, expected.transitions_plain);
68 5 : lts::lts_aut_t l=l_in;
69 5 : reduce(l,lts::lts_eq_none);
70 5 : test_lts(test_description + " (no reduction)",l, expected.labels_plain,expected.states_plain, expected.transitions_plain);
71 5 : l=l_in;
72 5 : reduce(l,lts::lts_eq_bisim);
73 5 : test_lts(test_description + " (bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
74 5 : l=l_in;
75 5 : reduce(l,lts::lts_eq_bisim_gv);
76 5 : test_lts(test_description + " (bisimulation [Groote/Vaandrager 1990])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
77 5 : l=l_in;
78 5 : reduce(l,lts::lts_eq_bisim_gjkw);
79 5 : test_lts(test_description + " (bisimulation [Groote/Jansen/Keiren/Wijs 2017)",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
80 5 : l=l_in;
81 5 : reduce(l,lts::lts_eq_bisim_sigref);
82 5 : test_lts(test_description + " (bisimulation signature [Blom/Orzan 2003])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
83 5 : l=l_in;
84 5 : reduce(l,lts::lts_eq_branching_bisim);
85 5 : test_lts(test_description + " (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
86 5 : l=l_in;
87 5 : reduce(l,lts::lts_eq_branching_bisim_gv);
88 5 : test_lts(test_description + " (branching bisimulation [Groote/Vaandrager 1990])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
89 5 : l=l_in;
90 5 : reduce(l,lts::lts_eq_branching_bisim_gjkw);
91 5 : test_lts(test_description + " (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
92 5 : l=l_in;
93 5 : reduce(l,lts::lts_eq_branching_bisim_sigref);
94 5 : test_lts(test_description + " (branching bisimulation signature [Blom/Orzan 2003])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
95 5 : l=l_in;
96 5 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim);
97 5 : test_lts(test_description + " (divergence-preserving branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,
98 5 : expected.labels_divergence_preserving_branching_bisimulation,
99 5 : expected.states_divergence_preserving_branching_bisimulation,
100 5 : expected.transitions_divergence_preserving_branching_bisimulation);
101 5 : l=l_in;
102 5 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gv);
103 5 : test_lts(test_description + " (divergence-preserving branching bisimulation [Groote/Vaandrager 1990])",l,
104 5 : expected.labels_divergence_preserving_branching_bisimulation,
105 5 : expected.states_divergence_preserving_branching_bisimulation,
106 5 : expected.transitions_divergence_preserving_branching_bisimulation);
107 5 : l=l_in;
108 5 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gjkw);
109 5 : test_lts(test_description + " (divergence-preserving branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,
110 5 : expected.labels_divergence_preserving_branching_bisimulation,
111 5 : expected.states_divergence_preserving_branching_bisimulation,
112 5 : expected.transitions_divergence_preserving_branching_bisimulation);
113 5 : l=l_in;
114 5 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_sigref);
115 5 : test_lts(test_description + " (divergence-preserving branching bisimulation signature [Blom/Orzan 2003])",l,
116 5 : expected.labels_divergence_preserving_branching_bisimulation,
117 5 : expected.states_divergence_preserving_branching_bisimulation,
118 5 : expected.transitions_divergence_preserving_branching_bisimulation);
119 5 : l=l_in;
120 5 : reduce(l,lts::lts_eq_weak_bisim);
121 5 : test_lts(test_description + " (weak bisimulation)",l, expected.labels_weak_bisimulation,expected.states_weak_bisimulation, expected.transitions_weak_bisimulation);
122 5 : l=l_in;
123 5 : reduce(l,lts::lts_eq_divergence_preserving_weak_bisim);
124 5 : test_lts(test_description + " (divergence-preserving weak bisimulation)",l,
125 5 : expected.labels_divergence_preserving_weak_bisimulation,
126 5 : expected.states_divergence_preserving_weak_bisimulation,
127 5 : expected.transitions_divergence_preserving_weak_bisimulation);
128 5 : l=l_in;
129 5 : reduce(l,lts::lts_eq_sim);
130 5 : test_lts(test_description + " (simulation equivalence)",l, expected.labels_simulation,expected.states_simulation, expected.transitions_simulation);
131 5 : l=l_in;
132 5 : reduce(l,lts::lts_eq_trace);
133 5 : test_lts(test_description + " (trace equivalence)",l, expected.labels_trace_equivalence,expected.states_trace_equivalence, expected.transitions_trace_equivalence);
134 5 : l=l_in;
135 5 : reduce(l,lts::lts_eq_weak_trace);
136 5 : test_lts(test_description + " (weak trace equivalence)",l, expected.labels_weak_trace_equivalence,expected.states_weak_trace_equivalence, expected.transitions_weak_trace_equivalence);
137 5 : l=l_in;
138 5 : if (expected.is_deterministic)
139 : {
140 3 : BOOST_CHECK(is_deterministic(l));
141 : }
142 : else
143 : {
144 2 : BOOST_CHECK(!is_deterministic(l));
145 : }
146 :
147 5 : reduce(l,lts::lts_red_determinisation);
148 5 : test_lts(test_description + " (determinisation)",l, expected.labels_determinisation,expected.states_determinisation, expected.transitions_determinisation);
149 5 : BOOST_CHECK(is_deterministic(l));
150 5 : }
151 :
152 2 : BOOST_AUTO_TEST_CASE(reduce_simple_loop)
153 : {
154 : std::string SIMPLE_AUT =
155 : "des (0,2,2)\n"
156 : "(0,\"a\",1)\n"
157 1 : "(1,\"a\",0)\n"
158 : ;
159 :
160 : expected_sizes expected;
161 1 : expected.states_plain=2; expected.transitions_plain=2; expected.labels_plain=2;
162 1 : expected.states_bisimulation=1, expected.transitions_bisimulation=1, expected.labels_bisimulation=2;
163 1 : expected.states_branching_bisimulation=1, expected.transitions_branching_bisimulation=1, expected.labels_branching_bisimulation=2;
164 1 : expected.states_divergence_preserving_branching_bisimulation=1, expected.transitions_divergence_preserving_branching_bisimulation=1, expected.labels_divergence_preserving_branching_bisimulation=2;
165 1 : expected.states_weak_bisimulation=1, expected.transitions_weak_bisimulation=1, expected.labels_weak_bisimulation=2;
166 1 : expected.states_divergence_preserving_weak_bisimulation=1, expected.transitions_divergence_preserving_weak_bisimulation=1, expected.labels_divergence_preserving_weak_bisimulation=3;
167 1 : expected.states_simulation=1, expected.transitions_simulation=1, expected.labels_simulation=2;
168 1 : expected.states_trace_equivalence=1, expected.transitions_trace_equivalence=1, expected.labels_trace_equivalence=2;
169 1 : expected.states_weak_trace_equivalence=1, expected.transitions_weak_trace_equivalence=1, expected.labels_weak_trace_equivalence=2;
170 1 : expected.states_determinisation=2, expected.transitions_determinisation=2, expected.labels_determinisation=2;
171 1 : expected.is_deterministic=true;
172 :
173 1 : reduce_lts_in_various_ways("Simple loop", SIMPLE_AUT, expected);
174 1 : }
175 :
176 2 : BOOST_AUTO_TEST_CASE(reduce_simple_loop_with_tau)
177 : {
178 : std::string SIMPLE_AUT =
179 : "des (0,2,2)\n"
180 : "(0,\"a\",1)\n"
181 1 : "(1,\"tau\",0)\n"
182 : ;
183 :
184 : expected_sizes expected;
185 1 : expected.states_plain=2; expected.transitions_plain=2; expected.labels_plain=2;
186 1 : expected.states_bisimulation=2, expected.transitions_bisimulation=2, expected.labels_bisimulation=2;
187 1 : expected.states_branching_bisimulation=1, expected.transitions_branching_bisimulation=1, expected.labels_branching_bisimulation=2;
188 1 : expected.states_divergence_preserving_branching_bisimulation=1, expected.transitions_divergence_preserving_branching_bisimulation=1, expected.labels_divergence_preserving_branching_bisimulation=2;
189 1 : expected.states_weak_bisimulation=1, expected.transitions_weak_bisimulation=1, expected.labels_weak_bisimulation=2;
190 1 : expected.states_divergence_preserving_weak_bisimulation=1, expected.transitions_divergence_preserving_weak_bisimulation=1, expected.labels_divergence_preserving_weak_bisimulation=3;
191 1 : expected.states_simulation=2, expected.transitions_simulation=2, expected.labels_simulation=2;
192 1 : expected.states_trace_equivalence=2, expected.transitions_trace_equivalence=2, expected.labels_trace_equivalence=2;
193 1 : expected.states_weak_trace_equivalence=1, expected.transitions_weak_trace_equivalence=1, expected.labels_weak_trace_equivalence=2;
194 1 : expected.states_determinisation=2, expected.transitions_determinisation=2, expected.labels_determinisation=2;
195 1 : expected.is_deterministic=true;
196 :
197 1 : reduce_lts_in_various_ways("Simple loop with tau", SIMPLE_AUT, expected);
198 1 : }
199 :
200 : /* The example below was encountered by David Jansen. The problem is that
201 : * for branching bisimulations the tau may supersede the b, not leading to the
202 : * necessary splitting into two equivalence classes. */
203 2 : BOOST_AUTO_TEST_CASE(tricky_example_for_branching_bisimulation)
204 : {
205 : std::string TRICKY_BB =
206 : "des (0,3,2)\n"
207 : "(0,\"a\",1)\n"
208 : "(1,\"b\",0)\n"
209 1 : "(1,\"tau\",0)\n"
210 : ;
211 :
212 : expected_sizes expected;
213 1 : expected.states_plain=2; expected.transitions_plain=3; expected.labels_plain=3;
214 1 : expected.states_bisimulation=2, expected.transitions_bisimulation=3, expected.labels_bisimulation=3;
215 1 : expected.states_branching_bisimulation=2, expected.transitions_branching_bisimulation=3, expected.labels_branching_bisimulation=3;
216 1 : expected.states_divergence_preserving_branching_bisimulation=2, expected.transitions_divergence_preserving_branching_bisimulation=3, expected.labels_divergence_preserving_branching_bisimulation=3;
217 1 : expected.states_weak_bisimulation=2, expected.transitions_weak_bisimulation=3, expected.labels_weak_bisimulation=3;
218 1 : expected.states_divergence_preserving_weak_bisimulation=2, expected.transitions_divergence_preserving_weak_bisimulation=3, expected.labels_divergence_preserving_weak_bisimulation=4;
219 1 : expected.states_simulation=2, expected.transitions_simulation=3, expected.labels_simulation=3;
220 1 : expected.states_trace_equivalence=2, expected.transitions_trace_equivalence=3, expected.labels_trace_equivalence=3;
221 1 : expected.states_weak_trace_equivalence=2, expected.transitions_weak_trace_equivalence=3, expected.labels_weak_trace_equivalence=3;
222 1 : expected.states_determinisation=2, expected.transitions_determinisation=3, expected.labels_determinisation=3;
223 1 : expected.is_deterministic=true;
224 :
225 1 : reduce_lts_in_various_ways("Tricky example for branching bisimulation", TRICKY_BB, expected);
226 1 : }
227 :
228 :
229 2 : BOOST_AUTO_TEST_CASE(reduce_abp)
230 : {
231 : std::string ABP_AUT =
232 : "des (0,92,74)\n"
233 : "(0,\"r1(d1)\",1)\n"
234 : "(0,\"r1(d2)\",2)\n"
235 : "(1,\"tau\",3)\n"
236 : "(2,\"tau\",4)\n"
237 : "(3,\"tau\",5)\n"
238 : "(3,\"tau\",6)\n"
239 : "(4,\"tau\",7)\n"
240 : "(4,\"tau\",8)\n"
241 : "(5,\"tau\",9)\n"
242 : "(6,\"tau\",10)\n"
243 : "(7,\"tau\",11)\n"
244 : "(8,\"tau\",12)\n"
245 : "(9,\"tau\",13)\n"
246 : "(10,\"s4(d1)\",14)\n"
247 : "(11,\"tau\",15)\n"
248 : "(12,\"s4(d2)\",16)\n"
249 : "(13,\"tau\",17)\n"
250 : "(13,\"tau\",18)\n"
251 : "(14,\"tau\",19)\n"
252 : "(15,\"tau\",20)\n"
253 : "(15,\"tau\",21)\n"
254 : "(16,\"tau\",22)\n"
255 : "(17,\"tau\",1)\n"
256 : "(18,\"tau\",1)\n"
257 : "(19,\"tau\",23)\n"
258 : "(19,\"tau\",24)\n"
259 : "(20,\"tau\",2)\n"
260 : "(21,\"tau\",2)\n"
261 : "(22,\"tau\",25)\n"
262 : "(22,\"tau\",26)\n"
263 : "(23,\"tau\",27)\n"
264 : "(24,\"tau\",28)\n"
265 : "(25,\"tau\",29)\n"
266 : "(26,\"tau\",28)\n"
267 : "(27,\"tau\",30) \n"
268 : "(28,\"r1(d1)\",31)\n"
269 : "(28,\"r1(d2)\",32)\n"
270 : "(29,\"tau\",33)\n"
271 : "(30,\"tau\",34)\n"
272 : "(30,\"tau\",35)\n"
273 : "(31,\"tau\",36)\n"
274 : "(32,\"tau\",37)\n"
275 : "(33,\"tau\",38)\n"
276 : "(33,\"tau\",39)\n"
277 : "(34,\"tau\",40)\n"
278 : "(35,\"tau\",40)\n"
279 : "(36,\"tau\",41)\n"
280 : "(36,\"tau\",42)\n"
281 : "(37,\"tau\",43)\n"
282 : "(37,\"tau\",44)\n"
283 : "(38,\"tau\",45)\n"
284 : "(39,\"tau\",45)\n"
285 : "(40,\"tau\",19)\n"
286 : "(41,\"tau\",46)\n"
287 : "(42,\"tau\",47)\n"
288 : "(43,\"tau\",48)\n"
289 : "(44,\"tau\",49)\n"
290 : "(45,\"tau\",22)\n"
291 : "(46,\"tau\",50)\n"
292 : "(47,\"s4(d1)\",51)\n"
293 : "(48,\"tau\",52)\n"
294 : "(49,\"s4(d2)\",53)\n"
295 : "(50,\"tau\",54)\n"
296 : "(50,\"tau\",55)\n"
297 : "(51,\"tau\",56)\n"
298 : "(52,\"tau\",57)\n"
299 : "(52,\"tau\",58)\n"
300 : "(53,\"tau\",59)\n"
301 : "(54,\"tau\",31)\n"
302 : "(55,\"tau\",31)\n"
303 : "(56,\"tau\",60)\n"
304 : "(56,\"tau\",61)\n"
305 : "(57,\"tau\",32)\n"
306 : "(58,\"tau\",32)\n"
307 : "(59,\"tau\",62)\n"
308 : "(59,\"tau\",63)\n"
309 : "(60,\"tau\",64)\n"
310 : "(61,\"tau\",0)\n"
311 : "(62,\"tau\",65)\n"
312 : "(63,\"tau\",0)\n"
313 : "(64,\"tau\",66)\n"
314 : "(65,\"tau\",67)\n"
315 : "(66,\"tau\",68)\n"
316 : "(66,\"tau\",69)\n"
317 : "(67,\"tau\",70)\n"
318 : "(67,\"tau\",71)\n"
319 : "(68,\"tau\",72)\n"
320 : "(69,\"tau\",72)\n"
321 : "(70,\"tau\",73)\n"
322 : "(71,\"tau\",73)\n"
323 : "(72,\"tau\",56)\n"
324 1 : "(73,\"tau\",59)\n"
325 : ;
326 :
327 : expected_sizes expected;
328 1 : expected.states_plain=74; expected.transitions_plain=92; expected.labels_plain=5;
329 1 : expected.states_bisimulation=24, expected.transitions_bisimulation=28, expected.labels_bisimulation=5;
330 1 : expected.states_branching_bisimulation=3, expected.transitions_branching_bisimulation=4, expected.labels_branching_bisimulation=5;
331 1 : expected.states_divergence_preserving_branching_bisimulation=6, expected.transitions_divergence_preserving_branching_bisimulation=10, expected.labels_divergence_preserving_branching_bisimulation=5;
332 1 : expected.states_weak_bisimulation=3, expected.transitions_weak_bisimulation=4, expected.labels_weak_bisimulation=5;
333 1 : expected.states_divergence_preserving_weak_bisimulation=6, expected.transitions_divergence_preserving_weak_bisimulation=10, expected.labels_divergence_preserving_weak_bisimulation=6;
334 1 : expected.states_simulation=24, expected.transitions_simulation=28, expected.labels_simulation=5;
335 1 : expected.states_trace_equivalence=19, expected.transitions_trace_equivalence=24, expected.labels_trace_equivalence=5;
336 1 : expected.states_weak_trace_equivalence=3, expected.transitions_weak_trace_equivalence=4, expected.labels_weak_trace_equivalence=5;
337 1 : expected.states_determinisation=53, expected.transitions_determinisation=66, expected.labels_determinisation=5;
338 1 : expected.is_deterministic=false;
339 :
340 1 : reduce_lts_in_various_ways("Alternating bit protocol", ABP_AUT, expected);
341 1 : }
342 :
343 : // Peterson's protocol has the interesting property that the number of states modulo branching bisimulation
344 : // differs from the number of states modulo weak bisimulation, as observed by Rob van Glabbeek.
345 2 : BOOST_AUTO_TEST_CASE(reduce_peterson)
346 : {
347 : std::string PETERSON_AUT =
348 : "des (0,59,35)\n"
349 : "(0,\"wish(1)\",1)\n"
350 : "(0,\"wish(0)\",2)\n"
351 : "(1,\"tau\",3)\n"
352 : "(1,\"wish(0)\",4)\n"
353 : "(2,\"wish(1)\",4)\n"
354 : "(2,\"tau\",5)\n"
355 : "(3,\"tau\",6)\n"
356 : "(3,\"wish(0)\",7)\n"
357 : "(4,\"tau\",7)\n"
358 : "(4,\"tau\",8)\n"
359 : "(5,\"wish(1)\",8)\n"
360 : "(6,\"enter(1)\",9)\n"
361 : "(6,\"wish(0)\",10)\n"
362 : "(7,\"tau\",11)\n"
363 : "(8,\"tau\",12)\n"
364 : "(9,\"leave(1)\",13)\n"
365 : "(9,\"wish(0)\",14)\n"
366 : "(10,\"enter(1)\",14)\n"
367 : "(10,\"tau\",15)\n"
368 : "(11,\"tau\",15)\n"
369 : "(12,\"tau\",16)\n"
370 : "(13,\"tau\",17)\n"
371 : "(13,\"wish(0)\",18)\n"
372 : "(14,\"leave(1)\",18)\n"
373 : "(14,\"tau\",19)\n"
374 : "(15,\"enter(1)\",19)\n"
375 : "(16,\"enter(0)\",20)\n"
376 : "(17,\"wish(1)\",1)\n"
377 : "(17,\"wish(0)\",21)\n"
378 : "(18,\"tau\",21)\n"
379 : "(18,\"tau\",22)\n"
380 : "(19,\"leave(1)\",22)\n"
381 : "(20,\"leave(0)\",23)\n"
382 : "(21,\"wish(1)\",4)\n"
383 : "(21,\"tau\",24)\n"
384 : "(22,\"tau\",24)\n"
385 : "(23,\"tau\",3)\n"
386 : "(24,\"wish(1)\",8)\n"
387 : "(24,\"tau\",25)\n"
388 : "(25,\"enter(0)\",26)\n"
389 : "(25,\"wish(1)\",27)\n"
390 : "(26,\"leave(0)\",28)\n"
391 : "(26,\"wish(1)\",29)\n"
392 : "(27,\"enter(0)\",29)\n"
393 : "(27,\"tau\",16)\n"
394 : "(28,\"wish(1)\",30)\n"
395 : "(28,\"tau\",31)\n"
396 : "(29,\"leave(0)\",30)\n"
397 : "(29,\"tau\",20)\n"
398 : "(30,\"tau\",23)\n"
399 : "(30,\"tau\",32)\n"
400 : "(31,\"wish(1)\",32)\n"
401 : "(31,\"wish(0)\",33)\n"
402 : "(32,\"tau\",3)\n"
403 : "(32,\"wish(0)\",34)\n"
404 : "(33,\"wish(1)\",34)\n"
405 : "(33,\"tau\",24)\n"
406 : "(34,\"tau\",7)\n"
407 1 : "(34,\"tau\",8)\n"
408 : ;
409 :
410 : expected_sizes expected;
411 1 : expected.states_plain=35; expected.transitions_plain=59; expected.labels_plain=7;
412 1 : expected.states_bisimulation=31, expected.transitions_bisimulation=51, expected.labels_bisimulation=7;
413 1 : expected.states_branching_bisimulation=21, expected.transitions_branching_bisimulation=37, expected.labels_branching_bisimulation=7;
414 1 : expected.states_divergence_preserving_branching_bisimulation=21, expected.transitions_divergence_preserving_branching_bisimulation=37, expected.labels_divergence_preserving_branching_bisimulation=7;
415 1 : expected.states_weak_bisimulation=19, expected.transitions_weak_bisimulation=33, expected.labels_weak_bisimulation=7;
416 1 : expected.states_divergence_preserving_weak_bisimulation=19, expected.transitions_divergence_preserving_weak_bisimulation=33, expected.labels_divergence_preserving_weak_bisimulation=8;
417 1 : expected.states_simulation=31, expected.transitions_simulation=49, expected.labels_simulation=7;
418 1 : expected.states_trace_equivalence=34, expected.transitions_trace_equivalence=52, expected.labels_trace_equivalence=7;
419 1 : expected.states_weak_trace_equivalence=18, expected.transitions_weak_trace_equivalence=29, expected.labels_weak_trace_equivalence=7;
420 1 : expected.states_determinisation=40, expected.transitions_determinisation=63, expected.labels_determinisation=7;
421 1 : expected.is_deterministic=false;
422 :
423 1 : reduce_lts_in_various_ways("Peterson protocol", PETERSON_AUT, expected);
424 1 : }
425 :
426 2 : BOOST_AUTO_TEST_CASE(test_reachability)
427 : {
428 : std::string REACH =
429 : "des (0,4,5) \n"
430 : "(0,\"reachable\",1)\n"
431 : "(1,\"reachable1\",2)\n"
432 : "(1,\"reachable2\",3)\n"
433 1 : "(4,\"unreachable\",0)\n"
434 : ;
435 :
436 1 : std::size_t expected_label_count = 5;
437 1 : std::size_t expected_state_count = 5;
438 1 : std::size_t expected_transition_count = 4;
439 :
440 1 : std::istringstream is(REACH);
441 1 : lts::lts_aut_t l_reach;
442 1 : l_reach.load(is);
443 1 : test_lts("reach test",l_reach, expected_label_count, expected_state_count, expected_transition_count);
444 1 : BOOST_CHECK(!reachability_check(l_reach,false));
445 1 : reachability_check(l_reach,true);
446 1 : test_lts("reach test after reachability reduction",l_reach, expected_label_count-1, expected_state_count-1, expected_transition_count-1);
447 1 : BOOST_CHECK(reachability_check(l_reach,false));
448 1 : }
449 :
450 : // The example below caused failures in the GW mlogn branching bisimulation
451 : // algorithm when cleaning the code up.
452 2 : BOOST_AUTO_TEST_CASE(failing_test_groote_wijs_algorithm)
453 : {
454 : std::string GWLTS =
455 : "des(0,29,10)\n"
456 : "(0,\"a\",5)\n"
457 : "(1,\"a\",3)\n"
458 : "(2,\"a\",6)\n"
459 : "(3,\"a\",8)\n"
460 : "(4,\"a\",5)\n"
461 : "(5,\"a\",6)\n"
462 : "(6,\"a\",4)\n"
463 : "(7,\"a\",8)\n"
464 : "(8,\"a\",9)\n"
465 : "(9,\"a\",6)\n"
466 : "(0,\"b\",9)\n"
467 : "(1,\"b\",3)\n"
468 : "(2,\"b\",3)\n"
469 : "(3,\"b\",7)\n"
470 : "(4,\"b\",9)\n"
471 : "(5,\"b\",8)\n"
472 : "(6,\"b\",5)\n"
473 : "(7,\"b\",9)\n"
474 : "(8,\"b\",1)\n"
475 : "(9,\"b\",6)\n"
476 : "(6,\"c\",7)\n"
477 : "(8,\"c\",9)\n"
478 : "(2,\"d\",7)\n"
479 : "(3,\"d\",2)\n"
480 : "(5,\"d\",6)\n"
481 : "(7,\"d\",4)\n"
482 : "(8,\"tau\",0)\n"
483 : "(4,\"tau\",1)\n"
484 1 : "(3,\"tau\",7)\n"
485 : ;
486 :
487 1 : std::size_t expected_label_count = 5;
488 1 : std::size_t expected_state_count = 10;
489 1 : std::size_t expected_transition_count = 29;
490 :
491 1 : std::istringstream is(GWLTS);
492 1 : lts::lts_aut_t l_gw;
493 1 : l_gw.load(is);
494 1 : lts::lts_aut_t l=l_gw;
495 1 : reduce(l,lts::lts_eq_branching_bisim);
496 1 : test_lts("gw problem (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
497 1 : l=l_gw;
498 1 : reduce(l,lts::lts_eq_branching_bisim_gv);
499 1 : test_lts("gw problem (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
500 1 : l=l_gw;
501 1 : reduce(l,lts::lts_eq_branching_bisim_gjkw);
502 1 : test_lts("gw problem (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
503 1 : l=l_gw;
504 1 : reduce(l,lts::lts_eq_branching_bisim_sigref);
505 1 : test_lts("gw problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
506 1 : }
507 :
508 : // The following counterexample was taken from
509 : // Jansen/Keiren: Stuttering equivalence is too slow! Eprint arXiv: 1603.05789,
510 : // 2016. http://arxiv.org/abs/1603.05789
511 : // It has not been implemented fully. The problem is that it is difficult to
512 : // prescribe the order in which refinements have to be done.
513 :
514 0 : void counterexample_jk_1(std::size_t k)
515 : {
516 : // numbering scheme of states:
517 : // states 0..k-1 are the blue squares
518 : // state k is the orange circle
519 : // states k+1..2k are the red triangles
520 : // states 2k+1 and 2k+2 are the grey pentagons
521 : // The grey diamonds are inserted as extra Kripke states.
522 :
523 0 : assert(1 < k);
524 0 : std::string CJK1 = "des(0," + std::to_string(5*k+2) + "," + std::to_string(2*k+3) + ")\n";
525 :
526 0 : for (std::size_t i = 0; i < k; ++i)
527 : {
528 0 : CJK1 += "(" + std::to_string(k) + ",a" + std::to_string(i) + "," + std::to_string(k) + ")\n"
529 0 : "(" + std::to_string(k) + ",tau," + std::to_string(i) + ")\n"
530 0 : "(0,a" + std::to_string(i) + "," + std::to_string(k) + ")\n";
531 : }
532 0 : for (std::size_t i = k-1; i > 0; --i)
533 : {
534 0 : CJK1 += "(" + std::to_string(i) + ",tau," + std::to_string(i-1) + ")\n"
535 0 : "(" + std::to_string(i+k+1) + ",tau," + std::to_string(i+k) + ")\n";
536 : }
537 0 : CJK1 += "(" + std::to_string(k+1) + ",tau," + std::to_string(k) + ")\n"
538 0 : "(" + std::to_string(2*k+1) + ",a," + std::to_string(2*k+2) + ")\n"
539 0 : "(" + std::to_string(k) + ",tau," + std::to_string(2*k+1) + ")\n"
540 0 : "(0,tau," + std::to_string(2*k+2) + ")\n";
541 :
542 0 : std::size_t expected_label_count = k+2;
543 0 : std::size_t expected_state_count = 4;
544 0 : std::size_t expected_transition_count = 10;
545 :
546 0 : std::istringstream is(CJK1);
547 0 : lts::lts_aut_t l_cjk1;
548 0 : l_cjk1.load(is);
549 0 : lts::lts_aut_t l=l_cjk1;
550 0 : reduce(l,lts::lts_eq_branching_bisim);
551 0 : test_lts("counterexample JK 1 (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
552 0 : l=l_cjk1;
553 0 : reduce(l,lts::lts_eq_branching_bisim_gv);
554 0 : test_lts("counterexample JK 1 (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
555 0 : }
556 :
557 :
558 : // The following LTS is a counterexample to the algorithm to postprocess new
559 : // bottom states. Found the error in November 2016.
560 : // The central part of the model consists of states 0--3. The algorithm will
561 : // split w. r. t. the constellation for "a"-labelled transitions. This makes
562 : // state 1 blue and the other states red. Also, state 2 will become a new
563 : // bottom state. After that, it should split for "b"-labelled transitions, so
564 : // that state 3 will get into a separate block; however, it will not find this
565 : // label.
566 :
567 : // If the algorithm later splits w. r. t. "b", then the final result would
568 : // still be correct. The model is therefore sensitive to the order in which
569 : // transitions appear. To remove this sensitivity, I added copies of the
570 : // states for other permutations.
571 :
572 : // In the meantime, the bug is corrected: this is why the first part of the
573 : // algorithm now follows a much simpler line than previously.
574 2 : BOOST_AUTO_TEST_CASE(counterexample_postprocessing)
575 : {
576 : std::string POSTPROCESS_AUT =
577 : "des(0,33,13)\n"
578 : "(0,\"a\",0)\n"
579 : "(0,\"b\",0)\n"
580 : "(0,\"c\",0)\n"
581 :
582 : "(1,\"b\",0)\n"
583 : "(1,\"c\",0)\n"
584 : "(2,\"tau\",1)\n"
585 : "(2,\"a\",0)\n"
586 : "(3,\"tau\",2)\n"
587 : "(3,\"a\",0)\n"
588 : "(3,\"b\",0)\n"
589 : "(4,\"tau\",2)\n" // state 3 copied, with b and c swapped
590 : "(4,\"a\",0)\n"
591 : "(4,\"c\",0)\n"
592 :
593 : "(5,\"a\",0)\n" // states 1-4 copied, with a and b swapped
594 : "(5,\"c\",0)\n"
595 : "(6,\"tau\",5)\n"
596 : "(6,\"b\",0)\n"
597 : "(7,\"tau\",6)\n"
598 : "(7,\"a\",0)\n"
599 : "(7,\"b\",0)\n"
600 : "(8,\"tau\",6)\n"
601 : "(8,\"b\",0)\n"
602 : "(8,\"c\",0)\n"
603 :
604 : "(9,\"a\",0)\n" // states 1-4 copied, with a and c swapped
605 : "(9,\"b\",0)\n"
606 : "(10,\"tau\",9)\n"
607 : "(10,\"c\",0)\n"
608 : "(11,\"tau\",10)\n"
609 : "(11,\"b\",0)\n"
610 : "(11,\"c\",0)\n"
611 : "(12,\"tau\",10)\n"
612 : "(12,\"a\",0)\n"
613 1 : "(12,\"c\",0)\n"
614 : ;
615 :
616 1 : std::size_t expected_label_count = 4;
617 1 : std::size_t expected_state_count = 13;
618 1 : std::size_t expected_transition_count = 33;
619 :
620 1 : std::istringstream is(POSTPROCESS_AUT);
621 1 : lts::lts_aut_t l_gw;
622 1 : l_gw.load(is);
623 1 : lts::lts_aut_t l=l_gw;
624 1 : reduce(l,lts::lts_eq_branching_bisim);
625 1 : test_lts("postprocessing problem (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
626 1 : l=l_gw;
627 1 : reduce(l,lts::lts_eq_branching_bisim_gv);
628 1 : test_lts("postprocessing problem (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
629 1 : l=l_gw;
630 1 : reduce(l,lts::lts_eq_branching_bisim_gjkw);
631 1 : test_lts("postprocessing problem (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
632 1 : l=l_gw;
633 1 : reduce(l,lts::lts_eq_branching_bisim_sigref);
634 1 : test_lts("postprocessing problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
635 1 : }
636 :
637 2 : BOOST_AUTO_TEST_CASE(regression_delete_old_bb_slice)
638 : {
639 : std::string POSTPROCESS_AUT =
640 : "des(0,163,100)\n"
641 : "(33,\"a\",79)\n"
642 : "(87,\"a\",2)\n"
643 : "(4,\"b\",35)\n"
644 : "(13,\"b\",10)\n"
645 : "(15,\"b\",32)\n"
646 : "(31,\"b\",3)\n"
647 : "(35,\"b\",86)\n"
648 : "(47,\"b\",73)\n"
649 : "(61,\"b\",10)\n"
650 : "(67,\"b\",59)\n"
651 : "(81,\"b\",38)\n"
652 : "(89,\"b\",77)\n"
653 : "(94,\"b\",34)\n"
654 : "(20,\"tau\",10)\n"
655 : "(65,\"tau\",61)\n"
656 : "(38,\"tau\",64)\n"
657 : "(86,\"tau\",41)\n"
658 : "(18,\"tau\",55)\n"
659 : "(50,\"tau\",65)\n"
660 : "(28,\"tau\",50)\n"
661 : "(29,\"tau\",55)\n"
662 : "(43,\"tau\",85)\n"
663 : "(93,\"tau\",8)\n"
664 : "(54,\"tau\",72)\n"
665 : "(52,\"tau\",47)\n"
666 : "(7,\"tau\",36)\n"
667 : "(6,\"tau\",60)\n"
668 : "(48,\"tau\",43)\n"
669 : "(77,\"tau\",68)\n"
670 : "(90,\"tau\",34)\n"
671 : "(18,\"tau\",21)\n"
672 : "(18,\"tau\",56)\n"
673 : "(36,\"tau\",70)\n"
674 : "(54,\"tau\",28)\n"
675 : "(62,\"tau\",40)\n"
676 : "(5,\"tau\",18)\n"
677 : "(91,\"tau\",47)\n"
678 : "(42,\"tau\",27)\n"
679 : "(34,\"tau\",70)\n"
680 : "(23,\"tau\",63)\n"
681 : "(19,\"tau\",70)\n"
682 : "(39,\"tau\",43)\n"
683 : "(86,\"tau\",34)\n"
684 : "(25,\"tau\",73)\n"
685 : "(16,\"tau\",4)\n"
686 : "(34,\"tau\",30)\n"
687 : "(70,\"tau\",20)\n"
688 : "(30,\"tau\",22)\n"
689 : "(51,\"tau\",97)\n"
690 : "(5,\"tau\",67)\n"
691 : "(80,\"tau\",13)\n"
692 : "(66,\"tau\",59)\n"
693 : "(24,\"tau\",23)\n"
694 : "(95,\"tau\",82)\n"
695 : "(5,\"tau\",2)\n"
696 : "(82,\"tau\",9)\n"
697 : "(40,\"tau\",46)\n"
698 : "(94,\"tau\",31)\n"
699 : "(19,\"tau\",96)\n"
700 : "(34,\"tau\",32)\n"
701 : "(62,\"tau\",24)\n"
702 : "(74,\"tau\",8)\n"
703 : "(9,\"tau\",76)\n"
704 : "(98,\"tau\",50)\n"
705 : "(25,\"tau\",62)\n"
706 : "(89,\"tau\",95)\n"
707 : "(1,\"tau\",56)\n"
708 : "(44,\"tau\",66)\n"
709 : "(1,\"tau\",45)\n"
710 : "(73,\"tau\",60)\n"
711 : "(70,\"tau\",98)\n"
712 : "(36,\"tau\",14)\n"
713 : "(18,\"tau\",27)\n"
714 : "(87,\"tau\",27)\n"
715 : "(65,\"tau\",17)\n"
716 : "(57,\"tau\",97)\n"
717 : "(98,\"tau\",8)\n"
718 : "(29,\"tau\",25)\n"
719 : "(59,\"tau\",97)\n"
720 : "(1,\"tau\",94)\n"
721 : "(30,\"tau\",74)\n"
722 : "(53,\"tau\",90)\n"
723 : "(50,\"tau\",19)\n"
724 : "(41,\"tau\",81)\n"
725 : "(73,\"tau\",97)\n"
726 : "(97,\"tau\",62)\n"
727 : "(40,\"tau\",59)\n"
728 : "(33,\"tau\",86)\n"
729 : "(16,\"tau\",47)\n"
730 : "(50,\"tau\",72)\n"
731 : "(90,\"tau\",68)\n"
732 : "(90,\"tau\",63)\n"
733 : "(17,\"tau\",75)\n"
734 : "(70,\"tau\",49)\n"
735 : "(85,\"tau\",33)\n"
736 : "(25,\"tau\",52)\n"
737 : "(63,\"tau\",99)\n"
738 : "(22,\"tau\",29)\n"
739 : "(47,\"tau\",31)\n"
740 : "(39,\"tau\",88)\n"
741 : "(41,\"tau\",88)\n"
742 : "(49,\"tau\",83)\n"
743 : "(60,\"tau\",34)\n"
744 : "(85,\"tau\",59)\n"
745 : "(12,\"tau\",6)\n"
746 : "(47,\"tau\",99)\n"
747 : "(47,\"tau\",23)\n"
748 : "(77,\"tau\",73)\n"
749 : "(78,\"tau\",55)\n"
750 : "(7,\"tau\",6)\n"
751 : "(0,\"tau\",67)\n"
752 : "(66,\"tau\",12)\n"
753 : "(75,\"tau\",31)\n"
754 : "(25,\"tau\",80)\n"
755 : "(53,\"tau\",35)\n"
756 : "(83,\"tau\",79)\n"
757 : "(74,\"tau\",88)\n"
758 : "(57,\"tau\",80)\n"
759 : "(7,\"tau\",77)\n"
760 : "(77,\"tau\",8)\n"
761 : "(87,\"tau\",1)\n"
762 : "(59,\"tau\",54)\n"
763 : "(66,\"tau\",33)\n"
764 : "(86,\"tau\",80)\n"
765 : "(90,\"tau\",30)\n"
766 : "(1,\"tau\",4)\n"
767 : "(47,\"tau\",78)\n"
768 : "(75,\"tau\",47)\n"
769 : "(26,\"tau\",7)\n"
770 : "(6,\"tau\",93)\n"
771 : "(51,\"tau\",14)\n"
772 : "(7,\"tau\",77)\n"
773 : "(13,\"tau\",67)\n"
774 : "(65,\"tau\",77)\n"
775 : "(41,\"tau\",39)\n"
776 : "(91,\"tau\",96)\n"
777 : "(69,\"tau\",38)\n"
778 : "(71,\"tau\",77)\n"
779 : "(81,\"tau\",56)\n"
780 : "(53,\"tau\",44)\n"
781 : "(50,\"tau\",88)\n"
782 : "(65,\"tau\",4)\n"
783 : "(39,\"tau\",49)\n"
784 : "(82,\"tau\",93)\n"
785 : "(20,\"tau\",13)\n"
786 : "(4,\"tau\",49)\n"
787 : "(16,\"tau\",6)\n"
788 : "(42,\"tau\",9)\n"
789 : "(74,\"tau\",3)\n"
790 : "(17,\"tau\",21)\n"
791 : "(7,\"tau\",80)\n"
792 : "(58,\"tau\",84)\n"
793 : "(74,\"tau\",62)\n"
794 : "(81,\"tau\",58)\n"
795 : "(19,\"tau\",87)\n"
796 : "(42,\"tau\",45)\n"
797 : "(26,\"tau\",30)\n"
798 : "(57,\"tau\",87)\n"
799 : "(57,\"tau\",96)\n"
800 : "(34,\"tau\",32)\n"
801 : "(43,\"tau\",11)\n"
802 : "(53,\"tau\",35)\n"
803 1 : "(30,\"tau\",56)\n"
804 : ;
805 :
806 1 : std::size_t expected_label_count = 3;
807 1 : std::size_t expected_state_count = 17;
808 1 : std::size_t expected_transition_count = 43;
809 :
810 1 : std::istringstream is(POSTPROCESS_AUT);
811 1 : lts::lts_aut_t l_gw;
812 1 : l_gw.load(is);
813 1 : lts::lts_aut_t l=l_gw;
814 1 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim);
815 1 : test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
816 1 : l=l_gw;
817 1 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gv);
818 1 : test_lts("regression test for GJKW bug (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
819 1 : l=l_gw;
820 1 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gjkw);
821 1 : test_lts("regression test for GJKW bug (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
822 1 : l=l_gw;
823 1 : reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_sigref);
824 1 : test_lts("regression test for GJKW bug (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
825 1 : }
826 :
827 2 : BOOST_AUTO_TEST_CASE(is_deterministic_test1)
828 : {
829 : std::string automaton =
830 : "des(0,2,2)\n"
831 : "(0,\"a\",1)\n"
832 1 : "(0,\"a\",1)\n";
833 :
834 1 : std::istringstream is(automaton);
835 1 : lts::lts_aut_t l_det;
836 1 : l_det.load(is);
837 1 : BOOST_CHECK(is_deterministic(l_det));
838 1 : }
839 :
840 2 : BOOST_AUTO_TEST_CASE(is_deterministic_test2)
841 : {
842 : std::string automaton =
843 : "des(0,2,2)\n"
844 : "(0,\"a\",1)\n"
845 1 : "(0,\"a\",0)\n";
846 :
847 1 : std::istringstream is(automaton);
848 1 : lts::lts_aut_t l_det;
849 1 : l_det.load(is);
850 1 : BOOST_CHECK(!is_deterministic(l_det));
851 1 : }
852 :
853 2 : BOOST_AUTO_TEST_CASE(hide_actions1)
854 : {
855 : std::string automaton =
856 : "des (0,4,3)\n"
857 : "(0,\"<state>\",1)\n"
858 : "(1,\"return|hello\",2)\n"
859 : "(1,\"return\",2)\n"
860 1 : "(2,\"world\",1)\n";
861 :
862 1 : std::istringstream is(automaton);
863 1 : lts::lts_aut_t l;
864 1 : l.load(is);
865 2 : std::vector<std::string>hidden_actions(1,"hello");
866 1 : l.apply_hidden_actions(hidden_actions);
867 1 : reduce(l,lts::lts_eq_bisim);
868 1 : std::size_t expected_label_count = 5;
869 1 : std::size_t expected_state_count = 3;
870 1 : std::size_t expected_transition_count = 3;
871 1 : test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
872 1 : }
873 :
874 :
875 2 : BOOST_AUTO_TEST_CASE(hide_actions2)
876 : {
877 : std::string automaton =
878 : "des (0,4,3)\n"
879 : "(0,\"state\",1)\n"
880 : "(1,\"hello\",2)\n"
881 : "(0,\"return\",2)\n"
882 1 : "(2,\"world\",1)\n";
883 :
884 1 : std::istringstream is(automaton);
885 1 : lts::lts_aut_t l;
886 1 : l.load(is);
887 2 : std::vector<std::string>hidden_actions(1,"hello");
888 1 : l.apply_hidden_actions(hidden_actions);
889 1 : reduce(l,lts::lts_eq_branching_bisim);
890 1 : std::size_t expected_label_count = 5;
891 1 : std::size_t expected_state_count = 2;
892 1 : std::size_t expected_transition_count = 3;
893 1 : test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
894 1 : }
895 :
896 2 : BOOST_AUTO_TEST_CASE(hide_actions3)
897 : {
898 : std::string automaton =
899 : "des (0,4,3)\n"
900 : "(0,\"<state>\",1)\n"
901 : "(1,\"return|hello\",2)\n"
902 : "(1,\"return\",2)\n"
903 1 : "(2,\"world\",1)\n";
904 :
905 1 : std::istringstream is(automaton);
906 1 : lts::lts_aut_t l;
907 1 : l.load(is);
908 2 : std::vector<std::string>hidden_actions(1,"hello");
909 1 : l.record_hidden_actions(hidden_actions);
910 1 : reduce(l,lts::lts_eq_bisim);
911 1 : std::size_t expected_label_count = 5;
912 1 : std::size_t expected_state_count = 3;
913 1 : std::size_t expected_transition_count = 3;
914 1 : test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
915 1 : }
916 :
917 :
918 2 : BOOST_AUTO_TEST_CASE(hide_actions4)
919 : {
920 : std::string automaton =
921 : "des (0,4,3)\n"
922 : "(0,\"state\",1)\n"
923 : "(1,\"hello\",2)\n"
924 : "(0,\"return\",2)\n"
925 1 : "(2,\"world\",1)\n";
926 :
927 1 : std::istringstream is(automaton);
928 1 : lts::lts_aut_t l;
929 1 : l.load(is);
930 2 : std::vector<std::string>hidden_actions(1,"hello");
931 1 : l.record_hidden_actions(hidden_actions);
932 1 : reduce(l,lts::lts_eq_branching_bisim);
933 1 : std::size_t expected_label_count = 5;
934 1 : std::size_t expected_state_count = 2;
935 1 : std::size_t expected_transition_count = 3;
936 1 : test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
937 1 : }
938 :
|
