From 46d967945ba6439331e340bc1f733d5b10776433 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 22 Jan 2015 15:51:12 +0100
Subject: [PATCH] simulation: do not mark codeterministic automata as
 deterministic

* src/tgbaalgos/simulation.cc: Here.
* src/tgbatest/det.test: Test it.
---
 src/tgbaalgos/simulation.cc | 3 +--
 src/tgbatest/det.test       | 8 ++++++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 345402caa..69bd2e89f 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -632,11 +632,10 @@ namespace spot
 		         true,  // weakness preserved,
 			 false, // determinism checked and set below
 		       });
-        if (nb_minato == nb_satoneset)
+        if (nb_minato == nb_satoneset && !Cosimulation)
 	  res->prop_deterministic();
 	if (Sba)
 	  res->prop_state_based_acc();
-
 	return res;
       }
 
diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test
index 5b8b94676..641eaa345 100755
--- a/src/tgbatest/det.test
+++ b/src/tgbatest/det.test
@@ -144,3 +144,11 @@ digraph G {
 }
 EOF
 diff out.tgba ex.tgba
+
+
+# This formula produce a co-deterministic automaton that is not deterministic,
+# and a bug in the cosimulation caused the result to be marked as deterministic.
+run 0 ../../bin/ltl2tgba -H '(0 R Xa) R (a xor Fa)' > out.hoa
+grep deterministic out.hoa && exit 1
+
+true