From 095ac93b5b55af45ea37bda27006588ec565960f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 25 Feb 2015 23:38:24 +0100
Subject: [PATCH] postproc: make sure WDBA have an acceptance set if BA is
 desired

* src/tgbaalgos/postproc.cc: Here.
* src/tgbatest/ltl2tgba.test: Make sure ltl2tgba -B 0 has one
acceptance set.
---
 src/tgbaalgos/postproc.cc  | 30 +++++++++++++++++++++++++-----
 src/tgbatest/ltl2tgba.test |  3 +++
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index 7cf4f61fe..c9fec4684 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -33,6 +33,20 @@
 
 namespace spot
 {
+  namespace
+  {
+    static tgba_digraph_ptr
+    ensure_ba(tgba_digraph_ptr& a)
+    {
+      if (a->acc().num_sets() == 0)
+	{
+	  auto m = a->set_single_acceptance_set();
+	  for (auto& t: a->transitions())
+	    t.acc = m;
+	}
+      return a;
+    }
+  }
 
   postprocessor::postprocessor(const option_map* opt)
     : type_(TGBA), pref_(Small), level_(High),
@@ -106,7 +120,6 @@ namespace spot
       }
   }
 
-
   tgba_digraph_ptr
   postprocessor::do_degen(const tgba_digraph_ptr& a)
   {
@@ -204,11 +217,18 @@ namespace spot
 	bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
 	dba = minimize_obligation(a, f, 0, reject_bigger);
 	if (dba && dba->is_inherently_weak() && dba->is_deterministic())
-	  dba_is_minimal = dba_is_wdba = true;
+	  {
+	    // The WDBA is a BA, so no degeneralization is required.
+	    // We just need to add an acceptance set if there is none.
+	    dba_is_minimal = dba_is_wdba = true;
+	    if (type_ == BA)
+	      ensure_ba(dba);
+	  }
 	else
-	  // Minimization failed.
-	  dba = nullptr;
-	// The WDBA is a BA, so no degeneralization is required.
+	  {
+	    // Minimization failed.
+	    dba = nullptr;
+	  }
       }
 
     // Run a simulation when wdba failed (or was not run), or
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index 6e43f7a99..72e6f18e5 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -97,6 +97,9 @@ EOF
 
 run 0 ../checkpsl check.txt
 
+# Make sure False has one acceptance set when generating Büchi automata
+test 1 -eq `../../bin/ltl2tgba -B false --stats %a`
+
 # In particular, Spot 0.9 would incorrectly reject the sequence:
 # (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}'
 # This means the following automaton was incorrectly empty in Spot 0.9.