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 lts_pbisim_test
14 : #include <boost/test/included/unit_test.hpp>
15 :
16 : #include "mcrl2/lts/probabilistic_arbitrary_precision_fraction.h"
17 : #include "mcrl2/lts/detail/liblts_pbisim_bem.h"
18 : #include "mcrl2/lts/detail/liblts_pbisim_grv.h"
19 :
20 : using namespace mcrl2::lts;
21 :
22 7 : static probabilistic_lts_aut_t parse_aut(const std::string& s)
23 : {
24 7 : std::stringstream is(s);
25 7 : probabilistic_lts_aut_t l;
26 7 : l.load(is);
27 14 : return l;
28 7 : }
29 :
30 7 : void execute_test(const std::string test_name,
31 : const std::string input_lts,
32 : const std::size_t expected_number_of_states,
33 : const std::size_t expected_number_of_transitions,
34 : const std::size_t expected_number_of_probabilistic_states)
35 : {
36 14 : mcrl2::utilities::execution_timer timer;
37 7 : probabilistic_lts_aut_t t1 = parse_aut(input_lts);
38 7 : probabilistic_lts_aut_t t2=t1;
39 7 : BOOST_CHECK(t1==t2);
40 7 : detail::probabilistic_bisimulation_reduce_grv(t1,timer);
41 7 : if (t1.num_states()!=expected_number_of_states || t1.num_transitions() != expected_number_of_transitions || t1.num_probabilistic_states()!=expected_number_of_probabilistic_states)
42 : {
43 0 : std::cerr << "The test " << test_name << " failed using Groote, Rivera Verduzco, de Vink reduction.\n";
44 0 : std::cerr << "Expected number of states: " << expected_number_of_states << ". Actual number of states: " << t1.num_states() << "\n";
45 0 : std::cerr << "Expected number of transitions: " << expected_number_of_transitions << ". Actual number of transitions: " << t1.num_transitions() << "\n";
46 0 : std::cerr << "Expected number of probabilistic states: " << expected_number_of_probabilistic_states << ". Actual number of probabilistic states: " << t1.num_probabilistic_states() << "\n";
47 0 : BOOST_CHECK(false);
48 : }
49 :
50 7 : detail::probabilistic_bisimulation_reduce_bem(t2,timer);
51 7 : if (t2.num_states()!=expected_number_of_states || t2.num_transitions() != expected_number_of_transitions || t2.num_probabilistic_states()!=expected_number_of_probabilistic_states)
52 : {
53 0 : std::cerr << "The test " << test_name << " failed using Baier, Engelen, Majster-Cederbaum reduction.\n";
54 0 : std::cerr << "Expected number of states: " << expected_number_of_states << ". Actual number of states: " << t2.num_states() << "\n";
55 0 : std::cerr << "Expected number of transitions: " << expected_number_of_transitions << ". Actual number of transitions: " << t2.num_transitions() << "\n";
56 0 : std::cerr << "Expected number of probabilistic states: " << expected_number_of_probabilistic_states << ". Actual number of probabilistic states: " << t2.num_probabilistic_states() << "\n";
57 0 : BOOST_CHECK(false);
58 : }
59 :
60 7 : }
61 :
62 : // Example below represents an example using probabilistic lts.
63 : const std::string test1 =
64 : "des(1 1 / 9 2 1 / 9 3 1 / 9 4 1 / 9 5 1 / 9 6 1 / 9 7 1 / 9 8 1 / 9 0, 9, 10)\n"
65 : "(0, \"player_collects_prize(false)\", 9)\n"
66 : "(1, \"player_collects_prize(true)\", 9)\n"
67 : "(2, \"player_collects_prize(true)\", 9)\n"
68 : "(3, \"player_collects_prize(true)\", 9)\n"
69 : "(4, \"player_collects_prize(false)\", 9)\n"
70 : "(5, \"player_collects_prize(true)\", 9)\n"
71 : "(6, \"player_collects_prize(true)\", 9)\n"
72 : "(7, \"player_collects_prize(true)\", 9)\n"
73 : "(8, \"player_collects_prize(false)\", 9)\n";
74 :
75 : // Example below represents a.(1/2 b + 1/2 b) which can be reduced to a.b.
76 : const std::string test2 =
77 : "des (0,3,5)\n"
78 : "(0,\"a\",1 1/2 2)\n"
79 : "(1,\"b\",3)\n"
80 : "(2,\"b\",4)\n";
81 :
82 : // Example below represents a.(1/2 b + 1/2 b)+ a.(1/4 b + 3/4 b) which can be reduced to a.b.
83 : const std::string test3 =
84 : "des (0,4,5)\n"
85 : "(0,\"a\",1 1/2 2)\n"
86 : "(0,\"a\",1 1/4 2)\n"
87 : "(1,\"b\",3)\n"
88 : "(2,\"b\",4)\n";
89 :
90 : //Example in paper of Christel Bier. Deciding Bisimilarity and Similarity for Probabilistic Processes.
91 : const std::string test4 =
92 : "des (0 1/4 5 1/4 11 1/4 14,11,19)\n"
93 : "(0,\"a\",1)\n"
94 : "(0,\"a\",2 1/2 3)\n"
95 : "(2,\"b\",4)\n"
96 : "(5,\"a\",6)\n"
97 : "(5,\"a\",7 1/2 8 1/8 9)\n"
98 : "(7,\"b\",10)\n"
99 : "(11,\"a\",12)\n"
100 : "(12,\"b\",13)\n"
101 : "(14,\"a\",15 1/3 16)\n"
102 : "(15,\"c\",17)\n"
103 : "(16,\"b\",18)\n";
104 :
105 : // Airplane ticket example test
106 : const std::string test5 =
107 : "des (1 1/3 0,14,15)\n"
108 : "(0,\"enter\",3 1/4 4 1/4 5 1/4 2)\n"
109 : "(1,\"enter\",7 1/2 6)\n"
110 : "(2,\"enter_plane\",8)\n"
111 : "(3,\"enter_plane\",9)\n"
112 : "(4,\"enter_plane\",8)\n"
113 : "(5,\"enter_plane\",8)\n"
114 : "(6,\"enter_plane\",9)\n"
115 : "(7,\"enter_plane\",9)\n"
116 : "(8,\"enter\",10)\n"
117 : "(9,\"enter\",11)\n"
118 : "(10,\"enter_plane\",12)\n"
119 : "(11,\"enter_plane\",13)\n"
120 : "(12,\"last_passenger_has_his_own_seat(false)\",14)\n"
121 : "(13,\"last_passenger_has_his_own_seat(true)\",14)\n";
122 :
123 : // Ant grid test
124 : const std::string test6 =
125 : "des (1 1/4 2 1/4 3 1/4 0,240,240)\n"
126 : "(0,\"step\",5 1/4 6 1/4 7 1/4 4)\n"
127 : "(1,\"step\",9 1/4 10 1/4 11 1/4 8)\n"
128 : "(2,\"step\",13 1/4 14 1/4 15 1/4 12)\n"
129 : "(3,\"step\",17 1/4 18 1/4 19 1/4 16)\n"
130 : "(4,\"step\",21 1/4 22 1/4 23 1/4 20)\n"
131 : "(5,\"step\",1 1/4 2 1/4 3 1/4 0)\n"
132 : "(6,\"step\",25 1/4 26 1/4 27 1/4 24)\n"
133 : "(7,\"step\",29 1/4 30 1/4 31 1/4 28)\n"
134 : "(8,\"step\",1 1/4 2 1/4 3 1/4 0)\n"
135 : "(9,\"step\",33 1/4 34 1/4 35 1/4 32)\n"
136 : "(10,\"step\",37 1/4 38 1/4 39 1/4 36)\n"
137 : "(11,\"step\",41 1/4 42 1/4 43 1/4 40)\n"
138 : "(12,\"step\",25 1/4 26 1/4 27 1/4 24)\n"
139 : "(13,\"step\",37 1/4 38 1/4 39 1/4 36)\n"
140 : "(14,\"step\",45 1/4 46 1/4 47 1/4 44)\n"
141 : "(15,\"step\",1 1/4 2 1/4 3 1/4 0)\n"
142 : "(16,\"step\",29 1/4 30 1/4 31 1/4 28)\n"
143 : "(17,\"step\",41 1/4 42 1/4 43 1/4 40)\n"
144 : "(18,\"step\",1 1/4 2 1/4 3 1/4 0)\n"
145 : "(19,\"step\",49 1/4 50 1/4 51 1/4 48)\n"
146 : "(20,\"step\",53 1/4 54 1/4 55 1/4 52)\n"
147 : "(21,\"step\",5 1/4 6 1/4 7 1/4 4)\n"
148 : "(22,\"step\",57 1/4 58 1/4 59 1/4 56)\n"
149 : "(23,\"step\",61 1/4 62 1/4 63 1/4 60)\n"
150 : "(24,\"step\",57 1/4 58 1/4 59 1/4 56)\n"
151 : "(25,\"step\",13 1/4 14 1/4 15 1/4 12)\n"
152 : "(26,\"step\",65 1/4 66 1/4 67 1/4 64)\n"
153 : "(27,\"step\",5 1/4 6 1/4 7 1/4 4)\n"
154 : "(28,\"step\",61 1/4 62 1/4 63 1/4 60)\n"
155 : "(29,\"step\",17 1/4 18 1/4 19 1/4 16)\n"
156 : "(30,\"step\",5 1/4 6 1/4 7 1/4 4)\n"
157 : "(31,\"step\",69 1/4 70 1/4 71 1/4 68)\n"
158 : "(32,\"step\",9 1/4 10 1/4 11 1/4 8)\n"
159 : "(33,\"step\",73 1/4 74 1/4 75 1/4 72)\n"
160 : "(34,\"step\",77 1/4 78 1/4 79 1/4 76)\n"
161 : "(35,\"step\",81 1/4 82 1/4 83 1/4 80)\n"
162 : "(36,\"step\",13 1/4 14 1/4 15 1/4 12)\n"
163 : "(37,\"step\",77 1/4 78 1/4 79 1/4 76)\n"
164 : "(38,\"step\",85 1/4 86 1/4 87 1/4 84)\n"
165 : "(39,\"step\",9 1/4 10 1/4 11 1/4 8)\n"
166 : "(40,\"step\",17 1/4 18 1/4 19 1/4 16)\n"
167 : "(41,\"step\",81 1/4 82 1/4 83 1/4 80)\n"
168 : "(42,\"step\",9 1/4 10 1/4 11 1/4 8)\n"
169 : "(43,\"step\",89 1/4 90 1/4 91 1/4 88)\n"
170 : "(44,\"dead\",45 1/4 46 1/4 47 1/4 44)\n"
171 : "(45,\"dead\",45 1/4 46 1/4 47 1/4 44)\n"
172 : "(46,\"dead\",45 1/4 46 1/4 47 1/4 44)\n"
173 : "(47,\"dead\",45 1/4 46 1/4 47 1/4 44)\n"
174 : "(48,\"step\",69 1/4 70 1/4 71 1/4 68)\n"
175 : "(49,\"step\",89 1/4 90 1/4 91 1/4 88)\n"
176 : "(50,\"step\",17 1/4 18 1/4 19 1/4 16)\n"
177 : "(51,\"step\",93 1/4 94 1/4 95 1/4 92)\n"
178 : "(52,\"step\",97 1/4 98 1/4 99 1/4 96)\n"
179 : "(53,\"step\",21 1/4 22 1/4 23 1/4 20)\n"
180 : "(54,\"step\",101 1/4 102 1/4 103 1/4 100)\n"
181 : "(55,\"step\",105 1/4 106 1/4 107 1/4 104)\n"
182 : "(56,\"step\",101 1/4 102 1/4 103 1/4 100)\n"
183 : "(57,\"step\",25 1/4 26 1/4 27 1/4 24)\n"
184 : "(58,\"step\",109 1/4 110 1/4 111 1/4 108)\n"
185 : "(59,\"step\",21 1/4 22 1/4 23 1/4 20)\n"
186 : "(60,\"step\",105 1/4 106 1/4 107 1/4 104)\n"
187 : "(61,\"step\",29 1/4 30 1/4 31 1/4 28)\n"
188 : "(62,\"step\",21 1/4 22 1/4 23 1/4 20)\n"
189 : "(63,\"step\",113 1/4 114 1/4 115 1/4 112)\n"
190 : "(64,\"dead\",65 1/4 66 1/4 67 1/4 64)\n"
191 : "(65,\"dead\",65 1/4 66 1/4 67 1/4 64)\n"
192 : "(66,\"dead\",65 1/4 66 1/4 67 1/4 64)\n"
193 : "(67,\"dead\",65 1/4 66 1/4 67 1/4 64)\n"
194 : "(68,\"step\",113 1/4 114 1/4 115 1/4 112)\n"
195 : "(69,\"step\",49 1/4 50 1/4 51 1/4 48)\n"
196 : "(70,\"step\",29 1/4 30 1/4 31 1/4 28)\n"
197 : "(71,\"step\",117 1/4 118 1/4 119 1/4 116)\n"
198 : "(72,\"live\",73 1/4 74 1/4 75 1/4 72)\n"
199 : "(73,\"live\",73 1/4 74 1/4 75 1/4 72)\n"
200 : "(74,\"live\",73 1/4 74 1/4 75 1/4 72)\n"
201 : "(75,\"live\",73 1/4 74 1/4 75 1/4 72)\n"
202 : "(76,\"step\",37 1/4 38 1/4 39 1/4 36)\n"
203 : "(77,\"step\",121 1/4 122 1/4 123 1/4 120)\n"
204 : "(78,\"step\",125 1/4 126 1/4 127 1/4 124)\n"
205 : "(79,\"step\",33 1/4 34 1/4 35 1/4 32)\n"
206 : "(80,\"step\",41 1/4 42 1/4 43 1/4 40)\n"
207 : "(81,\"step\",129 1/4 130 1/4 131 1/4 128)\n"
208 : "(82,\"step\",33 1/4 34 1/4 35 1/4 32)\n"
209 : "(83,\"step\",133 1/4 134 1/4 135 1/4 132)\n"
210 : "(84,\"dead\",85 1/4 86 1/4 87 1/4 84)\n"
211 : "(85,\"dead\",85 1/4 86 1/4 87 1/4 84)\n"
212 : "(86,\"dead\",85 1/4 86 1/4 87 1/4 84)\n"
213 : "(87,\"dead\",85 1/4 86 1/4 87 1/4 84)\n"
214 : "(88,\"step\",49 1/4 50 1/4 51 1/4 48)\n"
215 : "(89,\"step\",133 1/4 134 1/4 135 1/4 132)\n"
216 : "(90,\"step\",41 1/4 42 1/4 43 1/4 40)\n"
217 : "(91,\"step\",137 1/4 138 1/4 139 1/4 136)\n"
218 : "(92,\"step\",117 1/4 118 1/4 119 1/4 116)\n"
219 : "(93,\"step\",137 1/4 138 1/4 139 1/4 136)\n"
220 : "(94,\"step\",49 1/4 50 1/4 51 1/4 48)\n"
221 : "(95,\"step\",141 1/4 142 1/4 143 1/4 140)\n"
222 : "(96,\"live\",97 1/4 98 1/4 99 1/4 96)\n"
223 : "(97,\"live\",97 1/4 98 1/4 99 1/4 96)\n"
224 : "(98,\"live\",97 1/4 98 1/4 99 1/4 96)\n"
225 : "(99,\"live\",97 1/4 98 1/4 99 1/4 96)\n"
226 : "(100,\"step\",145 1/4 146 1/4 147 1/4 144)\n"
227 : "(101,\"step\",57 1/4 58 1/4 59 1/4 56)\n"
228 : "(102,\"step\",149 1/4 150 1/4 151 1/4 148)\n"
229 : "(103,\"step\",53 1/4 54 1/4 55 1/4 52)\n"
230 : "(104,\"step\",153 1/4 154 1/4 155 1/4 152)\n"
231 : "(105,\"step\",61 1/4 62 1/4 63 1/4 60)\n"
232 : "(106,\"step\",53 1/4 54 1/4 55 1/4 52)\n"
233 : "(107,\"step\",157 1/4 158 1/4 159 1/4 156)\n"
234 : "(108,\"dead\",109 1/4 110 1/4 111 1/4 108)\n"
235 : "(109,\"dead\",109 1/4 110 1/4 111 1/4 108)\n"
236 : "(110,\"dead\",109 1/4 110 1/4 111 1/4 108)\n"
237 : "(111,\"dead\",109 1/4 110 1/4 111 1/4 108)\n"
238 : "(112,\"step\",157 1/4 158 1/4 159 1/4 156)\n"
239 : "(113,\"step\",69 1/4 70 1/4 71 1/4 68)\n"
240 : "(114,\"step\",61 1/4 62 1/4 63 1/4 60)\n"
241 : "(115,\"step\",161 1/4 162 1/4 163 1/4 160)\n"
242 : "(116,\"step\",161 1/4 162 1/4 163 1/4 160)\n"
243 : "(117,\"step\",93 1/4 94 1/4 95 1/4 92)\n"
244 : "(118,\"step\",69 1/4 70 1/4 71 1/4 68)\n"
245 : "(119,\"step\",165 1/4 166 1/4 167 1/4 164)\n"
246 : "(120,\"live\",121 1/4 122 1/4 123 1/4 120)\n"
247 : "(121,\"live\",121 1/4 122 1/4 123 1/4 120)\n"
248 : "(122,\"live\",121 1/4 122 1/4 123 1/4 120)\n"
249 : "(123,\"live\",121 1/4 122 1/4 123 1/4 120)\n"
250 : "(124,\"dead\",125 1/4 126 1/4 127 1/4 124)\n"
251 : "(125,\"dead\",125 1/4 126 1/4 127 1/4 124)\n"
252 : "(126,\"dead\",125 1/4 126 1/4 127 1/4 124)\n"
253 : "(127,\"dead\",125 1/4 126 1/4 127 1/4 124)\n"
254 : "(128,\"live\",129 1/4 130 1/4 131 1/4 128)\n"
255 : "(129,\"live\",129 1/4 130 1/4 131 1/4 128)\n"
256 : "(130,\"live\",129 1/4 130 1/4 131 1/4 128)\n"
257 : "(131,\"live\",129 1/4 130 1/4 131 1/4 128)\n"
258 : "(132,\"step\",89 1/4 90 1/4 91 1/4 88)\n"
259 : "(133,\"step\",169 1/4 170 1/4 171 1/4 168)\n"
260 : "(134,\"step\",81 1/4 82 1/4 83 1/4 80)\n"
261 : "(135,\"step\",173 1/4 174 1/4 175 1/4 172)\n"
262 : "(136,\"step\",93 1/4 94 1/4 95 1/4 92)\n"
263 : "(137,\"step\",173 1/4 174 1/4 175 1/4 172)\n"
264 : "(138,\"step\",89 1/4 90 1/4 91 1/4 88)\n"
265 : "(139,\"step\",177 1/4 178 1/4 179 1/4 176)\n"
266 : "(140,\"step\",165 1/4 166 1/4 167 1/4 164)\n"
267 : "(141,\"step\",177 1/4 178 1/4 179 1/4 176)\n"
268 : "(142,\"step\",93 1/4 94 1/4 95 1/4 92)\n"
269 : "(143,\"step\",181 1/4 182 1/4 183 1/4 180)\n"
270 : "(144,\"live\",145 1/4 146 1/4 147 1/4 144)\n"
271 : "(145,\"live\",145 1/4 146 1/4 147 1/4 144)\n"
272 : "(146,\"live\",145 1/4 146 1/4 147 1/4 144)\n"
273 : "(147,\"live\",145 1/4 146 1/4 147 1/4 144)\n"
274 : "(148,\"dead\",149 1/4 150 1/4 151 1/4 148)\n"
275 : "(149,\"dead\",149 1/4 150 1/4 151 1/4 148)\n"
276 : "(150,\"dead\",149 1/4 150 1/4 151 1/4 148)\n"
277 : "(151,\"dead\",149 1/4 150 1/4 151 1/4 148)\n"
278 : "(152,\"live\",153 1/4 154 1/4 155 1/4 152)\n"
279 : "(153,\"live\",153 1/4 154 1/4 155 1/4 152)\n"
280 : "(154,\"live\",153 1/4 154 1/4 155 1/4 152)\n"
281 : "(155,\"live\",153 1/4 154 1/4 155 1/4 152)\n"
282 : "(156,\"step\",185 1/4 186 1/4 187 1/4 184)\n"
283 : "(157,\"step\",113 1/4 114 1/4 115 1/4 112)\n"
284 : "(158,\"step\",105 1/4 106 1/4 107 1/4 104)\n"
285 : "(159,\"step\",189 1/4 190 1/4 191 1/4 188)\n"
286 : "(160,\"step\",189 1/4 190 1/4 191 1/4 188)\n"
287 : "(161,\"step\",117 1/4 118 1/4 119 1/4 116)\n"
288 : "(162,\"step\",113 1/4 114 1/4 115 1/4 112)\n"
289 : "(163,\"step\",193 1/4 194 1/4 195 1/4 192)\n"
290 : "(164,\"step\",193 1/4 194 1/4 195 1/4 192)\n"
291 : "(165,\"step\",141 1/4 142 1/4 143 1/4 140)\n"
292 : "(166,\"step\",117 1/4 118 1/4 119 1/4 116)\n"
293 : "(167,\"step\",197 1/4 198 1/4 199 1/4 196)\n"
294 : "(168,\"live\",169 1/4 170 1/4 171 1/4 168)\n"
295 : "(169,\"live\",169 1/4 170 1/4 171 1/4 168)\n"
296 : "(170,\"live\",169 1/4 170 1/4 171 1/4 168)\n"
297 : "(171,\"live\",169 1/4 170 1/4 171 1/4 168)\n"
298 : "(172,\"step\",137 1/4 138 1/4 139 1/4 136)\n"
299 : "(173,\"step\",201 1/4 202 1/4 203 1/4 200)\n"
300 : "(174,\"step\",133 1/4 134 1/4 135 1/4 132)\n"
301 : "(175,\"step\",205 1/4 206 1/4 207 1/4 204)\n"
302 : "(176,\"step\",141 1/4 142 1/4 143 1/4 140)\n"
303 : "(177,\"step\",205 1/4 206 1/4 207 1/4 204)\n"
304 : "(178,\"step\",137 1/4 138 1/4 139 1/4 136)\n"
305 : "(179,\"step\",209 1/4 210 1/4 211 1/4 208)\n"
306 : "(180,\"dead\",181 1/4 182 1/4 183 1/4 180)\n"
307 : "(181,\"dead\",181 1/4 182 1/4 183 1/4 180)\n"
308 : "(182,\"dead\",181 1/4 182 1/4 183 1/4 180)\n"
309 : "(183,\"dead\",181 1/4 182 1/4 183 1/4 180)\n"
310 : "(184,\"live\",185 1/4 186 1/4 187 1/4 184)\n"
311 : "(185,\"live\",185 1/4 186 1/4 187 1/4 184)\n"
312 : "(186,\"live\",185 1/4 186 1/4 187 1/4 184)\n"
313 : "(187,\"live\",185 1/4 186 1/4 187 1/4 184)\n"
314 : "(188,\"step\",213 1/4 214 1/4 215 1/4 212)\n"
315 : "(189,\"step\",161 1/4 162 1/4 163 1/4 160)\n"
316 : "(190,\"step\",157 1/4 158 1/4 159 1/4 156)\n"
317 : "(191,\"step\",217 1/4 218 1/4 219 1/4 216)\n"
318 : "(192,\"step\",217 1/4 218 1/4 219 1/4 216)\n"
319 : "(193,\"step\",165 1/4 166 1/4 167 1/4 164)\n"
320 : "(194,\"step\",161 1/4 162 1/4 163 1/4 160)\n"
321 : "(195,\"step\",221 1/4 222 1/4 223 1/4 220)\n"
322 : "(196,\"dead\",197 1/4 198 1/4 199 1/4 196)\n"
323 : "(197,\"dead\",197 1/4 198 1/4 199 1/4 196)\n"
324 : "(198,\"dead\",197 1/4 198 1/4 199 1/4 196)\n"
325 : "(199,\"dead\",197 1/4 198 1/4 199 1/4 196)\n"
326 : "(200,\"live\",201 1/4 202 1/4 203 1/4 200)\n"
327 : "(201,\"live\",201 1/4 202 1/4 203 1/4 200)\n"
328 : "(202,\"live\",201 1/4 202 1/4 203 1/4 200)\n"
329 : "(203,\"live\",201 1/4 202 1/4 203 1/4 200)\n"
330 : "(204,\"step\",177 1/4 178 1/4 179 1/4 176)\n"
331 : "(205,\"step\",225 1/4 226 1/4 227 1/4 224)\n"
332 : "(206,\"step\",173 1/4 174 1/4 175 1/4 172)\n"
333 : "(207,\"step\",229 1/4 230 1/4 231 1/4 228)\n"
334 : "(208,\"dead\",209 1/4 210 1/4 211 1/4 208)\n"
335 : "(209,\"dead\",209 1/4 210 1/4 211 1/4 208)\n"
336 : "(210,\"dead\",209 1/4 210 1/4 211 1/4 208)\n"
337 : "(211,\"dead\",209 1/4 210 1/4 211 1/4 208)\n"
338 : "(212,\"live\",213 1/4 214 1/4 215 1/4 212)\n"
339 : "(213,\"live\",213 1/4 214 1/4 215 1/4 212)\n"
340 : "(214,\"live\",213 1/4 214 1/4 215 1/4 212)\n"
341 : "(215,\"live\",213 1/4 214 1/4 215 1/4 212)\n"
342 : "(216,\"step\",233 1/4 234 1/4 235 1/4 232)\n"
343 : "(217,\"step\",193 1/4 194 1/4 195 1/4 192)\n"
344 : "(218,\"step\",189 1/4 190 1/4 191 1/4 188)\n"
345 : "(219,\"step\",237 1/4 238 1/4 239 1/4 236)\n"
346 : "(220,\"dead\",221 1/4 222 1/4 223 1/4 220)\n"
347 : "(221,\"dead\",221 1/4 222 1/4 223 1/4 220)\n"
348 : "(222,\"dead\",221 1/4 222 1/4 223 1/4 220)\n"
349 : "(223,\"dead\",221 1/4 222 1/4 223 1/4 220)\n"
350 : "(224,\"live\",225 1/4 226 1/4 227 1/4 224)\n"
351 : "(225,\"live\",225 1/4 226 1/4 227 1/4 224)\n"
352 : "(226,\"live\",225 1/4 226 1/4 227 1/4 224)\n"
353 : "(227,\"live\",225 1/4 226 1/4 227 1/4 224)\n"
354 : "(228,\"dead\",229 1/4 230 1/4 231 1/4 228)\n"
355 : "(229,\"dead\",229 1/4 230 1/4 231 1/4 228)\n"
356 : "(230,\"dead\",229 1/4 230 1/4 231 1/4 228)\n"
357 : "(231,\"dead\",229 1/4 230 1/4 231 1/4 228)\n"
358 : "(232,\"live\",233 1/4 234 1/4 235 1/4 232)\n"
359 : "(233,\"live\",233 1/4 234 1/4 235 1/4 232)\n"
360 : "(234,\"live\",233 1/4 234 1/4 235 1/4 232)\n"
361 : "(235,\"live\",233 1/4 234 1/4 235 1/4 232)\n"
362 : "(236,\"dead\",237 1/4 238 1/4 239 1/4 236)\n"
363 : "(237,\"dead\",237 1/4 238 1/4 239 1/4 236)\n"
364 : "(238,\"dead\",237 1/4 238 1/4 239 1/4 236)\n"
365 : "(239,\"dead\",237 1/4 238 1/4 239 1/4 236)\n"
366 : ;
367 :
368 : /* The example below turned out to be a tricky example on which
369 : * an intermediate version of the Groote/Verduzco/Vink algorithm failed. */
370 : std::string test7 =
371 : "des(0,5,3)\n"
372 : "(0,\"a\", 2)\n"
373 : "(1,\"a\", 2 2/4 2)\n"
374 : "(0,\"tau\",0 1/4 1 2/4 1)\n"
375 : "(1,\"tau\",1 3/4 1)\n"
376 : "(0,\"tau\",2 3/4 2)\n"
377 : ;
378 :
379 :
380 2 : BOOST_AUTO_TEST_CASE(test_state_space_reductions)
381 : {
382 1 : execute_test("Test1",test1,3,2,1);
383 1 : execute_test("Test2",test1,3,2,1);
384 1 : execute_test("Test3",test3,3,2,2);
385 1 : execute_test("Test4",test4,6,6,4);
386 1 : execute_test("Test5",test5,11,10,9);
387 1 : execute_test("Test6",test6,13,13,11);
388 1 : execute_test("Test7",test7,3,5,3);
389 1 : }
390 :
391 : // Test whether a probabilistic state of length 1,
392 : // stored as a single number, and stored as a vector of length 1
393 : // are considered the same object for equality and the hash function.
394 2 : BOOST_AUTO_TEST_CASE(hash_and_equality_test)
395 : {
396 : typedef probabilistic_state<std::size_t, mcrl2::lps::probabilistic_data_expression> prob_state;
397 1 : prob_state s1(1);
398 1 : prob_state s2;
399 1 : s2.add(1,mcrl2::lps::probabilistic_data_expression::one());
400 1 : BOOST_CHECK(s1==s2);
401 : std::hash<prob_state> hasher;
402 1 : BOOST_CHECK(hasher(s1)==hasher(s2));
403 :
404 : typedef probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> prob_state_alt;
405 1 : prob_state_alt s3(1);
406 1 : prob_state_alt s4;
407 1 : s4.add(1,mcrl2::lts::probabilistic_arbitrary_precision_fraction::one());
408 1 : BOOST_CHECK(s3==s4);
409 : std::hash<prob_state_alt> hasher_alt;
410 1 : BOOST_CHECK(hasher_alt(s3)==hasher_alt(s4));
411 1 : }
|
