From 89a06772b853a17630d6e794d0ffabc5013ce617 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 30 Aug 2024 16:05:50 +0200 Subject: [PATCH] game: fix solving "parity min" games with multi-colored edges * spot/twaalgos/game.cc: If the original acceptance is "parity min", use min_set(), not max_set(), to read edge priorities. * tests/python/game.py: Add a test case. * NEWS: Mention the bug. --- NEWS | 5 +++++ spot/twaalgos/game.cc | 3 ++- tests/python/game.py | 25 ++++++++++++++++++++++++- 3 files changed, 31 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index a288b097c..c9bfab98e 100644 --- a/NEWS +++ b/NEWS @@ -76,6 +76,11 @@ New in spot 2.12.0.dev (not yet released) - Generating random formulas without any unary opertor would very often create formulas much smaller than specified. + - The parity game solver, which internally works on "parity max + odd", but actually accept any type of parity acceptance, could be + confused by games with "parity min" acceptance using transition + with several colors (a rather uncommon situation). + New in spot 2.12 (2024-05-16) Build: diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 404fa4778..e2c550531 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -357,7 +357,8 @@ namespace spot // Takes an edge and returns the "equivalent" max odd parity auto equiv_par = [max, odd, next_max_par, inv = 2*max-1](const auto& e) { - par_t e_par = e.acc.max_set() - 1; // -1 for empty + par_t e_par = + (max ? e.acc.max_set() : e.acc.min_set()) - 1; // -1 for empty // If "min" and empty -> set to n if (!max & (e_par == -1)) e_par = next_max_par; diff --git a/tests/python/game.py b/tests/python/game.py index 3462cc7d2..f8007c372 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -368,6 +368,21 @@ tc.assertTrue(all([wn == wr for (wn, wr, p) in zip(winners_new, winners_ref, players_ref) if not p])) +def maximize_colors(aut, is_max): + ns = aut.num_sets() + v = [] + if is_max: + for c in range(ns+1): + v.append(spot.mark_t(list(range(c)))) + for e in aut.edges(): + e.acc = v[e.acc.max_set()] + else: + for c in range(ns+1): + v.append(spot.mark_t(list(range(c, ns)))) + v.insert(0, spot.mark_t([])) + for e in aut.edges(): + e.acc = v[e.acc.min_set()] + # Test the different parity conditions gdpa = spot.tgba_determinize(spot.degeneralize_tba(g), False, True, True, False) @@ -387,6 +402,14 @@ for kind in [spot.parity_kind_min, spot.parity_kind_max]: tc.assertTrue(spot.solve_parity_game(g_test_split1)) c_strat1 = spot.get_strategy(g_test_split1) tc.assertTrue(c_strat == c_strat1) + # Same test, but adding a lot of useless colors in the game + g_test_split2 = spot.change_parity(g_test_split, kind, style) + maximize_colors(g_test_split2, kind == spot.parity_kind_max) + spot.set_state_players(g_test_split2, sp) + tc.assertTrue(spot.solve_parity_game(g_test_split2)) + c_strat2 = spot.get_strategy(g_test_split2) + tc.assertTrue(c_strat == c_strat2) + # Test that strategies are not appended # if solve is called multiple times @@ -537,4 +560,4 @@ f1 = "((((G (F (idle))) && (G (((idle) && (X ((! (grant_0)) \ && (! (F (G ((request_0) && (X (! (grant_0)))))))) \ && (! (F (G ((request_1) && (X (! (grant_1)))))))))" outs = ["grant_0", "grant1"] -tc.assertEqual(synt_ltlf(f1, outs)[0], False) \ No newline at end of file +tc.assertEqual(synt_ltlf(f1, outs)[0], False)