From ce5e3b654f9d68366bcd01dcb58ffc8661888433 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 28 Sep 2017 20:38:13 +0200
Subject: [PATCH] simulation: incorrect setting of non-deterministic property

Fixes #286.

* spot/twaalgos/simulation.cc: Only set the deterministic
property, not the non-deterministic one.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the issue.
---
 NEWS                        |  3 +++
 spot/twaalgos/simulation.cc | 10 +++++++---
 tests/core/ltl2tgba.test    |  5 +++++
 3 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 79b66274a..55dfa117f 100644
--- a/NEWS
+++ b/NEWS
@@ -126,6 +126,9 @@ New in spot 2.4.0.dev (not yet released)
     still correct outputs) depending on the BDD operations performed
     before.
 
+  - spot::simulation() would occasionally incorrectly flag an
+    automaton as non-deterministic.
+
 New in spot 2.4 (2017-09-06)
 
   Build:
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index d6828f8bb..cddc529cc 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -582,7 +582,9 @@ namespace spot
         res->set_init_state(gb->get_state(previous_class_
                                           [a_->get_init_state_number()].id()));
 
-        res->merge_edges(); // FIXME: is this really needed?
+        res->merge_edges(); // This helps merging some edges with
+                            // identical conditions, but different
+                            // mark sets.
 
         // Mark all accepting state in a second pass, when
         // dealing with SBA in cosimulation.
@@ -616,8 +618,10 @@ namespace spot
                          true, // stutter inv.
                        });
         // !unambiguous and !semi-deterministic are not preserved
-        if (!Cosimulation)
-          res->prop_universal(nb_minato == nb_satoneset);
+        if (!Cosimulation && nb_minato == nb_satoneset)
+          // Note that nb_minato != nb_satoneset does not imply
+          // non-deterministic, because of the merge_edges() above.
+          res->prop_universal(true);
         if (Sba)
           res->prop_state_acc(true);
         return res;
diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test
index 50703a1a1..6a7131774 100755
--- a/tests/core/ltl2tgba.test
+++ b/tests/core/ltl2tgba.test
@@ -265,3 +265,8 @@ ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2
 diff res1 res2
 
 test 3 = `ltl2tgba -f 'G(Fa & Fb) U a' --stats=%s`
+
+# issue #286, the following automaton caused the print_hoa() function to
+# report inconsistent "universal" property.
+ltl2tgba --low 'X(((1) U (p1)) | (((p1) | (F(p0))) U ((0) R ((p2) M (p1)))))'>o
+grep deterministic o