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