From 0e29d30d1b24197b3e73e9f79aa4045d59c5be95 Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Tue, 13 Mar 2018 11:58:48 +0100
Subject: [PATCH] ltlsynt: fix the construction of the arena

* bin/ltlsynt.cc: implement it
* tests/core/ltlsynt.test: update tests
---
 bin/ltlsynt.cc          | 44 +++++++++++++++++++++++++++--------------
 tests/core/ltlsynt.test | 23 +++++++++++----------
 2 files changed, 40 insertions(+), 27 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index f257c1a4c..ee72ab1a5 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -185,32 +185,47 @@ namespace
     return split;
   }
 
-  // Generates a vector indicating the owner of each state, with the
-  // convention that false is player 0 (the environment) and true is player 1
-  // (the controller).  Starting with player 0 on the initial state, the owner
-  // is switched after each transition.
+  // Ensures that the game is complete for player 0.
+  // Also computes the owner of each state (false for player 0, i.e. env).
+  // Initial state belongs to Player 0 and the game is turn-based.
   static std::vector<bool>
-  make_alternating_owner(const spot::twa_graph_ptr& dpa,
-                         bool init_owner = false)
+  complete_env(spot::twa_graph_ptr& arena)
   {
-    std::vector<bool> seen(dpa->num_states(), false);
-    std::vector<unsigned> todo({dpa->get_init_state_number()});
-    std::vector<bool> owner(dpa->num_states());
-    owner[dpa->get_init_state_number()] = init_owner;
+    unsigned sink_env = arena->new_state();
+    unsigned sink_con = arena->new_state();
+
+    auto um = arena->acc().unsat_mark();
+    if (!um.first)
+      throw std::runtime_error("game winning condition is a tautology");
+    arena->new_edge(sink_con, sink_env, bddtrue, um.second);
+    arena->new_edge(sink_env, sink_con, bddtrue, um.second);
+
+    std::vector<bool> seen(arena->num_states(), false);
+    std::vector<unsigned> todo({arena->get_init_state_number()});
+    std::vector<bool> owner(arena->num_states(), false);
+    owner[arena->get_init_state_number()] = false;
+    owner[sink_env] = true;
     while (!todo.empty())
       {
         unsigned src = todo.back();
         todo.pop_back();
         seen[src] = true;
-        for (auto& e: dpa->out(src))
+        bdd missing = bddtrue;
+        for (const auto& e: arena->out(src))
           {
+            if (!owner[src])
+              missing -= e.cond;
+
             if (!seen[e.dst])
               {
                 owner[e.dst] = !owner[src];
                 todo.push_back(e.dst);
               }
           }
+        if (!owner[src] && missing != bddfalse)
+          arena->new_edge(src, sink_con, missing, um.second);
       }
+
     return owner;
   }
 
@@ -219,12 +234,11 @@ namespace
   {
     auto dpa = spot::tgba_determinize(split);
     dpa->merge_edges();
-    spot::complete_here(dpa);
+    if (opt_print_pg)
+      dpa = spot::sbacc(dpa);
     spot::colorize_parity_here(dpa, true);
     spot::change_parity_here(dpa, spot::parity_kind_max,
                              spot::parity_style_odd);
-    if (opt_print_pg)
-      dpa = spot::sbacc(dpa);
     bool max, odd;
     dpa->acc().is_parity(max, odd);
     assert(max && odd);
@@ -330,7 +344,7 @@ namespace
       auto dpa = to_dpa(split);
       if (verbose)
         std::cerr << "determinization done" << std::endl;
-      auto owner = make_alternating_owner(dpa);
+      auto owner = complete_env(dpa);
       auto pg = spot::parity_game(dpa, owner);
       if (verbose)
         std::cerr << "parity game built" << std::endl;
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index b2b509c88..ab76a5527 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -23,24 +23,23 @@
 set -e
 
 cat >exp <<EOF
-parity 15;
-0 4294967295 0 1,2 "INIT";
-2 4 1 3;
+parity 16;
+0 0 0 1,2 "INIT";
+2 0 1 3;
 3 2 0 4,5;
-5 4294967295 1 3,6;
+5 0 1 3,6;
 6 3 0 4,5;
-4 4294967295 1 7,8;
+4 0 1 7,8;
 8 2 0 9,10;
 10 3 1 3,11;
 11 0 0 4,5;
 9 0 1 8,12;
-12 1 0 10,13;
-13 4294967295 1 8,12;
-7 1 0 4,14;
-14 2 1 3,6;
-4 4294967295 1 7,8;
-1 3 1 3,15;
-15 3 0 1,2;
+12 1 0 9,10;
+7 1 0 4,13;
+13 2 1 3,6;
+4 0 1 7,8;
+1 3 1 3,14;
+14 3 0 1,2;
 EOF
 ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --print-pg > out
 diff out exp