is_unambiguous: fix false negatives

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

@@ -14,6 +14,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:

THANKS

@@ -34,6 +34,7 @@ Nikos Gorogiannis
 Reuben Rowe
 Rüdiger Ehlers
 Silien Hong
+Simon Jantsch
 Shufang Zhu
 Sonali Dutta
 Tobias Meggendorfer.

spot/twaalgos/isunamb.cc

@@ -96,7 +96,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;

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`