From b082df201f6b01a30ba9e4979e26cad33942f442 Mon Sep 17 00:00:00 2001
From: Jerome Dubois <jdubois@lrde.epita.fr>
Date: Fri, 19 Feb 2021 17:09:22 +0100
Subject: [PATCH] postproc: Add the new simulation in do_simul()

* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add the new simulation
  in do_simul().
* bin/man/spot-x.x, bin/spot-x.cc: Add documentation for
  SPOT_SIMULATION_REDUCTION environnement variable and the simul-method
  fine tunning option.
* NEWS: Mention the changes.
---
 NEWS                      |  9 +++++++++
 bin/man/spot-x.x          |  6 ++++++
 bin/spot-x.cc             |  6 +++++-
 spot/twaalgos/postproc.cc | 25 +++++++++++++++++++++++--
 spot/twaalgos/postproc.hh |  1 +
 5 files changed, 44 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index b4d8a42d5..f100b1734 100644
--- a/NEWS
+++ b/NEWS
@@ -182,6 +182,15 @@ New in spot 2.9.6.dev (not yet released)
     outgoing edge of some state.  It can be used together with
     purge_dead_states() to remove selected states.
 
+  - Add reduce_direct_sim(), reduce_direct_cosim() and reduce_iterated()
+    (and their state based acceptance version, reduce_direct_sim_sba(),
+    reduce_direct_cosim_sba() and reduce_iterated_sba()), a new reduction
+    based simulation using a matrix-based implementation. This new version
+    should be faster than the signature-based BDD implementation in most
+    cases. By default, the old one is used. This behavior can be changed by
+    setting SPOT_SIMULATION_REDUCTION environment variable or using the
+    "-x simul-method=..." option (see spot-x(7)).
+
   Python:
 
   - Bindings for functions related to games.
diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x
index 69d8e35d9..51ea95edf 100644
--- a/bin/man/spot-x.x
+++ b/bin/man/spot-x.x
@@ -234,6 +234,12 @@ This variable is used by the \fB--check=stutter-invariance\fR and
 \fB--stutter-invariant\fR options, but it is ignored by
 \fB--check=stutter-sensitive-example\fR.
 
+.TP
+\fBSPOT_SIMULATION_REDUCTION\fR
+Choose which simulation based reduction to use: 1 force signature-based
+BDD implementation, 2 force matrix-based implementation and 0 is default, a
+heuristic is used to choose which implementation to use.
+
 .TP
 \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
 These variables control in which directory temporary files (e.g.,
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index 63170ad4b..b6b0d57c9 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -211,7 +211,11 @@ sets sat-minimize to 1 if not set differently.") },
           "Set to 1 to instruct the SAT-minimization procedure to produce \
 a TGBA where all outgoing transition of a state have the same acceptance \
 sets.  By default this is only enabled when option -B is used.") },
-    { nullptr, 0, nullptr, 0, nullptr, 0 }
+    { DOC("simul-method",
+          "Chose which simulation based reduction to use: 1 force the \
+signature-based BDD implementation, 2 force matrix-based and 0, the default, \
+is a heristic wich choose which implementation to use.") },
+    { nullptr, 0, nullptr, 0, nullptr, 0 },
   };
 
 const struct argp_child children[] =
diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc
index 3da54a67e..dcd27a68b 100644
--- a/spot/twaalgos/postproc.cc
+++ b/spot/twaalgos/postproc.cc
@@ -74,6 +74,7 @@ namespace spot
         det_max_states_ = opt->get("det-max-states", -1);
         det_max_edges_ = opt->get("det-max-edges", -1);
         simul_ = opt->get("simul", -1);
+        simul_method_ = opt->get("simul-method", -1);
         scc_filter_ = opt->get("scc-filter", -1);
         ba_simul_ = opt->get("ba-simul", -1);
         tba_determinisation_ = opt->get("tba-det", 0);
@@ -115,19 +116,39 @@ namespace spot
     if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states())
       return a;
 
+    if (opt == 0)
+      return a;
+
+    static unsigned sim = [&]()
+    {
+      if (simul_method_ != -1)
+        return simul_method_;
+
+      char* s = getenv("SPOT_SIMULATION_REDUCTION");
+      return s ? *s - '0' : 0;
+    }();
+
+    if (sim == 2)
+      opt += 3;
+
     // FIXME: simulation-based reduction how have work-arounds for
     // non-separated sets, so we can probably try them.
     if (!has_separate_sets(a))
       return a;
     switch (opt)
       {
-      case 0:
-        return a;
       case 1:
         return simulation(a);
       case 2:
         return cosimulation(a);
       case 3:
+        return iterated_simulations(a);
+      case 4:
+        return reduce_direct_sim(a);
+      case 5:
+        return reduce_direct_cosim(a);
+      case 6:
+        return reduce_iterated(a);
       default:
         return iterated_simulations(a);
       }
diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh
index 375bf43b4..b6e77ffec 100644
--- a/spot/twaalgos/postproc.hh
+++ b/spot/twaalgos/postproc.hh
@@ -252,6 +252,7 @@ namespace spot
     int det_max_states_ = -1;
     int det_max_edges_ = -1;
     int simul_ = -1;
+    int simul_method_ = -1;
     int scc_filter_ = -1;
     int ba_simul_ = -1;
     bool tba_determinisation_ = false;