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
92369d68c6
commit
68a155a818
3 changed files with 11 additions and 2 deletions
7
NEWS
7
NEWS
|
|
@ -1,6 +1,11 @@
|
|||
New in spot 2.6.2.dev (not yet released)
|
||||
|
||||
Nothing yet.
|
||||
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)
|
||||
|
||||
|
|
|
|||
|
|
@ -322,7 +322,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
|
||||
|
|
|
|||
|
|
@ -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 |
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue