From f5b261d80e515a165b840c737c3ea527bedab295 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 24 Dec 2016 20:41:43 +0100
Subject: [PATCH] remfin: call remove_alternation if needed

* spot/twaalgos/remfin.cc: Here.
* tests/core/alternating.test: Add a test case.
---
 spot/twaalgos/remfin.cc     |  4 ++++
 tests/core/alternating.test | 45 +++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)

diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index 93fbe0887..30ff83a75 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -24,6 +24,7 @@
 #include <spot/twaalgos/totgba.hh>
 #include <spot/twaalgos/isdet.hh>
 #include <spot/twaalgos/mask.hh>
+#include <spot/twaalgos/alternation.hh>
 
 //#define TRACE
 #ifdef TRACE
@@ -494,6 +495,9 @@ namespace spot
     if (aut->prop_weak().is_true())
       return remove_fin_weak(aut);
 
+    if (aut->is_alternating())
+      return remove_fin(remove_alternation(aut));
+
     if (auto maybe = streett_to_generalized_buchi_maybe(aut))
       return maybe;
 
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 158cb99eb..345dd7203 100644
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -157,3 +157,48 @@ State: 2 "t"
 EOF
 test 3 = `autfilt --stats=%s out.hoa`
 test 2 = `autfilt --tgba --stats=%s out.hoa`
+
+# If we have a weak input, remove-fin can just transform co-Büchi into
+# Büchi.
+autfilt --remove-fin out.hoa >res
+cat >expected <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete
+properties: very-weak
+--BODY--
+State: 0 {0}
+[t] 1&0
+State: 1
+[0] 2
+[t] 1
+State: 2 {0}
+[t] 2
+--END--
+EOF
+diff expected res
+
+# If we do not know that the input is weak, remove-fin will call
+# remove_alternation().
+autfilt --remove-fin --trust-hoa=no out.hoa >res
+cat >expected <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[t] 1 {0}
+State: 1
+[t] 1
+[0] 1 {0}
+--END--
+EOF
+diff expected res