diff --git a/NEWS b/NEWS index 85610c261..2a5bf4893 100644 --- a/NEWS +++ b/NEWS @@ -34,6 +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: + --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 + Zielonka algorithm. Calude's quasi-polynomial time algorithm has + been dropped as it was not used. + Bugs fixed: - scc_info::split_on_sets() did not correctly register the diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index e04e71a73..301978bc9 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -70,10 +70,10 @@ static const argp_option options[] = " propositions", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, - { "algo", OPT_ALGO, "qp|rec", 0, - "choose the parity game algorithm, valid ones are rec (Zielonka's" - " recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial" - " time algorithm)", 0 }, + { "algo", OPT_ALGO, "ds|sd", 0, + "choose the algorithm for synthesis:\n" + " - sd: split then determinize (default)\n" + " - ds: determinize then split", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, @@ -112,27 +112,26 @@ bool opt_print_pg(false); bool opt_real(false); bool opt_print_aiger(false); -// FIXME rename options to choose the algorithm enum solver { - QP, - REC + DET_SPLIT, + SPLIT_DET }; static char const *const solver_args[] = { - "qp", "quasi-polynomial", - "recursive", + "detsplit", "ds", + "splitdet", "sd", nullptr }; static solver const solver_types[] = { - QP, QP, - REC, + DET_SPLIT, DET_SPLIT, + SPLIT_DET, SPLIT_DET }; ARGMATCH_VERIFY(solver_args, solver_types); -static solver opt_solver = REC; +static solver opt_solver = SPLIT_DET; static bool verbose = false; namespace @@ -187,7 +186,8 @@ namespace { // if the input automaton is deterministic, degeneralize it to be sure to // end up with a parity automaton - auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split)); + auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split), + false, true, true, false); dpa->merge_edges(); if (opt_print_pg) dpa = spot::sbacc(dpa); @@ -293,12 +293,40 @@ namespace all_outputs &= bdd_ithvar(v); } - auto split = split_2step(aut, all_inputs); - if (verbose) - std::cerr << "split inputs and outputs done" << std::endl; - auto dpa = to_dpa(split); - if (verbose) - std::cerr << "determinization done" << std::endl; + spot::twa_graph_ptr dpa = nullptr; + if (opt_solver == 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); + } + 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; + } auto owner = complete_env(dpa); auto pg = spot::parity_game(dpa, owner); if (verbose) @@ -310,58 +338,33 @@ namespace pg.print(std::cout); return 0; } - switch (opt_solver) - { - case REC: - { - spot::parity_game::strategy_t strategy[2]; - spot::parity_game::region_t winning_region[2]; - pg.solve(winning_region, strategy); - if (winning_region[1].count(pg.get_init_state_number())) - { - std::cout << "REALIZABLE\n"; - if (!opt_real) - { - auto strat_aut = - strat_to_aut(pg, strategy[1], dpa, all_outputs); - // output the winning strategy - if (opt_print_aiger) - spot::print_aiger(std::cout, strat_aut); - else - { - automaton_printer printer; - printer.print(strat_aut, timer); - } - } - return 0; - } + spot::parity_game::strategy_t strategy[2]; + spot::parity_game::region_t winning_region[2]; + pg.solve(winning_region, strategy); + if (winning_region[1].count(pg.get_init_state_number())) + { + std::cout << "REALIZABLE\n"; + if (!opt_real) + { + auto strat_aut = + strat_to_aut(pg, strategy[1], dpa, all_outputs); + + // output the winning strategy + if (opt_print_aiger) + spot::print_aiger(std::cout, strat_aut); else { - std::cout << "UNREALIZABLE\n"; - return 1; + automaton_printer printer; + printer.print(strat_aut, timer); } } - case QP: - if (!opt_real) - { - std::cout << "The quasi-polynomial time algorithm does not" - " implement synthesis yet, use --realizability\n"; - return 2; - } - else if (pg.solve_qp()) - { - std::cout << "REALIZABLE\n"; - return 0; - } - else - { - std::cout << "UNREALIZABLE\n"; - return 1; - } - default: - SPOT_UNREACHABLE(); - return 2; + return 0; + } + else + { + std::cout << "UNREALIZABLE\n"; + return 1; } } }; diff --git a/spot/misc/game.cc b/spot/misc/game.cc index 4db32694e..cbdd81733 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -82,11 +82,6 @@ void parity_game::solve(region_t (&w)[2], strategy_t (&s)[2]) const solve_rec(states_, m, w, s); } -bool parity_game::solve_qp() const -{ - return reachability_game(*this).is_reachable(); -} - parity_game::strategy_t parity_game::attractor(const region_t& subgame, region_t& set, unsigned max_parity, int p, bool attr_max) const @@ -223,166 +218,4 @@ void parity_game::solve_rec(region_t& subgame, unsigned max_parity, subgame.insert(w0[!p].begin(), w0[!p].end()); } -int reachability_state::compare(const state* other) const -{ - auto o = down_cast(other); - assert(o); - if (num_ != o->num()) - return num_ - o->num(); - if (b_ < o->b()) - return -1; - if (b_ > o->b()) - return 1; - return 0; -} - -bool reachability_state::operator<(const reachability_state& o) const -{ - // Heuristic to process nodes with a higher chance of leading to a target - // node first. - assert(b_.size() == o.b().size()); - for (unsigned i = b_.size(); i > 0; --i) - if (b_[i - 1] != o.b()[i - 1]) - return b_[i - 1] > o.b()[i - 1]; - return num_ < o.num(); -} - - - -const reachability_state* reachability_game_succ_iterator::dst() const -{ - // NB: colors are indexed at 1 in Calude et al.'s paper and at 0 in spot - // All acceptance sets are therefore incremented (which is already done by - // max_set), so that 0 can be kept as a special value indicating that no - // i-sequence is tracked at this index. Hence the parity switch in the - // following implementation, compared to the paper. - std::vector b = state_.b(); - unsigned a = it_->acc.max_set(); - assert(a); - unsigned i = -1U; - bool all_even = a % 2 == 0; - for (unsigned j = 0; j < b.size(); ++j) - { - if ((b[j] % 2 == 1 || b[j] == 0) && all_even) - i = j; - else if (b[j] > 0 && a > b[j]) - i = j; - all_even = all_even && b[j] > 0 && b[j] % 2 == 0; - } - if (i != -1U) - { - b[i] = a; - for (unsigned j = 0; j < i; ++j) - b[j] = 0; - } - return new reachability_state(it_->dst, b, !state_.anke()); -} - - - -const reachability_state* reachability_game::get_init_state() const -{ - // b[ceil(log(n + 1))] != 0 implies there is an i-sequence of length - // 2^(ceil(log(n + 1))) >= 2^log(n + 1) = n + 1, so it has to contain a - // cycle. - unsigned i = std::ceil(std::log2(pg_.num_states() + 1)); - return new reachability_state(pg_.get_init_state_number(), - std::vector(i + 1), - false); -} - -reachability_game_succ_iterator* -reachability_game::succ_iter(const state* s) const -{ - auto state = down_cast(s); - return new reachability_game_succ_iterator(pg_, *state); -} - -std::string reachability_game::format_state(const state* s) const -{ - auto state = down_cast(s); - std::ostringstream fmt; - bool first = true; - fmt << state->num() << ", "; - fmt << '['; - for (unsigned b : state->b()) - { - if (!first) - fmt << ','; - else - first = false; - fmt << b; - } - fmt << ']'; - return fmt.str(); -} - -bool reachability_game::is_reachable() -{ - std::set todo{*init_state_}; - while (!todo.empty()) - { - spot::reachability_state v = *todo.begin(); - todo.erase(todo.begin()); - - std::vector succs; - spot::reachability_game_succ_iterator* it = succ_iter(&v); - for (it->first(); !it->done(); it->next()) - succs.push_back(spot::const_reachability_state_ptr(it->dst())); - - if (is_target(v)) - { - c_[v] = 1; - if (mark(v)) - return true; - continue; - } - else if (v.anke()) - c_[v] = 1; - else - c_[v] = succs.size(); - for (auto succ: succs) - { - if (parents_[*succ].empty()) - { - if (*succ != *init_state_) - { - todo.insert(*succ); - parents_[*succ] = { v }; - c_[*succ] = -1U; - } - } - else - { - parents_[*succ].push_back(v); - if (c_[*succ] == 0 && mark(v)) - return true; - } - } - } - return false; -} - -bool reachability_game::mark(const spot::reachability_state& s) -{ - if (c_[s] > 0) - { - --c_[s]; - if (c_[s] == 0) - { - if (s == *init_state_) - return true; - for (auto& u: parents_[s]) - if (mark(u)) - return true; - } - } - return false; -} - -bool reachability_game::is_target(const reachability_state& v) -{ - return v.b().back(); -} - } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index e43123985..64a155ece 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -108,31 +108,6 @@ public: \endverbatim */ void solve(region_t (&w)[2], strategy_t (&s)[2]) const; - /// Whether player 1 has a winning strategy from the initial state. - /// Implements Calude et al.'s quasipolynomial time algorithm. - /** \verbatim - @inproceedings{calude.17.stoc, - author = {Calude, Cristian S. and Jain, Sanjay and Khoussainov, - Bakhadyr and Li, Wei and Stephan, Frank}, - title = {Deciding Parity Games in Quasipolynomial Time}, - booktitle = {Proceedings of the 49th Annual ACM SIGACT Symposium on - Theory of Computing}, - series = {STOC 2017}, - year = {2017}, - isbn = {978-1-4503-4528-6}, - location = {Montreal, Canada}, - pages = {252--263}, - numpages = {12}, - url = {http://doi.acm.org/10.1145/3055399.3055409}, - doi = {10.1145/3055399.3055409}, - acmid = {3055409}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {Muller Games, Parity Games, Quasipolynomial Time Algorithm}, - } - \endverbatim */ - bool solve_qp() const; - private: typedef twa_graph::graph_t::edge_storage_t edge_t; @@ -149,159 +124,4 @@ private: region_t (&w)[2], strategy_t (&s)[2]) const; }; - -class reachability_state: public state -{ -private: - unsigned num_; - std::vector b_; - bool anke_; - -public: - reachability_state(unsigned state, const std::vector& b, - bool anke) - : num_(state), b_(b), anke_(anke) - { - } - - int compare(const state* other) const override; - - bool operator==(const reachability_state& o) const - { - return compare(&o) == 0; - } - - bool operator!=(const reachability_state& o) const - { - return compare(&o) != 0; - } - - bool operator<(const reachability_state& o) const; - - size_t hash() const override - { - size_t hash = wang32_hash(num_); - for (unsigned i = 0; i < b_.size(); ++i) - hash ^= wang32_hash(b_[i]) ^ wang32_hash(i); - return hash; - } - - reachability_state* clone() const override - { - return new reachability_state(*this); - } - - std::vector b() const - { - return b_; - } - - unsigned num() const - { - return num_; - } - - bool anke() const - { - return anke_; - } -}; - -typedef std::shared_ptr - const_reachability_state_ptr; - -struct reachability_state_hash -{ - size_t operator()(const reachability_state& state) const - { - return state.hash(); - } -}; - -class reachability_game_succ_iterator final: public twa_succ_iterator -{ -private: - const parity_game& pg_; - const reachability_state& state_; - internal::edge_iterator it_; - -public: - reachability_game_succ_iterator(const parity_game& pg, - const reachability_state& s) - : pg_(pg), state_(s) - { - } - - bool first() override - { - it_ = pg_.out(state_.num()).begin(); - return it_ != pg_.out(state_.num()).end(); - } - - bool next() override - { - ++it_; - return it_ != pg_.out(state_.num()).end(); - } - - bool done() const override - { - return it_ == pg_.out(state_.num()).end(); - } - - const reachability_state* dst() const override; - - bdd cond() const override - { - return bddtrue; - } - - acc_cond::mark_t acc() const override - { - return {}; - } -}; - -// On-the-fly reachability game interface for a max even parity game such -// that a target is reachable iff there is a memoryless winning strategy -// in the parity game for player 1. -class reachability_game final: public twa -{ -private: - typedef std::unordered_map wincount_t; - typedef std::unordered_map, - spot::reachability_state_hash> parents_t; - - const parity_game& pg_; - // number of successors that need to have a winning strategy in order for - // a given node to have a winning strategy. - wincount_t c_; - parents_t parents_; - const_reachability_state_ptr init_state_; // cache - -public: - - reachability_game(const parity_game& pg) - : twa(std::make_shared()), pg_(pg) - { - init_state_ = std::shared_ptr(get_init_state()); - } - - const reachability_state* get_init_state() const override; - - reachability_game_succ_iterator* succ_iter(const state* s) const override; - - std::string format_state(const state* s) const override; - - bool is_reachable(); - -private: - bool mark(const spot::reachability_state& s); - - bool is_target(const reachability_state& s); - -}; - } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 8efc4948c..0fea27156 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -104,7 +104,11 @@ diff out exp cat >exp < GFb' --verbose --realizability 2> out @@ -179,10 +183,11 @@ for i in 0 1 7 8 9; do IN=$(eval echo \$IN$i) OUT=$(eval echo \$OUT$i) EXP=$(eval echo \$EXP$i) - test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \ - --algo=rec) - test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \ - --algo=qp) + + for algo in sd ds; do + test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \ + --algo=$algo) + done done for i in 2 3 4 5 6 10; do @@ -190,11 +195,18 @@ for i in 2 3 4 5 6 10; do IN=$(eval echo \$IN$i) OUT=$(eval echo \$OUT$i) EXP=$(eval echo \$EXP$i) - ltlsynt -f "$F" --ins="$IN" --outs="$OUT" > out$i - REAL=`head -1 out$i` - test $REAL = $EXP - tail -n +2 out$i > res$i + ltl2tgba -f "!($F)" > negf_aut$i - # check that the L(strategy) is included in L(F) - autfilt -q -v --intersect=negf_aut$i res$i + + # test ltlsynt + for algo in sd ds; do + ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true + REAL=`head -1 out$i` + test $REAL = $EXP + tail -n +2 out$i > res$i + # check that the L(strategy) is included in L(F) + autfilt -q -v --intersect=negf_aut$i res$i + # check that all environment actions are possible + autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q + done done