Line data Source code
1 : // Author(s): Jan Friso Groote
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 ltsconvert_test.cpp
10 : /// \brief This file contains tests to see whether ltsconvert
11 : // reduces problems well.
12 :
13 : #define BOOST_TEST_MODULE ltsconvert_test
14 : // #include <iostream>
15 :
16 : #include <boost/test/included/unit_test.hpp>
17 :
18 : #include "mcrl2/lts/lts_algorithm.h"
19 :
20 : using namespace mcrl2::lts;
21 :
22 181 : static lts_aut_t parse_aut(const std::string& s)
23 : {
24 181 : std::stringstream is(s);
25 181 : lts_aut_t l;
26 181 : l.load(is);
27 362 : return l;
28 181 : }
29 :
30 : const std::string test1=
31 : "des (0,2,2)\n"
32 : "(0,\"move_to_ERROR\",1)\n"
33 : "(1,\"move_to_ERROR\",0)\n";
34 :
35 : const std::string test2=
36 : "des (0,2,2)\n"
37 : "(0,\"move_to_ERROR\",1)\n"
38 : "(1,\"move_to_ERROR1\",0)\n";
39 :
40 : const std::string test3=
41 : "des (0,3,2)\n"
42 : "(0,\"tau\",1)\n"
43 : "(1,\"tau\",0)\n"
44 : "(0,\"a\",1)\n";
45 :
46 : // Example below represents a(tau(b+c)+b) which can be reduced to a(b+c).
47 : const std::string test4=
48 : "des (0,5,6)\n"
49 : "(0,\"a\",1)\n"
50 : "(1,\"tau\",2)\n"
51 : "(2,\"b\",3)\n"
52 : "(2,\"c\",4)\n"
53 : "(1,\"b\",5)\n";
54 :
55 : // Example below is inspired by the rhs of Milner's third tau law, a(tau.b+c)=a(tau.b+c)+a.b
56 : // which contains a non inert tau.
57 : const std::string test5=
58 : "des (0,6,7)\n"
59 : "(0,\"a\",1)\n"
60 : "(0,\"a\",2)\n"
61 : "(1,\"tau\",3)\n"
62 : "(1,\"c\",4)\n"
63 : "(3,\"b\",5)\n"
64 : "(2,\"b\",6)\n";
65 :
66 : // Example below is inspired by Milner's third tau law, a(tau.b+c)=a(tau.b+c)+a.b.
67 : // The states 1 and 2 should be identified in weak bisimulation, but not in branching
68 : // bisimulation.
69 : const std::string test5a=
70 : "des (0,10,7)\n"
71 : "(0,\"d\",1)\n"
72 : "(0,\"d\",2)\n"
73 : "(1,\"a\",3)\n"
74 : "(2,\"a\",4)\n"
75 : "(2,\"a\",5)\n"
76 : "(3,\"b\",6)\n"
77 : "(3,\"tau\",4)\n"
78 : "(4,\"c\",6)\n"
79 : "(5,\"b\",6)\n"
80 : "(5,\"tau\",4)\n";
81 :
82 :
83 : // In the term a.Y with Y=tau.Y divergence-preserving bisimulation must not remove the tau.
84 : const std::string test6=
85 : "des (0,2,2)\n"
86 : "(0,\"a\",1)\n"
87 : "(1,\"tau\",1)\n";
88 :
89 : // Test whether a mixed up sequence of tau's is properly dealt with.
90 : // Example is essentially: tau.X where X=tau.tau.tau.tau.tau.a.X.
91 : const std::string test7=
92 : "des (0,7,7)\n"
93 : "(0,\"tau\",4)\n"
94 : "(2,\"tau\",1)\n"
95 : "(3,\"tau\",2)\n"
96 : "(4,\"tau\",3)\n"
97 : "(1,\"tau\",5)\n"
98 : "(5,\"tau\",6)\n"
99 : "(6,\"a\",3)\n";
100 :
101 : // Test whether a mixed up sequence of tau's is properly dealt with.
102 : // Example is essentially: tau.X where X=tau.tau.tau.tau.tau.a.X.
103 : const std::string test8=
104 : "des (0,6,5)\n"
105 : "(0,\"tau\",1)\n"
106 : "(0,\"tau\",2)\n"
107 : "(0,\"tau\",3)\n"
108 : "(0,\"tau\",4)\n"
109 : "(3,\"tau\",3)\n"
110 : "(4,\"tau\",4)\n";
111 :
112 : // Test whether a tau-loop at the end of a process is correctly dealt with.
113 : const std::string test9=
114 : "des (0,4,4)\n"
115 : "(0,\"a\",1)\n"
116 : "(1,\"tau\",2)\n"
117 : "(2,\"tau\",3)\n"
118 : "(3,\"tau\",1)\n";
119 :
120 : // Test whether a tau that does become non inert will act to split blocks.
121 : const std::string test10=
122 : "des (0,7,8)\n"
123 : "(0,\"b\",1)\n"
124 : "(0,\"b\",2)\n"
125 : "(1,\"a\",3)\n"
126 : "(1,\"tau\",4)\n"
127 : "(2,\"a\",5)\n"
128 : "(2,\"tau\",6)\n"
129 : "(6,\"a\",7)\n";
130 :
131 : // Test whether tau's can repeatedly become non inert
132 : const std::string test11=
133 : "des (0,5,5)\n"
134 : "(0,\"tau\",1)\n"
135 : "(0,\"tau\",3)\n"
136 : "(1,\"a\",2)\n"
137 : "(1,\"tau\",3)\n"
138 : "(3,\"tau\",4)\n";
139 :
140 : // The test below caused the tau_star reduction to go astray, as there
141 : // were problems with the reachability check.
142 : const std::string test12=
143 : "des (0,7,6)\n"
144 : "(0,\"tau\",1)\n"
145 : "(0,\"tau\",2)\n"
146 : "(1,\"tau\",3)\n"
147 : "(2,\"tau\",4)\n"
148 : "(2,\"a\",5)\n"
149 : "(3,\"c\",5)\n"
150 : "(4,\"b\",5)\n";
151 :
152 : // Test whether subtle tau loops are handled properly in divergence-preserving weak and branching bisimulation.
153 : const std::string test13=
154 : "des (0,4,4)\n"
155 : "(0,\"tau\",1)\n"
156 : "(1,\"tau\",2)\n"
157 : "(2,\"tau\",2)\n"
158 : "(1,\"a\",3)\n";
159 :
160 : // Test whether LTSs with one state and one essential transition are reduced
161 : const std::string test14=
162 : "des (0,2,1)\n"
163 : "(0,\"a\",0)\n"
164 : "(0,\"a\",0)\n";
165 :
166 : // Test whether LTSs with one state and more than one essential transitions are reduced
167 : const std::string test15=
168 : "des (0,3,1)\n"
169 : "(0,\"a\",0)\n"
170 : "(0,\"b\",0)\n"
171 : "(0,\"b\",0)\n";
172 :
173 2 : BOOST_AUTO_TEST_CASE(test_state_space_reductions)
174 : {
175 : {
176 1 : std::cerr << "Test1\n";
177 1 : lts_aut_t t1=parse_aut(test1);
178 1 : reduce(t1,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
179 1 : BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
180 1 : t1 = parse_aut(test1);
181 1 : reduce(t1,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
182 1 : BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
183 1 : t1 = parse_aut(test1);
184 1 : reduce(t1,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
185 1 : BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
186 1 : t1 = parse_aut(test1);
187 1 : reduce(t1,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
188 1 : BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
189 1 : }
190 : {
191 1 : std::cerr << "Test2\n";
192 1 : lts_aut_t t2=parse_aut(test2);
193 1 : reduce(t2,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
194 1 : BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
195 1 : t2 = parse_aut(test2);
196 1 : reduce(t2,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
197 1 : BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
198 1 : t2 = parse_aut(test2);
199 1 : reduce(t2,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
200 1 : BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
201 1 : t2 = parse_aut(test2);
202 1 : reduce(t2,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
203 1 : BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
204 1 : }
205 : {
206 1 : std::cerr << "Test3\n";
207 1 : lts_aut_t t3=parse_aut(test3);
208 1 : reduce(t3,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
209 1 : BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
210 1 : t3=parse_aut(test3);
211 1 : reduce(t3,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
212 1 : BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
213 1 : t3=parse_aut(test3);
214 1 : reduce(t3,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
215 1 : BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
216 1 : t3=parse_aut(test3);
217 1 : reduce(t3,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
218 1 : BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
219 1 : t3=parse_aut(test3);
220 1 : reduce(t3,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
221 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
222 1 : t3=parse_aut(test3);
223 1 : reduce(t3,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
224 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
225 1 : t3=parse_aut(test3);
226 1 : reduce(t3,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
227 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
228 1 : t3=parse_aut(test3);
229 1 : reduce(t3,lts_eq_branching_bisim_sigref); //Branching bisimulation reduction sigref [Blom/Orzan 2003]
230 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
231 1 : t3=parse_aut(test3);
232 1 : reduce(t3,lts_eq_weak_bisim); //Weak bisimulation reduction
233 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
234 :
235 : //Divergence-preserving branching bisimulation reduction
236 1 : t3=parse_aut(test3);
237 1 : reduce(t3,lts_eq_divergence_preserving_branching_bisim_gjkw);
238 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
239 1 : t3=parse_aut(test3);
240 1 : reduce(t3,lts_eq_divergence_preserving_branching_bisim_gv);
241 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
242 1 : t3=parse_aut(test3);
243 1 : reduce(t3,lts_eq_divergence_preserving_branching_bisim);
244 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
245 1 : t3=parse_aut(test3);
246 1 : reduce(t3,lts_eq_divergence_preserving_branching_bisim_sigref);
247 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
248 1 : t3=parse_aut(test3);
249 1 : reduce(t3,lts_eq_divergence_preserving_weak_bisim);
250 1 : BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
251 1 : }
252 : {
253 1 : std::cerr << "Test4\n";
254 1 : lts_aut_t t4=parse_aut(test4);
255 1 : reduce(t4,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
256 1 : BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
257 1 : t4=parse_aut(test4);
258 1 : reduce(t4,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
259 1 : BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
260 1 : t4=parse_aut(test4);
261 1 : reduce(t4,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
262 1 : BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
263 1 : t4=parse_aut(test4);
264 1 : reduce(t4,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
265 1 : BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
266 1 : t4=parse_aut(test4);
267 1 : reduce(t4,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
268 1 : BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
269 1 : t4=parse_aut(test4);
270 1 : reduce(t4,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
271 1 : BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
272 1 : t4=parse_aut(test4);
273 1 : reduce(t4,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
274 1 : BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
275 1 : t4=parse_aut(test4);
276 1 : reduce(t4,lts_eq_branching_bisim_sigref);
277 1 : BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
278 1 : t4=parse_aut(test4);
279 1 : reduce(t4,lts_eq_weak_bisim); //Weak bisimulation reduction
280 1 : BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
281 1 : }
282 : {
283 1 : std::cerr << "Test5\n";
284 1 : lts_aut_t t5=parse_aut(test5);
285 1 : reduce(t5,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
286 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
287 1 : t5=parse_aut(test5);
288 1 : reduce(t5,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
289 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
290 1 : t5=parse_aut(test5);
291 1 : reduce(t5,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
292 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
293 1 : t5=parse_aut(test5);
294 1 : reduce(t5,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
295 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
296 1 : t5=parse_aut(test5);
297 1 : reduce(t5,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
298 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
299 1 : t5=parse_aut(test5);
300 1 : reduce(t5,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
301 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
302 1 : t5=parse_aut(test5);
303 1 : reduce(t5,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
304 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
305 1 : t5=parse_aut(test5);
306 1 : reduce(t5,lts_eq_branching_bisim_sigref);
307 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
308 1 : t5=parse_aut(test5);
309 1 : reduce(t5,lts_eq_weak_bisim); //Weak bisimulation reduction
310 1 : BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==4);
311 1 : }
312 : {
313 1 : std::cerr << "Test5a\n";
314 1 : lts_aut_t t5a=parse_aut(test5a);
315 1 : reduce(t5a,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
316 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
317 1 : t5a=parse_aut(test5a);
318 1 : reduce(t5a,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
319 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
320 1 : t5a=parse_aut(test5a);
321 1 : reduce(t5a,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
322 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
323 1 : t5a=parse_aut(test5a);
324 1 : reduce(t5a,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
325 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
326 1 : t5a=parse_aut(test5a);
327 1 : reduce(t5a,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
328 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
329 1 : t5a=parse_aut(test5a);
330 1 : reduce(t5a,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
331 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
332 1 : t5a=parse_aut(test5a);
333 1 : reduce(t5a,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
334 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
335 1 : t5a=parse_aut(test5a);
336 1 : reduce(t5a,lts_eq_branching_bisim_sigref); //Branching bisimulation reduction sigref
337 1 : BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
338 1 : t5a=parse_aut(test5a);
339 1 : reduce(t5a,lts_eq_weak_bisim); //Weak bisimulation reduction
340 1 : BOOST_CHECK(t5a.num_states()==5 && t5a.num_transitions()==5);
341 1 : }
342 : {
343 1 : std::cerr << "Test6\n";
344 1 : lts_aut_t t6=parse_aut(test6);
345 1 : reduce(t6,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
346 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
347 1 : t6=parse_aut(test6);
348 1 : reduce(t6,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
349 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
350 1 : t6=parse_aut(test6);
351 1 : reduce(t6,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
352 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
353 1 : t6=parse_aut(test6);
354 1 : reduce(t6,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
355 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
356 :
357 1 : std::cerr << "Test6a\n";
358 1 : t6=parse_aut(test6);
359 1 : reduce(t6,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
360 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
361 1 : t6=parse_aut(test6);
362 1 : reduce(t6,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
363 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
364 1 : t6=parse_aut(test6);
365 1 : reduce(t6,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
366 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
367 1 : t6=parse_aut(test6);
368 1 : reduce(t6,lts_eq_divergence_preserving_branching_bisim_sigref);
369 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
370 1 : t6=parse_aut(test6);
371 1 : reduce(t6,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
372 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
373 :
374 1 : std::cerr << "Test6b\n";
375 1 : t6=parse_aut(test6);
376 1 : reduce(t6,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
377 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
378 1 : t6=parse_aut(test6);
379 1 : reduce(t6,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
380 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
381 1 : t6=parse_aut(test6);
382 1 : reduce(t6,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
383 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
384 1 : t6=parse_aut(test6);
385 1 : reduce(t6,lts_eq_branching_bisim_sigref);
386 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
387 1 : t6=parse_aut(test6);
388 1 : reduce(t6,lts_eq_weak_bisim); //Weak bisimulation reduction
389 1 : BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
390 1 : }
391 : {
392 1 : std::cerr << "Test7\n";
393 1 : lts_aut_t t7=parse_aut(test7);
394 1 : reduce(t7,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
395 1 : BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
396 1 : t7=parse_aut(test7);
397 1 : reduce(t7,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
398 1 : BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
399 1 : t7=parse_aut(test7);
400 1 : reduce(t7,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
401 1 : BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
402 1 : t7=parse_aut(test7);
403 1 : reduce(t7,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
404 1 : BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
405 1 : t7=parse_aut(test7);
406 1 : reduce(t7,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
407 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
408 1 : t7=parse_aut(test7);
409 1 : reduce(t7,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
410 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
411 1 : t7=parse_aut(test7);
412 1 : reduce(t7,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
413 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
414 1 : t7=parse_aut(test7);
415 1 : reduce(t7,lts_eq_divergence_preserving_branching_bisim_sigref);
416 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
417 1 : t7=parse_aut(test7);
418 1 : reduce(t7,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
419 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
420 1 : t7=parse_aut(test7);
421 1 : reduce(t7,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
422 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
423 1 : t7=parse_aut(test7);
424 1 : reduce(t7,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
425 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
426 1 : t7=parse_aut(test7);
427 1 : reduce(t7,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
428 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
429 1 : t7=parse_aut(test7);
430 1 : reduce(t7,lts_eq_branching_bisim_sigref);
431 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
432 1 : t7=parse_aut(test7);
433 1 : reduce(t7,lts_eq_weak_bisim); //Weak bisimulation reduction
434 1 : BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
435 1 : }
436 : {
437 1 : std::cerr << "Test8\n";
438 1 : lts_aut_t t8=parse_aut(test8);
439 1 : reduce(t8,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
440 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
441 1 : t8 = parse_aut(test8);
442 1 : reduce(t8,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
443 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
444 1 : t8 = parse_aut(test8);
445 1 : reduce(t8,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
446 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
447 1 : t8 = parse_aut(test8);
448 1 : reduce(t8,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
449 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
450 :
451 1 : std::cerr << "Test8a\n";
452 1 : t8=parse_aut(test8);
453 1 : reduce(t8,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
454 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
455 1 : t8=parse_aut(test8);
456 1 : reduce(t8,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
457 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
458 1 : t8=parse_aut(test8);
459 1 : reduce(t8,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
460 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
461 1 : t8=parse_aut(test8);
462 1 : reduce(t8,lts_eq_divergence_preserving_branching_bisim_sigref);
463 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
464 1 : t8=parse_aut(test8);
465 1 : reduce(t8,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
466 1 : BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
467 :
468 1 : std::cerr << "Test8b\n";
469 1 : t8=parse_aut(test8);
470 1 : reduce(t8,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
471 1 : BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
472 1 : t8=parse_aut(test8);
473 1 : reduce(t8,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
474 1 : BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
475 1 : t8=parse_aut(test8);
476 1 : reduce(t8,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
477 1 : BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
478 1 : t8=parse_aut(test8);
479 1 : reduce(t8,lts_eq_branching_bisim_sigref);
480 1 : BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
481 1 : t8=parse_aut(test8);
482 1 : reduce(t8,lts_eq_weak_bisim); //Weak bisimulation reduction
483 1 : BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
484 1 : }
485 : {
486 1 : std::cerr << "Test9\n";
487 1 : lts_aut_t t9=parse_aut(test9);
488 1 : reduce(t9,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
489 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
490 1 : t9=parse_aut(test9);
491 1 : reduce(t9,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
492 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
493 1 : t9=parse_aut(test9);
494 1 : reduce(t9,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
495 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
496 1 : t9=parse_aut(test9);
497 1 : reduce(t9,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
498 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
499 1 : t9=parse_aut(test9);
500 1 : reduce(t9,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
501 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
502 1 : t9=parse_aut(test9);
503 1 : reduce(t9,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
504 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
505 1 : t9=parse_aut(test9);
506 1 : reduce(t9,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
507 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
508 1 : t9=parse_aut(test9);
509 1 : reduce(t9,lts_eq_branching_bisim_sigref);
510 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
511 1 : t9=parse_aut(test9);
512 1 : reduce(t9,lts_eq_weak_bisim); //Weak bisimulation reduction
513 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
514 1 : t9=parse_aut(test9);
515 1 : reduce(t9,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
516 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
517 1 : t9=parse_aut(test9);
518 1 : reduce(t9,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
519 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
520 1 : t9=parse_aut(test9);
521 1 : reduce(t9,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
522 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
523 1 : t9=parse_aut(test9);
524 1 : reduce(t9,lts_eq_divergence_preserving_branching_bisim_sigref);
525 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
526 1 : t9=parse_aut(test9);
527 1 : reduce(t9,lts_eq_divergence_preserving_weak_bisim); //Divergence preserving weak bisimulation reduction
528 1 : BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
529 1 : }
530 : {
531 1 : std::cerr << "Test10\n";
532 1 : lts_aut_t t10=parse_aut(test10);
533 1 : reduce(t10,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
534 1 : BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
535 1 : t10=parse_aut(test10);
536 1 : reduce(t10,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
537 1 : BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
538 1 : t10=parse_aut(test10);
539 1 : reduce(t10,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
540 1 : BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
541 1 : t10=parse_aut(test10);
542 1 : reduce(t10,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
543 1 : BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
544 1 : t10=parse_aut(test10);
545 1 : reduce(t10,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
546 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
547 1 : t10=parse_aut(test10);
548 1 : reduce(t10,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
549 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
550 1 : t10=parse_aut(test10);
551 1 : reduce(t10,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
552 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
553 1 : t10=parse_aut(test10);
554 1 : reduce(t10,lts_eq_branching_bisim_sigref);
555 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
556 1 : t10=parse_aut(test10);
557 1 : reduce(t10,lts_eq_weak_bisim); //Weak bisimulation reduction
558 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
559 1 : t10=parse_aut(test10);
560 1 : reduce(t10,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
561 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
562 1 : t10=parse_aut(test10);
563 1 : reduce(t10,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
564 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
565 1 : t10=parse_aut(test10);
566 1 : reduce(t10,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
567 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
568 1 : t10=parse_aut(test10);
569 1 : reduce(t10,lts_eq_divergence_preserving_branching_bisim_sigref);
570 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
571 1 : t10=parse_aut(test10);
572 1 : reduce(t10,lts_eq_divergence_preserving_weak_bisim); //Divergence preserving weak bisimulation reduction
573 1 : BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
574 1 : }
575 : {
576 1 : std::cerr << "Test11\n";
577 1 : lts_aut_t t11=parse_aut(test11);
578 1 : reduce(t11,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
579 1 : BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
580 1 : t11=parse_aut(test11);
581 1 : reduce(t11,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
582 1 : BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
583 1 : t11=parse_aut(test11);
584 1 : reduce(t11,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
585 1 : BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
586 1 : t11=parse_aut(test11);
587 1 : reduce(t11,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
588 1 : BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
589 1 : t11=parse_aut(test11);
590 1 : reduce(t11,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
591 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
592 1 : t11=parse_aut(test11);
593 1 : reduce(t11,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
594 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
595 1 : t11=parse_aut(test11);
596 1 : reduce(t11,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
597 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
598 1 : t11=parse_aut(test11);
599 1 : reduce(t11,lts_eq_branching_bisim_sigref);
600 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
601 1 : t11=parse_aut(test11);
602 1 : reduce(t11,lts_eq_weak_bisim); //Weak bisimulation reduction
603 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
604 1 : t11=parse_aut(test11);
605 1 : reduce(t11,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
606 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
607 1 : t11=parse_aut(test11);
608 1 : reduce(t11,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
609 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
610 1 : t11=parse_aut(test11);
611 1 : reduce(t11,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
612 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
613 1 : t11=parse_aut(test11);
614 1 : reduce(t11,lts_eq_divergence_preserving_branching_bisim_sigref);
615 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
616 1 : t11=parse_aut(test11);
617 1 : reduce(t11,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
618 1 : BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
619 1 : }
620 : {
621 1 : std::cerr << "Test12\n";
622 1 : lts_aut_t t12=parse_aut(test12);
623 1 : reduce(t12,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
624 1 : BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
625 1 : t12=parse_aut(test12);
626 1 : reduce(t12,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
627 1 : BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
628 1 : t12=parse_aut(test12);
629 1 : reduce(t12,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
630 1 : BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
631 1 : t12=parse_aut(test12);
632 1 : reduce(t12,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
633 1 : BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
634 1 : t12=parse_aut(test12);
635 1 : reduce(t12,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
636 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
637 1 : t12=parse_aut(test12);
638 1 : reduce(t12,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
639 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
640 1 : t12=parse_aut(test12);
641 1 : reduce(t12,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
642 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
643 1 : t12=parse_aut(test12);
644 1 : reduce(t12,lts_eq_branching_bisim_sigref);
645 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
646 1 : t12=parse_aut(test12);
647 1 : reduce(t12,lts_eq_weak_bisim); //Weak bisimulation reduction
648 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
649 1 : t12=parse_aut(test12);
650 1 : reduce(t12,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
651 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
652 1 : t12=parse_aut(test12);
653 1 : reduce(t12,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
654 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
655 1 : t12=parse_aut(test12);
656 1 : reduce(t12,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
657 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
658 1 : t12=parse_aut(test12);
659 1 : reduce(t12,lts_eq_divergence_preserving_branching_bisim_sigref);
660 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
661 1 : t12=parse_aut(test12);
662 1 : reduce(t12,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
663 1 : BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
664 1 : t12=parse_aut(test12);
665 1 : reduce(t12,lts_red_tau_star); //Tau star reduction
666 1 : BOOST_CHECK(t12.num_states()==2 && t12.num_transitions()==3);
667 1 : }
668 : {
669 1 : std::cerr << "Test13\n";
670 1 : lts_aut_t t13=parse_aut(test13);
671 1 : reduce(t13,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
672 1 : BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
673 1 : t13=parse_aut(test13);
674 1 : reduce(t13,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
675 1 : BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
676 1 : t13=parse_aut(test13);
677 1 : reduce(t13,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
678 1 : BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
679 1 : t13=parse_aut(test13);
680 1 : reduce(t13,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
681 1 : BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
682 1 : t13=parse_aut(test13);
683 1 : reduce(t13,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
684 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
685 1 : t13=parse_aut(test13);
686 1 : reduce(t13,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
687 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
688 1 : t13=parse_aut(test13);
689 1 : reduce(t13,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
690 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
691 1 : t13=parse_aut(test13);
692 1 : reduce(t13,lts_eq_branching_bisim_sigref);
693 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
694 1 : t13=parse_aut(test13);
695 1 : reduce(t13,lts_eq_weak_bisim); //Weak bisimulation reduction
696 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
697 1 : t13=parse_aut(test13);
698 1 : reduce(t13,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
699 1 : BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
700 1 : t13=parse_aut(test13);
701 1 : reduce(t13,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
702 1 : BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
703 1 : t13=parse_aut(test13);
704 1 : reduce(t13,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
705 1 : BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
706 1 : t13=parse_aut(test13);
707 1 : reduce(t13,lts_eq_divergence_preserving_branching_bisim_sigref);
708 1 : BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
709 1 : t13=parse_aut(test13);
710 1 : reduce(t13,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
711 1 : BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
712 1 : t13=parse_aut(test13);
713 1 : reduce(t13,lts_red_tau_star); //Tau star reduction
714 1 : BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==1);
715 1 : }
716 : {
717 1 : std::cerr << "Test14\n";
718 1 : lts_aut_t t14=parse_aut(test14);
719 1 : reduce(t14,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
720 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
721 1 : t14=parse_aut(test14);
722 1 : reduce(t14,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
723 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
724 1 : t14=parse_aut(test14);
725 1 : reduce(t14,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
726 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
727 1 : t14=parse_aut(test14);
728 1 : reduce(t14,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
729 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
730 1 : t14=parse_aut(test14);
731 1 : reduce(t14,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
732 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
733 1 : t14=parse_aut(test14);
734 1 : reduce(t14,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
735 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
736 1 : t14=parse_aut(test14);
737 1 : reduce(t14,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
738 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
739 1 : t14=parse_aut(test14);
740 1 : reduce(t14,lts_eq_branching_bisim_sigref);
741 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
742 1 : t14=parse_aut(test14);
743 1 : reduce(t14,lts_eq_weak_bisim); //Weak bisimulation reduction
744 1 : BOOST_CHECK(t14.num_states()==1 && t14.num_transitions()==1);
745 1 : }
746 : {
747 1 : std::cerr << "Test15\n";
748 1 : lts_aut_t t15=parse_aut(test15);
749 1 : reduce(t15,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
750 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
751 1 : t15=parse_aut(test15);
752 1 : reduce(t15,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
753 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
754 1 : t15=parse_aut(test15);
755 1 : reduce(t15,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
756 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
757 1 : t15=parse_aut(test15);
758 1 : reduce(t15,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
759 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
760 1 : t15=parse_aut(test15);
761 1 : reduce(t15,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
762 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
763 1 : t15=parse_aut(test15);
764 1 : reduce(t15,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
765 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
766 1 : t15=parse_aut(test15);
767 1 : reduce(t15,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
768 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
769 1 : t15=parse_aut(test15);
770 1 : reduce(t15,lts_eq_branching_bisim_sigref);
771 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
772 1 : t15=parse_aut(test15);
773 1 : reduce(t15,lts_eq_weak_bisim); //Weak bisimulation reduction
774 1 : BOOST_CHECK(t15.num_states()==1 && t15.num_transitions()==2);
775 1 : }
776 1 : }
777 :
|
