Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file bisimulation_test.cpp
10 : /// \brief Test the bisimulation algorithm.
11 :
12 : #define BOOST_TEST_MODULE bisimulation_test
13 : #include <boost/test/included/unit_test.hpp>
14 : #include "mcrl2/lps/detail/test_input.h"
15 : #include "mcrl2/lps/linearise.h"
16 : #include "mcrl2/pbes/bisimulation.h"
17 : #include "mcrl2/pbes/detail/pbessolve.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::lps;
21 : using namespace mcrl2::pbes_system;
22 : using namespace mcrl2::log;
23 :
24 8 : void test_bisimulation(const std::string& s1, const std::string& s2,
25 : bool strongly_bisimilar,
26 : bool branching_bisimilar,
27 : bool branching_similar,
28 : bool weakly_bisimilar,
29 : bool linearize = false)
30 : {
31 8 : specification spec1;
32 8 : specification spec2;
33 8 : if (linearize)
34 : {
35 0 : spec1 = remove_stochastic_operators(linearise(s1));
36 0 : spec2 = remove_stochastic_operators(linearise(s2));
37 : }
38 : else
39 : {
40 8 : spec1 = parse_linear_process_specification(s1);
41 8 : spec2 = parse_linear_process_specification(s2);
42 : }
43 :
44 8 : std::clog << "Testing strong bisimulation" << std::endl;
45 8 : pbes sb = strong_bisimulation(spec1, spec2);
46 8 : BOOST_CHECK(sb.is_well_typed());
47 8 : bool sb_solution = pbes_system::detail::pbessolve(sb);
48 8 : BOOST_CHECK(sb_solution == strongly_bisimilar);
49 :
50 8 : std::clog << "Testing branching bisimulation" << std::endl;
51 8 : pbes bb = branching_bisimulation(spec1, spec2);
52 8 : bool bb_solution = pbes_system::detail::pbessolve(bb);
53 8 : BOOST_CHECK(bb.is_well_typed());
54 8 : BOOST_CHECK(bb_solution == branching_bisimilar);
55 :
56 8 : std::clog << "Testing branching simulation" << std::endl;
57 8 : pbes bs = branching_simulation_equivalence(spec1, spec2);
58 8 : bool bs_solution = pbes_system::detail::pbessolve(bs);
59 8 : BOOST_CHECK(bs.is_well_typed());
60 8 : BOOST_CHECK(bs_solution == branching_similar);
61 :
62 8 : std::clog << "Testing weak bisimulation" << std::endl;
63 8 : pbes wb = weak_bisimulation(spec1, spec2);
64 8 : bool wb_solution = pbes_system::detail::pbessolve(wb);
65 8 : BOOST_CHECK(wb.is_well_typed());
66 8 : BOOST_CHECK(wb_solution == weakly_bisimilar);
67 8 : }
68 :
69 2 : BOOST_AUTO_TEST_CASE(ABP)
70 : {
71 1 : test_bisimulation(lps::detail::LINEAR_ABP_SPECIFICATION(), lps::detail::LINEAR_ABP_SPECIFICATION(), true, true, true, true);
72 1 : }
73 :
74 2 : BOOST_AUTO_TEST_CASE(SMALLSPEC)
75 : {
76 : const std::string SMALLSPEC =
77 : "act a,b; \n"
78 : "proc X(s: Pos) = \n"
79 : " (s == 1) -> a . X(2) \n"
80 : "+ (s == 2) -> tau . X(3) \n"
81 : "+ (s == 3) -> tau . X(4) \n"
82 : "+ (s == 4) -> b . X(1); \n"
83 1 : "init X(1); \n"
84 : ;
85 1 : test_bisimulation(SMALLSPEC, SMALLSPEC, true, true, true, true);
86 1 : }
87 :
88 2 : BOOST_AUTO_TEST_CASE(small_different_specs)
89 : {
90 : const std::string s1 =
91 : "act a,b; \n"
92 : "proc X(s: Pos) = \n"
93 : " (s == 1) -> a . X(2) \n"
94 : "+ (s == 2) -> b . X(1); \n"
95 1 : "init X(1); \n"
96 : ;
97 : const std::string s2 =
98 : "act a,b,c; \n"
99 : "proc X(s: Pos) = \n"
100 : " (s == 1) -> a . X(2) \n"
101 : "+ (s == 1) -> c . X(1) \n"
102 : "+ (s == 2) -> b . X(1); \n"
103 1 : "init X(1); \n"
104 : ;
105 : ;
106 1 : test_bisimulation(s1, s2, false, false, false, false);
107 1 : test_bisimulation(s2, s1, false, false, false, false);
108 1 : }
109 :
110 2 : BOOST_AUTO_TEST_CASE(buffers_silent_lose)
111 : {
112 : const std::string buffer =
113 : "sort D = struct d1 | d2;\n"
114 : "map n: Pos;\n"
115 : "eqn n = 2;\n"
116 : "act r,s: D;\n"
117 : "proc P(b_Buffer: List(D)) =\n"
118 : " !(b_Buffer == []) ->\n"
119 : " s(rhead(b_Buffer)) .\n"
120 : " P(b_Buffer = rtail(b_Buffer))\n"
121 : " + sum d_Buffer: D.\n"
122 : " (#b_Buffer < 2) ->\n"
123 : " r(d_Buffer) .\n"
124 : " P(b_Buffer = d_Buffer |> b_Buffer)\n"
125 : " + delta;\n"
126 1 : "init P([]);\n";
127 :
128 : const std::string lossy_buffer =
129 : "sort D = struct d1 | d2;\n"
130 : "map n: Pos;\n"
131 : "eqn n = 2;\n"
132 : "act r,s: D;\n"
133 : "proc P(s3_Buffer: Pos, d_Buffer: D, b_Buffer: List(D)) =\n"
134 : " sum e_Buffer: Bool.\n"
135 : " (s3_Buffer == 2) ->\n"
136 : " tau .\n"
137 : " P(s3_Buffer = 1, d_Buffer = d1, b_Buffer = if(e_Buffer, d_Buffer |> b_Buffer, b_Buffer))\n"
138 : " + (s3_Buffer == 1 && !(b_Buffer == [])) ->\n"
139 : " s(rhead(b_Buffer)) .\n"
140 : " P(s3_Buffer = 1, d_Buffer = d1, b_Buffer = rtail(b_Buffer))\n"
141 : " + sum d0_Buffer: D.\n"
142 : " (s3_Buffer == 1 && #b_Buffer < 2) ->\n"
143 : " r(d0_Buffer) .\n"
144 : " P(s3_Buffer = 2, d_Buffer = d0_Buffer)\n"
145 : " + delta;\n"
146 1 : "init P(1, d1, []);\n";
147 :
148 1 : test_bisimulation(buffer, lossy_buffer, false, false, false, false);
149 1 : test_bisimulation(lossy_buffer, buffer, false, false, false, false);
150 1 : }
151 :
152 2 : BOOST_AUTO_TEST_CASE(buffers_explicit_lose)
153 : {
154 : const std::string buffer =
155 : "sort D = struct d1 | d2;\n"
156 : "map n: Pos;\n"
157 : "eqn n = 2;\n"
158 : "act r,s: D;\n"
159 : "proc P(b_Buffer: List(D)) =\n"
160 : " !(b_Buffer == []) ->\n"
161 : " s(rhead(b_Buffer)) .\n"
162 : " P(b_Buffer = rtail(b_Buffer))\n"
163 : " + sum d_Buffer: D.\n"
164 : " (#b_Buffer < 2) ->\n"
165 : " r(d_Buffer) .\n"
166 : " P(b_Buffer = d_Buffer |> b_Buffer)\n"
167 : " + delta;\n"
168 1 : "init P([]);\n";
169 :
170 : const std::string lossy_buffer =
171 : "sort D = struct d1 | d2;\n"
172 : "map n: Pos;\n"
173 : "eqn n = 2;\n"
174 : "act r,s: D;\n"
175 : " lose;\n"
176 : "proc P(s3_Buffer: Pos, d_Buffer: D, b_Buffer: List(D)) =\n"
177 : " sum d0_Buffer: D.\n"
178 : " (s3_Buffer == 1 && #b_Buffer < 2) ->\n"
179 : " r(d0_Buffer) .\n"
180 : " P(s3_Buffer = 2, d_Buffer = d0_Buffer)\n"
181 : " + (s3_Buffer == 1 && !(b_Buffer == [])) ->\n"
182 : " s(rhead(b_Buffer)) .\n"
183 : " P(s3_Buffer = 1, d_Buffer = d1, b_Buffer = rtail(b_Buffer))\n"
184 : " + (s3_Buffer == 2) ->\n"
185 : " tau .\n"
186 : " P(s3_Buffer = 3, d_Buffer = d1)\n"
187 : " + (s3_Buffer == 2) ->\n"
188 : " tau .\n"
189 : " P(s3_Buffer = 1, d_Buffer = d1, b_Buffer = d_Buffer |> b_Buffer)\n"
190 : " + (s3_Buffer == 3) ->\n"
191 : " lose .\n"
192 : " P(s3_Buffer = 1, d_Buffer = d1)\n"
193 : " + delta;\n"
194 1 : "init P(1, d1, []);\n";
195 :
196 1 : test_bisimulation(buffer, lossy_buffer, false, false, false, false);
197 1 : test_bisimulation(lossy_buffer, buffer, false, false, false, false);
198 1 : }
|
