Line data Source code
1 : // Author(s): Muck van Weerdenburg, 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 : #define BOOST_TEST_MODULE compare
10 : #include <boost/test/included/unit_test.hpp>
11 :
12 : #include "mcrl2/lts/lts_algorithm.h"
13 :
14 : using namespace mcrl2::lts;
15 :
16 260 : static lts_aut_t parse_aut(const std::string& s)
17 : {
18 260 : std::stringstream is(s);
19 260 : lts_aut_t l;
20 260 : l.load(is);
21 520 : return l;
22 260 : }
23 :
24 : // a.(b+c)
25 : const std::string l1 =
26 : "des(0,3,4)\n"
27 : "(0,\"a\",1)\n"
28 : "(1,\"b\",2)\n"
29 : "(1,\"c\",3)\n";
30 :
31 : // a.b+a.c
32 : const std::string l2 =
33 : "des(0,4,5)\n"
34 : "(0,\"a\",1)\n"
35 : "(0,\"a\",2)\n"
36 : "(1,\"b\",3)\n"
37 : "(2,\"c\",4)\n";
38 :
39 : // a.b+a.c+ a.(b+c)
40 : const std::string l2a =
41 : "des(0,7,8)\n"
42 : "(0,\"a\",1)\n"
43 : "(0,\"a\",2)\n"
44 : "(1,\"b\",3)\n"
45 : "(2,\"c\",4)\n"
46 : "(0,\"a\",5)\n"
47 : "(5,\"b\",6)\n"
48 : "(5,\"c\",7)\n";
49 :
50 : // a.tau.(b+c)
51 : const std::string l3 =
52 : "des(0,4,5)\n"
53 : "(0,\"a\",1)\n"
54 : "(1,\"tau\",2)\n"
55 : "(2,\"b\",3)\n"
56 : "(2,\"c\",4)\n";
57 :
58 : // a.(b+b)
59 : const std::string l4 =
60 : "des(0,3,4)\n"
61 : "(0,\"a\",1)\n"
62 : "(1,\"b\",2)\n"
63 : "(1,\"b\",3)\n";
64 :
65 : // a
66 : const std::string a =
67 : "des (0,1,2)\n"
68 : "(0,\"a\",1)\n";
69 :
70 : // b
71 : const std::string b =
72 : "des (0,1,2)\n"
73 : "(0,\"b\",1)\n";
74 :
75 : static inline
76 89 : bool preorder_compare(const std::string& s1, const std::string& s2, lts_preorder pre)
77 : {
78 89 : lts_aut_t t1=parse_aut(s1);
79 89 : lts_aut_t t2=parse_aut(s2);
80 178 : return compare(t1, t2, pre,false);
81 89 : }
82 :
83 : static inline
84 41 : bool compare(const std::string& s1, const std::string& s2, lts_equivalence eq, bool counterexample=false)
85 : {
86 41 : lts_aut_t t1=parse_aut(s1);
87 41 : lts_aut_t t2=parse_aut(s2);
88 82 : return compare(t1, t2, eq, counterexample);
89 41 : }
90 :
91 2 : BOOST_AUTO_TEST_CASE(test_reflexive)
92 : {
93 1 : BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_sim));
94 1 : BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_trace));
95 1 : BOOST_CHECK(compare(l2a,l2a,lts_eq_sim));
96 1 : BOOST_CHECK(compare(l2a,l2a,lts_eq_trace));
97 1 : BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_ready_sim));
98 1 : BOOST_CHECK(compare(l2a,l2a,lts_eq_ready_sim));
99 1 : }
100 :
101 :
102 2 : BOOST_AUTO_TEST_CASE(test_sim_1_2)
103 : {
104 1 : BOOST_CHECK(!preorder_compare(l1,l2,lts_pre_sim));
105 1 : BOOST_CHECK(preorder_compare(l2,l1,lts_pre_sim));
106 1 : BOOST_CHECK(!compare(l2,l1,lts_eq_sim));
107 1 : BOOST_CHECK(!compare(l1,l2,lts_eq_sim));
108 1 : }
109 :
110 2 : BOOST_AUTO_TEST_CASE(test_sim_2_2a)
111 : {
112 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_sim));
113 1 : BOOST_CHECK(!preorder_compare(l2a,l2,lts_pre_sim));
114 1 : BOOST_CHECK(!compare(l2a,l2,lts_eq_sim));
115 1 : BOOST_CHECK(!compare(l2,l2a,lts_eq_sim));
116 1 : }
117 :
118 2 : BOOST_AUTO_TEST_CASE(test_sim_1_3)
119 : {
120 1 : BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_sim));
121 1 : BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_sim));
122 1 : BOOST_CHECK(!compare(l3,l1,lts_eq_sim));
123 1 : BOOST_CHECK(!compare(l1,l3,lts_eq_sim));
124 1 : }
125 :
126 :
127 2 : BOOST_AUTO_TEST_CASE(test_sim_1_4)
128 : {
129 1 : BOOST_CHECK(!preorder_compare(l1,l4,lts_pre_sim));
130 1 : BOOST_CHECK(preorder_compare(l4,l1,lts_pre_sim));
131 1 : BOOST_CHECK(!compare(l1,l4,lts_eq_sim));
132 1 : BOOST_CHECK(!compare(l4,l1,lts_eq_sim));
133 1 : }
134 :
135 :
136 2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_2)
137 : {
138 1 : BOOST_CHECK(!preorder_compare(l1,l2,lts_pre_ready_sim));
139 1 : BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_ready_sim));
140 1 : BOOST_CHECK(!compare(l2,l1,lts_eq_ready_sim));
141 1 : BOOST_CHECK(!compare(l1,l2,lts_eq_ready_sim));
142 1 : }
143 :
144 2 : BOOST_AUTO_TEST_CASE(test_ready_sim_2_2a)
145 : {
146 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_ready_sim));
147 1 : BOOST_CHECK(!preorder_compare(l2a,l2,lts_pre_ready_sim));
148 1 : BOOST_CHECK(!compare(l2,l2a,lts_eq_ready_sim));
149 1 : BOOST_CHECK(!compare(l2a,l2,lts_eq_ready_sim));
150 1 : }
151 :
152 2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_3)
153 : {
154 1 : BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_ready_sim));
155 1 : BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_ready_sim));
156 1 : BOOST_CHECK(!compare(l3,l1,lts_eq_ready_sim));
157 1 : }
158 :
159 2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_4)
160 : {
161 1 : BOOST_CHECK(!preorder_compare(l1,l4,lts_pre_ready_sim));
162 1 : BOOST_CHECK(!preorder_compare(l4,l1,lts_pre_ready_sim));
163 1 : BOOST_CHECK(!compare(l1,l4,lts_eq_ready_sim));
164 1 : }
165 :
166 2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_2)
167 : {
168 1 : BOOST_CHECK(compare(l1,l2,lts_eq_trace));
169 1 : BOOST_CHECK(compare(l2,l1,lts_eq_trace));
170 1 : BOOST_CHECK(!compare(l2,l1,lts_eq_bisim));
171 1 : BOOST_CHECK(!compare(l2,l1,lts_eq_bisim_gv));
172 1 : BOOST_CHECK(!compare(l2,l1,lts_eq_bisim_gjkw));
173 1 : BOOST_CHECK(preorder_compare(l1,l2,lts_pre_trace));
174 1 : BOOST_CHECK(preorder_compare(l2,l1,lts_pre_trace));
175 1 : BOOST_CHECK(preorder_compare(l1,l2,lts_pre_trace_anti_chain));
176 1 : BOOST_CHECK(preorder_compare(l2,l1,lts_pre_trace_anti_chain));
177 1 : BOOST_CHECK(preorder_compare(l1,l2,lts_pre_failures_refinement));
178 1 : BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_failures_refinement));
179 1 : BOOST_CHECK(preorder_compare(l1,l2,lts_pre_failures_divergence_refinement));
180 1 : BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_failures_divergence_refinement));
181 1 : }
182 :
183 2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_2a)
184 : {
185 1 : BOOST_CHECK(compare(l2,l2a,lts_eq_trace));
186 1 : BOOST_CHECK(compare(l2a,l2,lts_eq_trace));
187 1 : BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim));
188 1 : BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim_gv));
189 1 : BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim_gjkw));
190 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_trace));
191 1 : BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_trace));
192 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_trace_anti_chain));
193 1 : BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_trace_anti_chain));
194 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_failures_refinement));
195 1 : BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_failures_refinement));
196 1 : BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_failures_divergence_refinement));
197 1 : BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_failures_divergence_refinement));
198 1 : }
199 :
200 2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_3)
201 : {
202 1 : BOOST_CHECK(!compare(l1,l3,lts_eq_trace));
203 1 : BOOST_CHECK(!compare(l3,l1,lts_eq_trace));
204 1 : BOOST_CHECK(compare(l1,l3,lts_eq_weak_trace));
205 1 : BOOST_CHECK(compare(l3,l1,lts_eq_weak_trace));
206 1 : BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_trace_anti_chain));
207 1 : BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_trace_anti_chain));
208 1 : BOOST_CHECK(preorder_compare(l1,l3,lts_pre_weak_trace_anti_chain));
209 1 : BOOST_CHECK(preorder_compare(l3,l1,lts_pre_weak_trace_anti_chain));
210 1 : BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_failures_refinement));
211 1 : BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_failures_refinement));
212 1 : BOOST_CHECK(preorder_compare(l1,l3,lts_pre_weak_failures_refinement));
213 1 : BOOST_CHECK(preorder_compare(l3,l1,lts_pre_weak_failures_refinement));
214 1 : BOOST_CHECK(preorder_compare(l1,l3,lts_pre_failures_divergence_refinement));
215 1 : BOOST_CHECK(preorder_compare(l3,l1,lts_pre_failures_divergence_refinement));
216 1 : }
217 :
218 2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_4)
219 : {
220 1 : BOOST_CHECK(!compare(l1,l4,lts_eq_trace));
221 1 : BOOST_CHECK(!compare(l4,l1,lts_eq_trace));
222 1 : }
223 :
224 2 : BOOST_AUTO_TEST_CASE(test_symmetric_weak_trace_2_3)
225 : {
226 1 : BOOST_CHECK(compare(l2,l3,lts_eq_weak_trace));
227 1 : BOOST_CHECK(compare(l3,l2,lts_eq_weak_trace));
228 1 : }
229 :
230 2 : BOOST_AUTO_TEST_CASE(test_symmetric_weak_trace_3_4)
231 : {
232 1 : BOOST_CHECK(!compare(l4,l3,lts_eq_weak_trace));
233 1 : BOOST_CHECK(!compare(l3,l4,lts_eq_weak_trace));
234 1 : }
235 :
236 : // Regression test for bug #1082
237 2 : BOOST_AUTO_TEST_CASE(test_bisim_a_b)
238 : {
239 1 : BOOST_CHECK(!compare(a,b,lts_eq_bisim, true));
240 1 : }
241 :
242 : // a.(b.c1+d1) + a.(b.c2+d2)
243 : const std::string failures_law_left_hand_side =
244 : "des(0,8,6)\n"
245 : "(0,\"a\",1)\n"
246 : "(1,\"b\",2)\n"
247 : "(2,\"c1\",3)\n"
248 : "(1,\"d1\",3)\n"
249 : "(0,\"a\",4)\n"
250 : "(4,\"b\",5)\n"
251 : "(5,\"c2\",3)\n"
252 : "(4,\"d2\",3)\n";
253 :
254 : // a.(b.c1+b.c2+d1) + a.(b.c2+b.c1+d2)
255 : const std::string failures_law_right_hand_side =
256 : "des(0,10,6)\n"
257 : "(0,\"a\",1)\n"
258 : "(1,\"b\",2)\n"
259 : "(2,\"c1\",3)\n"
260 : "(1,\"d1\",3)\n"
261 : "(1,\"b\",5)\n"
262 : "(0,\"a\",4)\n"
263 : "(4,\"b\",5)\n"
264 : "(4,\"b\",2)\n"
265 : "(5,\"c2\",3)\n"
266 : "(4,\"d2\",3)\n";
267 :
268 : // The typical law for strong failures equivalence is
269 : // a.(b.x+u)+a.(b.y+v) = a.(b.x+b.y+u)+a.(b.x+b.y+v).
270 : // The validity of this law is tested here, where the
271 : // variables have been replaced by single actions.
272 2 : BOOST_AUTO_TEST_CASE(laws_for_failures_equivalence)
273 : {
274 1 : BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_failures_refinement));
275 1 : BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_failures_refinement));
276 1 : BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_trace));
277 1 : BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_trace));
278 1 : BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_trace_anti_chain));
279 1 : BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_trace_anti_chain));
280 1 : BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_failures_divergence_refinement));
281 1 : BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_failures_divergence_refinement));
282 1 : }
283 :
284 : // a.b + a.(b+c)
285 : const std::string ababc =
286 : "des(0,5,6)\n"
287 : "(0,\"a\",1)\n"
288 : "(1,\"b\",2)\n"
289 : "(0,\"a\",3)\n"
290 : "(3,\"b\",4)\n"
291 : "(3,\"c\",5)\n";
292 :
293 : // a.(b+c) is typically failure included in a.b+a(b+c), but not vice versa.
294 2 : BOOST_AUTO_TEST_CASE(failures_inclusion_test)
295 : {
296 1 : BOOST_CHECK(preorder_compare(l1,ababc,lts_pre_failures_refinement));
297 1 : BOOST_CHECK(!preorder_compare(ababc,l1,lts_pre_failures_refinement));
298 1 : }
299 :
300 : // a.(tau.b + tau.c)
301 : const std::string a_taub_tauc =
302 : "des(0,5,6)\n"
303 : "(0,\"a\",1)\n"
304 : "(1,\"tau\",2)\n"
305 : "(2,\"b\",3)\n"
306 : "(1,\"tau\",4)\n"
307 : "(4,\"c\",5)\n";
308 :
309 : // a.(tau.b+tau.c) and a.b + a.c are weak failure equivalent.
310 2 : BOOST_AUTO_TEST_CASE(weak_failures_equivalence_test)
311 : {
312 1 : BOOST_CHECK(!preorder_compare(l2,a_taub_tauc,lts_pre_failures_refinement));
313 1 : BOOST_CHECK(!preorder_compare(a_taub_tauc,l2,lts_pre_failures_refinement));
314 1 : BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_trace));
315 1 : BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_trace));
316 1 : BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_trace_anti_chain));
317 1 : BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_trace_anti_chain));
318 1 : BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_failures_refinement));
319 1 : BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_failures_refinement));
320 1 : }
321 :
322 : // a.b + a.(b+c)
323 : const std::string abc_div =
324 : "des(0,4,4)\n"
325 : "(0,\"a\",1)\n"
326 : "(1,\"tau\",1)\n"
327 : "(1,\"b\",2)\n"
328 : "(1,\"c\",3)\n";
329 :
330 : // a.tau*(b+c) is typically failures equivalent to a.(b+c).
331 : // But a.tau*.(b+c) is not failures-divergence included in a.(b+c). The reverse however holds.
332 2 : BOOST_AUTO_TEST_CASE(failures_divergence_inclusion_test)
333 : {
334 1 : BOOST_CHECK(!preorder_compare(l1,abc_div,lts_pre_failures_refinement));
335 1 : BOOST_CHECK(!preorder_compare(abc_div,l1,lts_pre_failures_refinement));
336 1 : BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_trace));
337 1 : BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_weak_trace));
338 1 : BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_trace_anti_chain));
339 1 : BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_weak_trace_anti_chain));
340 1 : BOOST_CHECK(!preorder_compare(l1,abc_div,lts_pre_weak_failures_refinement));
341 1 : BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_failures_refinement));
342 1 : BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_failures_divergence_refinement));
343 1 : BOOST_CHECK(!preorder_compare(abc_div,l1,lts_pre_failures_divergence_refinement));
344 1 : }
345 :
346 : // Example by Verum showing an error in the weak failures inclusion check. Did not work with
347 : // the -c flag (which does not preprocess using branching bisimulation) but did work after
348 : // applying branching bisimulation.
349 :
350 : const std::string lts_impl =
351 : "des (1,8,6)\n"
352 : "(0,f,1)\n"
353 : "(1,b,2)\n"
354 : "(1,a,2)\n"
355 : "(2,tau,0)\n"
356 : "(2,tau,5)\n"
357 : "(3,tau,5)\n"
358 : "(4,tau,0)\n"
359 : "(5,t,1)\n";
360 :
361 : const std::string lts_spec =
362 : "des (1,5,3)\n"
363 : "(0,f,1)\n"
364 : "(1,b,2)\n"
365 : "(1,b,0)\n"
366 : "(1,a,2)\n"
367 : "(2,t,1)\n";
368 :
369 2 : BOOST_AUTO_TEST_CASE(verum_test)
370 : {
371 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_failures_refinement));
372 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_failures_divergence_refinement));
373 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_failures_refinement));
374 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_trace));
375 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_trace));
376 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_trace_anti_chain));
377 1 : BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_trace_anti_chain));
378 :
379 1 : BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_failures_refinement));
380 1 : BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_failures_divergence_refinement));
381 1 : BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_failures_refinement));
382 1 : BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_trace));
383 1 : BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_trace));
384 1 : BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_trace_anti_chain));
385 1 : BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_trace_anti_chain));
386 1 : }
387 :
388 : // P = a.P + tau.P
389 : const std::string aPtauP =
390 : "des (0,2,1)\n"
391 : "(0,\"a\",0)\n"
392 : "(0,\"tau\",0)\n";
393 :
394 : // P = b.P
395 : const std::string bP =
396 : "des (0,1,1)\n"
397 : "(0,\"b\",0)\n";
398 :
399 : // Check that diverging behaviour in a specification for failures-divergence refinement is
400 : // regarded as catastrophic. Meaning that all failures are allowed after a divergence in spec.
401 : // Furthermore check that for failures refinement that trace refinement holds as well. For
402 : // failures refinement this does not hold, but here trace refinement is required so it does
403 : // not hold.
404 2 : BOOST_AUTO_TEST_CASE(failures_divergence_incomparable_test)
405 : {
406 1 : BOOST_CHECK(!preorder_compare(aPtauP, bP, lts_pre_failures_refinement)); // empty = failures(aPtauP) subset failures(bP); traces(aPtauP) nsubset traces(bP).
407 1 : BOOST_CHECK(preorder_compare(bP, aPtauP, lts_pre_failures_divergence_refinement)); // failures(bP) subset failures(aPtau) != empty because divergences.
408 1 : }
409 :
410 :
411 : // Test belonging to #1595. Check wheter action a|b and b|a are considered equal.
412 2 : BOOST_AUTO_TEST_CASE(properly_order_multiactions)
413 : {
414 :
415 : const std::string ab =
416 : "des (0,1,1)\n"
417 1 : "(0,\"a|b\",0)\n";
418 :
419 : // P = b.P
420 : const std::string ba =
421 : "des (0,1,1)\n"
422 2 : "(0,\"b|a\",0)\n";
423 :
424 1 : BOOST_CHECK(compare(ab, ba, lts_eq_bisim)); // These transition systems must be equal.
425 1 : }
426 :
427 : // Test cases for coupled similarity
428 :
429 : const std::string philosophers_gradual =
430 : "des (0,8,6)\n"
431 : "(0,\"tau\",1)\n"
432 : "(0,\"tau\",2)\n"
433 : "(1,\"tau\",3)\n"
434 : "(2,\"tau\",4)\n"
435 : "(2,\"tau\",5)\n"
436 : "(3,\"aEats\",3)\n"
437 : "(4,\"bEats\",4)\n"
438 : "(5,\"cEats\",5)\n"
439 : ;
440 :
441 : const std::string philosophers_merged =
442 : "des (0,6,4)\n"
443 : "(0,\"tau\",1)\n"
444 : "(0,\"tau\",2)\n"
445 : "(0,\"tau\",3)\n"
446 : "(1,\"aEats\",1)\n"
447 : "(2,\"bEats\",2)\n"
448 : "(3,\"cEats\",3)\n"
449 : ;
450 :
451 2 : BOOST_AUTO_TEST_CASE(coupled_similarity_test)
452 : {
453 1 : BOOST_CHECK(compare(philosophers_gradual, philosophers_merged, lts_eq_coupled_sim)); // These transition systems must be equal.
454 1 : BOOST_CHECK(!compare(philosophers_gradual, philosophers_merged, lts_eq_bisim)); // These transition systems must be different.
455 1 : }
|