alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

game: fix appending strategies bug

Browse source 
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.
This commit is contained in:
Philipp Schlehuber-Caissier 2022-11-27 01:16:46 +01:00 • committed by Alexandre Duret-Lutz
parent 86c433cf80
commit 37d4e513d9
4 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
tests/python/game.py
View file

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