parity game: add Zielonka's recursive algorithm

* spot/misc/game.cc, spot/misc/game.hh: Implement it.
* bin/ltlsynt.cc: Use it.
* doc/org/ltlsynt.org: Document it.

bin/ltlsynt.cc

@@ -39,12 +39,24 @@
 
 enum
 {
-  OPT_INPUT = 256,
+  OPT_ALGO = 256,
+  OPT_INPUT,
+  OPT_OUTPUT,
   OPT_PRINT
 };
 
+enum solver
+{
+  QP,
+  REC
+};
+
 static const argp_option options[] =
   {
+    { "algo", OPT_ALGO, "ALGO", 0,
+      "choose the parity game algorithm, valid ones are rec (Zielonka's"
+      " recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
+      " time algorithm)", 0 },
     { "input", OPT_INPUT, "PROPS", 0,
       "comma-separated list of atomic propositions", 0},
     { "print-pg", OPT_PRINT, nullptr, 0,
@@ -65,7 +77,9 @@ const char argp_program_doc[] =
 
 std::vector<std::string> input_aps;
 
-bool opt_print_pg{false};
+bool opt_print_pg(false);
+bool opt_real(false);
+solver opt_solver(REC);
 
 namespace
 {
@@ -195,11 +209,26 @@ namespace
           pg.print(std::cout);
           return 0;
         }
-      if (pg.solve_qp())
+      switch (opt_solver)
-        std::cout << "realizable\n";
+        {
-      else
+          case REC:
-        std::cout << "unrealizable\n";
+            {
-      return 0;
+              if (pg.winner())
+                std::cout << "REALIZABLE\n";
+              else
+                std::cout << "UNREALIZABLE\n";
+              return 0;
+            }
+          case QP:
+            if (pg.solve_qp())
+              std::cout << "REALIZABLE\n";
+            else
+              std::cout << "UNREALIZABLE\n";
+            return 0;
+          default:
+            SPOT_UNREACHABLE();
+            return 0;
+        }
     }
   };
 }
@@ -223,6 +252,17 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_PRINT:
       opt_print_pg = true;
       break;
+    case OPT_ALGO:
+      if (arg && strcmp(arg, "rec") == 0)
+        opt_solver = REC;
+      else if (arg && strcmp(arg, "qp") == 0)
+        opt_solver = QP;
+      else
+        {
+          std::cout << "Unknown solver: " << (arg ? arg : "") << '\n';
+          return 1;
+        }
+      break;
     }
   return 0;
 }
@@ -234,6 +274,8 @@ int main(int argc, char **argv)
                     argp_program_doc, children, nullptr, nullptr };
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
     exit(err);
+  check_no_formula();
+
   spot::translator trans;
   ltl_processor processor(trans, input_aps);
   processor.run();

doc/org/ltlsynt.org

@@ -50,6 +50,10 @@ The tool reduces the synthesis problem to a parity game, and solves the parity
 game using Zielonka's recursive algorithm.  The full reduction from LTL to
 parity game is described in a paper yet to be written and published.
 
-You can ask =ltlsynt= not to solve the game and print it instead (in the
+You can control the parity game solving step in two ways:
+- By choosing a different algorithm using the =--algo= option. The default is
+=rec= for Zielonka's recursive algorithm, and as of now the only other
+available option is =qp= for Calude et al.'s quasi-polynomial time algorithm.
+- By asking =ltlsynt= not to solve the game and print it instead (in the
 PGSolver format) using the =--print-pg= option, and leaving you the choice of
 an external solver such as PGSolver.

spot/misc/game.cc

@@ -54,11 +54,111 @@ void parity_game::print(std::ostream& os)
     }
 }
 
+bool parity_game::winner() const
+{
+  std::unordered_set<unsigned> states_;
+  for (unsigned i = 0; i < num_states(); ++i)
+    states_.insert(i);
+  unsigned m = max_parity();
+  auto w1 = winning_region(states_, m);
+  return w1.find(get_init_state_number()) != w1.end();
+}
+
 bool parity_game::solve_qp() const
 {
   return reachability_game(*this).is_reachable();
 }
 
+void parity_game::attractor(const std::unordered_set<unsigned>& subgame,
+                            std::unordered_set<unsigned>& set,
+                            unsigned max_parity, bool odd,
+                            bool attr_max) const
+{
+  unsigned size;
+  do
+    {
+      size = set.size();
+      for (unsigned s: subgame)
+        {
+          bool any = false;
+          bool all = true;
+          for (auto& e: out(s))
+            {
+              if (e.acc.max_set() - 1 <= max_parity
+                  && subgame.find(e.dst) != subgame.end())
+                {
+                  if (set.find(e.dst) != set.end()
+                      || (attr_max && e.acc.max_set() - 1 == max_parity))
+                    any = true;
+                  else
+                    all = false;
+                }
+            }
+          if ((owner_[s] == odd && any) || (owner_[s] != odd && all))
+            set.insert(s);
+        }
+    } while (set.size() != size);
+}
+
+std::unordered_set<unsigned>
+parity_game::winning_region(std::unordered_set<unsigned>& subgame,
+                            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>();
+  bool odd = max_parity % 2 == 1;
+  std::unordered_set<unsigned> w1;
+  std::unordered_set<unsigned> removed;
+
+  while (!subgame.empty())
+    {
+      // Recursion on max_parity.
+      std::unordered_set<unsigned> u;
+      attractor(subgame, u, max_parity, odd, true);
+
+      for (unsigned s: u)
+        subgame.erase(s);
+      auto w1_ = winning_region(subgame, max_parity - 1);
+      std::unordered_set<unsigned> w0_;
+      if (odd && w1_.size() != subgame.size())
+        std::set_difference(subgame.begin(), subgame.end(),
+                            w1_.begin(), w1_.end(),
+                            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);
+          break;
+        }
+      else if (!odd && w1_.empty())
+        break;
+
+      // Unrolled tail-recursion on game size.
+      auto& wni = odd ? w0_ : w1_;
+      attractor(subgame, wni, max_parity, !odd);
+
+      for (unsigned s: wni)
+      {
+        subgame.erase(s);
+        removed.insert(s);
+      }
+
+      if (!odd)
+        for (unsigned s: wni)
+          w1.insert(s);
+    }
+  for (unsigned s: removed)
+    subgame.insert(s);
+  return w1;
+}
+
 int reachability_state::compare(const state* other) const
 {
   auto o = down_cast<const reachability_state*>(other);

spot/misc/game.hh

@@ -82,33 +82,74 @@ public:
     return owner_[src];
   }
 
+  unsigned max_parity() const
+  {
+    unsigned max_parity = 0;
+      for (auto& e: dpa_->edges())
+        max_parity = std::max(max_parity, e.acc.max_set());
+    SPOT_ASSERT(max_parity);
+    return max_parity - 1;
+  }
+
   /// Print the parity game in PGSolver's format.
   void print(std::ostream& os);
 
+  // Compute the winner of this game using Zielonka's recursive algorithm.
+  // False is Even and True is Odd.
+  /** \verbatim
+      @article{ zielonka.98.tcs
+        title = "Infinite games on finitely coloured graphs with applications to
+        automata on infinite trees",
+        journal = "Theoretical Computer Science",
+        volume = "200",
+        number = "1",
+        pages = "135 - 183",
+        year = "1998",
+        author = "Wieslaw Zielonka",
+      }
+      \endverbatim */
+  bool winner() const;
+
   /// Whether player 1 has a winning strategy from the initial state.
   /// Implements Calude et al.'s quasipolynomial time algorithm.
   /** \verbatim
       @inproceedings{calude.17.stoc,
-       author = {Calude, Cristian S. and Jain, Sanjay and Khoussainov,
+        author = {Calude, Cristian S. and Jain, Sanjay and Khoussainov,
-                 Bakhadyr and Li, Wei and Stephan, Frank},
+                  Bakhadyr and Li, Wei and Stephan, Frank},
-       title = {Deciding Parity Games in Quasipolynomial Time},
+        title = {Deciding Parity Games in Quasipolynomial Time},
-       booktitle = {Proceedings of the 49th Annual ACM SIGACT Symposium on
+        booktitle = {Proceedings of the 49th Annual ACM SIGACT Symposium on
-                    Theory of Computing},
+                     Theory of Computing},
-       series = {STOC 2017},
+        series = {STOC 2017},
-       year = {2017},
+        year = {2017},
-       isbn = {978-1-4503-4528-6},
+        isbn = {978-1-4503-4528-6},
-       location = {Montreal, Canada},
+        location = {Montreal, Canada},
-       pages = {252--263},
+        pages = {252--263},
-       numpages = {12},
+        numpages = {12},
-       url = {http://doi.acm.org/10.1145/3055399.3055409},
+        url = {http://doi.acm.org/10.1145/3055399.3055409},
-       doi = {10.1145/3055399.3055409},
+        doi = {10.1145/3055399.3055409},
-       acmid = {3055409},
+        acmid = {3055409},
-       publisher = {ACM},
+        publisher = {ACM},
-       address = {New York, NY, USA},
+        address = {New York, NY, USA},
-       keywords = {Muller Games, Parity Games, Quasipolynomial Time Algorithm},
+        keywords = {Muller Games, Parity Games, Quasipolynomial Time Algorithm},
       }
       \endverbatim */
   bool solve_qp() const;
+
+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.
+  // 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,
+                 std::unordered_set<unsigned>& set, unsigned max_parity,
+                 bool player, bool attr_max = false) const;
+
+  // Compute the winning region for player Odd.
+  std::unordered_set<unsigned>
+  winning_region(std::unordered_set<unsigned>& subgame,
+                 unsigned max_parity) const;
 };
 
 
@@ -246,8 +287,7 @@ private:
 public:
 
   reachability_game(const parity_game& pg)
-    : twa(std::make_shared<bdd_dict>()),
+    : twa(std::make_shared<bdd_dict>()), pg_(pg)
-      pg_(pg)
   {
     init_state_ = std::shared_ptr<const reachability_state>(get_init_state());
   }