From 83dfb4a971baa7375a224b13470b50264f25bafc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 24 Feb 2015 21:51:20 +0100
Subject: [PATCH] remfin: cleanup acceptance

* src/tgbaalgos/remfin.cc: Call cleanup_acceptance().
* src/tgbatest/remfin.test: Adjust.
---
 src/tgbaalgos/remfin.cc  |  2 +
 src/tgbatest/remfin.test | 92 +++++++++++++++++-----------------------
 2 files changed, 41 insertions(+), 53 deletions(-)

diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc
index f6a87bcb5..5a084904e 100644
--- a/src/tgbaalgos/remfin.cc
+++ b/src/tgbaalgos/remfin.cc
@@ -20,6 +20,7 @@
 #include "remfin.hh"
 #include "sccinfo.hh"
 #include <iostream>
+#include "cleanacc.hh"
 
 //#define TRACE
 #ifdef TRACE
@@ -303,6 +304,7 @@ namespace spot
 
 
       }
+    cleanup_acceptance(res);
     return res;
   }
 }
diff --git a/src/tgbatest/remfin.test b/src/tgbatest/remfin.test
index ef93b38fb..5607c2cc9 100755
--- a/src/tgbatest/remfin.test
+++ b/src/tgbatest/remfin.test
@@ -30,7 +30,7 @@ cat >test1 <<EOF
 ** This was a TGBA for GFa & GFb, but
 ** the acceptance has been changed to Fin(0)|Fin(1)
 ** so this is now the complement automaton.
-**/
+*/
 HOA: v1
 States: 1
 Start: 0
@@ -46,18 +46,18 @@ State: 0
 /*
 ** This one has a mix of Inf and Fin acceptance, but no interference
 ** between the Fin sets
-**/
+*/
 HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
 Acceptance: 5 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(4)
 --BODY--
-State: 0
+State: 0 {3 4}
 [t] 0
 [0] 1 {1}
 [!0] 2 {0}
-State: 1
+State: 1 {3}
 [1] 0
 [0&1] 1 {0}
 [!0&1] 2 {2}
@@ -67,9 +67,9 @@ State: 2
 [!0&!1] 2 {0}
 --END--
 /*
-** This one is similar, but Inf(0) is ised in two terms, so
-** we to introduce extra sets in the output.
-**/
+** This one is similar, but Inf(0) is used in two terms, so
+** we need to introduce extra sets in the output.
+*/
 HOA: v1
 States: 3
 Start: 0
@@ -77,11 +77,11 @@ AP: 2 "a" "b"
 acc-name: Buchi
 Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0)
 --BODY--
-State: 0
+State: 0 {3}
 [t] 0
 [0] 1 {1}
 [!0] 2 {0}
-State: 1
+State: 1 {3}
 [1] 0
 [0&1] 1 {0}
 [!0&1] 2 {2}
@@ -132,7 +132,8 @@ HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 3 Inf(2)
+acc-name: Buchi
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc
 --BODY--
 State: 0
@@ -144,10 +145,10 @@ State: 0
 [!0&1] 1
 [!0&!1] 2
 [0&!1] 2
-State: 1 {2}
+State: 1 {0}
 [!0&!1] 1
 [!0&1] 1
-State: 2 {2}
+State: 2 {0}
 [!0&!1] 2
 [0&!1] 2
 --END--
@@ -155,20 +156,17 @@ HOA: v1
 States: 6
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 5 Inf(0) | Inf(4) | (Inf(2)&Inf(3))
+Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2))
 properties: trans-labels explicit-labels trans-acc
 --BODY--
 State: 0
-[t] 0
-[0] 1
-[!0] 2
-[t] 3
+[t] 0 {2 3}
+[0] 1 {2 3}
+[!0] 2 {2 3}
 State: 1
-[1] 0
-[0&1] 1
-[!0&1] 2 {2}
-[1] 3
-[0&1] 4
+[1] 0 {2}
+[0&1] 1 {2}
+[!0&1] 2 {1 2}
 State: 2
 [!1] 0
 [0&!1] 1
@@ -177,12 +175,7 @@ State: 2
 [0&!1] 4
 [!0&!1] 5
 State: 3
-[t] 3
-[!0] 5 {0}
 State: 4
-[1] 3
-[0&1] 4 {0}
-[!0&1] 5
 State: 5
 [!1] 3
 [0&!1] 4 {0}
@@ -192,38 +185,30 @@ HOA: v1
 States: 6
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 6 (Inf(0)&Inf(5)) | ((Inf(0) | (Inf(2)&Inf(3))) & Inf(4))
+Acceptance: 5 (Inf(0)&Inf(4)) | ((Inf(0) | (Inf(1)&Inf(2))) & Inf(3))
 properties: trans-labels explicit-labels trans-acc
 --BODY--
 State: 0
-[t] 0 {4}
-[0] 1 {4}
-[!0] 2 {0 4}
-[t] 3 {4}
+[t] 0 {2 3}
+[0] 1 {2 3}
+[!0] 2 {0 2 3}
 State: 1
-[1] 0 {4}
-[0&1] 1 {0 4}
-[!0&1] 2 {2 4}
-[1] 3 {4}
-[0&1] 4 {0 4}
+[1] 0 {2 3}
+[0&1] 1 {0 2 3}
+[!0&1] 2 {1 2 3}
 State: 2
-[!1] 0 {4}
-[0&!1] 1 {0 4}
-[!0&!1] 2 {0 4}
+[!1] 0 {3}
+[0&!1] 1 {0 3}
+[!0&!1] 2 {0 3}
+[!1] 3 {3}
+[0&!1] 4 {0 3}
+[!0&!1] 5 {0 3}
+State: 3
+State: 4
+State: 5
 [!1] 3 {4}
 [0&!1] 4 {0 4}
 [!0&!1] 5 {0 4}
-State: 3
-[t] 3 {5}
-[!0] 5 {0 5}
-State: 4
-[1] 3 {5}
-[0&1] 4 {0 5}
-[!0&1] 5 {5}
-State: 5
-[!1] 3 {5}
-[0&!1] 4 {0 5}
-[!0&!1] 5 {0 5}
 --END--
 HOA: v1
 States: 1
@@ -249,13 +234,14 @@ HOA: v1
 States: 2
 Start: 0
 AP: 1 "p0"
-Acceptance: 2 Inf(1)
+acc-name: Buchi
+Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc complete deterministic
 --BODY--
 State: 0
 [!0] 0
 [0] 1
-State: 1 {1}
+State: 1 {0}
 [!0] 1
 [0] 1
 --END--