From 99a622059c31d16fb294657b02186406523570f4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 12 Sep 2024 14:00:08 +0200
Subject: [PATCH] synthesis: fix handling of deadstates

* spot/twaalgos/synthesis.cc: Remove a debuging print
from the semisym code, and add an additional case
in the fullysym code.
* tests/core/ltlsynt.test: Add a some test case,
and remove some bashism.
---
 spot/twaalgos/synthesis.cc | 14 +++++---------
 tests/core/ltlsynt.test    | 10 +++++-----
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index 5231f98ad..c064ccc93 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -1386,6 +1386,8 @@ namespace spot
           {
             assert(std::holds_alternative<bdd>(ccondin));
             const bdd& ccond = std::get<bdd>(ccondin);
+            if (ccond == bddfalse)
+              return;
             int clvl = ccond == bddtrue ? inIdx : bdd_var(ccond);
             if (clvl >= inIdx)
               {
@@ -1468,17 +1470,11 @@ namespace spot
             for (const auto &e: aut->out(s))
               enc_out_s |= encode_edge(e);  // Switch to new ins and outs
 
-            // Can only be false if there is no outgoing edge
-            // In this case: Nothing to do
-            assert(enc_out_s != bddfalse
-                   || (!(aut->out(s).begin())));
-
             if (enc_out_s == bddfalse)
             {
-              std::cerr << "Dead end state: " << s << '\n';
-#ifndef NDEBUG
-              print_hoa(std::cerr, aut);
-#endif
+              // Can only be false if there is no outgoing edge
+              // In this case: Nothing to do
+              assert(!(aut->out(s).begin()));
               continue;
             }
 
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index f0cb242d2..d89ecd292 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -494,12 +494,12 @@ diff out exp
 
 for splitt in expl semisym fullysym auto
 do
-  res=$(ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" \
+  # REALIZABLE
+  ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" \
           --outs="o0,o1" --aiger=isop+ud --algo=lar --decompose=no \
-          --simpl=no --splittype="$splitt" --realizability)
-  if [[ "$res" != "REALIZABLE" ]]; then
-    echo "Expected realizable"
-  fi
+          --simpl=no --splittype="$splitt" --realizability || exit 2
+  # UNREALIZABLE
+  ltlsynt -f "Gi & Fo" --splittype="$splitt" --realizability && exit 2
 done