From 8d5d453efaa1c68446b992305777a0b32896605e Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Tue, 24 Jul 2018 01:01:11 +0200 Subject: [PATCH] ltlsynt: new algorithm, based on LAR * bin/ltlsynt.cc: here * tests/core/ltlsynt.test: test it * NEWS: document it --- NEWS | 13 +++-- bin/ltlsynt.cc | 116 +++++++++++++++++++++++++++------------- tests/core/ltlsynt.test | 4 +- 3 files changed, 88 insertions(+), 45 deletions(-) diff --git a/NEWS b/NEWS index 2a5bf4893..9ae023490 100644 --- a/NEWS +++ b/NEWS @@ -34,13 +34,16 @@ New in spot 2.6.0.dev (not yet released) - "ltlfilt --suspendable" is now a synonym for "ltlfilt --universal --eventual". - - ltlsynt now has two algorithms for synthesis: + - ltlsynt now has three algorithms for synthesis: --algo=sd is the historical one. The automaton of the formula is split to separate inputs and outputs, then - determinized. - --algo=ds the automaton of the formula is determinized, then - split to separate inputs and outputs. - In both cases, the obtained parity game is solved using + determinized (with Safra construction). + --algo=ds the automaton of the formula is determinized (Safra), + then split to separate inputs and outputs. + --alog=lar translate the formula to a deterministic automaton + with an arbitrary acceptance condition, then turn it + into a parity automaton using LAR, and split it. + In all three cases, the obtained parity game is solved using Zielonka algorithm. Calude's quasi-polynomial time algorithm has been dropped as it was not used. diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 301978bc9..73e5ea839 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -46,6 +46,7 @@ #include #include #include +#include enum { @@ -72,8 +73,11 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { "algo", OPT_ALGO, "ds|sd", 0, "choose the algorithm for synthesis:\n" - " - sd: split then determinize (default)\n" - " - ds: determinize then split", 0 }, + " - sd: split then determinize with Safra (default)\n" + " - ds: determinize (Safra) then split\n" + " - lar: translate to a deterministic automaton with arbitrary" + " acceptance condition, then use LAR to turn to parity," + " then split", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, @@ -115,19 +119,22 @@ bool opt_print_aiger(false); enum solver { DET_SPLIT, - SPLIT_DET + SPLIT_DET, + LAR, }; static char const *const solver_args[] = { "detsplit", "ds", "splitdet", "sd", + "lar", nullptr }; static solver const solver_types[] = { DET_SPLIT, DET_SPLIT, - SPLIT_DET, SPLIT_DET + SPLIT_DET, SPLIT_DET, + LAR, }; ARGMATCH_VERIFY(solver_args, solver_types); @@ -194,9 +201,13 @@ namespace spot::colorize_parity_here(dpa, true); spot::change_parity_here(dpa, spot::parity_kind_max, spot::parity_style_odd); - bool max, odd; - dpa->acc().is_parity(max, odd); - assert(max && odd); + assert(( + [&dpa]() -> bool + { + bool max, odd; + dpa->acc().is_parity(max, odd); + return max && odd; + }())); assert(spot::is_deterministic(dpa)); return dpa; } @@ -271,6 +282,12 @@ namespace spot::process_timer timer; timer.start(); + if (opt_solver == LAR) + { + trans_.set_type(spot::postprocessor::Generic); + trans_.set_pref(spot::postprocessor::Deterministic); + } + auto aut = trans_.run(&f); if (verbose) std::cerr << "translating formula done" << std::endl; @@ -294,38 +311,61 @@ namespace } spot::twa_graph_ptr dpa = nullptr; - if (opt_solver == DET_SPLIT) + switch (opt_solver) { - auto tmp = to_dpa(aut); - if (verbose) - std::cerr << "determinization done\n" - << "dpa has " << tmp->num_states() << " states" << std::endl; - tmp->merge_states(); - if (verbose) - std::cerr << "simulation done\n" - << "dpa has " << tmp->num_states() << " states" << std::endl; - dpa = split_2step(tmp, all_inputs); - if (verbose) - std::cerr << "split inputs and outputs done\n" - << "automaton has " << dpa->num_states() << " states" - << std::endl; - spot::colorize_parity_here(dpa, true); - } - else - { - auto split = split_2step(aut, all_inputs); - if (verbose) - std::cerr << "split inputs and outputs done\n" - << "automaton has " << split->num_states() << " states" - << std::endl; - dpa = to_dpa(split); - if (verbose) - std::cerr << "determinization done\n" - << "dpa has " << dpa->num_states() << " states" << std::endl; - dpa->merge_states(); - if (verbose) - std::cerr << "simulation done\n" - << "dpa has " << dpa->num_states() << " states" << std::endl; + case DET_SPLIT: + { + auto tmp = to_dpa(aut); + if (verbose) + std::cerr << "determinization done\n" + << "dpa has " << tmp->num_states() << " states" << std::endl; + tmp->merge_states(); + if (verbose) + std::cerr << "simulation done\n" + << "dpa has " << tmp->num_states() << " states" << std::endl; + dpa = split_2step(tmp, all_inputs); + if (verbose) + std::cerr << "split inputs and outputs done\n" + << "automaton has " << dpa->num_states() << " states" + << std::endl; + spot::colorize_parity_here(dpa, true); + break; + } + case SPLIT_DET: + { + auto split = split_2step(aut, all_inputs); + if (verbose) + std::cerr << "split inputs and outputs done\n" + << "automaton has " << split->num_states() << " states" + << std::endl; + dpa = to_dpa(split); + if (verbose) + std::cerr << "determinization done\n" + << "dpa has " << dpa->num_states() << " states" << std::endl; + dpa->merge_states(); + if (verbose) + std::cerr << "simulation done\n" + << "dpa has " << dpa->num_states() << " states" << std::endl; + break; + } + case LAR: + { + dpa = split_2step(aut, all_inputs); + dpa->merge_states(); + if (verbose) + std::cerr << "split inputs and outputs done\n" + << "automaton has " << dpa->num_states() << " states" + << std::endl; + dpa = spot::to_parity(dpa); + spot::cleanup_parity_here(dpa); + spot::change_parity_here(dpa, spot::parity_kind_max, + spot::parity_style_odd); + if (verbose) + std::cerr << "LAR construction done\n" + << "dpa has " << dpa->num_states() << " states" << std::endl; + spot::colorize_parity_here(dpa, true); + break; + } } auto owner = complete_env(dpa); auto pg = spot::parity_game(dpa, owner); diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 0fea27156..babc27238 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -184,7 +184,7 @@ for i in 0 1 7 8 9; do OUT=$(eval echo \$OUT$i) EXP=$(eval echo \$EXP$i) - for algo in sd ds; do + for algo in sd ds lar; do test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \ --algo=$algo) done @@ -199,7 +199,7 @@ for i in 2 3 4 5 6 10; do ltl2tgba -f "!($F)" > negf_aut$i # test ltlsynt - for algo in sd ds; do + for algo in sd ds lar; do ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true REAL=`head -1 out$i` test $REAL = $EXP