From 4c2791e042fbbb5424a1c23e3373da7c91ae19a8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 26 Apr 2013 11:03:47 +0200
Subject: [PATCH] postproc: Perform simulation on the BA in --high mode.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Do simulation
on the BA produced in --high mode.
* src/bin/spot-x.cc: Document the ba-simul option that can be used
to disable it.
---
 src/bin/spot-x.cc         |  5 +++++
 src/tgbaalgos/postproc.cc | 32 +++++++++++++++++++++++---------
 src/tgbaalgos/postproc.hh |  3 ++-
 3 files changed, 30 insertions(+), 10 deletions(-)

diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc
index c097ffa19..c667b1075 100644
--- a/src/bin/spot-x.cc
+++ b/src/bin/spot-x.cc
@@ -67,6 +67,11 @@ number of \"don't care\" transitions considered by the \
 \"don't care\"-simulation algorithm. A negative value (the default) \
 does not enforce any limit. Note that if there are N \"don't care\" \
 transitions, the algorithm may potentially test 2^N configurations.") },
+    { DOC("ba-simul", "Set to 0 to disable simulation-based reductions \
+on the Büchi automaton (i.e., after degeneralization has been performed). \
+Set to 1 to use only direct simulation.  Set to 2 to use only reverse \
+simulation.  Set to 3 to iterate both direct and reverse simulations.   \
+The default is 3 in --high mode, and 0 otherwise.") },
     { 0, 0, 0, 0, 0, 0 }
   };
 
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index 279319bac..5c77324e8 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), scc_filter_(-1)
+      simul_(-1), scc_filter_(-1), ba_simul_(-1)
   {
     if (opt)
       {
@@ -56,12 +56,13 @@ namespace spot
 	simul_ = opt->get("simul", -1);
 	simul_limit_ = opt->get("simul-limit", -1);
 	scc_filter_ = opt->get("scc-filter", -1);
+	ba_simul_ = opt->get("ba-simul", -1);
       }
   }
 
-  const tgba* postprocessor::do_simul(const tgba* a)
+  const tgba* postprocessor::do_simul(const tgba* a, int opt)
   {
-    switch (simul_)
+    switch (opt)
       {
       case 0:
 	return a;
@@ -86,7 +87,14 @@ namespace spot
 				 degen_order_,
 				 degen_cache_);
     delete a;
-    return d;
+    if (ba_simul_ <= 0)
+      return d;
+
+    const tgba* s = do_simul(d, ba_simul_);
+    if (s != d)
+      delete d;
+
+    return s;
   }
 
   const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
@@ -96,6 +104,8 @@ namespace spot
 
     if (simul_ < 0)
       simul_ = (level_ == Low) ? 1 : 3;
+    if (ba_simul_ < 0)
+      ba_simul_ = (level_ == High) ? 3 : 0;
     if (scc_filter_ < 0)
       scc_filter_ = 1;
 
@@ -124,7 +134,7 @@ namespace spot
 	if (pref_ == Any)
 	  return a;
 
-	const tgba* sim = do_simul(a);
+	const tgba* sim = do_simul(a, simul_);
 	if (a == sim)
 	  // simulation was disabled.
 	  return a;
@@ -174,15 +184,19 @@ namespace spot
     // at hard levels if we want a small output.
     if (!wdba || (level_ == High && pref_ == Small))
       {
-	sim = do_simul(a);
+	sim = do_simul(a, simul_);
+
+	if (sim != a)
+	  delete a;
 
 	// Degeneralize the result of the simulation if needed.
 	if (type_ == BA)
 	  sim = do_degen(sim);
       }
-
-    if (sim != a)
-      delete a;
+    else
+      {
+	delete a;
+      }
 
     if (wdba && sim)
       {
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index 849039872..c5575fc6c 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -90,7 +90,7 @@ namespace spot
     const tgba* run(const tgba* input_disown, const ltl::formula* f);
 
   protected:
-    const tgba* do_simul(const tgba* input);
+    const tgba* do_simul(const tgba* input, int opt);
     const tgba* do_degen(const tgba* input);
 
     output_type type_;
@@ -103,6 +103,7 @@ namespace spot
     int simul_;
     int simul_limit_;
     int scc_filter_;
+    int ba_simul_;
   };
   /// @}
 }