From ada8185361ef8a7be2356ca499f1c8e3e09f0df9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 30 Dec 2016 09:58:56 +0100
Subject: [PATCH] simulation: does not preserve !unambiguous,
 !semi-deterministic

* spot/twaalgos/simulation.cc: Reset those to maybe.
* tests/core/semidet.test: Add some tests.
---
 spot/twaalgos/simulation.cc |  5 +++++
 tests/core/semidet.test     | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+)

diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index 541118274..bceb97f42 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -598,6 +598,11 @@ namespace spot
                                // and "unambiguous" property preserved
                          true, // stutter inv.
                        });
+        // !unambiguous and !semi-deterministic are not preserved
+        if (original_->prop_semi_deterministic().is_false())
+          res->prop_semi_deterministic(trival::maybe());
+        if (original_->prop_unambiguous().is_false())
+          res->prop_unambiguous(trival::maybe());
         if (!Cosimulation)
           res->prop_deterministic(nb_minato == nb_satoneset);
         if (Sba)
diff --git a/tests/core/semidet.test b/tests/core/semidet.test
index a1e3bc4db..be15515dd 100755
--- a/tests/core/semidet.test
+++ b/tests/core/semidet.test
@@ -79,3 +79,36 @@ cat >expected <<EOF
 X(!p0 W Xp1)
 EOF
 diff out expected
+
+
+# This automaton becomes semi-deterministic once simplified with
+# simulation-based reductions.
+cat >ex <<EOF
+HOA: v1
+AP: 2 "a" "b"
+Start: 0
+States: 6
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[!0] 0
+[0] 1
+[1] 5
+State: 1 {0}
+[0] 1
+State: 2
+[!1] 4
+State: 3
+[1] 4
+State: 4 {0}
+[!0] 4
+State: 5 {0}
+[!1] 5
+[1] 2
+[1] 3
+--END--
+EOF
+
+autfilt -H1.1 ex -v --is-semi-det > out
+autfilt -H1.1 --small out >out2
+autfilt --trust=no -H1.1 --is-semi-det out2