game: add solve_reachability_game

* spot/misc/game.cc, spot/misc/game.hh: Add solve_reachability_game.

spot/misc/game.cc

@@ -935,13 +935,13 @@ namespace spot
 
   const std::vector<bool>& get_state_players(const_twa_graph_ptr arena)
   {
-    std::vector<bool> *onwers = arena->get_named_prop<std::vector<bool>>
+    std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
       ("state-player");
-    if (!onwers)
+    if (!owners)
       throw std::runtime_error
         ("get_state_players(): state-player property not defined, not a game");
 
-    return *onwers;
+    return *owners;
   }
 
   unsigned get_state_player(const_twa_graph_ptr arena, unsigned state)
@@ -949,12 +949,63 @@ namespace spot
     if (state >= arena->num_states())
       throw std::runtime_error("get_state_player(): invalid state number");
 
-    std::vector<bool>* onwers = arena->get_named_prop<std::vector<bool>>
+    std::vector<bool>* owners = arena->get_named_prop<std::vector<bool>>
       ("state-player");
-    if (!onwers)
+    if (!owners)
       throw std::runtime_error
         ("get_state_player(): state-player property not defined, not a game");
 
-    return (*onwers)[state] ? 1 : 0;
+    return (*owners)[state] ? 1 : 0;
+  }
+
+  bool solve_reachability_game(twa_graph_ptr game)
+  {
+    auto owners = get_state_players(game);
+
+    auto winners = new region_t(game->num_states(), true);
+    game->set_named_prop("state-winner", winners);
+    auto strategy = new strategy_t(game->num_states(), 0);
+    game->set_named_prop("strategy", strategy);
+
+    std::vector<bool> seen(game->num_states(), false);
+    std::vector<unsigned> todo;
+    todo.reserve(game->num_states());
+
+    auto& g = game->get_graph();
+    todo.push_back(game->get_init_state_number());
+
+    while (!todo.empty())
+    {
+      unsigned cur = todo.back();
+      auto edges = game->out(cur);
+
+      if (!seen[cur])
+      {
+        for (const auto& e : edges)
+          todo.push_back(e.dst);
+        seen[cur] = true;
+      }
+      else
+      {
+        todo.pop_back();
+        bool player = owners[cur];
+
+        auto it = std::find_if(edges.begin(), edges.end(),
+          [&winners, player](auto& e)
+          {
+            return (*winners)[e.dst] == player;
+          });
+
+        if (it != edges.end())
+        {
+          (*strategy)[cur] = g.index_of_edge(*it);
+          (*winners)[cur] = player;
+        }
+        else
+          (*winners)[cur] = !player;
+       }
+    }
+
+    return (*winners)[game->get_init_state_number()];
   }
 }

spot/misc/game.hh

@@ -100,4 +100,8 @@ namespace spot
   /// \brief Get the owner of a state.
   SPOT_API
   unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
+
+  /// \brief Solve a reachability game.
+  SPOT_API
+  bool solve_reachability_game(twa_graph_ptr game);
 }