From 0143f0d4358424d039d92bcb92750b91f2d7e44e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 14 Aug 2015 11:31:25 +0200
Subject: [PATCH] sccsimpl: Remove Fin sets between SCCs

We do not remove them in rejecting SCCs (as it might make the SCC
accepting), but we can remove them between SCCs.

Fixes #101.

* src/twaalgos/sccfilter.cc: Here.
* src/tests/sccsimpl.test: Add test case.
* NEWS: Mention this.
---
 NEWS                      |  4 +++
 src/tests/sccsimpl.test   | 72 +++++++++++++++++++--------------------
 src/twaalgos/sccfilter.cc | 10 +++---
 3 files changed, 46 insertions(+), 40 deletions(-)

diff --git a/NEWS b/NEWS
index d83235908..eb8cd057a 100644
--- a/NEWS
+++ b/NEWS
@@ -6,6 +6,10 @@ New in spot 1.99.2a (not yet released)
   * The html documentation now includes a HTML copies of the man
     pages, and HTML copies of the Python notebooks.
 
+  * scc_filter(aut, true) does not remove Fin marks from rejecting
+    SCCs, but it now does remove Fin marks from transitions between
+    SCCs.
+
   * Bugs fixed
     - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3)
       were not detected as generalized-Rabin.
diff --git a/src/tests/sccsimpl.test b/src/tests/sccsimpl.test
index 65a02bb4b..5fdaf6513 100755
--- a/src/tests/sccsimpl.test
+++ b/src/tests/sccsimpl.test
@@ -255,7 +255,7 @@ State: 0
 [t] 0
 State: 1
 [!0] 1 {0}
-[0] 0
+[0] 0 {0}
 --END--
 HOA: v1
 States: 2
@@ -271,41 +271,41 @@ State: 1
 --END--
 EOF
 
-# run 0 ../../bin/autfilt -C -H --any --high input >output
-# cat >expected <<EOF
-# HOA: v1
-# States: 2
-# Start: 1
-# AP: 1 "p0"
-# acc-name: Buchi
-# Acceptance: 1 Inf(0)
-# properties: trans-labels explicit-labels state-acc complete
-# properties: deterministic inherently-weak
-# --BODY--
-# State: 0 {0}
-# [t] 0
-# State: 1
-# [0] 0
-# [!0] 1
-# --END--
-# HOA: v1
-# States: 2
-# Start: 1
-# AP: 1 "p0"
-# acc-name: Buchi
-# Acceptance: 1 Inf(0)
-# properties: trans-labels explicit-labels state-acc complete
-# properties: deterministic inherently-weak
-# --BODY--
-# State: 0 {0}
-# [t] 0
-# State: 1
-# [0] 0
-# [!0] 1
-# --END--
-# EOF
-# cat output
-# diff output expected
+run 0 ../../bin/autfilt -H --any --medium -x scc-filter=2 input >output
+cat >expected <<EOF
+HOA: v1
+States: 2
+Start: 1
+AP: 1 "p0"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0
+State: 1
+[0] 0
+[!0] 1 {0}
+--END--
+HOA: v1
+States: 2
+Start: 1
+AP: 1 "p0"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[t] 0 {1}
+State: 1
+[0] 0
+[!0] 1 {0}
+--END--
+EOF
+cat output
+diff output expected
 
 run 0 ../../bin/autfilt -C -H --det --high input >output
 cat >expected <<EOF
diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc
index ccab52d96..c1b15fa38 100644
--- a/src/twaalgos/sccfilter.cc
+++ b/src/twaalgos/sccfilter.cc
@@ -155,10 +155,12 @@ namespace spot
 	if (keep)
 	  {
 	    unsigned u = this->si->scc_of(dst);
-	    // If the edge is between two SCCs, or in a
-	    // non-accepting SCC.  Remove the acceptance sets.
-	    if ((this->si->is_rejecting_scc(u))
-		|| (RemoveAll && u != this->si->scc_of(src)))
+	    // If the edge is between two SCCs, we can simplify
+	    // remove the acceptance sets.  If the SCC is non-accepting,
+	    // we can only remove the Inf sets.
+	    if (RemoveAll && u != this->si->scc_of(src))
+	      acc = 0U;
+	    else if (this->si->is_rejecting_scc(u))
 	      acc &= accmask;
 	  }