ltlsynt: replace -x specification-decomposition by --decompose

* bin/ltlsynt.cc: Implement the option, and enable it by default.
* doc/org/ltlsynt.org, doc/org/ltlsynt.tex, bin/spot-x.cc, NEWS:
Document it.
* tests/core/ltlsynt.test: Adjust test cases.

NEWS

@@ -33,10 +33,10 @@ New in spot 2.9.8.dev (not yet released)
   - ltlsynt --verify checks the computed strategy or aiger circuit
     against the specification.
 
-  - ltlsynt -x "specification-decomposition" determines whether or not
+  - ltlsynt --decompose=yes|no determines whether or not the algorithm
-    the algorithm should try to decompose the formula into subformulas
+    should try to decompose the formula into subformulas and generate
-    and generate a strategy for each subformula before recombining them
+    a strategy for each subformula before recombining them into a
-    into a circuit.
+    circuit.
 
   - ltlsynt -x "minimization-level=[0-5]" determines how to minimize
     the strategy (a monitor). 0, no minimization; 1, regular DFA

bin/ltlsynt.cc

@@ -44,6 +44,7 @@ enum
 {
   OPT_ALGO = 256,
   OPT_CSV,
+  OPT_DECOMPOSE,
   OPT_INPUT,
   OPT_OUTPUT,
   OPT_PRINT,
@@ -75,6 +76,9 @@ static const argp_option options[] =
       " acceptance condition, then use LAR to turn to parity,"
       " then split;"
       " \"lar.old\": old version of LAR, for benchmarking.\n", 0 },
+    { "decompose", OPT_DECOMPOSE, "yes|no", 0,
+      "whether to decompose the specification as multiple output-disjoint "
+      "problems to solve independently (enabled by default)", 0},
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output options:", 20 },
     { "print-pg", OPT_PRINT, nullptr, 0,
@@ -164,6 +168,20 @@ static spot::game_info::solver const solver_types[] =
 };
 ARGMATCH_VERIFY(solver_args, solver_types);
 
+static const char* const decompose_args[] =
+  {
+    "yes", "true", "enabled", "1",
+    "no", "false", "disabled", "0",
+    nullptr
+  };
+static bool decompose_values[] =
+  {
+    true, true, true, true,
+    false, false, false, false,
+  };
+ARGMATCH_VERIFY(decompose_args, decompose_values);
+bool opt_decompose_ltl = true;
+
 namespace
 {
   auto str_tolower = [] (std::string s)
@@ -253,8 +271,6 @@ namespace
         gi->bv->total_time = sw.stop();
     };
 
-    bool opt_decompose_ltl =
-      gi->opt.get("specification-decomposition", 0);
     std::vector<spot::formula> sub_form;
     std::vector<std::set<spot::formula>> sub_outs;
     if (opt_decompose_ltl)
@@ -269,7 +285,7 @@ namespace
     // When trying to split the formula, we can apply transformations that
     // increase its size. This is why we will use the original formula if it
     // has not been cut.
-    if (!opt_decompose_ltl || sub_form.empty())
+    if (sub_form.empty())
     {
       sub_form = { f };
       sub_outs.resize(1);
@@ -563,6 +579,10 @@ parse_opt(int key, char *arg, struct argp_state *)
       if (not gi->bv)
         gi->bv = spot::game_info::bench_var();
       break;
+    case OPT_DECOMPOSE:
+      opt_decompose_ltl = XARGMATCH("--decompose", arg,
+                                    decompose_args, decompose_values);
+      break;
     case OPT_INPUT:
       {
         std::istringstream aps(arg);

bin/spot-x.cc

@@ -238,8 +238,6 @@ sets.  By default this is only enabled when options -B or -S are used.") },
 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, "Synthesis options:", 0 },
-    { DOC("specification-decomposition",
-          "Set to 0 to disable specification decomposition.  Default is 1.") },
     { DOC("minimization-level",
           "Specify how AIGER circuits should be simplified.  "
           "(0) no simplification, "

doc/org/ltlsynt.org

@@ -121,12 +121,12 @@ game using Zielonka's recursive algorithm.  The process can be pictured as follo
 
 [[file:ltlsynt.svg]]
 
-LTL decomposition is described by [[https://arxiv.org/abs/2103.08459][Finkbeiner, Geier, and Passing]], and
+LTL decomposition consist in splitting the specification into multiple
-can be disabled by passing option =-x specification-decomposition=0=.
+smaller constraints on disjoint subsets of the output values (as
-The idea is to split the specification into multiple smaller
+described by [[https://arxiv.org/abs/2103.08459][Finkbeiner, Geier, and Passing]]), solve those constraints
-constraints on disjoint subsets of the output values, solve those
+separately, and then combine them while encoding the AIGER circuit.
-constraints separately, and then combine them while encoding the AIGER
+This is enabled by default, but can be disabled by passing option
-circuit.
+=--decompose=no=.
 
 The ad hoc construction on the top is just a shortcut for some type of
 constraints that can be solved directly by converting the constraint

doc/org/ltlsynt.tex

@@ -20,6 +20,7 @@
                       lproc/.style={proc,text width=2cm},
                       choice/.style={circle,fill=yellow!20,inner sep=0,minimum size=2mm,draw},
                       algoopt/.style={postaction={decorate,decoration={text along path, raise=1mm,text={|\ttfamily\small|#1}}}},
+                      algooptd/.style={postaction={decorate,decoration={text along path, raise=-1em,text={|\ttfamily\small|#1}}}},
                       outopt/.style={postaction={decorate,decoration={text along path, text align=right,raise=1mm,text={|\ttfamily\small|#1}}}},
                       ]
     \node[proc] (transSD) {translate to NBA};
@@ -64,7 +65,7 @@
     \draw[->] (decomp) to[out=-45,in=180] (bypassin);
     \draw[->,gray] (decomp) to[out=-55,in=180] ($(bypassin.west)+(0,-0.33)$);
     \draw[->,gray] (decomp) to[out=-65,in=180] ($(bypassin.west)+(0,-0.66)$);
-    \draw[->,gray] (decomp) to[out=-75,in=180] ($(bypassin.west)+(0,-1)$);
+    \draw[->,gray,algooptd={-{}-decompose}] (decomp) to[out=-75,in=180] ($(bypassin.west)+(0,-1)$);
     \draw[->] (bypassin) -- (algoin);
 
     \node[lproc, right=of detSD, xshift=4mm] (solve) {solve\linebreak parity game};

tests/core/ltlsynt.test

@@ -458,7 +458,7 @@ o0 o0
 o1 o1
 EOF
 ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
-  --aiger=isop --algo=lar -x"specification-decomposition=0" >out
+        --aiger=isop --algo=lar --decompose=no >out
 diff out exp
 
 cat >exp <<EOF
@@ -492,7 +492,10 @@ o0 o0
 o1 o1
 EOF
 ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
-  --aiger=isop --algo=lar -x"specification-decomposition=1" >out
+  --aiger=isop --algo=lar --decompose=yes >out
+diff out exp
+ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
+  --aiger=isop --algo=lar >out
 diff out exp
 
 # Issue #477