From a965af711c1dcd129984dc5e9580cf9275560b24 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 Feb 2013 14:35:14 +0100
Subject: [PATCH] postproc: add an scc-filter option

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add an
scc-filter option.
* src/bin/man/ltl2tgba.x: Document it.
---
 src/bin/man/ltl2tgba.x    |  8 ++++++++
 src/tgbaalgos/postproc.cc | 10 +++++++---
 src/tgbaalgos/postproc.hh |  1 +
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 5f95f19ac..6a2ff04f0 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -14,6 +14,14 @@ shorthand for \fIKEY\fR=1, and !\fIKEY\fR is a shorthand for
 
 Supported options are:
 .TP
+\fBscc\-filter\fR
+Set to 1 (the default) to enable SCC-pruning and acceptance
+simplification at the beginning of post-processing.  Transitions that
+are outside of accepting SCC are removed from accepting sets, except
+those that enter into an accepting SCC.  Set to 2 to remove even these
+entering transition from the accepting sets.  Set to 0 to disable this
+SCC-pruning and acceptance simpification pass.
+.TP
 \fBdegen\-reset\fR
 If non-zero (the default), the degeneralization algorithm will reset
 its level any time it exits a non-accepting SCC.
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index 25feaaca2..279319bac 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -46,7 +46,7 @@ namespace spot
   postprocessor::postprocessor(const option_map* opt)
     : type_(TGBA), pref_(Small), level_(High),
       degen_reset_(true), degen_order_(false), degen_cache_(true),
-      simul_(-1)
+      simul_(-1), scc_filter_(-1)
   {
     if (opt)
       {
@@ -55,6 +55,7 @@ namespace spot
 	degen_cache_ = opt->get("degen-lcache", 1);
 	simul_ = opt->get("simul", -1);
 	simul_limit_ = opt->get("simul-limit", -1);
+	scc_filter_ = opt->get("scc-filter", -1);
       }
   }
 
@@ -95,10 +96,13 @@ namespace spot
 
     if (simul_ < 0)
       simul_ = (level_ == Low) ? 1 : 3;
+    if (scc_filter_ < 0)
+      scc_filter_ = 1;
 
     // Remove useless SCCs.
+    if (scc_filter_ > 0 || type_ == Monitor)
     {
-      const tgba* s = scc_filter(a, simul_ > 3);
+      const tgba* s = scc_filter(a, scc_filter_ > 1);
       delete a;
       a = s;
     }
@@ -194,7 +198,7 @@ namespace spot
 	  }
       }
 
-    if (sim && type_ == TGBA && level_ == High)
+    if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
       {
 	const tgba* s = scc_filter(sim, true);
 	delete sim;
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index cfe92f135..35d44d7b6 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -102,6 +102,7 @@ namespace spot
     bool degen_cache_;
     int simul_;
     int simul_limit_;
+    int scc_filter_;
   };
   /// @}
 }