From efb15a91716aa92b431f7832d3bf919fb82909d9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 3 Mar 2010 08:40:21 +0100
Subject: [PATCH] ltl2tgba: apply -R3 before -D or -DS.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions.  I realized this while looking at experiments from
Rüdiger Ehlers.
---
 ChangeLog                |  9 +++++++++
 THANKS                   |  1 +
 src/tgbatest/ltl2tgba.cc | 21 +++++++++++----------
 3 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 98061a860..27bdd8e41 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2010-03-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	ltl2tgba: apply -R3 before -D or -DS.
+
+	* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
+	degeneralization, because it might remove useless acceptance
+	conditions.  I realized this while looking at experiments from
+	Rüdiger Ehlers.
+
 2010-02-24  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/sanity/style.test: Better fix for the previous error.
diff --git a/THANKS b/THANKS
index 0d8159baf..a5e245bb2 100644
--- a/THANKS
+++ b/THANKS
@@ -5,4 +5,5 @@ Heikki Tauriainen
 Jean-Michel Couvreur
 Jean-Michel Ilié
 Kristin Y. Rozier
+Rüdiger Ehlers
 Yann Thierry-Mieg
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 5214a3332..d4c8b4753 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -800,6 +800,16 @@ main(int argc, char** argv)
 	    }
 	}
 
+      // Remove dead SCCs and useless acceptance conditions before
+      // degeneralization.
+      spot::tgba* aut_scc = 0;
+      if (reduc_aut & spot::Reduce_Scc)
+	{
+	  tm.start("reducing A_f w/ SCC");
+	  a = aut_scc = spot::scc_filter(a);
+	  tm.stop("reducing A_f w/ SCC");
+	}
+
       spot::tgba_tba_proxy* degeneralized = 0;
       spot::tgba_sgba_proxy* state_labeled = 0;
 
@@ -819,17 +829,8 @@ main(int argc, char** argv)
       }
 
       spot::tgba_reduc* aut_red = 0;
-      spot::tgba* aut_scc = 0;
       if (reduc_aut != spot::Reduce_None)
 	{
-
-	  if (reduc_aut & spot::Reduce_Scc)
-	    {
-	      tm.start("reducing A_f w/ SCC");
-	      a = aut_scc = spot::scc_filter(a);
-	      tm.stop("reducing A_f w/ SCC");
-	    }
-
 	  if (reduc_aut & ~spot::Reduce_Scc)
 	    {
 	      tm.start("reducing A_f w/ sim.");
@@ -1132,8 +1133,8 @@ main(int argc, char** argv)
       delete system;
       delete expl;
       delete aut_red;
-      delete aut_scc;
       delete degeneralized;
+      delete aut_scc;
       delete state_labeled;
       delete to_free;
       delete echeck_inst;