From bc7a2865de92990424bc5d8f5b6fe0ae0f58043f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 12 Feb 2013 19:28:13 +0100
Subject: [PATCH] postproc: add some experimental don't care options

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a
"simul-limit" option, and add two new cases to "simul"
for the two don't care simulation
* src/bin/man/ltl2tgba.x: Mention the new options.
---
 src/bin/man/ltl2tgba.x    | 15 ++++++++++++---
 src/tgbaalgos/postproc.cc | 17 ++++++++---------
 src/tgbaalgos/postproc.hh |  1 +
 3 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 95dca4099..5f95f19ac 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -30,6 +30,15 @@ order for each SCC it processes.  This is currently disabled by default.
 \fBsimul\fR
 Set to 0 to disable simulation-based reductions.  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,
-except when option \fB\-\-low\fR is specified, in which case the
-default is 1.
+to iterate both direct and reverse simulations.  Set to 4 to apply
+only "don't care" direct simulation.  Set to 5 to iterate "don't care"
+direct simulation and reverse simulation.  The default is 3, except
+when option \fB\-\-low\fR is specified, in which case the default is
+1.
+.TP
+\fBsimul-limit\fR
+Can be set to a positive integer to cap the 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 \fIN\fR "don't care" transitions, the algorithm may
+potentially test 2^\fIN\fR configurations.
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index dd7e2edef..25feaaca2 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -54,18 +54,12 @@ namespace spot
 	degen_reset_ = opt->get("degen-reset", 1);
 	degen_cache_ = opt->get("degen-lcache", 1);
 	simul_ = opt->get("simul", -1);
+	simul_limit_ = opt->get("simul-limit", -1);
       }
   }
 
   const tgba* postprocessor::do_simul(const tgba* a)
   {
-    // supported values for simul_:
-    // 1 => direct simulation
-    // 2 => reverse-simulation only
-    // 3 => both simulations, iterated
-    if (simul_ < 0)
-      simul_ = (level_ == Low) ? 1 : 3;
-
     switch (simul_)
       {
       case 0:
@@ -77,6 +71,10 @@ namespace spot
       case 3:
       default:
 	return iterated_simulations(a);
+      case 4:
+	return dont_care_simulation(a, simul_limit_);
+      case 5:
+	return dont_care_iterated_simulations(a, simul_limit_);
       }
   }
 
@@ -95,11 +93,12 @@ namespace spot
     if (type_ == TGBA && pref_ == Any && level_ == Low)
       return a;
 
-
+    if (simul_ < 0)
+      simul_ = (level_ == Low) ? 1 : 3;
 
     // Remove useless SCCs.
     {
-      const tgba* s = scc_filter(a, false);
+      const tgba* s = scc_filter(a, simul_ > 3);
       delete a;
       a = s;
     }
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index f099fcf80..cfe92f135 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -101,6 +101,7 @@ namespace spot
     bool degen_order_;
     bool degen_cache_;
     int simul_;
+    int simul_limit_;
   };
   /// @}
 }