diff --git a/NEWS b/NEWS index 92a77acb6..b9d0f1b46 100644 --- a/NEWS +++ b/NEWS @@ -65,6 +65,8 @@ New in spot 1.99.4a (not yet released) * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. * "ltlgrind --help" did not document FORMAT. * unabbreviate could easily use forbidden operators. + * "autfilt --is-unambiguous" could fail to detect the nonambiguity + of some automata with empty languages. New in spot 1.99.4 (2015-10-01) diff --git a/THANKS b/THANKS index 5ecf64bf7..81ed6c3a2 100644 --- a/THANKS +++ b/THANKS @@ -21,6 +21,7 @@ Kristin Y. Rozier Martin Dieguez Lodeiro Michael Tautschnig Michael Weber +Ming-Hsien Tsai Nikos Gorogiannis RĂ¼diger Ehlers Silien Hong diff --git a/src/tests/unambig.test b/src/tests/unambig.test index bfcba6a93..24a826470 100755 --- a/src/tests/unambig.test +++ b/src/tests/unambig.test @@ -153,4 +153,22 @@ test `grep -c unambiguous output` = 0 ../../bin/randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H | $autfilt -v --is-unamb --stats=%M && exit 1 -: +cat >input <is_deterministic() || aut->is_unambiguous()) return true; auto clean_a = scc_filter_states(aut); + if (clean_a->num_edges() == 0) + return true; auto prod = product(clean_a, clean_a); auto clean_p = scc_filter_states(prod); return clean_a->num_states() == clean_p->num_states() diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc index 098b8a2ee..9dd844440 100644 --- a/src/twaalgos/sccfilter.cc +++ b/src/twaalgos/sccfilter.cc @@ -324,11 +324,12 @@ namespace spot } if (!given_si) delete si; - // If the initial state has been filtered out, we don't attempt - // to fix it. + // If the initial state has been filtered out, we have to create + // a new one (not doing so may cause empty automata, which in turn + // cause all sort of issue with algorithms assuming an automaton + // has one initial state). auto init = inout[aut->get_init_state_number()]; - if (init < out_n) - filtered->set_init_state(init); + filtered->set_init_state(init < out_n ? init : filtered->new_state()); return filtered; }