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

@@ -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:

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;

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)
+tc.assertEqual(synt_ltlf(f1, outs)[0], False)