From ec393708bb12a692de4037f5bfecf8a5803c0d83 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 24 Dec 2017 19:07:24 +0100
Subject: [PATCH] sbacc: more fixes related to #312

The issue also exists with determinism.

* tests/core/sbacc.test: New test case.
* spot/twaalgos/sbacc.cc: Fix it.
* NEWS: Update.
---
 NEWS                   |  7 ++++---
 spot/twaalgos/sbacc.cc | 13 ++++++++-----
 tests/core/sbacc.test  | 13 +++++++++++++
 3 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/NEWS b/NEWS
index 7ed8f04c5..56cb88a14 100644
--- a/NEWS
+++ b/NEWS
@@ -248,9 +248,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.
+  - If the automaton passed to sbacc() was incomplete or
+    non-deterministic because of some unreachable states, then it was
+    possible that the output would marked similarly while it was in
+    fact complete or deterministic.
 
 New in spot 2.4.3 (2017-12-19)
 
diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc
index a5fae38c4..3cff71f1a 100644
--- a/spot/twaalgos/sbacc.cc
+++ b/spot/twaalgos/sbacc.cc
@@ -169,14 +169,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())
+    // If the automaton was marked as not complete or not universal,
+    // and we have ignored some unreachable state, then it is possible
+    // that the result becomes complete or universal.
+    if (res->prop_complete().is_false() || res->prop_universal().is_false())
       for (unsigned i = 0; i < ns; ++i)
         if (!si.reachable_state(i))
           {
-            res->prop_complete(trival::maybe());
+            if (res->prop_complete().is_false())
+              res->prop_complete(trival::maybe());
+            if (res->prop_universal().is_false())
+              res->prop_universal(trival::maybe());
             break;
           }
     return res;
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index a3a96ba8f..229e4a1ee 100755
--- a/tests/core/sbacc.test
+++ b/tests/core/sbacc.test
@@ -276,3 +276,16 @@ State: 0 [t] 0 {0}
 State: 1
 --END--
 EOF
+
+autfilt -S <<EOF | autfilt --is-deterministic
+HOA: v1
+States: 2
+Start: 0
+AP: 1 "a"
+Acceptance: 1 Inf(0)
+properties: !complete !deterministic
+--BODY--
+State: 0 [0] 0 {0}
+State: 1 [0] 1 [0] 0
+--END--
+EOF
-- 
GitLab