parity game: compute winning strategy

* spot/misc/game.cc, spot/misc/game.hh: Here.
* bin/ltlsynt.cc: Realizability is now done by checking if the winning
strategy contains the initial state.

bin/ltlsynt.cc

@@ -213,7 +213,7 @@ namespace
         {
           case REC:
             {
-              if (pg.winner())
+              if (std::get<0>(pg.solve()).count(pg.get_init_state_number()))
                 std::cout << "REALIZABLE\n";
               else
                 std::cout << "UNREALIZABLE\n";

spot/misc/game.cc

@@ -54,14 +54,14 @@ void parity_game::print(std::ostream& os)
     }
 }
 
-bool parity_game::winner() const
+std::pair<parity_game::region_t, parity_game::strategy_t>
+parity_game::solve() const
 {
-  std::unordered_set<unsigned> states_;
+  region_t states_;
   for (unsigned i = 0; i < num_states(); ++i)
     states_.insert(i);
   unsigned m = max_parity();
-  auto w1 = winning_region(states_, m);
+  return solve_rec(states_, m);
-  return w1.find(get_init_state_number()) != w1.end();
 }
 
 bool parity_game::solve_qp() const
@@ -69,94 +69,111 @@ bool parity_game::solve_qp() const
   return reachability_game(*this).is_reachable();
 }
 
-void parity_game::attractor(const std::unordered_set<unsigned>& subgame,
+parity_game::strategy_t
-                            std::unordered_set<unsigned>& set,
+parity_game::attractor(const region_t& subgame, region_t& set,
-                            unsigned max_parity, bool odd,
+                       unsigned max_parity, bool odd, bool attr_max) const
-                            bool attr_max) const
 {
+  strategy_t strategy;
   unsigned size;
+  std::unordered_set<unsigned> complement = subgame;
+  std::unordered_set<unsigned> delta = set;
   do
     {
       size = set.size();
-      for (unsigned s: subgame)
+      for (unsigned s: delta)
+        complement.erase(s);
+      for (unsigned s: complement)
         {
           bool any = false;
           bool all = true;
+          unsigned i = 0;
           for (auto& e: out(s))
             {
-              if (e.acc.max_set() - 1 <= max_parity
+              if (e.acc.max_set() - 1 <= max_parity && subgame.count(e.dst))
-                  && subgame.find(e.dst) != subgame.end())
                 {
-                  if (set.find(e.dst) != set.end()
+                  if (set.count(e.dst)
                       || (attr_max && e.acc.max_set() - 1 == max_parity))
+                    {
+                      if (!any && owner_[s] && odd)
+                        strategy[s] = i;
                       any = true;
+                    }
                   else
                     all = false;
                 }
+              ++i;
             }
           if ((owner_[s] == odd && any) || (owner_[s] != odd && all))
+            {
               set.insert(s);
+              delta.insert(s);
+            }
         }
     } while (set.size() != size);
+  return strategy;
 }
 
-std::unordered_set<unsigned>
+auto parity_game::solve_rec(region_t& subgame, unsigned max_parity) const
-parity_game::winning_region(std::unordered_set<unsigned>& subgame,
+  -> std::pair<region_t, strategy_t>
-                            unsigned max_parity) const
 {
   // The algorithm works recursively on subgames. To avoid useless copies of
   // the game at each call, subgame and max_parity are used to filter states
   // and transitions.
   if (max_parity == 0 || subgame.empty())
-    return std::unordered_set<unsigned>();
+    return {};
   bool odd = max_parity % 2 == 1;
-  std::unordered_set<unsigned> w1;
+  region_t w1;
-  std::unordered_set<unsigned> removed;
+  strategy_t strategy;
 
-  while (!subgame.empty())
-    {
   // Recursion on max_parity.
-      std::unordered_set<unsigned> u;
+  region_t u;
-      attractor(subgame, u, max_parity, odd, true);
+  auto strat_u = attractor(subgame, u, max_parity, odd, true);
 
   for (unsigned s: u)
     subgame.erase(s);
-      auto w1_ = winning_region(subgame, max_parity - 1);
+  region_t w00; // Even's winning region in the first recursive call.
-      std::unordered_set<unsigned> w0_;
+  region_t w10; // Odd's winning region in the first recursive call.
-      if (odd && w1_.size() != subgame.size())
+  strategy_t s10; // Odd's winning strategy in the first recursive call.
-        std::set_difference(subgame.begin(), subgame.end(),
+  std::tie(w10, s10) = solve_rec(subgame, max_parity - 1);
-                            w1_.begin(), w1_.end(),
+  if (odd && w10.size() != subgame.size())
-                            std::inserter(w0_, w0_.begin()));
-      // if !odd, w0_ is not used.
-      for (unsigned s: u)
-        subgame.insert(s);
-
-      if (odd && w1_.size() + u.size() == subgame.size())
-        {
     for (unsigned s: subgame)
-            w1.insert(s);
+      if (w10.find(s) == w10.end())
-          break;
+        w00.insert(s);
-        }
+  // If !odd, w00 is not used, no need to compute it.
-      else if (!odd && w1_.empty())
+  subgame.insert(u.begin(), u.end());
-        break;
 
-      // Unrolled tail-recursion on game size.
+  if (odd && w10.size() + u.size() == subgame.size())
-      auto& wni = odd ? w0_ : w1_;
-      attractor(subgame, wni, max_parity, !odd);
-
-      for (unsigned s: wni)
     {
-        subgame.erase(s);
+      strategy.insert(s10.begin(), s10.end());
-        removed.insert(s);
+      strategy.insert(strat_u.begin(), strat_u.end());
+      w1.insert(subgame.begin(), subgame.end());
+      return {w1, strategy};
     }
+  else if (!odd && w10.empty())
+    return {};
 
+  // Recursion on game size.
+  auto& wni = odd ? w00 : w10;
+  auto strat_wni = attractor(subgame, wni, max_parity, !odd);
   if (!odd)
+    strat_wni.insert(s10.begin(), s10.end());
+
   for (unsigned s: wni)
-          w1.insert(s);
+    subgame.erase(s);
+
+  region_t w11; // Odd's winning region in the second recursive call.
+  strategy_t s11; // Odd's winning strategy in the second recursive call.
+  std::tie(w11, s11) = solve_rec(subgame, max_parity);
+
+  w1.insert(w11.begin(), w11.end());
+  strategy.insert(s11.begin(), s11.end());
+  if (!odd)
+    {
+      strategy.insert(strat_wni.begin(), strat_wni.end());
+      w1.insert(wni.begin(), wni.end());
     }
-  for (unsigned s: removed)
+  subgame.insert(wni.begin(), wni.end());
-    subgame.insert(s);
+  return {w1, strategy};
-  return w1;
 }
 
 int reachability_state::compare(const state* other) const

spot/misc/game.hh

@@ -22,6 +22,7 @@
 #include <algorithm>
 #include <memory>
 #include <ostream>
+#include <unordered_map>
 #include <vector>
 
 #include <bddx.h>
@@ -94,8 +95,12 @@ public:
   /// Print the parity game in PGSolver's format.
   void print(std::ostream& os);
 
-  // Compute the winner of this game using Zielonka's recursive algorithm.
+  typedef std::unordered_set<unsigned> region_t;
-  // False is Even and True is Odd.
+  // Map state number to index of the transition to take.
+  typedef std::unordered_map<unsigned, unsigned> strategy_t;
+
+  /// Compute the winning strategy and winning region of this game for player
+  /// 1 using Zielonka's recursive algorithm.
   /** \verbatim
       @article{ zielonka.98.tcs
         title = "Infinite games on finitely coloured graphs with applications to
@@ -108,7 +113,7 @@ public:
         author = "Wieslaw Zielonka",
       }
       \endverbatim */
-  bool winner() const;
+  std::pair<region_t, strategy_t> solve() const;
 
   /// Whether player 1 has a winning strategy from the initial state.
   /// Implements Calude et al.'s quasipolynomial time algorithm.
@@ -139,17 +144,16 @@ private:
   typedef twa_graph::graph_t::edge_storage_t edge_t;
 
   // Compute (in place) a set of states from which player can force a visit
-  // through set.
+  // through set, and a strategy to do it.
   // if attr_max is true, states that can force a visit through an edge with
   // max parity are also counted in.
-  void attractor(const std::unordered_set<unsigned>& subgame,
+  strategy_t attractor(const region_t& subgame, region_t& set,
-                 std::unordered_set<unsigned>& set, unsigned max_parity,
+                       unsigned max_parity, bool odd,
-                 bool player, bool attr_max = false) const;
+                       bool attr_max = false) const;
 
-  // Compute the winning region for player Odd.
+  // Compute the winning strategy and winning region for player 1.
-  std::unordered_set<unsigned>
+  std::pair<region_t, strategy_t>
-  winning_region(std::unordered_set<unsigned>& subgame,
+  solve_rec(region_t& subgame, unsigned max_parity) const;
-                 unsigned max_parity) const;
 };