From 7353e47f0c942a8fdad7c588d887854a5477fcdb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 25 Mar 2015 18:29:07 +0100
Subject: [PATCH] cleanacc: better cleanup

Sometimes, simplifying the acceptance condition (because it refers to
sets that do not appear in the automaton) cause more sets to be removed
from the acceptance condition, and therefore warrant another pass to
remove those sets from the automaton.

* src/tgbaalgos/cleanacc.cc: Here.
* src/tgbatest/hoaparse.test: Add a test case.
---
 src/tgbaalgos/cleanacc.cc  |  4 +++
 src/tgbatest/hoaparse.test | 52 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)

diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc
index cdfd776ba..5ee8027fc 100644
--- a/src/tgbaalgos/cleanacc.cc
+++ b/src/tgbaalgos/cleanacc.cc
@@ -47,6 +47,10 @@ namespace spot
 
     // Remove useless marks from the acceptance condition
     aut->set_acceptance(useful.count(), c.strip(useless, true));
+
+    // This may in turn cause even more set to be unused, because of
+    // some simplifications, so do it again.
+    return cleanup_acceptance(aut);
   }
 
 }
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 7d9e663d1..a8953036a 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -1371,6 +1371,23 @@ State: 0
 [0&!1&!2] 0 {0}
 [!0&!1&!2] 0
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {2}
+[0&!1] 1
+[!0&1] 0
+[0&1] 1
+State: 1 {1 2}
+[!0&!1] 1
+[0&!1] 1
+[!0&1] 1
+[0&1] 1
+--END--
 EOF
 
 expectok input -v --is-empty <<EOF
@@ -1407,6 +1424,23 @@ State: 0
 [0&!1&!2] 0 {0 5}
 [!0&!1&!2] 0 {5}
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {2}
+[0&!1] 1
+[!0&1] 0
+[0&1] 1
+State: 1 {1 2}
+[!0&!1] 1
+[0&!1] 1
+[!0&1] 1
+[0&1] 1
+--END--
 EOF
 
 
@@ -1456,6 +1490,24 @@ State: 0
 [0&!1&!2] 0 {0 3}
 [!0&!1&!2] 0 {3}
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&!1] 1
+[!0&1] 0
+[0&1] 1
+State: 1 {0}
+[!0&!1] 1
+[0&!1] 1
+[!0&1] 1
+[0&1] 1
+--END--
 EOF