From aca6bd90429b2c4d6828c61ba08ccd9d7e97f2b6 Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 31 May 2022 13:40:58 +0200
Subject: [PATCH] synthesis: Deletion of an incorrect case in the bypass

With a formula like G(b1) & (GFi <-> GF(b1)), a direct strategy was
created while it is unrealizable.

* spot/twaalgos/synthesis.cc: here.
* tests/core/ltlsynt.test: add tests
---
 spot/twaalgos/synthesis.cc | 55 ++++++++++++++++++++------------------
 tests/core/ltlsynt.test    | 41 ++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+), 26 deletions(-)

diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index b249acce9..5a5d1297a 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -1168,6 +1168,27 @@ namespace spot
   //Anonymous for try_create_strat
   namespace
   {
+    // Checks that 2 sets have a common element. Use it instead
+    // of set_intersection when we just want to check if they have a common
+    // element because it avoids going through the rest of the sets after an
+    // element is found.
+    static bool
+    are_intersecting(const std::set<formula> &v1,
+                    const std::set<formula> &v2)
+    {
+      auto v1_pos = v1.begin(), v2_pos = v2.begin(), v1_end = v1.end(),
+          v2_end = v2.end();
+      while (v1_pos != v1_end && v2_pos != v2_end)
+        {
+          if (*v1_pos < *v2_pos)
+            ++v1_pos;
+          else if (*v2_pos < *v1_pos)
+            ++v2_pos;
+          else
+            return true;
+        }
+      return false;
+    }
     class formula_2_inout_props
     {
     private:
@@ -1372,10 +1393,6 @@ namespace spot
       if (combin == -1U)
         return ret_sol_maybe();
 
-      // We know that a strategy exists and we don't want to construct it.
-      if (!want_strategy)
-        return ret_sol_exists(nullptr);
-
       formula f_left = f_other[(combin + 1) % 2];
       formula f_right = f_other[combin % 2];
       if (!(combin % 2))
@@ -1384,6 +1401,14 @@ namespace spot
         std::swap(left_outs, right_outs);
       }
 
+      auto [_, g_outs] = form2props.aps_of(f_g);
+      if (are_intersecting(g_outs, right_outs))
+        return ret_sol_maybe();
+
+      // We know that a strategy exists and we don't want to construct it.
+      if (!want_strategy)
+        return ret_sol_exists(nullptr);
+
       auto trans = create_translator(gi);
 
       trans.set_pref(postprocessor::Deterministic | postprocessor::Complete);
@@ -1484,28 +1509,6 @@ namespace spot
 namespace // anonymous for subsformula
 {
   using namespace spot;
-  // Checks that 2 sets have a common element. Use it instead
-  // of set_intersection when we just want to check if they have a common
-  // element because it avoids going through the rest of the sets after an
-  // element is found.
-  static bool
-  are_intersecting(const std::set<formula> &v1,
-                   const std::set<formula> &v2)
-  {
-    auto v1_pos = v1.begin(), v2_pos = v2.begin(), v1_end = v1.end(),
-         v2_end = v2.end();
-    while (v1_pos != v1_end && v2_pos != v2_end)
-      {
-        if (*v1_pos < *v2_pos)
-          ++v1_pos;
-        else if (*v2_pos < *v1_pos)
-          ++v2_pos;
-        else
-          return true;
-      }
-    return false;
-  }
-
   static std::pair<std::set<formula>, std::set<formula>>
   algo4(const std::vector<formula> &assumptions,
         const std::set<std::string> &outs,
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 1badb9b4b..9319d96a8 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -944,3 +944,44 @@ ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose --bypass=no\
                                    --algo=acd 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
 diff outx exp
+
+# Bypass: check that in G(b1) ∧ (Büchi ↔ GF(b2)), b1 and b2 don't share an AP.
+# We do it because  G(o1 ∨ o2) ∧ (GFi ↔ GFo1) is realizable while
+# G(o1) ∧ (GFi ↔ GFo1) is not realizable. So we cannot conclude if
+# they share an AP.
+cat >exp <<EOF
+there are 1 subformulas
+trying to create strategy directly for Go1 & (GFi <-> GFo1)
+direct strategy might exist but was not found.
+translating formula done in X seconds
+automaton has 1 states and 1 colors
+LAR construction done in X seconds
+DPA has 1 states, 1 colors
+split inputs and outputs done in X seconds
+automaton has 3 states
+solving game with acceptance: Streett 1
+game solved in X seconds
+EOF
+ltlsynt -f "G(o1) & (GFi <-> GFo1)" --outs="o1" --verbose\
+                                    --bypass=yes 2> out || true
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp
+
+cat >exp <<EOF
+there are 1 subformulas
+trying to create strategy directly for G(o1 | o2) & (GFi <-> GFo1)
+direct strategy might exist but was not found.
+translating formula done in X seconds
+automaton has 1 states and 2 colors
+LAR construction done in X seconds
+DPA has 2 states, 2 colors
+split inputs and outputs done in X seconds
+automaton has 6 states
+solving game with acceptance: parity max odd 4
+game solved in X seconds
+simplification took X seconds
+EOF
+ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\
+                                       --bypass=yes 2> out
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp
\ No newline at end of file