From 37d4e513d95776f0144e4d8f8581f62d4e6a83f3 Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber-Caissier <philipp@lrde.epita.fr>
Date: Sun, 27 Nov 2022 01:16:46 +0100
Subject: [PATCH] game: fix appending strategies bug
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When calling solve_parity_game() multiple times on the same
automaton the strategies are appended one after the other.
Reported by Dávid Smolka.

* NEWS: Mention the bug.
* spot/twaalgos/game.cc: Fix it.
* tests/python/game.py: Test it.
* THANKS: Add Dávid.
---
 NEWS                  |  4 ++++
 THANKS                |  1 +
 spot/twaalgos/game.cc |  1 +
 tests/python/game.py  | 14 ++++++++++++++
 4 files changed, 20 insertions(+)

diff --git a/NEWS b/NEWS
index ec6cff1bf..b3f9b2c63 100644
--- a/NEWS
+++ b/NEWS
@@ -26,6 +26,10 @@ New in spot 2.11.2.dev  (not yet released)
   - 'autfilt -c ...' should display a match count even in present of
     parse errors.
 
+  - Calling solve_parity_game() multiple times on the same automaton
+    used to append the new strategy to the existing one instead of
+    overwriting it.
+
 New in spot 2.11.2  (2022-10-26)
 
   Command-line tools:
diff --git a/THANKS b/THANKS
index 2b054666c..356d187a1 100644
--- a/THANKS
+++ b/THANKS
@@ -11,6 +11,7 @@ Christian Dax
 Christopher Ziegler
 Clément Tamines
 David Müller
+Dávid Smolka
 Edmond Irani Liu
 Ernesto Posse
 Étienne Renault
diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc
index ccb3b818e..f5699bf49 100644
--- a/spot/twaalgos/game.cc
+++ b/spot/twaalgos/game.cc
@@ -227,6 +227,7 @@ namespace spot
         region_t &w = *arena->get_or_set_named_prop<region_t>("state-winner");
         strategy_t &s = *arena->get_or_set_named_prop<strategy_t>("strategy");
         w.swap(w_.winner_);
+        s.clear();
         s.reserve(s_.size());
         for (auto as : s_)
           s.push_back(as == no_strat_mark ? 0 : (unsigned) as);
diff --git a/tests/python/game.py b/tests/python/game.py
index 647c8d347..a7080b696 100644
--- a/tests/python/game.py
+++ b/tests/python/game.py
@@ -371,3 +371,17 @@ 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)
+
+# Test that strategies are not appended
+# if solve is called multiple times
+aut = spot.make_twa_graph()
+aut.set_buchi()
+aut.new_states(2)
+aut.new_edge(0,1,buddy.bddtrue, [0])
+aut.new_edge(1,0,buddy.bddtrue, [])
+spot.set_state_players(aut, [False, True])
+spot.solve_game(aut)
+S1 = list(spot.get_strategy(aut))
+spot.solve_game(aut)
+S2 = list(spot.get_strategy(aut))
+tc.assertEqual(S1, S2)
\ No newline at end of file