diff --git a/NEWS b/NEWS index 919e5b84f..4c099a86d 100644 --- a/NEWS +++ b/NEWS @@ -64,6 +64,13 @@ New in spot 2.6.2.dev (not yet released) with arbitrary acceptance condition into a parity automaton, based on a last-appearance record (LAR) construction. + Bugs fixed: + + - Running "ltl2tgba -B" on formulas of the type FG(safety) would + unexpectedly use a co-Büchi automaton as an intermediate step. + This in turn caused "ltl2tgba -U -B" to not produce unambiguous + automata. + New in spot 2.6.2 (2018-09-28) Build: diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 2123e039a..ae2f9d67f 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -337,7 +337,8 @@ namespace spot if (aut2 && ((type_ == BA) || (type_ & Parity)) && (pref_ & Deterministic)) return finalize(aut2); - if (!aut2 && (type_ & (Generic | Parity | CoBuchi))) + if (!aut2 && (type_ == Generic + || type_ & (Parity | CoBuchi))) { aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba); if (aut2 diff --git a/tests/core/unambig.test b/tests/core/unambig.test index 635ebc264..f90d6348f 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -26,6 +26,7 @@ for f in 'Ga' \ 'Ga | Gb' \ 'Ga | GFb' \ 'Ga | FGb' \ + 'F(Ga | Gb)' \ 'XFGa | GFb | Gc' \ '(Ga -> Gb) W c' \ 'F(a & !b & (!c W b))' \ @@ -33,6 +34,8 @@ for f in 'Ga' \ do ltl2tgba -UH "$f" | autfilt -q --is-unambiguous ltl2tgba -UH "!($f)" | autfilt -q --is-unambiguous + ltl2tgba -BUH "$f" | autfilt -q --is-unambiguous + ltl2tgba -BUH "!($f)" | autfilt -q --is-unambiguous ltl2tgba -UH "$f" | autfilt --check | grep -E 'properties:.* (unambiguous|deterministic)' ltl2tgba -UH "!($f)" | autfilt --check |