Büchi translation should not go through fg_safety_to_dca_maybe()
Fixes #366, reported by Simon Jantsch. * spot/twaalgos/translate.cc: type_&Generic will also match if type_==BA... use type_==Generic instead. * tests/core/unambig.test: Add a test corresponding to Simon's report. * NEWS: Describe the bug.
This commit is contained in:
parent
e5f76b77d4
commit
3c86f034fc
3 changed files with 12 additions and 1 deletions
7
NEWS
7
NEWS
|
|
@ -64,6 +64,13 @@ New in spot 2.6.2.dev (not yet released)
|
||||||
with arbitrary acceptance condition into a parity automaton,
|
with arbitrary acceptance condition into a parity automaton,
|
||||||
based on a last-appearance record (LAR) construction.
|
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)
|
New in spot 2.6.2 (2018-09-28)
|
||||||
|
|
||||||
Build:
|
Build:
|
||||||
|
|
|
||||||
|
|
@ -337,7 +337,8 @@ namespace spot
|
||||||
if (aut2 && ((type_ == BA) || (type_ & Parity))
|
if (aut2 && ((type_ == BA) || (type_ & Parity))
|
||||||
&& (pref_ & Deterministic))
|
&& (pref_ & Deterministic))
|
||||||
return finalize(aut2);
|
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);
|
aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba);
|
||||||
if (aut2
|
if (aut2
|
||||||
|
|
|
||||||
|
|
@ -26,6 +26,7 @@ for f in 'Ga' \
|
||||||
'Ga | Gb' \
|
'Ga | Gb' \
|
||||||
'Ga | GFb' \
|
'Ga | GFb' \
|
||||||
'Ga | FGb' \
|
'Ga | FGb' \
|
||||||
|
'F(Ga | Gb)' \
|
||||||
'XFGa | GFb | Gc' \
|
'XFGa | GFb | Gc' \
|
||||||
'(Ga -> Gb) W c' \
|
'(Ga -> Gb) W c' \
|
||||||
'F(a & !b & (!c W b))' \
|
'F(a & !b & (!c W b))' \
|
||||||
|
|
@ -33,6 +34,8 @@ for f in 'Ga' \
|
||||||
do
|
do
|
||||||
ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
|
ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
|
||||||
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 |
|
ltl2tgba -UH "$f" | autfilt --check |
|
||||||
grep -E 'properties:.* (unambiguous|deterministic)'
|
grep -E 'properties:.* (unambiguous|deterministic)'
|
||||||
ltl2tgba -UH "!($f)" | autfilt --check |
|
ltl2tgba -UH "!($f)" | autfilt --check |
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue