From 265332dedf88c0ae0123e36dd01ef8e46a084f8e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 31 Dec 2019 22:34:39 +0100
Subject: [PATCH] twagraph: merge_edge() can determinize automata
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by František Blahoudek.

* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.
---
 NEWS                 |  9 +++++++++
 spot/twa/twagraph.cc | 10 +++++++++-
 tests/core/det.test  | 22 ++++++++++++++++++++++
 3 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index a9f71cc0a..bfb505da0 100644
--- a/NEWS
+++ b/NEWS
@@ -5,6 +5,15 @@ New in spot 2.8.4.dev (not yet released)
   - ltl2tgba -B could return automata with "t" acceptance, instead
     of the expected Inf(0).
 
+  - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was
+    unaware that merging edges can sometimes transform a
+    non-deterministic automaton into a deterministic one, causing the
+    following unexpected diagnostic:
+    "print_hoa(): automaton is universal despite prop_universal()==false"
+    The kind of non-deterministic automata where this occurs is not
+    naturally produced by any Spot algorithm, but can be found for
+    instance in automata produced by Goal 2015-10-18.
+
 New in spot 2.8.4 (2019-12-08)
 
   Bugs fixed:
diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc
index 4c5218306..ee9fa13b9 100644
--- a/spot/twa/twagraph.cc
+++ b/spot/twa/twagraph.cc
@@ -148,7 +148,8 @@ namespace spot
                    });
 
     auto& trans = this->edge_vector();
-    unsigned tend = trans.size();
+    unsigned orig_size = trans.size();
+    unsigned tend = orig_size;
     unsigned out = 0;
     unsigned in = 1;
     // Skip any leading false edge.
@@ -233,6 +234,13 @@ namespace spot
       }
 
     g_.chain_edges_();
+
+    // Did we actually reduce the number of edges?
+    if (trans.size() != orig_size)
+      // Merging some edges may turn a non-deterministic automaton
+      // into a deterministic one.
+      if (prop_universal().is_false())
+        prop_universal(trival::maybe());
   }
 
   void twa_graph::merge_states()
diff --git a/tests/core/det.test b/tests/core/det.test
index f6080889f..e30f2b873 100755
--- a/tests/core/det.test
+++ b/tests/core/det.test
@@ -275,3 +275,25 @@ State: 1
 --END--
 EOF
 diff output expected
+
+# This is a syntactically non-deterministic automaton, which is
+# semantically equivalent to a deterministic automaton (once
+# transitions with compatible src/dst are merged).  Running
+# --merge-transition on this used to fail because merge_edges() would
+# preserve the determism bit (or rather, the non-determinism bit).
+cat >in.hoa <<EOF
+HOA: v1
+States: 2
+Start: 1
+AP: 2 "a" "b"
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0 {0}
+[t] 0
+State: 1
+[0] 0
+[1] 0
+--END--
+EOF
+autfilt -q --is-deterministic in.hoa && exit 1
+autfilt --merge-transitions in.hoa | autfilt --is-deterministic