From 60dbeb11286b1f26b9b2cbed53157b107cb88515 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 12 Apr 2010 16:39:28 +0200
Subject: [PATCH] Adjust ltl2tgba.py to call scc_filter() with the "full"
 option as appropriate.

* wrap/python/spot.i (spot::scc_filter): Make it available.
* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
Use the "full" option unless the show_degen_png or
show_never_claim are set.  Also reduce_scc the default.
---
 ChangeLog                       | 10 ++++++++++
 wrap/python/cgi-bin/ltl2tgba.in |  8 ++++++--
 wrap/python/spot.i              |  3 +++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 3e90d87c6..5a08cafd9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2010-04-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Adjust ltl2tgba.py to call scc_filter() with the "full" option as
+	appropriate.
+
+	* wrap/python/spot.i (spot::scc_filter): Make it available.
+	* wrap/python/cgi-bin/ltl2tgba.in (reduce_scc): Call scc_filter.
+	Use the "full" option unless the show_degen_png or
+	show_never_claim are set.  Also reduce_scc the default.
+
 2010-04-08  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/ltlvisit/basicreduce.cc: Typo in comment.
diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in
index 384d3df52..e5bf7129d 100755
--- a/wrap/python/cgi-bin/ltl2tgba.in
+++ b/wrap/python/cgi-bin/ltl2tgba.in
@@ -258,7 +258,7 @@ options_reduce = [
     ('reduce_langcont',     'language containment' + new,                  0),
     ]
 options_aut_reduce = [
-    ('reduce_scc',          'prune unaccepting SCCs' + new,                0),
+    ('reduce_scc',          'prune unaccepting SCCs' + new,                1),
     ]
 options_debug = [
     ('show_parse',          'show traces during parsing',                  0),
@@ -564,7 +564,11 @@ elif trans_taa:
     automaton = spot.ltl_to_taa(f, dict, refined_rules)
 
 if reduce_scc:
-    automaton = spot.reduc_tgba_sim(automaton, spot.Reduce_Scc)
+    # Do not suppress all useless acceptance conditions if
+    # degeneralization is requested: keeping those that lead to
+    # accepting states usually help.
+    automaton = spot.scc_filter(automaton, not (show_degen_png or
+                                                show_never_claim))
 
 print 'done.</p>'
 sys.stdout.flush()
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index cebfa02b5..249052837 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -91,6 +91,7 @@
 #include "tgbaalgos/reductgba_sim.hh"
 #include "tgbaalgos/rundotdec.hh"
 #include "tgbaalgos/save.hh"
+#include "tgbaalgos/sccfilter.hh"
 #include "tgbaalgos/stats.hh"
 
 using namespace spot::ltl;
@@ -151,6 +152,7 @@ using namespace spot;
 %feature("new") spot::reduc_tgba_sim;
 %feature("new") spot::emptiness_check_instantiator::construct;
 %feature("new") spot::emptiness_check_instantiator::instanciate;
+%feature("new") spot::scc_filter;
 
 // Help SWIG with namespace lookups.
 #define ltl spot::ltl
@@ -182,6 +184,7 @@ using namespace spot;
 %include "tgbaalgos/reductgba_sim.hh"
 %include "tgbaalgos/rundotdec.hh"
 %include "tgbaalgos/save.hh"
+%include "tgbaalgos/sccfilter.hh"
 %include "tgbaalgos/stats.hh"
 #undef ltl