translate, simplify: limit containment checks of n-ary operators

Fixes #521.

* spot/tl/simplify.cc, spot/tl/simplify.hh,
spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add an option
to limit automata-based implication checks of n-ary operators when too
many operands are used.  Defaults to 16.
* bin/spot-x.cc, NEWS, doc/tl/tl.tex: Document it.
* tests/core/bdd.test: Disable the limit for this test.

NEWS

@@ -6,6 +6,11 @@ New in spot 2.11.2.dev  (not yet released)
     slower than necessary because the translator was configured to
     favor determinism unnecessarily.  (Issue #521.)
 
+  - Automata-based implication checks for f&g and f|g could be
+    very slow when those n-ary operator had two many arguments.
+    They have been limited to 16 operands, but this value can be changed
+    with option -x tls-max-ops=N.  (Issue #521 too.)
+
 New in spot 2.11.2  (2022-10-26)
 
   Command-line tools:

bin/spot-x.cc

@@ -47,6 +47,9 @@ 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.") },
+    { DOC("tls-max-ops",
+          "Maximum number of operands in n-ary opertors (or, and) on which \
+implication-based simplifications are attempted.  Defaults to 16.") },
     { 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.") },

doc/tl/tl.tex

@@ -1926,6 +1926,12 @@ Many of the above rules were collected from the
 literature~\cite{somenzi.00.cav,tauriainen.03.tr,babiak.12.tacas} and
 sometimes generalized to support operators such as $\M$ and $\W$.
 
+The first six rules, about n-ary operators $\AND$ and $\OR$, are
+implemented for $n$ operands by testing each operand against all
+other.  To prevent the complexity to escalate, this is only performed
+with up to 16 operands.  That value can be changed in
+``\verb|tl_simplifier_options::containment_max_ops|''.
+
 The following rules mix implication-based checks with formulas that
 are pure eventualities ($e$) or that are purely universal ($u$).
 

spot/tl/simplify.cc

@@ -2507,8 +2507,11 @@ namespace spot
         unsigned mos = mo.size();
 
         if ((opt_.synt_impl | opt_.containment_checks)
-            && mo.is(op::Or, op::And))
+            && mo.is(op::Or, op::And)
+            && (opt_.containment_max_ops == 0
+                || opt_.containment_max_ops >= mos))
           {
+            bool is_and = mo.is(op::And);
             // Do not merge these two loops, as rewritings from the
             // second loop could prevent rewritings from the first one
             // to trigger.
@@ -2520,7 +2523,6 @@ namespace spot
                 // if fo => !fi, then fi & fo = false
                 // if !fi => fo, then fi | fo = true
                 // if !fo => fi, then fi | fo = true
-                bool is_and = mo.is(op::And);
                 if (c_->implication_neg(fi, fo, is_and)
                     || c_->implication_neg(fo, fi, is_and))
                   return recurse(is_and ? formula::ff() : formula::tt());
@@ -2531,8 +2533,8 @@ namespace spot
                 formula fo = mo.all_but(i);
                 // if fi => fo, then fi | fo = fo
                 // if fo => fi, then fi & fo = fo
-                if ((mo.is(op::Or) && c_->implication(fi, fo))
+                if (((!is_and) && c_->implication(fi, fo))
-                    || (mo.is(op::And) && c_->implication(fo, fi)))
+                    || (is_and && c_->implication(fo, fi)))
                   {
                     // We are about to pick fo, but hold on!
                     // Maybe we actually have fi <=> fo, in

spot/tl/simplify.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2017, 2019, 2020 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011-2022 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -96,6 +96,9 @@ namespace spot
     // If greater than 0, bound the number of states used by automata
     // in containment checks.
     unsigned containment_max_states = 0;
+    // If greater than 0, maximal number of terms in a multop to perform
+    // containment checks on this multop.
+    unsigned containment_max_ops = 16;
   };
 
   // fwd declaration to hide technical details.

spot/twaalgos/translate.cc

@@ -62,8 +62,8 @@ 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, opt->get("tls-max-states", 64));
-    tls_max_states_ = std::max(0, tls_max_states);
+    tls_max_ops_ = std::max(0, opt->get("tls-max-ops", 16));
     exprop_ = opt->get("exprop", -1);
     branchpost_ = opt->get("branch-post", -1);
   }
@@ -72,6 +72,7 @@ namespace spot
   {
     tl_simplifier_options options(false, false, false);
     options.containment_max_states = tls_max_states_;
+    options.containment_max_ops = tls_max_ops_;
     switch (level_)
       {
       case High:

spot/twaalgos/translate.hh

@@ -155,7 +155,8 @@ namespace spot
     bool gf_guarantee_set_ = false;
     bool ltl_split_;
     int branchpost_ = -1;
-    unsigned tls_max_states_ = 0;
+    unsigned tls_max_states_ = 64;
+    unsigned tls_max_ops_ = 16;
     int exprop_;
     const option_map* opt_;
   };

tests/core/bdd.test

@@ -24,20 +24,21 @@ set -e
 # Make sure that setting the SPOT_BDD_TRACE envvar actually does
 # something.
 genltl --kr-n=3 |
-    SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err
+  SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0,tls-max-ops=0 -D >out 2>err
 cat err
 grep spot: out && exit 1
 grep 'spot: BDD package initialized' err
 # This value below, which is the number of time we need to garbage
 # collect might change if we improve the tool or change the way BuDDy
 # is initialized.
-test 2 = `grep -c 'spot: BDD GC' err`
+test 15 = `grep -c 'spot: BDD GC' err`
 # Minimal size for this automaton.
 # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf
 test "2240,4214" = `autfilt --stats=%s,%e out`
 
 # With the default value of tls-max-states, no GC is needed
-genltl --kr-n=3 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err
+genltl --kr-n=3 |
+  SPOT_BDD_TRACE=1 ltl2tgba -D -x tls-max-ops=0 --stats=%s,%e >out 2>err
 cat err
 grep 'spot: BDD package initialized' err
 test 0 = `grep -c 'spot: BDD GC' err`