From af5474d7911bfa4a5861b7e3d005cbcdb3032fdf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 6 Oct 2021 10:50:41 +0200 Subject: [PATCH] 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 | 8 ++++---- bin/ltlsynt.cc | 26 +++++++++++++++++++++++--- bin/spot-x.cc | 2 -- doc/org/ltlsynt.org | 12 ++++++------ doc/org/ltlsynt.tex | 3 ++- tests/core/ltlsynt.test | 7 +++++-- 6 files changed, 40 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index 6807bac61..8284ce0cc 100644 --- a/NEWS +++ b/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 - the algorithm should try to decompose the formula into subformulas - and generate a strategy for each subformula before recombining them - into a circuit. + - ltlsynt --decompose=yes|no determines whether or not the algorithm + should try to decompose the formula into subformulas and generate + a strategy for each subformula before recombining them into a + circuit. - ltlsynt -x "minimization-level=[0-5]" determines how to minimize the strategy (a monitor). 0, no minimization; 1, regular DFA diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 55fd17a8e..9047046ef 100644 --- a/bin/ltlsynt.cc +++ b/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 sub_form; std::vector> 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); diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 9ab5f5e57..4977c8e42 100644 --- a/bin/spot-x.cc +++ b/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, " diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index da80dc9ce..9b62bb587 100644 --- a/doc/org/ltlsynt.org +++ b/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 -can be disabled by passing option =-x specification-decomposition=0=. -The idea is to split the specification into multiple smaller -constraints on disjoint subsets of the output values, solve those -constraints separately, and then combine them while encoding the AIGER -circuit. +LTL decomposition consist in splitting the specification into multiple +smaller constraints on disjoint subsets of the output values (as +described by [[https://arxiv.org/abs/2103.08459][Finkbeiner, Geier, and Passing]]), solve those constraints +separately, and then combine them while encoding the AIGER circuit. +This is enabled by default, but can be disabled by passing option +=--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 diff --git a/doc/org/ltlsynt.tex b/doc/org/ltlsynt.tex index ad9dac962..50cdd3b89 100644 --- a/doc/org/ltlsynt.tex +++ b/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}; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 550080523..a19da2fe9 100644 --- a/tests/core/ltlsynt.test +++ b/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 <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