Line data Source code
1 : // Author(s): Maurice Laveaux
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 :
10 : #define BOOST_TEST_MODULE symbolic_parity_game_test
11 : #include <boost/test/included/unit_test.hpp>
12 :
13 2 : BOOST_AUTO_TEST_CASE(dummy_test)
14 : {
15 : // This is an empty test since at least one test is required.
16 1 : }
17 :
18 : /*
19 : // Commented this test since Sylvan causes some address sanitizer failures that I cannot resolve.
20 : #ifdef MCRL2_ENABLE_SYLVAN
21 :
22 : #include "mcrl2/data/variable.h"
23 : #include "mcrl2/pbes/symbolic_parity_game.h"
24 : #include "mcrl2/pbes/symbolic_pbessolve.h"
25 : #include "mcrl2/pbes/pbes_summand_group.h"
26 : #include "mcrl2/symbolic/data_index.h"
27 : #include "mcrl2/symbolic/test_utility.h"
28 :
29 : #include <sylvan_ldd.hpp>
30 :
31 : #include <vector>
32 : #include <random>
33 :
34 : using namespace mcrl2::pbes_system;
35 : using namespace mcrl2::symbolic;
36 : using sylvan::ldds::ldd;
37 :
38 : /// A single randomly generated transition group for parameter i
39 : summand_group single_transition_group(const mcrl2::data::variable_list& parameters, std::size_t i, std::size_t N, std::size_t D)
40 : {
41 : boost::dynamic_bitset<> dependencies(parameters.size()*2);
42 : dependencies[i] = 1;
43 : dependencies[i+1] = 1;
44 :
45 : summand_group group(parameters, dependencies, false);
46 : group.L = random_set(N, 2, D);
47 :
48 : return group;
49 : }
50 :
51 : /// \brief Generates a random parity game with N vertices and at most P priorities.
52 : std::tuple<ldd, ldd, std::vector<ldd>, std::vector<summand_group>, std::vector<data_expression_index>> compute_random_game(std::size_t N, std::size_t P)
53 : {
54 : std::size_t D = 10; // Size of the state space domain.
55 : std::size_t length = 4; // Length of the state vector.
56 :
57 : ldd V = random_set(N, length, D);
58 : ldd Veven = random_subset(V, N / 2);
59 :
60 : ldd remaining = V;
61 : std::vector<ldd> prio(P);
62 : for (std::size_t i = 0; i < P; ++i)
63 : {
64 : prio[i] = random_subset(remaining, N/P);
65 : remaining = minus(remaining, prio[i]);
66 : }
67 :
68 : // Define some list of parameters.
69 : mcrl2::data::variable_list parameters;
70 : for (std::size_t j = 0; j < length; ++j)
71 : {
72 : parameters.emplace_front(mcrl2::data::variable());
73 : }
74 :
75 : // Generate random transition groups.
76 : std::vector<summand_group> groups;
77 : groups.emplace_back(single_transition_group(parameters, 0, 3*D, D));
78 : groups.emplace_back(single_transition_group(parameters, 1, 3*D, D));
79 : groups.emplace_back(single_transition_group(parameters, 2, 3*D, D));
80 : groups.emplace_back(single_transition_group(parameters, 3, 3*D, D));
81 :
82 : std::vector<data_expression_index> index;
83 :
84 : return std::make_tuple(V, Veven, prio, groups, index);
85 : }
86 :
87 : /// \returns Minimal fixpoint of the given (monotone) predicate transformer A -> A.
88 : template<typename F>
89 : ldd least_fixpoint(F pred)
90 : {
91 : ldd prev, current;
92 : do
93 : {
94 : prev = current;
95 : current = pred(current);
96 : }
97 : while (current != prev);
98 :
99 : return current;
100 : }
101 :
102 : /// \returns Maximal fixpoint of the given (monotone) predicate transformer A -> A.
103 : template<typename F>
104 : ldd greatest_fixpoint(F pred, ldd V)
105 : {
106 : ldd prev;
107 : ldd current = V;
108 : do
109 : {
110 : prev = current;
111 : current = pred(current);
112 : }
113 : while (current != prev);
114 :
115 : return current;
116 : }
117 :
118 : /// \returns The predecessors of U.
119 : ldd pre(const symbolic_parity_game& G, const ldd& V, const ldd& U)
120 : {
121 : return G.predecessors(V, U);
122 : }
123 :
124 : /// \returns The control predecessors of U.
125 : ldd cpre(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U)
126 : {
127 : std::array<const ldd, 2> Vplayer = G.players(V);
128 :
129 : return union_(
130 : intersect(Vplayer[alpha], pre(G, V, U)),
131 : minus(Vplayer[1 - alpha], union_(pre(G, V, minus(V, U)), G.sinks(V, V)))
132 : );
133 : }
134 :
135 : /// \returns Standard attractor set computation.
136 : ldd attr(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U)
137 : {
138 : return least_fixpoint(
139 : [&](const ldd& Z) -> ldd {
140 : return union_(U, cpre(G, V, alpha, Z));
141 : });
142 : }
143 :
144 : /// \returns The safe control predecessors of U.
145 : ldd spre(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U, const ldd& I)
146 : {
147 : std::array<const ldd, 2> Vplayer = G.players(V);
148 :
149 : return union_(
150 : intersect(Vplayer[alpha], G.predecessors(V, U)),
151 : minus(Vplayer[1 - alpha], union_(union_(G.predecessors(V, minus(V, U)), G.sinks(V, V)), I))
152 : );
153 : }
154 :
155 : /// \returns Safe attractor set computation.
156 : ldd sattr(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U, const ldd& I)
157 : {
158 : return least_fixpoint(
159 : [&](const ldd& Z) -> ldd {
160 : return union_(U, spre(G, V, alpha, Z, I));
161 : });
162 : }
163 :
164 : /// \brief Computes the monotone control predecessor.
165 : ldd Mcpre(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& Z, const ldd& U, std::size_t c)
166 : {
167 : return intersect(G.prio_above(V, c), cpre(G, V, alpha, union_(Z, U)));
168 : }
169 :
170 : /// \brief Computes monotone attractor for priority c.
171 : ldd Mattr(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U, std::size_t c)
172 : {
173 : return least_fixpoint(
174 : [&](const ldd& Z) -> ldd
175 : {
176 : return Mcpre(G, V, alpha, Z, U, c);
177 : }
178 : );
179 : }
180 :
181 : /// \returns Safe vertices computation.
182 : ldd safe(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& I)
183 : {
184 : std::array<const ldd, 2> Vplayer = G.players(V);
185 : return minus(V, attr(G, V, 1-alpha, intersect(Vplayer[1-alpha], I)));
186 : }
187 :
188 : /// \brief Computes fatal attractor for priority c.
189 : ldd fatal_attractor(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, std::size_t c, const ldd& I)
190 : {
191 : ldd Pequal = intersect(V, G.ranks().at(c));
192 : const ldd Vsafe = safe(G, V, alpha, I);
193 :
194 : return greatest_fixpoint(
195 : [&](const ldd& Z) -> ldd
196 : {
197 : // G \cap safe(G) is here represented by restricting V to Vsafe.
198 : return intersect(intersect(Pequal, Vsafe), Mattr(G, Vsafe, alpha, Z, c));
199 : },
200 : Vsafe
201 : );
202 : }
203 :
204 : /// \brief Computes the safe monotone control predecessor.
205 : ldd sMcpre(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& Z, const ldd& U, std::size_t c, const ldd& I)
206 : {
207 : return intersect(G.prio_above(V, c), spre(G, V, alpha, union_(Z, U), I));
208 : }
209 :
210 : /// \brief Computes monotone attractor for priority c.
211 : ldd sMattr(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& U, std::size_t c, const ldd& I)
212 : {
213 : return least_fixpoint(
214 : [&](const ldd& Z) -> ldd
215 : {
216 : return sMcpre(G, V, alpha, Z, U, c, I);
217 : }
218 : );
219 : }
220 :
221 : /// \brief Computes fatal attractor for priority c.
222 : ldd safe_fatal_attractor(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, std::size_t c, const ldd& I)
223 : {
224 : ldd Pequal = intersect(V, G.ranks().at(c));
225 :
226 : return greatest_fixpoint(
227 : [&](const ldd& Z) -> ldd
228 : {
229 : return intersect(Pequal, sMattr(G, V, alpha, Z, c, I));
230 : },
231 : V
232 : );
233 : }
234 :
235 : /// \brief Returns the solitair cycles.
236 : ldd solitair_cycles(const symbolic_parity_game& G, const ldd& V, std::size_t alpha)
237 : {
238 : std::array<const ldd, 2> Vplayer = G.players(V);
239 : std::array<const ldd, 2> parity = G.parity(V);
240 :
241 : return greatest_fixpoint(
242 : [&](const ldd& Z) -> ldd {
243 : return intersect(intersect(Vplayer[alpha], parity[alpha]), pre(G, V, Z));
244 : },
245 : V
246 : );
247 : }
248 :
249 : /// \brief Returns the forced cycles.
250 : ldd forced_cycles(const symbolic_parity_game& G, const ldd& V, std::size_t alpha, const ldd& I)
251 : {
252 : std::array<const ldd, 2> parity = G.parity(V);
253 : const ldd Vsafe = safe(G, V, alpha, I);
254 :
255 : return greatest_fixpoint(
256 : [&](const ldd& Z) -> ldd {
257 : return intersect(intersect(parity[alpha], Vsafe), cpre(G, V, alpha, Z));
258 : },
259 : V
260 : );
261 : }
262 :
263 : BOOST_AUTO_TEST_CASE(random_test_attractor)
264 : {
265 : initialise_sylvan();
266 :
267 : for (std::size_t i = 0; i < 100; ++i)
268 : {
269 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
270 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
271 :
272 : ldd U = random_subset(V, 250);
273 :
274 : std::array<const ldd, 2> Vplayer = G.players(V);
275 : ldd result = G.safe_attractor(U, 0, V, Vplayer);
276 : ldd expected = attr(G, V, 0, U);
277 : std::cerr << satcount(result) << std::endl;
278 :
279 : BOOST_CHECK_EQUAL(result, expected);
280 : }
281 :
282 : quit_sylvan();
283 : }
284 :
285 : BOOST_AUTO_TEST_CASE(random_test_safe_attractor)
286 : {
287 : initialise_sylvan();
288 :
289 : for (std::size_t i = 0; i < 100; ++i)
290 : {
291 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
292 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
293 :
294 : ldd U = random_subset(V, 250);
295 : ldd I = random_subset(minus(V, U), 250);
296 :
297 : std::array<const ldd, 2> Vplayer = G.players(V);
298 : ldd result = G.safe_attractor(U, 0, V, Vplayer, I);
299 : ldd expected = sattr(G, V, 0, U, I);
300 : std::cerr << satcount(result) << std::endl;
301 :
302 : BOOST_CHECK_EQUAL(result, expected);
303 : }
304 :
305 : quit_sylvan();
306 : }
307 :
308 : BOOST_AUTO_TEST_CASE(random_test_chaining_safe_attractor)
309 : {
310 : initialise_sylvan();
311 :
312 : for (std::size_t i = 0; i < 100; ++i)
313 : {
314 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
315 : symbolic_parity_game G(groups, index, V, Veven, prio, false, true);
316 :
317 : ldd U = random_subset(V, 250);
318 : ldd I = random_subset(minus(V, U), 250);
319 :
320 : std::array<const ldd, 2> Vplayer = G.players(V);
321 : ldd result = G.safe_attractor(U, 0, V, Vplayer, I);
322 : ldd expected = sattr(G, V, 0, U, I);
323 : std::cerr << satcount(result) << std::endl;
324 :
325 : BOOST_CHECK_EQUAL(result, expected);
326 : }
327 :
328 : quit_sylvan();
329 : }
330 :
331 : BOOST_AUTO_TEST_CASE(random_test_monotone_attractor)
332 : {
333 : initialise_sylvan();
334 :
335 : for (std::size_t i = 0; i < 100; ++i)
336 : {
337 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
338 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
339 :
340 : ldd U = random_subset(V, 250);
341 :
342 : std::array<const ldd, 2> Vplayer = G.players(V);
343 : ldd result = G.safe_monotone_attractor(U, 0, 0, V, Vplayer);
344 : ldd expected = Mattr(G, V, 0, U, 0);
345 : std::cerr << satcount(result) << std::endl;
346 :
347 : BOOST_CHECK_EQUAL(result, expected);
348 : }
349 :
350 : quit_sylvan();
351 : }
352 :
353 : BOOST_AUTO_TEST_CASE(random_test_safe_monotone_attractor)
354 : {
355 : initialise_sylvan();
356 :
357 : for (std::size_t i = 0; i < 100; ++i)
358 : {
359 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
360 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
361 :
362 : ldd U = random_subset(V, 250);
363 : ldd I = random_subset(minus(V, U), 250);
364 :
365 : std::array<const ldd, 2> Vplayer = G.players(V);
366 : ldd result = G.safe_monotone_attractor(U, 0, 0, V, Vplayer, I);
367 : ldd expected = sMattr(G, V, 0, U, 0, I);
368 : std::cerr << satcount(result) << std::endl;
369 :
370 : BOOST_CHECK_EQUAL(result, expected);
371 : }
372 :
373 : quit_sylvan();
374 : }
375 :
376 : BOOST_AUTO_TEST_CASE(random_test_chaining_monotone_attractor)
377 : {
378 : initialise_sylvan();
379 :
380 : for (std::size_t i = 0; i < 100; ++i)
381 : {
382 : auto [V, Veven, prio, groups, index] = compute_random_game(5000, 2);
383 : symbolic_parity_game G(groups, index, V, Veven, prio, false, true);
384 :
385 : ldd U = random_subset(V, 250);
386 : ldd I = random_subset(minus(V, U), 250);
387 :
388 : std::array<const ldd, 2> Vplayer = G.players(V);
389 : ldd result = G.safe_monotone_attractor(U, 0, 0, V, Vplayer, I);
390 : ldd expected = sMattr(G, V, 0, U, 0, I);
391 : std::cerr << satcount(result) << std::endl;
392 :
393 : BOOST_CHECK_EQUAL(result, expected);
394 : }
395 :
396 : quit_sylvan();
397 : }
398 :
399 : BOOST_AUTO_TEST_CASE(random_test_solitair_cycles)
400 : {
401 : initialise_sylvan();
402 :
403 : for (std::size_t i = 0; i < 1; ++i)
404 : {
405 : auto [V, Veven, prio, groups, index] = compute_random_game(100, 2);
406 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
407 : mcrl2::pbes_system::symbolic_pbessolve_algorithm solver(G);
408 :
409 : ldd initial = random_subset(V, 1);
410 : ldd I;
411 :
412 : // Use V as initial vertex so it does not terminate early.
413 : std::pair<ldd, ldd> Vresult = solver.detect_solitair_cycles(V, V, I, false, G.sinks(V, V));
414 :
415 : std::array<ldd, 2> winning;
416 : ldd Vtotal = G.compute_total_graph(V, sylvan::ldds::empty_set(), G.sinks(V, V), winning);
417 :
418 : std::pair<ldd, ldd> Vexpected = { union_(winning[0], attr(G, V, 0, solitair_cycles(G, V, 0))),
419 : union_(winning[1], attr(G, V, 1, solitair_cycles(G, V, 1))) };
420 : BOOST_CHECK_EQUAL(Vresult.first, Vexpected.first);
421 : BOOST_CHECK_EQUAL(Vresult.second, Vexpected.second);
422 : }
423 :
424 : quit_sylvan();
425 : }
426 :
427 : BOOST_AUTO_TEST_CASE(random_test_solitair_cycles)
428 : {
429 : initialise_sylvan();
430 :
431 : for (std::size_t i = 0; i < 1; ++i)
432 : {
433 : auto [V, Veven, prio, groups, index] = compute_random_game(500, 2);
434 : symbolic_parity_game G(groups, index, V, Veven, prio, false, false);
435 : mcrl2::pbes_system::symbolic_pbessolve_algorithm solver(G);
436 :
437 : ldd initial = random_subset(V, 1);
438 : ldd I;
439 :
440 : // Use V as initial vertex so it does not terminate early.
441 : std::pair<ldd, ldd> Vresult = solver.detect_forced_cycles(V, V, I, false, G.sinks(V, V));
442 :
443 : std::array<ldd, 2> winning;
444 : ldd Vtotal = G.compute_total_graph(V, sylvan::ldds::empty_set(), G.sinks(V, V), winning);
445 :
446 : std::pair<ldd, ldd> Vexpected = { union_(winning[0], attr(G, V, 0, forced_cycles(G, V, 0, I))),
447 : union_(winning[1], attr(G, V, 1, forced_cycles(G, V, 1, I))) };
448 : BOOST_CHECK_EQUAL(Vresult.first, Vexpected.first);
449 : BOOST_CHECK_EQUAL(Vresult.second, Vexpected.second);
450 : }
451 :
452 : quit_sylvan();
453 : }
454 :
455 : #endif // MCRL2_ENABLE_SYLVAN
456 : */
|
