From 68a155a818cdda6325e78ca156c42b9a5f08f0d6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 12 Oct 2018 11:47:00 +0200
Subject: [PATCH] =?UTF-8?q?B=C3=BCchi=20translation=20should=20not=20go=20?=
 =?UTF-8?q?through=20fg=5Fsafety=5Fto=5Fdca=5Fmaybe()?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 NEWS                       | 7 ++++++-
 spot/twaalgos/translate.cc | 3 ++-
 tests/core/unambig.test    | 3 +++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index b0642cf8f..7f33fbfa1 100644
--- a/NEWS
+++ b/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)
 
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index 806aa522b..a3c2a160c 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -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
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 |