diff --git a/NEWS b/NEWS index 47cd487cc..343c36543 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.12.0.dev (not yet released) - Generating random formula without any unary opertors would very often create formulas much smaller than asked. + - 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 e0d880647..3eba9bf41 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -351,6 +351,21 @@ State: 17 --END--""" ) +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) @@ -370,6 +385,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 @@ -520,4 +543,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)