translator: add tls-max-states option

This restricts the time spent in translating sub-formulas for
implication tests by limiting the associated automata to 64 states by
default.  Doing so this does worsen any test case, and actually remove
all calls the BuDDy's GC in bdd.test.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh,
spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh,
spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or
its constraint via an output_aborter.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/bdd.test: Adjust and augment test case.

NEWS

@@ -104,6 +104,13 @@ New in spot 2.9.4.dev  (not yet released)
     automaton, but we should not waste too much space and time trying
     that.
 
+    spot::translator additionally honor the following new variable:
+
+     tls-max-states  Maximum number of states of automata involved in
+                     automata-based implication checks for formula
+                     simplifications.  Defaults to 64.
+
+
   Python:
 
   - Bindings for functions related to parity games.

bin/spot-x.cc

@@ -44,6 +44,9 @@ static const argp_option options[] =
 (2) additionally allows automata-based implication checks, (3) enables \
 more rules based on automata-based implication checks.  The default value \
 depends on the --low, --medium, or --high settings.") },
+    { DOC("tls-max-states",
+          "Maximum number of states of automata involved in automata-based \
+implication checks for formula simplifications.  Defaults to 64.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("ltl-split", "Set to 0 to disable the translation of automata \
 as product or sum of subformulas.") },

spot/tl/contain.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2012, 2014-2016, 2018, 2019 Laboratoire de Recherche
+// Copyright (C) 2009-2012, 2014-2016, 2018-2020 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -52,12 +52,15 @@ namespace spot
 
   language_containment_checker::language_containment_checker
   (bdd_dict_ptr dict, bool exprop, bool symb_merge,
-   bool branching_postponement, bool fair_loop_approx)
+   bool branching_postponement, bool fair_loop_approx,
+   unsigned max_states)
     : dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
       branching_postponement_(branching_postponement),
       fair_loop_approx_(fair_loop_approx),
       translated_(new trans_map_)
   {
+    if (max_states)
+      aborter_ = std::make_unique<output_aborter>(max_states);
   }
 
   language_containment_checker::~language_containment_checker()
@@ -104,7 +107,11 @@ namespace spot
       return false;
     trim_common_Xs(l, g);
     record_* rl = register_formula_(l);
+    if (!rl->translation)
+      return false;
     record_* rg = register_formula_(g);
+    if (!rg->translation)
+      return false;
     return incompatible_(rl, rg);
   }
 
@@ -139,7 +146,11 @@ namespace spot
     if (l == g)
       return true;
     record_* rl = register_formula_(l);
+    if (!rl->translation)
+      return false;
     record_* rg = register_formula_(g);
+    if (!rg->translation)
+      return false;
     if (isomorphism_checker::are_isomorphic(rl->translation, rg->translation))
       return true;
     return contained(l, g) && contained(g, l);
@@ -153,7 +164,8 @@ namespace spot
       return &i->second;
 
     auto e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_,
-                            branching_postponement_, fair_loop_approx_);
+                            branching_postponement_, fair_loop_approx_,
+                            nullptr, nullptr, false, aborter_.get());
     return &translated_->emplace(f, std::move(e)).first->second;
   }
 }

spot/tl/contain.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2016, 2019 Laboratoire de Recherche
+// Copyright (C) 2011-2016, 2019, 2020 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -24,6 +24,7 @@
 
 #include <spot/tl/formula.hh>
 #include <spot/twa/bdddict.hh>
+#include <spot/twaalgos/powerset.hh>
 
 namespace spot
 {
@@ -41,7 +42,8 @@ namespace spot
                                  bool exprop = false,
                                  bool symb_merge = true,
                                  bool branching_postponement = false,
-                                 bool fair_loop_approx = false);
+                                 bool fair_loop_approx = false,
+                                 unsigned max_states = 0U);
 
     ~language_containment_checker();
 
@@ -72,5 +74,6 @@ namespace spot
     /* Translation Maps */
     trans_map_* translated_;
     tl_simplifier_cache* c_;
+    std::unique_ptr<const output_aborter> aborter_ = nullptr;
   };
 }

spot/tl/simplify.cc

@@ -70,7 +70,8 @@ namespace spot
 
     tl_simplifier_cache(const bdd_dict_ptr& d,
                          const tl_simplifier_options& opt)
-      : dict(d), options(opt), lcc(d, true, true, false, false)
+      : dict(d), options(opt),
+        lcc(d, true, true, false, false, opt.containment_max_states)
     {
       options.containment_checks |= options.containment_checks_stronger;
       options.event_univ |= options.favor_event_univ;

spot/tl/simplify.hh

@@ -93,6 +93,9 @@ namespace spot
     // &,|, and X operators.  Only rewrite Xor and Equiv under
     // temporal operators.
     bool keep_top_xor;
+    // If greater than 0, bound the number of states used by automata
+    // in containment checks.
+    unsigned containment_max_states = 0;
   };
 
   // fwd declaration to hide technical details.

spot/twaalgos/ltl2tgba_fm.cc

@@ -1947,7 +1947,8 @@ namespace spot
   ltl_to_tgba_fm(formula f2, const bdd_dict_ptr& dict,
                  bool exprop, bool symb_merge, bool branching_postponement,
                  bool fair_loop_approx, const atomic_prop_set* unobs,
-                 tl_simplifier* simplifier, bool unambiguous)
+                 tl_simplifier* simplifier, bool unambiguous,
+                 const output_aborter* aborter)
   {
     tl_simplifier* s = simplifier;
 
@@ -2051,6 +2052,13 @@ namespace spot
     dest_map dests;
     while (!formulae_to_translate.empty())
       {
+        if (aborter && aborter->too_large(a))
+          {
+            if (!simplifier)
+              delete s;
+            return nullptr;
+          }
+
         // Pick one formula.
         formula now = *formulae_to_translate.begin();
         formulae_to_translate.erase(formulae_to_translate.begin());

spot/twaalgos/ltl2tgba_fm.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2019 Laboratoire de
+// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -26,6 +26,7 @@
 #include <spot/twa/twagraph.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/twaalgos/powerset.hh>
 
 namespace spot
 {
@@ -73,6 +74,10 @@ namespace spot
   /// \param unambiguous When true, unambigous TGBA will be produced
   /// using the trick described in \cite benedikt.13.tacas .
   ///
+  /// \param aborter When given, aborts the construction whenever the
+  /// constructed automaton would become larger than specified by the
+  /// output_aborter.
+  ///
   /// \return A spot::twa_graph that recognizes the language of \a f.
   SPOT_API twa_graph_ptr
   ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict,
@@ -81,5 +86,6 @@ namespace spot
                  bool fair_loop_approx = false,
                  const atomic_prop_set* unobs = nullptr,
                  tl_simplifier* simplifier = nullptr,
-                 bool unambiguous = false);
+                 bool unambiguous = false,
+                 const output_aborter* aborter = nullptr);
 }

spot/twaalgos/translate.cc

@@ -60,11 +60,14 @@ namespace spot
         gf_guarantee_set_ = true;
       }
     ltl_split_ = opt->get("ltl-split", 1);
+    int tls_max_states = opt->get("tls-max-states", 64);
+    tls_max_states_ = std::max(0, tls_max_states);
   }
 
   void translator::build_simplifier(const bdd_dict_ptr& dict)
   {
     tl_simplifier_options options(false, false, false);
+    options.containment_max_states = tls_max_states_;
     switch (level_)
       {
       case High:

spot/twaalgos/translate.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -154,6 +154,7 @@ namespace spot
     bool gf_guarantee_ = true;
     bool gf_guarantee_set_ = false;
     bool ltl_split_;
+    unsigned tls_max_states_ = 0;
     const option_map* opt_;
   };
   /// @}

tests/core/bdd.test

@@ -23,7 +23,8 @@ set -e
 
 # Make sure that setting the SPOT_BDD_TRACE envvar actually does
 # something.
-genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D >out 2>err
+genltl --kr-nlogn=2 |
+    SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err
 cat err
 grep spot: out && exit 1
 grep 'spot: BDD package initialized' err
@@ -34,3 +35,10 @@ test 11 = `grep -c 'spot: BDD GC' err`
 # Minimal size for this automaton.
 # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf
 test "147,207" = `autfilt --stats=%s,%e out`
+
+# With the default value of tls-max-states, no GC is needed
+genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err
+cat err
+grep 'spot: BDD package initialized' err
+test 0 = `grep -c 'spot: BDD GC' err`
+test "147,207" = `cat out`