From cfe3ed707a361523e699da09d07d7bd4f8c2ea67 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 26 Dec 2019 12:00:44 +0100
Subject: [PATCH] fix ltl2tgba -B not always returning Inf(0)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by František Blahoudek.

* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.
---
 NEWS                      |  5 +++++
 spot/twaalgos/postproc.cc | 11 +++++++++++
 tests/core/ltl2tgba.test  |  3 +++
 3 files changed, 19 insertions(+)

diff --git a/NEWS b/NEWS
index f46ba9e62..6624fd57c 100644
--- a/NEWS
+++ b/NEWS
@@ -58,6 +58,11 @@ New in spot 2.8.4.dev (not yet released)
     degeneralization to get rid of conjunction of Inf terms in
     acceptance conditions.
 
+  Bugs fixed:
+
+  - ltl2tgba -B could return automata with "t" acceptance, instead
+    of the expected Inf(0).
+
 New in spot 2.8.4 (2019-12-08)
 
   Bugs fixed:
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index ca639d952..6165ac834 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -163,6 +163,15 @@ namespace spot
                             degen_lowinit_, degen_remscc_);
   }
 
+  static void
+  force_buchi(twa_graph_ptr& a)
+  {
+    assert(a->acc().is_t());
+    acc_cond::mark_t m = a->set_buchi();
+    for (auto& e: a->edges())
+      e.acc = m;
+  }
+
   twa_graph_ptr
   postprocessor::do_scc_filter(const twa_graph_ptr& a, bool arg) const
   {
@@ -196,6 +205,8 @@ namespace spot
       tmp = SBACC_ ? do_degen(tmp) : do_degen_tba(tmp);
     if (SBACC_)
       tmp = sbacc(tmp);
+    if (type_ == BA && tmp->acc().is_t())
+      force_buchi(tmp);
     if (want_parity)
       {
         reduce_parity_here(tmp, COLORED_);
diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test
index ccb892f75..8417df485 100755
--- a/tests/core/ltl2tgba.test
+++ b/tests/core/ltl2tgba.test
@@ -292,3 +292,6 @@ test 2 = `ltl2tgba -f "$f" --low -x tls-impl=3 --stats=%s`
 
 # This is not optimal, the smallest DBA for this formula has 2 states.
 test 3 = `ltl2tgba -BD -f 'GF((p0 & GF!p0) | (!p0 & FGp0))' --stats=%s`
+
+# Some versions of Spot incorrectly returned "t" automata with -B
+test "Inf(0)" = "`ltl2tgba -B 'Xb | G!b' --stats=%g`"