postproc: option to wdba-minimize only when sure

Fixes #15.

* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1.  Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.

NEWS

@@ -7,6 +7,17 @@ New in spot 2.9.0.dev (not yet released)
          ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
     now produces a 16-state automaton (instead of 31 in Spot 2.9).
 
+  - Option '-x wdba-minize=N' used to accept N=0 (off), or N=1 (on).
+    It can now take three values:
+      0: never attempt this optimization,
+      1: always try to determinize and minimize automata as WDBA,
+         and check (if needed) that the result is correct,
+      2: determinize and minimize automata as WDBA only if it is known
+         beforehand (by cheap syntactic means) that the result will be
+         correct (e.g., the input formula is a syntactic obligation).
+    The default is 1 in "--high" mode, 2 in "--medium" mode or in
+    "--deterministic --low" mode, and 0 in other "--low" modes.
+
   Library:
 
   - product_xor() and product_xnor() are two new versions of the

bin/spot-x.cc

@@ -152,8 +152,10 @@ abstracted as atomic propositions during the translation to automaton. \
 This relabeling can speeds the translation if a few Boolean subformulas \
 use a large number of atomic propositions.  By default N=4.  Setting \
 this value to 0 will disable the rewriting.") },
-    { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization.  \
-Enabled by default.") },
+    { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization, to 1 to \
+always try it, or 2 to attempt it only on syntactic obligations or on automata \
+that are weak and deterministic.  The default is 1 in --high mode, else 2 in \
+--medium or --deterministic modes, else 0 in --low mode.") },
     { 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.") },

spot/twaalgos/minimize.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2010-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -567,6 +567,16 @@ namespace spot
     return product(min_aut, aut_neg)->is_empty();
   }
 
+  bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f,
+                                             formula f)
+  {
+    // WDBA-minimization necessarily work for obligations
+    return ((f && f.is_syntactic_obligation())
+            // Weak deterministic automata are obligations
+            || (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
+            // Guarantee automata are obligations as well.
+            || is_terminal_automaton(aut_f));
+  }
 
   twa_graph_ptr
   minimize_obligation(const const_twa_graph_ptr& aut_f,
@@ -580,12 +590,7 @@ namespace spot
         ("minimize_obligation() does not support alternation");
 
     bool minimization_will_be_correct = false;
-    // WDBA-minimization necessarily work for obligations
-    if ((f && f.is_syntactic_obligation())
-        // Weak deterministic automata are obligations
-        || (aut_f->prop_weak() && is_deterministic(aut_f))
-        // Guarantee automata are obligations as well.
-        || is_terminal_automaton(aut_f))
+    if (minimize_obligation_garanteed_to_work(aut_f, f))
       {
         minimization_will_be_correct = true;
       }

spot/twaalgos/minimize.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018, 2019
-// Laboratoire de Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009-2016, 2018-2020 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -116,5 +116,23 @@ namespace spot
                       const_twa_graph_ptr aut_neg_f = nullptr,
                       bool reject_bigger = false,
                       const output_aborter* aborter = nullptr);
+
+  /// \brief Whether calling minimize_obligation is sure to work
+  ///
+  /// This checks whether \a f is a syntactic obligation, or if \a
+  /// aut_f obviously corresponds to an obligation (for instance if
+  /// this is a terminal automaton, or if it is both weak and
+  /// deterministic).  In this case, calling minimize_obligation()
+  /// should not be a waste of time, as it will return a new
+  /// automaton.
+  ///
+  /// If this function returns false, the input property might still
+  /// be a pathological obligation.  The only way to know is to call
+  /// minimize_obligation(), but as it is less likely, you might
+  /// decide to save time.
+  SPOT_API
+  bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f,
+                                             formula f = nullptr);
+
   /// @}
 }

spot/twaalgos/postproc.cc

@@ -83,7 +83,7 @@ namespace spot
         sat_acc_ = opt->get("sat-acc", 0);
         sat_states_ = opt->get("sat-states", 0);
         state_based_ = opt->get("state-based", 0);
-        wdba_minimize_ = opt->get("wdba-minimize", 1);
+        wdba_minimize_ = opt->get("wdba-minimize", -1);
         gen_reduce_parity_ = opt->get("gen-reduce-parity", 1);
 
         if (sat_acc_ && sat_minimize_ == 0)
@@ -371,9 +371,19 @@ namespace spot
     output_aborter* aborter =
       (det_max_states_ >= 0 || det_max_edges_ >= 0) ? &aborter_ : nullptr;
 
-    // (Small,Low) is the only configuration where we do not run
-    // WDBA-minimization.
-    if ((PREF_ != Small || level_ != Low) && wdba_minimize_)
+    int wdba_minimize = wdba_minimize_;
+    if (wdba_minimize == -1)
+      {
+        if (level_ == High)
+          wdba_minimize = 1;
+        else if (level_ == Medium || PREF_ == Deterministic)
+          wdba_minimize = 2;
+        else
+          wdba_minimize = 0;
+      }
+    if (wdba_minimize == 2)
+      wdba_minimize = minimize_obligation_garanteed_to_work(a, f);
+    if (wdba_minimize)
       {
         bool reject_bigger = (PREF_ == Small) && (level_ <= Medium);
         dba = minimize_obligation(a, f, nullptr, reject_bigger, aborter);

spot/twaalgos/postproc.hh

@@ -253,7 +253,7 @@ namespace spot
     int sat_states_ = 0;
     int gen_reduce_parity_ = 1;
     bool state_based_ = false;
-    bool wdba_minimize_ = true;
+    int wdba_minimize_ = -1;
   };
   /// @}
 }

tests/core/genltl.test

@@ -132,12 +132,12 @@ genltl --kr-n2=1..2 --kr-nlogn=1..2 --kr-n=1..2 --gxf-and=0..3 --fxg-or=0..3 \
        --pps-arbiter-standard=2..3 --pps-arbiter-strict=2..3 --format=%F=%L,%f |
     ltl2tgba --low --det -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
-kv-psi=1,15
-kv-psi=2,106
-kr-nlogn=1,19
-kr-nlogn=2,147
-kr-n=1,12
-kr-n=2,82
+kv-psi=1,10
+kv-psi=2,24
+kr-nlogn=1,16
+kr-nlogn=2,44
+kr-n=1,10
+kr-n=2,25
 gxf-and=0,1
 gxf-and=1,1
 gxf-and=2,1

tests/core/ltl2tgba2.test

@@ -458,4 +458,15 @@ res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
 test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
 ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
 
+f='G(p1 | G!p0) M Xp1'
+test "6,1" = `ltl2tgba "$f" --stats=%s,%d`
+test "6,0" = `ltl2tgba -x wdba-minimize=2 "$f" --stats=%s,%d`
+test "6,0" = `ltl2tgba -x wdba-minimize=0 "$f" --stats=%s,%d`
+test "6,0" = `ltl2tgba --med "$f" --stats=%s,%d`
+f='X((p1 & Xp1) M Fp1)'
+test "4,1" = `ltl2tgba -D "$f" --stats=%s,%d`
+test "4,1" = `ltl2tgba -D -x wdba-minimize=2 "$f" --stats=%s,%d`
+test "4,0" = `ltl2tgba -D -x wdba-minimize=0 "$f" --stats=%s,%d`
+test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d`
+
 :