diff --git a/NEWS b/NEWS index fed67a1ca..f4f142902 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,9 @@ New in spot 2.9.0.dev (not yet released) The default is 1 in "--high" mode, 2 in "--medium" mode or in "--deterministic --low" mode, and 0 in other "--low" modes. + - ltlsynt learned --algo=ps to use the default conversion to + deterministic parity automata (the same as ltl2tgba -DP'max odd'). + Library: - product_xor() and product_xnor() are two new versions of the diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index e805a9f3e..0c1ce9aae 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -74,10 +74,11 @@ static const argp_option options[] = " propositions", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, - { "algo", OPT_ALGO, "ds|sd|lar|lar.old", 0, + { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0, "choose the algorithm for synthesis:\n" - " - sd: split then determinize with Safra (default)\n" - " - ds: determinize (Safra) then split\n" + " - sd: translate to tgba, split, then determinize (default)\n" + " - ds: translate to tgba, determinize, then split\n" + " - ps: translate to dpa, then split\n" " - lar: translate to a deterministic automaton with arbitrary" " acceptance condition, then use LAR to turn to parity," " then split\n" @@ -136,6 +137,7 @@ enum solver { DET_SPLIT, SPLIT_DET, + DPA_SPLIT, LAR, LAR_OLD, }; @@ -144,6 +146,7 @@ static char const *const solver_names[] = { "ds", "sd", + "ps", "lar", "lar.old" }; @@ -152,6 +155,7 @@ static char const *const solver_args[] = { "detsplit", "ds", "splitdet", "sd", + "dpasplit", "ps", "lar", "lar.old", nullptr @@ -160,6 +164,7 @@ static solver const solver_types[] = { DET_SPLIT, DET_SPLIT, SPLIT_DET, SPLIT_DET, + DPA_SPLIT, DPA_SPLIT, LAR, LAR_OLD, }; @@ -354,10 +359,21 @@ namespace spot::stopwatch sw; bool want_time = verbose || opt_csv; - if (opt_solver == LAR || opt_solver == LAR_OLD) + switch (opt_solver) { + case LAR: + case LAR_OLD: trans_.set_type(spot::postprocessor::Generic); trans_.set_pref(spot::postprocessor::Deterministic); + break; + case DPA_SPLIT: + trans_.set_type(spot::postprocessor::ParityMaxOdd); + trans_.set_pref(spot::postprocessor::Deterministic + | spot::postprocessor::Colored); + break; + case DET_SPLIT: + case SPLIT_DET: + break; } if (want_time) @@ -423,6 +439,29 @@ namespace << tmp->num_states() << " states\n"; break; } + case DPA_SPLIT: + { + if (want_time) + sw.start(); + aut->merge_states(); + if (want_time) + paritize_time = sw.stop(); + if (verbose) + std::cerr << "simplification done in " << paritize_time + << " seconds\nDPA has " << aut->num_states() + << " states\n"; + if (want_time) + sw.start(); + dpa = split_2step(aut, all_inputs); + spot::colorize_parity_here(dpa, true); + if (want_time) + split_time = sw.stop(); + if (verbose) + std::cerr << "split inputs and outputs done in " << split_time + << " seconds\nautomaton has " + << dpa->num_states() << " states\n"; + break; + } case SPLIT_DET: { if (want_time) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 1584b8bf5..d677cf6fc 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -118,6 +118,20 @@ ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp +cat >exp < GFb' --verbose --algo=ps 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + cat >exp < GFb' --csv=FILE || : ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : + ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || : ltlsynt --algo=lar $opts 'FGc <-> GF(!b&XXb)' --csv='>>FILE' || : ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || : - test 5 = `wc -l < FILE` + test 6 = `wc -l < FILE` # Make sure all lines in FILE have the same number of comas sed 's/[^,]//g' < FILE | ( read first @@ -242,7 +257,7 @@ for i in 2 3 4 5 6 10; do ltl2tgba -f "!($F)" > negf_aut$i # test ltlsynt - for algo in sd ds lar lar.old; do + for algo in sd ds ps lar lar.old; do ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true REAL=`head -1 out$i` test $REAL = $EXP