From 7bc2c310432f2143f229681967c47ddadf3e1b54 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 7 Oct 2021 09:25:01 +0200
Subject: [PATCH] game: teach solve_game to use solve_safety_game

* spot/twaalgos/game.cc, spot/twaalgos/game.hh: Here.
* doc/org/tut40.org: Adjust example.
---
 doc/org/tut40.org     | 18 +++++++++++-------
 spot/twaalgos/game.cc |  7 +++++--
 spot/twaalgos/game.hh | 14 +++++++++++---
 3 files changed, 27 insertions(+), 12 deletions(-)

diff --git a/doc/org/tut40.org b/doc/org/tut40.org
index cc94a6ce9..f3b938d62 100644
--- a/doc/org/tut40.org
+++ b/doc/org/tut40.org
@@ -119,7 +119,7 @@ strategies.
 #+NAME: game40solved
 #+BEGIN_SRC python :exports none :noweb yes
 <<game40>>
-spot.solve_safety_game(g)
+spot.solve_game(g)
 spot.highlight_strategy(g)
 print(g.to_str('dot', '.g'))
 #+END_SRC
@@ -219,10 +219,13 @@ created using the usual interface:
 #+END_SRC
 
 To solve a safety game =g= that has been created by the above method,
-it is enough to just call =solve_safety_game(g)=.  This function
-returns the player winning in the initial state.  However, as a
-side-effect it defines additional automaton properties that indicate
-the winner of each state, and the associated strategy.
+it is enough to just call =solve_safety_game(g)=.  The function
+=solve_game(g)= used below is a more generic interface that looks at
+the acceptance condition of the game to dispatch to the more specific
+game solver.  These functions returns the player winning in the
+initial state.  However, as a side-effect they define additional
+automaton properties that indicate the winner of each state, and the
+associated strategy.
 
 Therefore to list all simulation pairs we learned from a game starting
 in state $(i,j)$, we could proceed as follow:
@@ -231,7 +234,7 @@ in state $(i,j)$, we could proceed as follow:
 #+BEGIN_SRC python :exports code
 def list_simulations(aut, i, j):
     g = direct_sim_game(aut, i, j)
-    spot.solve_safety_game(g)
+    spot.solve_game(g)
 
     winners = g.get_state_winners()
     owners = g.get_state_players()
@@ -254,6 +257,7 @@ On our running example, that gives:
 #+END_SRC
 
 #+RESULTS:
+: [(4, 0), (5, 1)]
 
 * C++
 
@@ -330,7 +334,7 @@ product of automata.
                   unsigned i, unsigned j)
   {
     auto g = direct_sim_game(aut, i, j);
-    spot::solve_safety_game(g);
+    spot::solve_game(g);
 
     const std::vector<bool>& winners = spot::get_state_winners(g);
     const std::vector<bool>& owners = spot::get_state_players(g);
diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc
index cfb839bcb..3a9a00088 100644
--- a/spot/twaalgos/game.cc
+++ b/spot/twaalgos/game.cc
@@ -774,9 +774,12 @@ namespace spot
     return pg.solve(arena);
   }
 
-  bool solve_game(twa_graph_ptr arena)
+  bool solve_game(const twa_graph_ptr& arena)
   {
     bool dummy1, dummy2;
+    auto& acc = arena->acc();
+    if (acc.is_t())
+      return solve_safety_game(arena);
     if (!arena->acc().is_parity(dummy1, dummy2, true))
       throw std::runtime_error
         ("solve_game(): unsupported acceptance condition.");
@@ -1090,7 +1093,7 @@ namespace spot
   }
 
 
-  bool solve_safety_game(twa_graph_ptr game)
+  bool solve_safety_game(const twa_graph_ptr& game)
   {
     if (!game->acc().is_t())
       throw std::runtime_error
diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh
index e65b48f18..64f8d52c8 100644
--- a/spot/twaalgos/game.hh
+++ b/spot/twaalgos/game.hh
@@ -93,14 +93,22 @@ namespace spot
   /// Returns the player winning in the initial state, and sets
   /// the state-winner and strategy named properties.
   SPOT_API
-  bool solve_safety_game(twa_graph_ptr game);
+  bool solve_safety_game(const twa_graph_ptr& game);
 
   /// \ingroup games
   /// \brief Generic interface for game solving
   ///
-  /// See solve_game(arena, gi)
+  /// Dispatch to solve_safety_game() if the acceptance condition is
+  /// t, or to solve_parity_game() if it is a parity acceptance.  Note that
+  /// parity acceptance include Büchi, co-Büchi, Rabin 1, and Streett 1.
+  ///
+  /// Currently unable to solve game with other acceptance conditions
+  /// that are not parity.
+  ///
+  /// Return the winning player for the initial state, and sets
+  /// the state-winner and strategy named properties.
   SPOT_API bool
-  solve_game(twa_graph_ptr arena);
+  solve_game(const twa_graph_ptr& arena);
 
 
   /// \ingroup games