Commit 37d0b0d0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlsynt: use wdba-minimize=2 and ba-simul=0

* bin/ltlsynt.cc: Here.
* tests/core/ltlsynt.test: Add extra test case.
* NEWS: Mention ltlsynt -x and related defaults.
parent 56c8d690
......@@ -21,6 +21,10 @@ New in spot 2.9.0.dev (not yet released)
- ltlsynt learned --algo=ps to use the default conversion to
deterministic parity automata (the same as ltl2tgba -DP'max odd').
- ltlsynt now has a -x option to fine-tune the translation. See the
spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults
to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2.
Library:
- product_xor() and product_xnor() are two new versions of the
......
......@@ -670,8 +670,10 @@ main(int argc, char **argv)
{
return protected_main(argv, [&] {
extra_options.set("simul", 0);
extra_options.set("ba-simul", 0);
extra_options.set("det-simul", 0);
extra_options.set("tls-impl", 1);
extra_options.set("wdba-minimize", 2);
const argp ap = { options, parse_opt, nullptr,
argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
......
......@@ -321,3 +321,9 @@ diff out exp
ltlsynt -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))'
ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
grep 'DPA has 14 states' err
ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
grep 'DPA has 12 states' err
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment