From 568a6180f137973e6001f88046b5a05b924748df Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 9 Apr 2018 10:22:49 +0200
Subject: [PATCH] is_unambiguous: fix false negatives
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by Simon Jantsch and David Müller.

* tests/core/unambig.test: Test the issue.
* spot/twaalgos/isunamb.cc: Fix it.
* NEWS: Mention it.
* THANKS: Add Simon.
---
 NEWS                     |  3 +++
 THANKS                   |  1 +
 spot/twaalgos/isunamb.cc |  2 +-
 tests/core/unambig.test  | 52 +++++++++++++++++++++++++++++++++++++++-
 4 files changed, 56 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 51ae727b3..d2a68e19f 100644
--- a/NEWS
+++ b/NEWS
@@ -74,6 +74,9 @@ New in spot 2.5.2.dev (not yet released)
   - Using spot.automata("cmd...|") to read just a few automata out of
     an infinite stream would not properly terminate the command.
 
+  - The is_unambiguous() check (rewritten in Spot 2.2) could mark some
+    unambiguous automata as ambiguous.
+
 New in spot 2.5.2 (2018-03-25)
 
   Bugs fixed:
diff --git a/THANKS b/THANKS
index 5c6151aee..83b50cf4d 100644
--- a/THANKS
+++ b/THANKS
@@ -34,6 +34,7 @@ Nikos Gorogiannis
 Reuben Rowe
 Rüdiger Ehlers
 Silien Hong
+Simon Jantsch
 Shufang Zhu
 Sonali Dutta
 Tobias Meggendorfer.
diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc
index 3adb787bd..11d5cb519 100644
--- a/spot/twaalgos/isunamb.cc
+++ b/spot/twaalgos/isunamb.cc
@@ -97,7 +97,7 @@ namespace spot
         unsigned one_state = sccmap_prod.states_of(n).front();
         bool accepting =
           v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second];
-        if (accepting)
+        if (accepting && !sccmap_prod.is_trivial(n))
           {
             useful[n] = true;
             continue;
diff --git a/tests/core/unambig.test b/tests/core/unambig.test
index a0ffa7954..c29b83e24 100755
--- a/tests/core/unambig.test
+++ b/tests/core/unambig.test
@@ -284,4 +284,54 @@ EOF
 
 run 1 autfilt -q --is-unambiguous smaller.hoa
 
-true
+# These automata come from Simon Jantsch and David Müller.
+cat >sjdb.hoa <<EOF
+HOA: v1
+name: "G(!a | !b) & (Ga | G(b | XGb))"
+States: 4
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc inherently-weak
+--BODY--
+State: 0
+[!0&1] 1
+[0&!1] 2
+[!1] 3
+State: 1
+[!0&1] 1
+[!1] 3
+State: 2
+[0&!1] 2
+State: 3
+[!0&1] 3
+--END--
+HOA: v1
+name: "F(!a & XGa) | (F(!b & XGb) & G(!a | !b))"
+States: 5
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc inherently-weak
+--BODY--
+State: 0
+[!0] 1
+[t] 2
+[!0 | !1] 3
+[!1] 4
+State: 1 {0}
+[0] 1
+State: 2
+[!0] 1
+[t] 2
+State: 3
+[!0 | !1] 3
+[!1] 4
+State: 4 {0}
+[!0&1] 4
+--END--
+EOF
+
+test 2 = `autfilt -c --is-unambiguous sjdb.hoa`