From cd8e53de09f5aaef6ff59cfbc26d72af4fc741b1 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 20 Oct 2015 08:06:31 +0200
Subject: [PATCH] is_unambiguous: fix detection of empty languages

* src/tests/unambig.test: New test case.  Reported by Ming-Hsien Tsai.
* src/twaalgos/sccfilter.cc: Always create an initial state.
* src/twaalgos/isunamb.cc: Speed up on empty languages.
* NEWS, THANKS: Update.
---
 NEWS                      |  2 ++
 THANKS                    |  1 +
 src/tests/unambig.test    | 20 +++++++++++++++++++-
 src/twaalgos/isunamb.cc   |  2 ++
 src/twaalgos/sccfilter.cc |  9 +++++----
 5 files changed, 29 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 92a77acb6..b9d0f1b46 100644
--- a/NEWS
+++ b/NEWS
@@ -65,6 +65,8 @@ New in spot 1.99.4a (not yet released)
   * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns.
   * "ltlgrind --help" did not document FORMAT.
   * unabbreviate could easily use forbidden operators.
+  * "autfilt --is-unambiguous" could fail to detect the nonambiguity
+    of some automata with empty languages.
 
 New in spot 1.99.4 (2015-10-01)
 
diff --git a/THANKS b/THANKS
index 5ecf64bf7..81ed6c3a2 100644
--- a/THANKS
+++ b/THANKS
@@ -21,6 +21,7 @@ Kristin Y. Rozier
 Martin Dieguez Lodeiro
 Michael Tautschnig
 Michael Weber
+Ming-Hsien Tsai
 Nikos Gorogiannis
 Rüdiger Ehlers
 Silien Hong
diff --git a/src/tests/unambig.test b/src/tests/unambig.test
index bfcba6a93..24a826470 100755
--- a/src/tests/unambig.test
+++ b/src/tests/unambig.test
@@ -153,4 +153,22 @@ test `grep -c unambiguous output` = 0
 ../../bin/randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H |
   $autfilt -v --is-unamb --stats=%M && exit 1
 
-:
+cat >input <<EOF
+HOA: v1
+properties: explicit-labels state-acc trans-labels
+States: 3
+Start: 0
+AP: 0
+Acceptance: 1 Inf(0)
+acc-name: Buchi
+name: ""
+tool: "GOAL" ""
+--BODY--
+State: 0
+[t] 2
+[t] 1
+State: 1
+State: 2
+--END--
+EOF
+run 0 $autfilt -q --is-unambiguous input
diff --git a/src/twaalgos/isunamb.cc b/src/twaalgos/isunamb.cc
index 5b5f500e9..85bab2405 100644
--- a/src/twaalgos/isunamb.cc
+++ b/src/twaalgos/isunamb.cc
@@ -30,6 +30,8 @@ namespace spot
     if (aut->is_deterministic() || aut->is_unambiguous())
       return true;
     auto clean_a = scc_filter_states(aut);
+    if (clean_a->num_edges() == 0)
+      return true;
     auto prod = product(clean_a, clean_a);
     auto clean_p = scc_filter_states(prod);
     return clean_a->num_states() == clean_p->num_states()
diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc
index 098b8a2ee..9dd844440 100644
--- a/src/twaalgos/sccfilter.cc
+++ b/src/twaalgos/sccfilter.cc
@@ -324,11 +324,12 @@ namespace spot
 	}
       if (!given_si)
 	delete si;
-      // If the initial state has been filtered out, we don't attempt
-      // to fix it.
+      // If the initial state has been filtered out, we have to create
+      // a new one (not doing so may cause empty automata, which in turn
+      // cause all sort of issue with algorithms assuming an automaton
+      // has one initial state).
       auto init = inout[aut->get_init_state_number()];
-      if (init < out_n)
-	filtered->set_init_state(init);
+      filtered->set_init_state(init < out_n ? init : filtered->new_state());
       return filtered;
     }