From 7957a231a146b3321b1f0368aed1fce9863d8621 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 28 Mar 2018 10:26:10 +0200
Subject: [PATCH] =?UTF-8?q?to=5Fdca/to=5Fnca:=20fix=20handling=20of=20co-B?=
 =?UTF-8?q?=C3=BCchi=20input?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* spot/twaalgos/cobuchi.cc (to_dca, to_nca): Do not process
the input if it is already co-Büchi.
* tests/core/dca.test: Test this.
* NEWS: Mention the bug.
---
 NEWS                     |  5 +++++
 spot/twaalgos/cobuchi.cc | 11 +++++++++--
 tests/core/dca.test      | 22 ++++++++++++++++++++++
 3 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 266b973bd..b699c3acc 100644
--- a/NEWS
+++ b/NEWS
@@ -27,6 +27,11 @@ New in spot 2.5.2.dev (not yet released)
     simplified to {1} or {SERE} depending on whether SERE accepts
     the empty word or not.
 
+  Bugs fixed:
+
+  - "autfilt --cobuchi --small/--det" would turn a transition-based
+    co-Büchi automaton into a state-based co-Büchi.
+
 New in spot 2.5.2 (2018-03-25)
 
   Bugs fixed:
diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc
index 634b3f6b2..40b0d86a7 100644
--- a/spot/twaalgos/cobuchi.cc
+++ b/spot/twaalgos/cobuchi.cc
@@ -338,6 +338,9 @@ namespace spot
   twa_graph_ptr
   to_nca(const_twa_graph_ptr aut, bool named_states)
   {
+    if (aut->acc().is_co_buchi())
+      return make_twa_graph(aut, twa::prop_set::all());
+
     if (auto weak = weak_to_cobuchi(aut))
       return weak;
 
@@ -684,8 +687,12 @@ namespace spot
   to_dca(const_twa_graph_ptr aut, bool named_states)
   {
     if (is_deterministic(aut))
-      if (auto weak = weak_to_cobuchi(aut))
-        return weak;
+      {
+        if (aut->acc().is_co_buchi())
+          return make_twa_graph(aut, twa::prop_set::all());
+        if (auto weak = weak_to_cobuchi(aut))
+          return weak;
+      }
 
     const acc_cond::acc_code& code = aut->get_acceptance();
 
diff --git a/tests/core/dca.test b/tests/core/dca.test
index a5ca7e9f1..8d9f3fcd6 100644
--- a/tests/core/dca.test
+++ b/tests/core/dca.test
@@ -369,3 +369,25 @@ State: 1 [!1] 1 {0 2} [!0&!1] 2 [1] 3 [!0&1] 4 State: 2 [!0&!1] 2 {0 3}
 [1] 7 {2} [!1] 8 {2} State: 9 [1] 3 {2} [!0] 4 [!1] 9 {2} State: 10 [1]
 7 [!1] 10 {0 2} --END--
 EOF
+
+cat >in.hoa <<EOF
+HOA: v1
+name: "FGa"
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0
+[0] 0
+[!0] 0 {0}
+--END--
+EOF
+# We had a problem that to_nca()/to_dca() would call sbacc()
+# even if the input was already of the good shape.  Make sure
+# this is not the case anymore.
+test '1,co-Buchi' = "`autfilt --cobuchi --small --stats='%s,%[]g' in.hoa`"
+test '1,co-Buchi' = "`autfilt --cobuchi --det --stats='%s,%[]g' in.hoa`"