diff --git a/NEWS b/NEWS index 6624fd57c..2cf4d305f 100644 --- a/NEWS +++ b/NEWS @@ -63,6 +63,15 @@ New in spot 2.8.4.dev (not yet released) - ltl2tgba -B could return automata with "t" acceptance, instead of the expected Inf(0). + - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was + unaware that merging edges can sometimes transform a + non-deterministic automaton into a deterministic one, causing the + following unexpected diagnostic: + "print_hoa(): automaton is universal despite prop_universal()==false" + The kind of non-deterministic automata where this occurs is not + naturally produced by any Spot algorithm, but can be found for + instance in automata produced by Goal 2015-10-18. + New in spot 2.8.4 (2019-12-08) Bugs fixed: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4c5218306..ee9fa13b9 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -148,7 +148,8 @@ namespace spot }); auto& trans = this->edge_vector(); - unsigned tend = trans.size(); + unsigned orig_size = trans.size(); + unsigned tend = orig_size; unsigned out = 0; unsigned in = 1; // Skip any leading false edge. @@ -233,6 +234,13 @@ namespace spot } g_.chain_edges_(); + + // Did we actually reduce the number of edges? + if (trans.size() != orig_size) + // Merging some edges may turn a non-deterministic automaton + // into a deterministic one. + if (prop_universal().is_false()) + prop_universal(trival::maybe()); } void twa_graph::merge_states() diff --git a/tests/core/det.test b/tests/core/det.test index f6080889f..e30f2b873 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -275,3 +275,25 @@ State: 1 --END-- EOF diff output expected + +# This is a syntactically non-deterministic automaton, which is +# semantically equivalent to a deterministic automaton (once +# transitions with compatible src/dst are merged). Running +# --merge-transition on this used to fail because merge_edges() would +# preserve the determism bit (or rather, the non-determinism bit). +cat >in.hoa <