From 18e65f3bc8f7760422e68d80b420e14f1833a1c2 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 22 Dec 2017 18:27:07 +0100
Subject: [PATCH] sbacc: fix sbacc producing complete automata marked as
 incomplete
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #312, reported by František Blahoudek.

* spot/twaalgos/sbacc.cc: Detect the case were this can happen,
and fix it.
* tests/core/sbacc.test: New test case.
* NEWS: Mention the bug.
---
 NEWS                   |  4 ++++
 spot/twaalgos/sbacc.cc | 11 +++++++++++
 tests/core/sbacc.test  | 14 ++++++++++++++
 3 files changed, 29 insertions(+)

diff --git a/NEWS b/NEWS
index be9acef7a..22d53f139 100644
--- a/NEWS
+++ b/NEWS
@@ -6,6 +6,10 @@ New in spot 2.4.3.dev (not yet released)
     Fin-less & CNF version of the acceptance condition had several
     unit clauses.
 
+  - If the automaton passed to sbacc() was incomplete because of some
+    unreachable states, then it was possible that the output would
+    marked incomplete while it was in fact complete.
+
 New in spot 2.4.3 (2017-12-19)
 
   Bugs fixed:
diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc
index 59701abdb..70862e432 100644
--- a/spot/twaalgos/sbacc.cc
+++ b/spot/twaalgos/sbacc.cc
@@ -168,6 +168,17 @@ namespace spot
           }
       }
     res->merge_edges();
+
+    // If the automaton was marked as not complete, and we have
+    // ignored some unreachable state, then it is possible that the
+    // result becomes complete.
+    if (res->prop_complete().is_false())
+      for (unsigned i = 0; i < ns; ++i)
+        if (!si.reachable_state(i))
+          {
+            res->prop_complete(trival::maybe());
+            break;
+          }
     return res;
   }
 }
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index 65482b54f..049473c26 100755
--- a/tests/core/sbacc.test
+++ b/tests/core/sbacc.test
@@ -265,3 +265,17 @@ EOF
 
 autfilt --sbacc alt.hoa > out.hoa
 diff out.hoa expect.hoa
+
+# Issue #312
+autfilt -S <<EOF | autfilt --is-complete
+HOA: v1
+States: 2
+Start: 0
+AP: 0
+Acceptance: 1 Inf(0)
+properties: !complete
+--BODY--
+State: 0 [t] 0 {0}
+State: 1
+--END--
+EOF