diff --git a/NEWS b/NEWS index 5eb462fa4..7c1e536cc 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.5.2.dev (not yet released) - Using spot.automata("cmd...|") to read just a few automata out of an infinite stream would not properly terminate the command. + - The is_unambiguous() check (rewritten in Spot 2.2) could mark some + unambiguous automata as ambiguous. + New in spot 2.5.2 (2018-03-25) Bugs fixed: diff --git a/THANKS b/THANKS index 5c6151aee..83b50cf4d 100644 --- a/THANKS +++ b/THANKS @@ -34,6 +34,7 @@ Nikos Gorogiannis Reuben Rowe Rüdiger Ehlers Silien Hong +Simon Jantsch Shufang Zhu Sonali Dutta Tobias Meggendorfer. diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index e0f8af6a0..8af04121c 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -96,7 +96,7 @@ namespace spot unsigned one_state = sccmap_prod.states_of(n).front(); bool accepting = v[(*sprod)[one_state].first] && v[(*sprod)[one_state].second]; - if (accepting) + if (accepting && !sccmap_prod.is_trivial(n)) { useful[n] = true; continue; diff --git a/tests/core/unambig.test b/tests/core/unambig.test index 25c52752d..ebeb65dd6 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -284,4 +284,54 @@ EOF run 1 autfilt -q --is-unambiguous smaller.hoa -true +# These automata come from Simon Jantsch and David Müller. +cat >sjdb.hoa <