ltlsynt: replace -x minimization-lvl=N by --simplify
* bin/ltlsynt.cc: Implement the new option, and make it default to bisimulation with output assignment (a.k.a. bwoa). * NEWS, bin/spot-x.cc, doc/org/ltlsynt.org: Update the documentation. * spot/twaalgos/game.hh: Make bwoa the default. * tests/core/ltlsynt.test: Add and adjust test cases. * tests/python/games.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
af5474d791
commit
0ac5bbc05d
7 changed files with 1538 additions and 1529 deletions
7
NEWS
7
NEWS
|
|
@ -38,11 +38,8 @@ New in spot 2.9.8.dev (not yet released)
|
|||
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
|
||||
minimization; 2, signature based minimization with
|
||||
output assignement; 3, SAT based minimization; 4, 1 then 3;
|
||||
5, 2 then 3.
|
||||
- ltlsynt --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
|
||||
specifies how to simplify the synthesized controler.
|
||||
|
||||
- ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi
|
||||
option, or -b for short. This outputs Büchi automata without
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ enum
|
|||
OPT_PRINT_AIGER,
|
||||
OPT_PRINT_HOA,
|
||||
OPT_REAL,
|
||||
OPT_SIMPLIFY,
|
||||
OPT_VERBOSE,
|
||||
OPT_VERIFY
|
||||
};
|
||||
|
|
@ -78,7 +79,13 @@ static const argp_option options[] =
|
|||
" \"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},
|
||||
"problems to solve independently (enabled by default)", 0 },
|
||||
{ "simplify", OPT_SIMPLIFY, "no|bisim|bwoa|sat|bisim-sat|bwoa-sat", 0,
|
||||
"simplification to apply to the controler (no) nothing, "
|
||||
"(bisim) bisimulation-based reduction, (bwoa) bissimulation-based "
|
||||
"reduction with output assignment, (sat) SAT-based minimization, "
|
||||
"(bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. Defaults "
|
||||
"to 'bwoa'.", 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
|
||||
{ "print-pg", OPT_PRINT, nullptr, 0,
|
||||
|
|
@ -182,6 +189,27 @@ static bool decompose_values[] =
|
|||
ARGMATCH_VERIFY(decompose_args, decompose_values);
|
||||
bool opt_decompose_ltl = true;
|
||||
|
||||
static const char* const simplify_args[] =
|
||||
{
|
||||
"no", "false", "disabled", "0",
|
||||
"bisim", "1",
|
||||
"bwoa", "bisim-with-output-assignment", "2",
|
||||
"sat", "3",
|
||||
"bisim-sat", "4",
|
||||
"bwoa-sat", "5",
|
||||
nullptr
|
||||
};
|
||||
static unsigned simplify_values[] =
|
||||
{
|
||||
0, 0, 0, 0,
|
||||
1, 1,
|
||||
2, 2, 2,
|
||||
3, 3,
|
||||
4, 4,
|
||||
5, 5,
|
||||
};
|
||||
ARGMATCH_VERIFY(simplify_args, simplify_values);
|
||||
|
||||
namespace
|
||||
{
|
||||
auto str_tolower = [] (std::string s)
|
||||
|
|
@ -389,11 +417,12 @@ namespace
|
|||
{
|
||||
spot::stopwatch sw_min;
|
||||
sw_min.start();
|
||||
bool do_split = 3 <= gi->opt.get("minimization-level", 1);
|
||||
unsigned simplify = gi->minimize_lvl;
|
||||
bool do_split = 3 <= simplify;
|
||||
if (do_split)
|
||||
split_2step_fast_here(strat.strat_like,
|
||||
spot::get_synthesis_outputs(strat.strat_like));
|
||||
minimize_strategy_here(strat.strat_like, gi->minimize_lvl);
|
||||
minimize_strategy_here(strat.strat_like, simplify);
|
||||
if (do_split)
|
||||
strat.strat_like = spot::unsplit_2step(strat.strat_like);
|
||||
auto delta = sw_min.stop();
|
||||
|
|
@ -619,6 +648,10 @@ parse_opt(int key, char *arg, struct argp_state *)
|
|||
case OPT_REAL:
|
||||
opt_real = true;
|
||||
break;
|
||||
case OPT_SIMPLIFY:
|
||||
gi->minimize_lvl = XARGMATCH("--simplify", arg,
|
||||
simplify_args, simplify_values);
|
||||
break;
|
||||
case OPT_VERBOSE:
|
||||
gi->verbose_stream = &std::cerr;
|
||||
if (not gi->bv)
|
||||
|
|
@ -632,8 +665,6 @@ parse_opt(int key, char *arg, struct argp_state *)
|
|||
const char* opt = gi->opt.parse_options(arg);
|
||||
if (opt)
|
||||
error(2, 0, "failed to parse --options near '%s'", opt);
|
||||
// Dispatch the options to the gi structure
|
||||
gi->minimize_lvl = gi->opt.get("minimization-level", 1);
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -237,18 +237,6 @@ sets. By default this is only enabled when options -B or -S are used.") },
|
|||
"Chose which simulation based reduction to use: 1 force the \
|
||||
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("minimization-level",
|
||||
"Specify how AIGER circuits should be simplified. "
|
||||
"(0) no simplification, "
|
||||
"(1) bisimulation-based reduction, "
|
||||
"(2) simplification using language inclusion and output assignments, "
|
||||
"(3) exact minimization using a SAT solver, "
|
||||
"(4) bisimulation-based reduction before exact minimization via "
|
||||
"SAT solver, "
|
||||
"(5) simplification using output assignments before exact "
|
||||
"minimization via SAT solver. "
|
||||
"The default value is 1.") },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -136,23 +136,35 @@ Otherwise, conversion to parity game (represented by the blue zone) is
|
|||
done using one of several algorithms specified by the =--algo= option.
|
||||
The game is then solved, producing a strategy if the game is realizable.
|
||||
|
||||
If an =ltlsynt= is in =--realizability= mode, the process stops here
|
||||
If =ltlsynt= is in =--realizability= mode, the process stops here
|
||||
|
||||
In synthesis mode, the strategy is first simplified. How this is done
|
||||
can be fine-tuned with option =--simplify=:
|
||||
#+BEGIN_SRC sh :exports results
|
||||
ltlsynt --help | sed -n '/--simplify=/,/^$/p' | sed '$d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
|
||||
: simplification to apply to the controler (no)
|
||||
: nothing, (bisim) bisimulation-based reduction,
|
||||
: (bwoa) bissimulation-based reduction with output
|
||||
: assignment, (sat) SAT-based minimization,
|
||||
: (bisim-sat) SAT after bisim, (bwoa-sat) SAT after
|
||||
: bwoa. Defaults to 'bwoa'.
|
||||
|
||||
In =--aiger= mode, the strategy is first simplified. How this is done
|
||||
is controled by option =-x minimize-level=N=. See the [[./man/spot-x.7.html][=spot-x=]](7)
|
||||
manpage for details.
|
||||
Finally, the strategy is encoded into [[http://fmv.jku.at/aiger/][AIGER]]. The =--aiger= option can
|
||||
take an argument to specify a type of encoding to use: by default
|
||||
it is =ite= for if-then-else, because it follows the structure of BDD
|
||||
used to encode the conditions in the strategy. An alternative encoding
|
||||
is =isop= where condition are first put into irredundant-sum-of-product,
|
||||
or =both= if both encodings should be tried. Additionally, these optiosn
|
||||
can accept the suffix =+ud= (use dual) to attempt to encode each condition
|
||||
and its negation and keep the smallest one, =+dc= (don't care) to take
|
||||
advantage of /don't care/ values in the output, and one of =+sub0=,
|
||||
=+sub1=, or =+sub2= to test various grouping of variables in the encoding.
|
||||
Multiple encodings can be tried by separating them using commas.
|
||||
For instance =--aiger=isop,isop+dc,isop+ud= will try three different encodings.
|
||||
take an argument to specify a type of encoding to use: by default it
|
||||
is =ite= for if-then-else, because it follows the structure of BDD
|
||||
used to encode the conditions in the strategy. An alternative
|
||||
encoding is =isop= where condition are first put into
|
||||
irredundant-sum-of-product, or =both= if both encodings should be
|
||||
tried. Additionally, these optiosn can accept the suffix =+ud= (use
|
||||
dual) to attempt to encode each condition and its negation and keep
|
||||
the smallest one, =+dc= (don't care) to take advantage of /don't care/
|
||||
values in the output, and one of =+sub0=, =+sub1=, or =+sub2= to test
|
||||
various grouping of variables in the encoding. Multiple encodings can
|
||||
be tried by separating them using commas. For instance
|
||||
=--aiger=isop,isop+dc,isop+ud= will try three different encodings.
|
||||
|
||||
* Other useful options
|
||||
|
||||
|
|
|
|||
|
|
@ -132,7 +132,7 @@ namespace spot
|
|||
game_info()
|
||||
: force_sbacc{false},
|
||||
s{solver::LAR},
|
||||
minimize_lvl{0},
|
||||
minimize_lvl{2},
|
||||
bv{},
|
||||
verbose_stream{nullptr},
|
||||
dict(make_bdd_dict())
|
||||
|
|
|
|||
|
|
@ -156,7 +156,8 @@ i0 a
|
|||
o0 b
|
||||
o1 c
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=isop >out
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
||||
--algo=ds --simplify=no --aiger=isop >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -171,7 +172,7 @@ o0 b
|
|||
o1 c
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
||||
--algo=ds --aiger=isop+dc >out
|
||||
--algo=ds --simplify=no --aiger=isop+dc >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -186,7 +187,8 @@ i0 a
|
|||
o0 b
|
||||
o1 c
|
||||
EOF
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=ite >out
|
||||
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
||||
--algo=ds --simplify=no --aiger=ite >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -380,7 +382,7 @@ State: 2
|
|||
[!0] 2
|
||||
--END--
|
||||
EOF
|
||||
ltlsynt --outs=p0 -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out
|
||||
ltlsynt --outs=p0 -x tls-impl=0 --simpl=no -f '!XXF(p0 & (p0 M Gp0))' > out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -411,6 +413,14 @@ grep 'DPA has 29 states' err
|
|||
ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
|
||||
grep 'DPA has 12 states' err
|
||||
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 5'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 5'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 4'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 4'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2'
|
||||
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4'
|
||||
|
||||
cat >exp <<EOF
|
||||
REALIZABLE
|
||||
aag 34 4 3 2 27
|
||||
|
|
@ -458,7 +468,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 --decompose=no >out
|
||||
--aiger=isop --algo=lar --decompose=no --simpl=no >out
|
||||
diff out exp
|
||||
|
||||
cat >exp <<EOF
|
||||
|
|
@ -492,10 +502,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 --decompose=yes >out
|
||||
--aiger=isop --algo=lar --decompose=yes --simpl=no >out
|
||||
diff out exp
|
||||
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
|
||||
--aiger=isop --algo=lar >out
|
||||
--aiger=isop --algo=lar --simpl=no >out
|
||||
diff out exp
|
||||
|
||||
# Issue #477
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue