From 25b8d50cf0d352658d2462c9cd39776176f0107c Mon Sep 17 00:00:00 2001
From: Thomas Badie <badie@lrde.epita.fr>
Date: Mon, 20 Aug 2012 17:34:20 +0200
Subject: [PATCH] Optimize the use of -RRS with -R3.

* src/tgbatest/ltl2tgba.cc: Change the order of the call to the
simulation and the cosimulation.
Call scc_filter when cosimulation is called with -R3.
Call scc_filter when simulation is called with -R3.
---
 src/tgbatest/ltl2tgba.cc | 36 ++++++++++++++++++++++++++++--------
 1 file changed, 28 insertions(+), 8 deletions(-)

diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 555c5cb6b..a69129825 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -1053,6 +1053,23 @@ main(int argc, char** argv)
 	    }
 	}
 
+      if (reduction_dir_sim)
+        {
+          tm.start("Reduction w/ direct simulation");
+          temp_dir_sim = spot::simulation(a);
+          a = temp_dir_sim;
+          tm.stop("Reduction w/ direct simulation");
+	  assume_sba = false;
+          if (scc_filter)
+            {
+              tm.start("reducing A_f w/ SCC");
+              delete aut_scc;
+              aut_scc = a = spot::scc_filter(a, scc_filter_all);
+              tm.stop("reducing A_f w/ SCC");
+              assume_sba = false;
+            }
+        }
+
 
       if (reduction_rev_sim)
         {
@@ -1061,16 +1078,19 @@ main(int argc, char** argv)
           a = temp_rev_sim;
           tm.stop("Reduction w/ reverse simulation");
 	  assume_sba = false;
+
+          if (scc_filter)
+            {
+              tm.start("reducing A_f w/ SCC");
+              delete aut_scc;
+              aut_scc = a = spot::scc_filter(a, scc_filter_all);
+              tm.stop("reducing A_f w/ SCC");
+              assume_sba = false;
+            }
+
+
         }
 
-      if (reduction_dir_sim)
-        {
-          tm.start("Reduction w/ direct simulation");
-          temp_dir_sim = spot::simulation(a);
-          a = temp_dir_sim;
-          tm.stop("Reduction w/ direct simulation");
-	  assume_sba = false;
-        }
 
       if (reduction_iterated_sim)
         {