From 133896d584a716279925f0f08dd60a9afcadb10a Mon Sep 17 00:00:00 2001 From: philipp Date: Tue, 22 Sep 2020 20:45:34 +0200 Subject: [PATCH] game: reimplement parity game solving * spot/misc/game.cc, spot/misc/game.hh: More efficient implementation of Zielonka's algorithm to solve parity games. Now supports SCC decomposition and efficient handling of certain special cases. * doc/org/concepts.org: Document "strategy" and "state-winner" properties. * bin/ltlsynt.cc, tests/python/paritygame.ipynb: Adjust. * tests/core/ltlsynt.test: Add more tests. --- bin/ltlsynt.cc | 126 +++-- doc/org/concepts.org | 4 +- spot/misc/game.cc | 898 +++++++++++++++++++++++++++------- spot/misc/game.hh | 34 +- tests/core/ltlsynt.test | 33 +- tests/python/paritygame.ipynb | 303 +----------- 6 files changed, 870 insertions(+), 528 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 4c5b10d7c..f9a02e951 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -212,51 +212,101 @@ namespace return dpa; } - // Construct a smaller automaton, filtering out states that are not - // accessible. Also merge back pairs of p --(i)--> q --(o)--> r - // transitions to p --(i&o)--> r. - static spot::twa_graph_ptr - strat_to_aut(const spot::const_twa_graph_ptr& pg, - const spot::strategy_t& strat, - bdd all_outputs) + + spot::twa_graph_ptr + apply_strategy(const spot::twa_graph_ptr& arena, + bdd all_outputs, + bool unsplit, bool keep_acc, bool leave_choice) { - auto aut = spot::make_twa_graph(pg->get_dict()); - aut->copy_ap_of(pg); - unsigned pg_init = pg->get_init_state_number(); - std::vector todo{pg_init}; - std::vector pg2aut(pg->num_states(), -1); + spot::region_t* w_ptr = + arena->get_named_prop("state-winner"); + spot::strategy_t* s_ptr = + arena->get_named_prop("strategy"); + std::vector* sp_ptr = + arena->get_named_prop>("state-player"); + + if (!w_ptr || !s_ptr || !sp_ptr) + throw std::runtime_error("Arena missing state-winner, strategy " + "or state-player"); + + if (!(w_ptr->at(arena->get_init_state_number()))) + throw std::runtime_error("Player does not win initial state, strategy " + "is not applicable"); + + spot::region_t& w = *w_ptr; + spot::strategy_t& s = *s_ptr; + + auto aut = spot::make_twa_graph(arena->get_dict()); + aut->copy_ap_of(arena); + if (keep_acc) + aut->copy_acceptance_of(arena); + + const unsigned unseen_mark = std::numeric_limits::max(); + std::vector todo{arena->get_init_state_number()}; + std::vector pg2aut(arena->num_states(), unseen_mark); aut->set_init_state(aut->new_state()); - pg2aut[pg_init] = aut->get_init_state_number(); + pg2aut[arena->get_init_state_number()] = aut->get_init_state_number(); + bdd out; while (!todo.empty()) { - unsigned s = todo.back(); + unsigned v = todo.back(); todo.pop_back(); - for (auto& e1: pg->out(s)) + // Env edge -> keep all + for (auto &e1: arena->out(v)) { - unsigned i = 0; - for (auto& e2: pg->out(e1.dst)) + assert(w.at(e1.dst)); + if (!unsplit) { - bool self_loop = false; - if (e1.dst == s || e2.dst == e1.dst) - self_loop = true; - if (self_loop || strat.at(e1.dst) == i) - { - bdd out = bdd_satoneset(e2.cond, all_outputs, bddfalse); - if (pg2aut[e2.dst] == -1) - { - pg2aut[e2.dst] = aut->new_state(); - todo.push_back(e2.dst); - } - aut->new_edge(pg2aut[s], pg2aut[e2.dst], - (e1.cond & out), {}); - break; - } - ++i; + if (pg2aut[e1.dst] == unseen_mark) + pg2aut[e1.dst] = aut->new_state(); + aut->new_edge(pg2aut[v], pg2aut[e1.dst], e1.cond, + keep_acc ? e1.acc : spot::acc_cond::mark_t({})); } + // Player strat + auto &e2 = arena->edge_storage(s[e1.dst]); + if (pg2aut[e2.dst] == unseen_mark) + { + pg2aut[e2.dst] = aut->new_state(); + todo.push_back(e2.dst); + } + if (leave_choice) + // Leave the choice + out = e2.cond; + else + // Save only one letter + out = bdd_satoneset(e2.cond, all_outputs, bddfalse); + + aut->new_edge(unsplit ? pg2aut[v] : pg2aut[e1.dst], + pg2aut[e2.dst], + unsplit ? (e1.cond & out):out, + keep_acc ? e2.acc : spot::acc_cond::mark_t({})); } } - aut->purge_dead_states(); + aut->set_named_prop("synthesis-outputs", new bdd(all_outputs)); + // If no unsplitting is demanded, it remains a two-player arena + // We do not need to track winner as this is a + // strategy automaton + if (!unsplit) + { + std::vector& sp_pg = * sp_ptr; + std::vector sp_aut(aut->num_states()); + spot::strategy_t str_aut(aut->num_states()); + for (unsigned i = 0; i < arena->num_states(); ++i) + { + if (pg2aut[i] == unseen_mark) + // Does not appear in strategy + continue; + sp_aut[pg2aut[i]] = sp_pg[i]; + str_aut[pg2aut[i]] = s[i]; + } + aut->set_named_prop("state-player", + new std::vector(std::move(sp_aut))); + aut->set_named_prop("state-winner", + new spot::region_t(aut->num_states(), true)); + aut->set_named_prop("strategy", + new spot::strategy_t(std::move(str_aut))); + } return aut; } @@ -523,22 +573,22 @@ namespace if (want_time) sw.start(); - auto solution = parity_game_solve(dpa); + bool player1winning = solve_parity_game(dpa); if (want_time) solve_time = sw.stop(); if (verbose) std::cerr << "parity game solved in " << solve_time << " seconds\n"; nb_states_parity_game = dpa->num_states(); timer.stop(); - if (solution.player_winning_at(1, dpa->get_init_state_number())) + if (player1winning) { std::cout << "REALIZABLE\n"; if (!opt_real) { if (want_time) sw.start(); - auto strat_aut = - strat_to_aut(dpa, solution.winning_strategy[1], all_outputs); + auto strat_aut = apply_strategy(dpa, all_outputs, + true, false, true); if (want_time) strat2aut_time = sw.stop(); diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 351dca2fe..eb9fef471 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1144,7 +1144,9 @@ Here is a list of named properties currently used inside Spot: | ~rejected-word~ | ~std::string~ | a word rejected by the automaton | | ~simulated-states~ | ~std::vector~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | | ~state-names~ | ~std::vector~ | vector naming each state of the automaton, for display purpose | -| ~state-player~ | ~std::vector~ | the automaton represents a two-player game, and the vector gives the player (0 or 1) associated to each state | +| ~state-player~ | ~std::vector~ | the automaton represents a two-player game, and the vector gives the player (0 or 1) associated to each state | +| ~state-winner~ | ~std::vector~ | vector indicating the player (0 or 1) winning from this state | +| ~strategy~ | ~std::vector~ | vector representing the memoryless strategy of the players in a parity game. The value corrsponds to the edge number of the transition to take. | | ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) | Objects referenced via named properties are automatically destroyed diff --git a/spot/misc/game.cc b/spot/misc/game.cc index 93815069e..ad9c9674b 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -21,6 +21,8 @@ #include #include +#include +#include namespace spot { @@ -47,154 +49,728 @@ namespace spot throw std::runtime_error (std::string(fnname) + ": automaton should define \"state-player\""); + if (owner->size() != arena->num_states()) + throw + (std::string(fnname) + ": \"state-player\" should have " + "as many states as the automaton"); + return owner; } - strategy_t attractor(const const_twa_graph_ptr& arena, - const std::vector* owner, - const region_t& subgame, region_t& set, - unsigned max_parity, int p, - bool attr_max) + // Internal structs + // winning regions for env and player + struct winner_t { - strategy_t strategy; - std::set complement(subgame.begin(), subgame.end()); - for (unsigned s: set) - complement.erase(s); + std::vector has_winner_; + std::vector winner_; - acc_cond::mark_t max_acc({}); - for (unsigned i = 0; i <= max_parity; ++i) - max_acc.set(i); + inline bool operator()(unsigned v, bool p) + { + // returns true if player p wins v + // false otherwise + if (!has_winner_[v]) + return false; - bool once_more; - do - { - once_more = false; - for (auto it = complement.begin(); it != complement.end();) - { - unsigned s = *it; - unsigned i = 0; + return winner_[v] == p; + } - bool is_owned = (*owner)[s] == p; - bool wins = !is_owned; + inline void set(unsigned v, bool p) + { + has_winner_[v] = true; + winner_[v] = p; + } - for (const auto& e: arena->out(s)) + inline void unset(unsigned v) + { + has_winner_[v] = false; + } + + inline bool winner(unsigned v) + { + assert(has_winner_.at(v)); + return winner_[v]; + } + }; // winner_t + + // When using scc decomposition we need to track the + // changes made to the graph + struct edge_stash_t + { + edge_stash_t(unsigned num, unsigned dst, acc_cond::mark_t acc) noexcept + : e_num(num), + e_dst(dst), + e_acc(acc) + { + } + const unsigned e_num, e_dst; + const acc_cond::mark_t e_acc; + }; // edge_stash_t + + // Internal structs used by parity_game + // Struct to change recursive calls to stack + struct work_t + { + work_t(unsigned wstep_, unsigned rd_, unsigned min_par_, + unsigned max_par_) noexcept + : wstep(wstep_), + rd(rd_), + min_par(min_par_), + max_par(max_par_) + { + } + const unsigned wstep, rd, min_par, max_par; + }; // work_t + + // Collects information about an scc + // Used to detect special cases + struct subgame_info_t + { + typedef std::set> all_parities_t; + + subgame_info_t() noexcept + { + } + + subgame_info_t(bool empty, bool one_parity, bool one_player0, + bool one_player1, all_parities_t parities) noexcept + : is_empty(empty), + is_one_parity(one_parity), + is_one_player0(one_player0), + is_one_player1(one_player1), + all_parities(parities) + {}; + bool is_empty; // empty subgame + bool is_one_parity; // only one parity appears in the subgame + // todo : Not used yet + bool is_one_player0; // one player subgame for player0 <-> p==false + bool is_one_player1; // one player subgame for player1 <-> p==true + all_parities_t all_parities; + }; // subgame_info_t + + + // A class to solve parity games + // The current implementation is inspired by + // by oink however without multicore and adapted to transition based + // acceptance + class parity_game + { + public: + + bool solve(const twa_graph_ptr &arena) + { + ensure_parity_game(arena, "solve_parity_game()"); + + // todo check if reordering states according to scc is worth it + set_up(arena); + // Start recursive zielonka in a bottom-up fashion on each scc + subgame_info_t subgame_info; + for (c_scc_idx_ = 0; c_scc_idx_ < info_->scc_count(); ++c_scc_idx_) + { + // Useless SCCs are winning for player 0. + if (!info_->is_useful_scc(c_scc_idx_)) + { + for (unsigned v: c_states()) + w_.set(v, false); + continue; + } + // Convert transitions leaving edges to self-loops + // and check if trivially solvable + subgame_info = fix_scc(); + // If empty, the scc was trivially solved + if (!subgame_info.is_empty) + { + // Check for special cases + if (subgame_info.is_one_parity) + one_par_subgame_solver(subgame_info, max_abs_par_); + else + { + // "Regular" solver + max_abs_par_ = *subgame_info.all_parities.begin(); + w_stack_.emplace_back(0, 0, 0, max_abs_par_); + zielonka(); + } + } + } + // All done -> restore graph, i.e. undo self-looping + restore(); + + if (!std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(), + [](bool b) + { return b; })) + { + for (unsigned n = 0; n < w_.has_winner_.size(); ++n) + std::cerr << "hw[" << n << "]=" << w_.has_winner_[n] << '\n'; + } + + assert(std::all_of(w_.has_winner_.cbegin(), w_.has_winner_.cend(), + [](bool b) + { return b; })); + assert(std::all_of(s_.cbegin(), s_.cend(), + [](unsigned e_idx) + { return e_idx > 0; })); + + // Put the solution as named property + region_t &w = *arena->get_or_set_named_prop("state-winner"); + strategy_t &s = *arena->get_or_set_named_prop("strategy"); + w.swap(w_.winner_); + s.resize(s_.size()); + std::copy(s_.begin(), s_.end(), s.begin()); + + clean_up(); + return w[arena->get_init_state_number()]; + } + + private: + + // Returns the vector of states currently considered + // i.e. the states of the current scc + // c_scc_idx_ is set in the 'main' loop + inline const std::vector &c_states() + { + assert(info_); + return info_->states_of(c_scc_idx_); + } + + void set_up(const twa_graph_ptr &arena) + { + owner_ptr_ = arena->get_named_prop>("state-player"); + arena_ = arena; + unsigned n_states = arena_->num_states(); + // Resize data structures + subgame_.clear(); + subgame_.resize(n_states, unseen_mark); + w_.has_winner_.clear(); + w_.has_winner_.resize(n_states, 0); + w_.winner_.clear(); + w_.winner_.resize(n_states, 0); + s_.clear(); + s_.resize(n_states, -1); + // Init + rd_ = 0; + max_abs_par_ = arena_->get_acceptance().used_sets().max_set() - 1; + info_ = std::make_unique(arena_); + // Every edge leaving an scc needs to be "fixed" + // at some point. + // We store: number of edge fixed, original dst, original acc + change_stash_.clear(); + change_stash_.reserve(info_->scc_count() * 2); + } + + // Checks if an scc is empty and reports the occurring parities + // or special cases + inline subgame_info_t + inspect_scc(unsigned max_par) + { + subgame_info_t info; + info.is_empty = true; + info.is_one_player0 = true; + info.is_one_player1 = true; + for (unsigned v : c_states()) + { + if (subgame_[v] != unseen_mark) + continue; + + bool multi_edge = false; + for (const auto &e : arena_->out(v)) + if (subgame_[e.dst] == unseen_mark) { - if ((e.acc & max_acc) && subgame.count(e.dst)) + info.is_empty = false; + unsigned this_par = e.acc.max_set() - 1; + if (this_par <= max_par) { - if (set.count(e.dst) - || (attr_max && e.acc.max_set() - 1 == max_parity)) - { - if (is_owned) - { - strategy[s] = i; - wins = true; - break; // no need to check all edges - } - } - else - { - if (!is_owned) - { - wins = false; - break; // no need to check all edges - } - } + info.all_parities.insert(this_par); + multi_edge = true; } - ++i; } + if (multi_edge) + { + // This state has multiple edges, so it is not + // a one player subgame for !owner + if ((*owner_ptr_)[v]) + info.is_one_player1 = false; + else + info.is_one_player0 = false; + } + } // v + assert(info.all_parities.size() || info.is_empty); + info.is_one_parity = info.all_parities.size() == 1; + // Done + return info; + } - if (wins) + // Checks if an scc can be trivially solved, + // that is, all vertices of the scc belong to the + // attractor of a transition leaving the scc + inline subgame_info_t + fix_scc() + { + auto scc_acc = info_->acc_sets_of(c_scc_idx_); + // We will override all parities of edges leaving the scc + bool added[] = {false, false}; + unsigned par_pair[2]; + unsigned scc_new_par = std::max(scc_acc.max_set(), 1u); + if (scc_new_par&1) + { + par_pair[1] = scc_new_par; + par_pair[0] = scc_new_par+1; + } + else + { + par_pair[1] = scc_new_par+1; + par_pair[0] = scc_new_par; + } + acc_cond::mark_t even_mark({par_pair[0]}); + acc_cond::mark_t odd_mark({par_pair[1]}); + + // Only necessary to pass tests + max_abs_par_ = std::max(par_pair[0], par_pair[1]); + + for (unsigned v : c_states()) + { + assert(subgame_[v] == unseen_mark); + for (auto &e : arena_->out(v)) + { + // The outgoing edges are taken finitely often + // -> disregard parity + if (subgame_[e.dst] != unseen_mark) + { + // Edge leaving the scc + change_stash_.emplace_back(arena_->edge_number(e), + e.dst, e.acc); + if (w_.winner(e.dst)) + { + // Winning region of player -> odd + e.acc = odd_mark; + added[1] = true; + } + else + { + // Winning region of env -> even + e.acc = even_mark; + added[0] = true; + } + // Replace with self-loop + e.dst = e.src; + } + } // e + } // v + + // Compute the attractors of the self-loops/transitions leaving scc + // These can be directly added to the winning states + // Note: attractors can not intersect therefore the order in which + // they are computed does not matter + unsigned dummy_rd; + + for (bool p : {false, true}) + if (added[p]) + attr(dummy_rd, p, par_pair[p], true, par_pair[p]); + + if (added[0] || added[1]) + // Fix "negative" strategy + for (unsigned v : c_states()) + if (subgame_[v] != unseen_mark) + s_[v] = std::abs(s_[v]); + + return inspect_scc(unseen_mark); + } // fix_scc + + inline bool + attr(unsigned &rd, bool p, unsigned max_par, + bool acc_par, unsigned min_win_par) + { + // Computes the attractor of the winning set of player p within a + // subgame given as rd. + // If acc_par is true, max_par transitions are also accepting and + // the subgame count will be increased + // The attracted vertices are directly added to the set + + // Increase rd meaning we create a new subgame + if (acc_par) + rd = ++rd_; + // todo replace with a variant of topo sort ? + // As proposed in Oink! / PGSolver + // Needs the transposed graph however + + assert((!acc_par) || (acc_par && (max_par&1) == p)); + assert(!acc_par || (0 < min_win_par)); + assert((min_win_par <= max_par) && (max_par <= max_abs_par_)); + + bool grown = false; + // We could also directly mark states as owned, + // instead of adding them to to_add first, + // possibly reducing the number of iterations. + // However by making the algorithm complete a loop + // before adding it is like a backward bfs and (generally) reduces + // the size of the strategy + static std::vector to_add; + + assert(to_add.empty()); + + do + { + if (!to_add.empty()) + { + grown = true; + for (unsigned v : to_add) + { + // v is winning + w_.set(v, p); + // Mark if demanded + if (acc_par) + { + assert(subgame_[v] == unseen_mark); + subgame_[v] = rd; + } + } + } + to_add.clear(); + + for (unsigned v : c_states()) + { + if ((subgame_[v] < rd) || (w_(v, p))) + // Not in subgame or winning + continue; + + bool is_owned = (*owner_ptr_)[v] == p; + bool wins = !is_owned; + // Loop over out-going + + // Optim: If given the choice, + // we seek to go to the "oldest" subgame + // That is the subgame with the lowest rd value + unsigned min_subgame_idx = -1u; + for (const auto &e: arena_->out(v)) + { + unsigned this_par = e.acc.max_set() - 1; + if ((subgame_[e.dst] >= rd) && (this_par <= max_par)) + { + // Check if winning + if (w_(e.dst, p) + || (acc_par && (min_win_par <= this_par))) + { + assert(!acc_par || (this_par < min_win_par) || + (acc_par && (min_win_par <= this_par) && + ((this_par&1) == p))); + if (is_owned) + { + wins = true; + if (acc_par) + { + s_[v] = arena_->edge_number(e); + if (min_win_par <= this_par) + // max par edge + // change sign -> mark as needs + // to be possibly fixed + s_[v] = -s_[v]; + break; + } + else + { + //snapping + if (subgame_[e.dst] < min_subgame_idx) + { + s_[v] = arena_->edge_number(e); + min_subgame_idx = subgame_[e.dst]; + if (!p) + // No optim for env + break; + } + } + }// owned + } + else + { + if (!is_owned) + { + wins = false; + break; + } + } // winning + } // subgame + }// for edges + if (wins) + to_add.push_back(v); + } // for v + } while (!to_add.empty()); + // done + + assert(to_add.empty()); + return grown; + } + + // We need to check if transitions that are accepted due + // to their parity remain in the winning region of p + inline bool + fix_strat_acc(unsigned rd, bool p, unsigned min_win_par, unsigned max_par) + { + for (unsigned v : c_states()) + { + // Only current attractor and owned + // and winning vertices are concerned + if ((subgame_[v] != rd) || !w_(v, p) + || ((*owner_ptr_)[v] != p) || (s_[v] > 0)) + continue; + + // owned winning vertex of attractor + // Get the strategy edge + s_[v] = -s_[v]; + const auto &e_s = arena_->edge_storage(s_[v]); + // Optimization only for player + if (!p && w_(e_s.dst, p)) + // If current strat is admissible -> nothing to do + // for env + continue; + + // This is an accepting edge that is no longer admissible + // or we seek a more desirable edge (for player) + assert(min_win_par <= e_s.acc.max_set() - 1); + assert(e_s.acc.max_set() - 1 <= max_par); + + // Strategy heuristic : go to the oldest subgame + unsigned min_subgame_idx = -1u; + + s_[v] = -1; + for (const auto &e_fix : arena_->out(v)) + { + if (subgame_[e_fix.dst] >= rd) + { + unsigned this_par = e_fix.acc.max_set() - 1; + // This edge must have less than max_par, + // otherwise it would have already been attracted + assert((this_par <= max_par) + || ((this_par&1) != (max_par&1))); + // if it is accepting and leads to the winning region + // -> valid fix + if ((min_win_par <= this_par) + && (this_par <= max_par) + && w_(e_fix.dst, p) + && (subgame_[e_fix.dst] < min_subgame_idx)) + { + // Max par edge to older subgame found + s_[v] = arena_->edge_number(e_fix); + min_subgame_idx = subgame_[e_fix.dst]; + } + } + } + if (s_[v] == -1) + // NO fix found + // This state is NOT won by p due to any accepting edges + return true; // true -> grown + } + // Nothing to fix or all fixed + return false; // false -> not grown == all good + } + + inline void zielonka() + { + while (!w_stack_.empty()) + { + auto this_work = w_stack_.back(); + w_stack_.pop_back(); + + switch (this_work.wstep) + { + case (0): { - // FIXME C++17 extract/insert could be useful here - set.emplace(s); - it = complement.erase(it); - once_more = true; + assert(this_work.rd == 0); + assert(this_work.min_par == 0); + + unsigned rd; + assert(this_work.max_par <= max_abs_par_); + + // Check if empty and get parities + subgame_info_t subgame_info = + inspect_scc(this_work.max_par); + + if (subgame_info.is_empty) + // Nothing to do + break; + if (subgame_info.is_one_parity) + { + // Can be trivially solved + one_par_subgame_solver(subgame_info, this_work.max_par); + break; + } + + // Compute the winning parity boundaries + // -> Priority compression + // Optional, improves performance + // Highest actually occurring + unsigned max_par = *subgame_info.all_parities.begin(); + unsigned min_win_par = max_par; + while ((min_win_par > 2) && + (!subgame_info.all_parities.count(min_win_par-1))) + min_win_par -= 2; + assert(max_par > 0); + assert(!subgame_info.all_parities.empty()); + assert(min_win_par > 0); + + // Get the player + bool p = min_win_par&1; + assert((max_par&1) == (min_win_par&1)); + // Attraction to highest par + // This increases rd_ and passes it to rd + attr(rd, p, max_par, true, min_win_par); + // All those attracted get subgame_[v] <- rd + + // Continuation + w_stack_.emplace_back(1, rd, min_win_par, max_par); + // Recursion + w_stack_.emplace_back(0, 0, 0, min_win_par-1); + // Others attracted will have higher counts in subgame + break; } - else - ++it; - } - } while (once_more); - return strategy; - } + case (1): + { + unsigned rd = this_work.rd; + unsigned min_win_par = this_work.min_par; + unsigned max_par = this_work.max_par; + assert((min_win_par&1) == (max_par&1)); + bool p = min_win_par&1; + // Check if the attractor of w_[!p] is equal to w_[!p] + // if so, player wins if there remain accepting transitions + // for max_par (see fix_strat_acc) + // This does not increase but reuse rd + bool grown = attr(rd, !p, max_par, false, min_win_par); + // todo investigate: A is an attractor, so the only way that + // attr(w[!p]) != w[!p] is if the max par "exit" edges lead + // to a trap for player/ exit the winning region of the + // player so we can do a fast check instead of the + // generic attr computation which only needs to be done + // if the fast check is positive - void solve_rec(const const_twa_graph_ptr& arena, - const std::vector* owner, - region_t& subgame, unsigned max_parity, - region_t (&w)[2], strategy_t (&s)[2]) - { - assert(w[0].empty()); - assert(w[1].empty()); - assert(s[0].empty()); - assert(s[1].empty()); - // The algorithm works recursively on subgames. To avoid useless copies of - // the game at each call, subgame and max_parity are used to filter states - // and transitions. - if (subgame.empty()) - return; - int p = max_parity % 2; + // Check if strategy needs to be fixed / is fixable + if (!grown) + // this only concerns parity accepting edges + grown = fix_strat_acc(rd, p, min_win_par, max_par); + // If !grown we are done, and the partitions are valid - // Recursion on max_parity. - region_t u; - auto strat_u = attractor(arena, owner, subgame, u, max_parity, p, true); + if (grown) + { + // Reset current game without !p attractor + for (unsigned v : c_states()) + if (!w_(v, !p) && (subgame_[v] >= rd)) + { + // delete ownership + w_.unset(v); + // Mark as unseen + subgame_[v] = unseen_mark; + // Unset strat for testing + s_[v] = -1; + } + w_stack_.emplace_back(0, 0, 0, max_par); + // No need to do anything else + // the attractor of !p of this level is not changed + } + break; + } + default: + throw std::runtime_error("No valid workstep"); + } // switch + } // while + } // zielonka - if (max_parity == 0) - { - s[p] = std::move(strat_u); - w[p] = std::move(u); - // FIXME what about w[!p]? - return; - } + // Undo change to the graph made along the way + inline void restore() + { + // "Unfix" the edges leaving the sccs + // This is called once the game has been solved + for (auto &e_stash : change_stash_) + { + auto &e = arena_->edge_storage(e_stash.e_num); + e.dst = e_stash.e_dst; + e.acc = e_stash.e_acc; + } + // Done + } - for (unsigned s: u) - subgame.erase(s); - region_t w0[2]; // Player's winning region in the first recursive call. - strategy_t s0[2]; // Player's winning strategy in the first - // recursive call. - solve_rec(arena, owner, subgame, max_parity - 1, w0, s0); - if (w0[0].size() + w0[1].size() != subgame.size()) - throw std::runtime_error("size mismatch"); - //if (w0[p].size() != subgame.size()) - // for (unsigned s: subgame) - // if (w0[p].find(s) == w0[p].end()) - // w0[!p].insert(s); - subgame.insert(u.begin(), u.end()); + // Empty all internal variables + inline void clean_up() + { + info_ = nullptr; + subgame_.clear(); + w_.has_winner_.clear(); + w_.winner_.clear(); + s_.clear(); + rd_ = 0; + max_abs_par_ = 0; + change_stash_.clear(); + } - if (w0[p].size() + u.size() == subgame.size()) - { - s[p] = std::move(strat_u); - s[p].insert(s0[p].begin(), s0[p].end()); - w[p].insert(subgame.begin(), subgame.end()); - return; - } + // Dedicated solver for special cases + inline void one_par_subgame_solver(const subgame_info_t &info, + unsigned max_par) + { + assert(info.all_parities.size() == 1); + // The entire subgame is won by the player of the only parity + // Any edge will do + // todo optim for smaller circuit + // This subgame gets its own counter + ++rd_; + unsigned rd = rd_; + unsigned one_par = *info.all_parities.begin(); + bool winner = one_par & 1; + assert(one_par <= max_par); - // Recursion on game size. - auto strat_wnp = attractor(arena, owner, - subgame, w0[!p], max_parity, !p, false); + for (unsigned v : c_states()) + { + if (subgame_[v] != unseen_mark) + continue; + // State of the subgame + subgame_[v] = rd; + w_.set(v, winner); + // Get the strategy + assert(s_[v] == -1); + for (const auto &e : arena_->out(v)) + { + unsigned this_par = e.acc.max_set() - 1; + if ((subgame_[e.dst] >= rd) && (this_par <= max_par)) + { + assert(this_par == one_par); + // Ok for strat + s_[v] = arena_->edge_number(e); + break; + } + } + assert((0 < s_[v]) && (s_[v] < unseen_mark)); + } + // Done + } - for (unsigned s: w0[!p]) - subgame.erase(s); + const unsigned unseen_mark = std::numeric_limits::max(); - region_t w1[2]; // Odd's winning region in the second recursive call. - strategy_t s1[2]; // Odd's winning strategy in the second recursive call. - solve_rec(arena, owner, subgame, max_parity, w1, s1); - if (w1[0].size() + w1[1].size() != subgame.size()) - throw std::runtime_error("size mismatch"); + twa_graph_ptr arena_; + const std::vector *owner_ptr_; + unsigned rd_; + winner_t w_; + // Subgame array similar to the one from oink! + std::vector subgame_; + // strategies for env and player; For synthesis only player is needed + // We need a signed value here in order to "fix" the strategy + // during construction + std::vector s_; - w[p] = std::move(w1[p]); - s[p] = std::move(s1[p]); - - w[!p] = std::move(w1[!p]); - w[!p].insert(w0[!p].begin(), w0[!p].end()); - s[!p] = std::move(strat_wnp); - s[!p].insert(s0[!p].begin(), s0[!p].end()); - s[!p].insert(s1[!p].begin(), s1[!p].end()); - - subgame.insert(w0[!p].begin(), w0[!p].end()); - } + // Informations about sccs andthe current scc + std::unique_ptr info_; + unsigned max_abs_par_; // Max parity occurring in the current scc + // Info on the current scc + unsigned c_scc_idx_; + // Fixes made to the sccs that have to be undone + // before returning + std::vector change_stash_; + // Change recursive calls to stack + std::vector w_stack_; + }; } // anonymous + bool solve_parity_game(const twa_graph_ptr& arena) + { + parity_game pg; + return pg.solve(arena); + } + void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) { auto owner = ensure_parity_game(arena, "pg_print"); @@ -230,35 +806,13 @@ namespace spot } } - solved_game parity_game_solve(const const_twa_graph_ptr& arena) - { - solved_game result; - result.arena = arena; - - const std::vector* owner = - ensure_parity_game(arena, "parity_game_solve"); - - region_t states_; - unsigned ns = arena->num_states(); - for (unsigned i = 0; i < ns; ++i) - states_.insert(i); - - acc_cond::mark_t m{}; - for (const auto& e: arena->edges()) - m |= e.acc; - - solve_rec(arena, owner, states_, m.max_set(), - result.winning_region, result.winning_strategy); - - return result; - } - void propagate_players(spot::twa_graph_ptr& arena, bool first_player, bool complete0) { auto um = arena->acc().unsat_mark(); if (!um.first) - throw std::runtime_error("game winning condition is a tautology"); + throw std::runtime_error + ("propagate_players(): game winning condition is a tautology"); unsigned sink_env = 0; unsigned sink_con = 0; @@ -311,45 +865,39 @@ namespace spot } twa_graph_ptr - highlight_strategy(twa_graph_ptr& aut, const strategy_t& s, - unsigned color) + highlight_strategy(twa_graph_ptr& aut, + int player0_color, + int player1_color) { - unsigned ns = aut->num_states(); - auto* highlight = aut->get_or_set_named_prop> - ("highlight-edges"); + auto owner = ensure_parity_game(aut, "highlight_strategy()"); + region_t* w = aut->get_named_prop("state-winner"); + strategy_t* s = aut->get_named_prop("strategy"); + if (!w || !s) + throw std::runtime_error("highlight_strategy(): " + "strategy not available, solve the game first"); - for (auto [src, n]: s) + unsigned ns = aut->num_states(); + auto* hl_edges = aut->get_or_set_named_prop> + ("highlight-edges"); + auto* hl_states = aut->get_or_set_named_prop> + ("highlight-states"); + + if (unsigned sz = std::min(w->size(), s->size()); sz < ns) + ns = sz; + + for (unsigned n = 0; n < ns; ++n) { - if (src >= ns) - throw std::runtime_error - ("highlight_strategy(): strategy refers to unexisting states"); - unsigned int i = 0; - for (auto& t: aut->out(src)) - if (i++ == n) - { - (*highlight)[aut->edge_number(t)] = color; - break; - } + int color = (*w)[n] ? player1_color : player0_color; + if (color == -1) + continue; + (*hl_states)[n] = color; + if ((*w)[n] == (*owner)[n]) + (*hl_edges)[(*s)[n]] = color; } return aut; } - twa_graph_ptr - solved_game::highlight_strategy(unsigned player, unsigned color) - { - auto aut = std::const_pointer_cast(arena); - - auto* highlight = aut->get_or_set_named_prop> - ("highlight-states"); - unsigned ns = aut->num_states(); - for (unsigned i = 0; i < ns; ++i) - if (player_winning_at(player, i)) - (*highlight)[i] = color; - - return spot::highlight_strategy(aut, winning_strategy[!!player], color); - } - void set_state_players(twa_graph_ptr arena, std::vector owners) { std::vector* owners_ptr = new std::vector(owners); diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 1f3bfd27b..4f92dca90 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -47,27 +47,12 @@ namespace spot bool complete0 = true); - typedef std::unordered_set region_t; - typedef std::unordered_map strategy_t; + // false -> env, true -> player + typedef std::vector region_t; + // state idx -> global edge number + typedef std::vector strategy_t; - struct SPOT_API solved_game - { - const_twa_graph_ptr arena; - - region_t winning_region[2]; - strategy_t winning_strategy[2]; - - /// \brief Highlight the edges of a strategy on the automaton. - twa_graph_ptr highlight_strategy(unsigned player, unsigned color); - - bool player_winning_at(unsigned player, unsigned state) - { - auto& w = winning_region[player]; - return w.find(state) != w.end(); - } - }; - /// \brief solve a parity-game /// /// The arena is a deterministic max odd parity automaton with a @@ -76,8 +61,11 @@ namespace spot /// This computes the winning strategy and winning region of this /// game for player 1 using Zielonka's recursive algorithm. /// \cite zielonka.98.tcs + /// + /// Return the player winning in the initial state, and set + /// the state-winner and strategy named properties. SPOT_API - solved_game parity_game_solve(const const_twa_graph_ptr& arena); + bool solve_parity_game(const twa_graph_ptr& arena); /// \brief Print a max odd parity game using PG-solver syntax SPOT_API @@ -85,10 +73,12 @@ namespace spot /// \brief Highlight the edges of a strategy on an automaton. + /// + /// Pass a negative color to not display the corresponding strategy. SPOT_API twa_graph_ptr highlight_strategy(twa_graph_ptr& arena, - const strategy_t& s, - unsigned color); + int player0_color = 5, + int player1_color = 4); /// \brief Set the owner for all the states. SPOT_API diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 55a2751a3..22627be88 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -23,6 +23,27 @@ set -e cat >exp < GFb' --print-pg >out + +: > out +for algo in ds sd lar; do + ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --algo=$algo --print-pg >>out +done diff out exp cat >exp <\n" ], "text/plain": [ - " *' at 0x7fcb3c55f9f0> >" + " *' at 0x7f9bf8477330> >" ] }, "execution_count": 2, @@ -360,29 +360,13 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The `parity_game_solve()` function returns a `solved_game` object." + "The `solve_parity_game()` function returns the player winning from the initial state (`False` for player 0, and `True` for player 1)." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, - "outputs": [], - "source": [ - "sol = spot.parity_game_solve(game)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "The solved game can be queried to know if a player is winning when the game starts in some given." - ] - }, - { - "cell_type": "code", - "execution_count": 5, - "metadata": {}, "outputs": [ { "data": { @@ -390,283 +374,27 @@ "True" ] }, - "execution_count": 5, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "sol.player_winning_at(1, game.get_init_state_number())" + "spot.solve_parity_game(game)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Calling the `highlight_strategy` method will decorate the original game with colors showing the winning region (states from which a player has a strategy to win), and strategy (which transition should be used for each winning state owned by that player) of a given player. Let's paint the strategy of player 1 in green (color 4) for this example:" + "Additional information about the player winning in each state, and the strategy have been stored in the automaton but are not displayed by default.\n", + "\n", + "Calling the `highlight_strategy` function will decorate the game's automaton with colors showing the winning regions (states from which a player has a strategy to win), and strategy (which transition should be used for each winning state owned by that player) of a given player. Here green corresponds to player 1 (who tries to satisfy the acceptance condition), and red to player 0 (who tries not to)." ] }, { "cell_type": "code", - "execution_count": 6, - "metadata": {}, - "outputs": [ - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "❷\n", - ") & (Inf(\n", - "❶\n", - ") | Fin(\n", - "⓿\n", - "))\n", - "[parity max odd 3]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a\n", - "❶\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!b\n", - "❶\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "b\n", - "❶\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b\n", - "❶\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "!b\n", - "❶\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "3->7\n", - "\n", - "\n", - "a\n", - "❷\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", - "\n", - "\n", - "\n", - "4->8\n", - "\n", - "\n", - "1\n", - "❷\n", - "\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "!a\n", - "❶\n", - "\n", - "\n", - "\n", - "5->7\n", - "\n", - "\n", - "a\n", - "❷\n", - "\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "1\n", - "❶\n", - "\n", - "\n", - "\n", - "7->5\n", - "\n", - "\n", - "1\n", - "❷\n", - "\n", - "\n", - "\n", - "8->4\n", - "\n", - "\n", - "b\n", - "❷\n", - "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "8->9\n", - "\n", - "\n", - "!b\n", - "❶\n", - "\n", - "\n", - "\n", - "10\n", - "\n", - "10\n", - "\n", - "\n", - "\n", - "9->10\n", - "\n", - "\n", - "1\n", - "❶\n", - "\n", - "\n", - "\n", - "10->9\n", - "\n", - "\n", - "1\n", - "❶\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - " *' at 0x7fcb3c55a1e0> >" - ] - }, - "execution_count": 6, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "sol.highlight_strategy(1, 4)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Because `highlight_strategy` simply decorates the original automaton, we can call it a second time to show that player 0 could win if it had a way to reach the red (color 5) region and play the red strategy." - ] - }, - { - "cell_type": "code", - "execution_count": 7, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -903,24 +631,17 @@ "\n" ], "text/plain": [ - " *' at 0x7fcb3c55a900> >" + " *' at 0x7f9bf83e1060> >" ] }, - "execution_count": 7, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "sol.highlight_strategy(0, 5)" + "spot.highlight_strategy(game)" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -939,7 +660,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.5" + "version": "3.8.6rc1" } }, "nbformat": 4,