postproc: introduce dba-simul, and have simul=0 disable all *-simul

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement the
dba-simul option, and disable ba-simul, dba-simul, dpa-simul,
det-simul when simul=0.
* bin/ltlsynt.cc: Adjust.
* bin/spot-x.cc: Document dba-simul and adjust other variables.
* tests/core/minusx.test: Add some test.

NEWS

@@ -164,8 +164,14 @@ New in spot 2.9.6.dev (not yet released)
 
       dpa-simul      Set to 0/1 to disable/enable simulation-based
                      reduction performed after running a Safra-like
-                     determinization to optain a DPA.  By default, it
-                     is activated at all levels but --low.
+                     determinization to optain a DPA.  By default, it is
+                     only disabled with --low or if simul=0.
+
+      dba-simul      Set to 0/1 to disable/enable simulation-based
+                     reduction performed after running the
+                     powerset-like construction (enabled by option
+                     tba-det) to obtain a DBA.  By default, it is
+                     only disabled with --low or if simul=0.
 
     spot::translator additionally honor the following new variables:
 
@@ -184,8 +190,15 @@ New in spot 2.9.6.dev (not yet released)
                       cannot be disabled.  (This feature is not new, but
                       was not tunable before.)
 
+  - In addition the to above new variables, the default value for
+    ba-simul (controling how degeneralized automata are reduced) and
+    for det-simul (simulation-based optimization of the
+    determinization) is now equal to the default value of simul.  This
+    changes allows "-x simul=0" to disable all of "ba-simul",
+    "dba-simul", "dpa-simul", and "det-simul" at once.
+
   - tgba_powerset() now takes an extra optional argument to specify a
-    list of accepting sinks states if some are known.  Doing so can
+    list of accepting sinks states if some arex known.  Doing so can
     cut the size of the powerset automaton by 2^|sinks| in favorable
     cases.
 

bin/ltlsynt.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2021 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -587,11 +587,10 @@ int
 main(int argc, char **argv)
 {
   return protected_main(argv, [&] {
-      extra_options.set("simul", 0);
-      extra_options.set("ba-simul", 0);
-      extra_options.set("det-simul", 0);
-      extra_options.set("tls-impl", 1);
-      extra_options.set("wdba-minimize", 2);
+      extra_options.set("simul", 0);     // no simulation, except...
+      extra_options.set("dpa-simul", 1); // ... after determinization
+      extra_options.set("tls-impl", 1);  // no automata-based implication check
+      extra_options.set("wdba-minimize", 2); // minimize only syntactic oblig
       const argp ap = { options, parse_opt, nullptr,
                         argp_program_doc, children, nullptr, nullptr };
       if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))

bin/spot-x.cc

@@ -123,15 +123,16 @@ will be returned.")},
     { DOC("det-scc", "Set to 0 to disable scc-based optimizations in \
 the determinization algorithm.") },
     { DOC("det-simul", "Set to 0 to disable simulation-based optimizations in \
-the determinization algorithm.  (Do not confuse this with option dpa-simul,  \
+the determinization algorithm.  This is enabled by default, unless \"simul\" \
+is set to 0.  (Do not confuse this with option \"dpa-simul\",  \
 which runs a simulation-based reduction after determinization.)") },
     { DOC("det-stutter", "Set to 0 to disable optimizations based on \
 the stutter-invariance in the determinization algorithm.") },
     { DOC("dpa-simul", "Set to 1 to enable simulation-based reduction after \
 running a Safra-like determinization to obtain a DPA, or 0 to disable.  By \
-default is is enabled at all levels except low.  (Do not confuse this with \
-option det-simul, which uses a simulation-based optimizations during \
-the determinization.)") },
+default this is disabled at low level or if parameter \"simul\" is set to 0.  \
+(Do not confuse this with option det-simul, which uses a simulation-based \
+optimizations during the determinization.)") },
     { DOC("gen-reduce-parity", "When the postprocessor routines are \
 configured to output automata with any kind of acceptance condition, \
 but they happen to process an automaton with parity acceptance, they \
@@ -160,7 +161,8 @@ only to Büchi automata for historical reasons; it really applies to any \
 state-based acceptance nowadays. \
 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.") },
+The default is the value of parameter \"simul\" in --high mode, and 0 \
+therwise.") },
     { DOC("simul-max", "Number of states above which simulation-based \
 reductions are skipped. Defaults to 4096.  Set to 0 to disable.  This \
 applies to all simulation-based optimization, including thoses of the \
@@ -193,6 +195,9 @@ or when det-max-states is set.") },
     { DOC("tba-det", "Set to 1 to attempt a powerset determinization \
 if the TGBA is not already deterministic.  Doing so will degeneralize \
 the automaton.  This is disabled by default, unless sat-minimize is set.") },
+    { DOC("dba-simul", "Set to 1 to enable simulation-based reduction after \
+running the powerset determinization enabled by \"tba-det\".  By default this \
+is disabled at low level or if parameter \"simul\" is set to 0.") },
     { DOC("sat-minimize",
           "Set to a value between 1 and 4 to enable SAT-based minimization \
 of deterministic ω-automata.  If the input has n states, a SAT solver is \

spot/twaalgos/postproc.cc

@@ -69,13 +69,14 @@ namespace spot
         degen_lowinit_ = opt->get("degen-lowinit", 0);
         degen_remscc_ = opt->get("degen-remscc", 1);
         det_scc_ = opt->get("det-scc", 1);
-        det_simul_ = opt->get("det-simul", 1);
+        det_simul_ = opt->get("det-simul", -1);
         det_stutter_ = opt->get("det-stutter", 1);
         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);
         dpa_simul_ = opt->get("dpa-simul", -1);
+        dba_simul_ = opt->get("dba-simul", -1);
         scc_filter_ = opt->get("scc-filter", -1);
         ba_simul_ = opt->get("ba-simul", -1);
         tba_determinisation_ = opt->get("tba-det", 0);
@@ -266,9 +267,14 @@ namespace spot
     if (simul_ < 0)
       simul_ = (level_ == Low) ? 1 : 3;
     if (ba_simul_ < 0)
-      ba_simul_ = (level_ == High) ? 3 : 0;
+      ba_simul_ = (level_ == High) ? simul_ : 0;
+    int detaut_simul_default = (level_ != Low && simul_ > 0) ? 1 : 0;
     if (dpa_simul_ < 0)
-      dpa_simul_ = (level_ != Low) ? 1 : 0;
+      dpa_simul_ = detaut_simul_default;
+    if (dba_simul_ < 0)
+      dba_simul_ = detaut_simul_default;
+    if (det_simul_ < 0)
+      det_simul_ = simul_ > 0;
     if (scc_filter_ < 0)
       scc_filter_ = 1;
     if (type_ == BA)
@@ -530,7 +536,7 @@ namespace spot
             // There is no point in running the reverse simulation on
             // a deterministic automaton, since all prefixes are
             // unique.
-            dba = simulation(tmp);
+            dba = do_simul(tmp, dba_simul_);
           }
         if (dba && PREF_ == Deterministic)
           {

spot/twaalgos/postproc.hh

@@ -247,7 +247,7 @@ namespace spot
     bool degen_lowinit_ = false;
     bool degen_remscc_ = true;
     bool det_scc_ = true;
-    bool det_simul_ = true;
+    int det_simul_ = -1;
     bool det_stutter_ = true;
     int det_max_states_ = -1;
     int det_max_edges_ = -1;
@@ -255,6 +255,7 @@ namespace spot
     int simul_method_ = -1;
     int simul_trans_pruning_ = 512;
     int dpa_simul_ = -1;
+    int dba_simul_ = -1;
     int scc_filter_ = -1;
     int ba_simul_ = -1;
     bool tba_determinisation_ = false;

tests/core/minusx.test

@@ -44,3 +44,13 @@ test 6,0 = `ltl2tgba -x wdba-det-max=4 --stats=%s,%d "$f"`
 f=`genltl --ms-phi-s=2`
 test 484 -eq `ltl2tgba -P -D --stats=%s "$f"`
 test 484 -lt `ltl2tgba -P -D -x simul-max=512 --stats=%s "$f"`
+
+# Illustrate issue #455: the simulation-based reduction applied before
+# tba-det can cause the creation of a DBA that is harder to reduce.
+# Hopefully and improvement to the simulation-based reduction should
+# reduce the third automaton in the same way as the fourth.
+L=ltl2tgba
+test 4,7 = `$L -xtba-det,simul=0 -D 'F(!p0 | GFp1)' --stats=%s,%e`
+test 4,8 = `$L -xtba-det,simul=1,dba-simul=0 -D 'F(!p0 | GFp1)' --stats=%s,%e`
+test 3,7 = `$L -xtba-det,simul=1 -D 'F(!p0 | GFp1)' --stats=%s,%e`
+test 2,4 = `$L -xtba-det,simul=0,dba-simul=1 -D 'F(!p0 | GFp1)' --stats=%s,%e`