From 37d0b0d04535a436a8298f7266179f4609e97b0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 May 2020 20:32:27 +0200 Subject: [PATCH] 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. --- NEWS | 4 ++++ bin/ltlsynt.cc | 2 ++ tests/core/ltlsynt.test | 6 ++++++ 3 files changed, 12 insertions(+) diff --git a/NEWS b/NEWS index 12d94cfd8..a485d33f9 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 630ed12f5..c82afb00d 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -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)) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 8a0d10a6c..86da4626d 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -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