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 <ex < out +autfilt -H1.1 --small out >out2 +autfilt --trust=no -H1.1 --is-semi-det out2