From 25c75c55b1e1fe7d3a502e1658839fa36416165c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Sep 2020 17:41:11 +0200 Subject: [PATCH] game: git rid of the parity_game class This class was a simple wrapper on top of twa_graph_ptr, but it's easier to simply use a twa_graph_ptr with a "state-player" property instead, this way we will be able to modify the automata I/O routines to support games directly. * spot/misc/game.cc, spot/misc/game.hh: Rewrite the solver and pg_printer interface. * bin/ltlsynt.cc: Adjust. * NEWS: Mention this change. * doc/org/concepts.org: Mention the state-player property. --- NEWS | 4 + bin/ltlsynt.cc | 44 +++--- doc/org/concepts.org | 1 + spot/misc/game.cc | 363 +++++++++++++++++++++++-------------------- spot/misc/game.hh | 93 ++--------- 5 files changed, 239 insertions(+), 266 deletions(-) diff --git a/NEWS b/NEWS index 59560fa19..c9ab0bd98 100644 --- a/NEWS +++ b/NEWS @@ -63,6 +63,10 @@ New in spot 2.9.4.dev (not yet released) be simplied to {0}, but the oppose rewriting can be useful as well. (Issue #418.) + - the parity_game class has been removed, now any twa_graph_ptr that + has a parity max odd acceptance and a "state-player" property is + considered to be a parity game. + New in spot 2.9.4 (2020-09-07) Bugs fixed: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index c82afb00d..92485c5ff 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -185,7 +185,7 @@ namespace // Ensures that the game is complete for player 0. // Also computes the owner of each state (false for player 0, i.e. env). // Initial state belongs to Player 0 and the game is turn-based. - static std::vector + static std::vector* complete_env(spot::twa_graph_ptr& arena) { unsigned sink_env = arena->new_state(); @@ -198,10 +198,11 @@ namespace arena->new_edge(sink_env, sink_con, bddtrue, um.second); std::vector seen(arena->num_states(), false); - std::vector todo({arena->get_init_state_number()}); - std::vector owner(arena->num_states(), false); - owner[arena->get_init_state_number()] = false; - owner[sink_env] = true; + unsigned init = arena->get_init_state_number(); + std::vector todo({init}); + auto owner = new std::vector(arena->num_states(), false); + (*owner)[init] = false; + (*owner)[sink_env] = true; while (!todo.empty()) { unsigned src = todo.back(); @@ -210,16 +211,16 @@ namespace bdd missing = bddtrue; for (const auto& e: arena->out(src)) { - if (!owner[src]) + if (!(*owner)[src]) missing -= e.cond; if (!seen[e.dst]) { - owner[e.dst] = !owner[src]; + (*owner)[e.dst] = !(*owner)[src]; todo.push_back(e.dst); } } - if (!owner[src] && missing != bddfalse) + if (!(*owner)[src] && missing != bddfalse) arena->new_edge(src, sink_con, missing, um.second); } @@ -254,17 +255,18 @@ namespace // 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::parity_game& pg, - const spot::parity_game::strategy_t& strat, + strat_to_aut(const spot::const_twa_graph_ptr& pg, + const spot::strategy_t& strat, const spot::twa_graph_ptr& dpa, bdd all_outputs) { auto aut = spot::make_twa_graph(dpa->get_dict()); aut->copy_ap_of(dpa); - std::vector todo{pg.get_init_state_number()}; - std::vector pg2aut(pg.num_states(), -1); + unsigned pg_init = pg->get_init_state_number(); + std::vector todo{pg_init}; + std::vector pg2aut(pg->num_states(), -1); aut->set_init_state(aut->new_state()); - pg2aut[pg.get_init_state_number()] = aut->get_init_state_number(); + pg2aut[pg_init] = aut->get_init_state_number(); while (!todo.empty()) { unsigned s = todo.back(); @@ -541,7 +543,7 @@ namespace if (want_time) sw.start(); auto owner = complete_env(dpa); - auto pg = spot::parity_game(dpa, owner); + dpa->set_named_prop("state-player", owner); if (want_time) bgame_time = sw.stop(); if (verbose) @@ -550,22 +552,22 @@ namespace if (opt_print_pg) { timer.stop(); - pg.print(std::cout); + pg_print(std::cout, dpa); return 0; } - spot::parity_game::strategy_t strategy[2]; - spot::parity_game::region_t winning_region[2]; + spot::strategy_t strategy[2]; + spot::region_t winning_region[2]; if (want_time) sw.start(); - pg.solve(winning_region, strategy); + parity_game_solve(dpa, winning_region, strategy); if (want_time) solve_time = sw.stop(); if (verbose) std::cerr << "parity game solved in " << solve_time << " seconds\n"; - nb_states_parity_game = pg.num_states(); + nb_states_parity_game = dpa->num_states(); timer.stop(); - if (winning_region[1].count(pg.get_init_state_number())) + if (winning_region[1].count(dpa->get_init_state_number())) { std::cout << "REALIZABLE\n"; if (!opt_real) @@ -573,7 +575,7 @@ namespace if (want_time) sw.start(); auto strat_aut = - strat_to_aut(pg, strategy[1], dpa, all_outputs); + strat_to_aut(dpa, strategy[1], dpa, all_outputs); if (want_time) strat2aut_time = sw.stop(); diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 520da136e..351dca2fe 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1144,6 +1144,7 @@ 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 | | ~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 cbdd81733..a21feface 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,198 +24,227 @@ namespace spot { + namespace + { -parity_game::parity_game(const twa_graph_ptr& arena, - const std::vector& owner) - : arena_(arena) - , owner_(owner) -{ - bool max, odd; - arena_->acc().is_parity(max, odd, true); - if (!(max && odd)) - throw std::runtime_error("arena must have max-odd acceptance condition"); - - for (const auto& e : arena_->edges()) - if (e.acc.max_set() == 0) - throw std::runtime_error("arena must be colorized"); - - assert(owner_.size() == arena_->num_states()); -} - -void parity_game::print(std::ostream& os) -{ - os << "parity " << num_states() - 1 << ";\n"; - std::vector seen(num_states(), false); - std::vector todo({get_init_state_number()}); - while (!todo.empty()) + static const std::vector* + ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname) { - unsigned src = todo.back(); - todo.pop_back(); - if (seen[src]) - continue; - seen[src] = true; - os << src << ' '; - os << out(src).begin()->acc.max_set() - 1 << ' '; - os << owner(src) << ' '; - bool first = true; - for (auto& e: out(src)) - { - if (!first) - os << ','; - first = false; - os << e.dst; - if (!seen[e.dst]) - todo.push_back(e.dst); - } - if (src == get_init_state_number()) - os << " \"INIT\""; - os << ";\n"; + bool max, odd; + arena->acc().is_parity(max, odd, true); + if (!(max && odd)) + throw std::runtime_error + (std::string(fnname) + + ": arena must have max-odd acceptance condition"); + + for (const auto& e : arena->edges()) + if (!e.acc) + throw std::runtime_error + (std::string(fnname) + ": arena must be colorized"); + + auto owner = arena->get_named_prop>("state-player"); + if (!owner) + throw std::runtime_error + (std::string(fnname) + ": automaton should define \"state-player\""); + + return owner; } -} -void parity_game::solve(region_t (&w)[2], strategy_t (&s)[2]) const -{ - region_t states_; - for (unsigned i = 0; i < num_states(); ++i) - states_.insert(i); - unsigned m = max_parity(); - solve_rec(states_, m, w, s); -} -parity_game::strategy_t -parity_game::attractor(const region_t& subgame, region_t& set, - unsigned max_parity, int p, bool attr_max) const -{ - strategy_t strategy; - std::set complement(subgame.begin(), subgame.end()); - for (unsigned s: set) - complement.erase(s); - - acc_cond::mark_t max_acc({}); - for (unsigned i = 0; i <= max_parity; ++i) - max_acc.set(i); - - bool once_more; - do + 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) { - once_more = false; - for (auto it = complement.begin(); it != complement.end();) + strategy_t strategy; + std::set complement(subgame.begin(), subgame.end()); + for (unsigned s: set) + complement.erase(s); + + acc_cond::mark_t max_acc({}); + for (unsigned i = 0; i <= max_parity; ++i) + max_acc.set(i); + + bool once_more; + do { - unsigned s = *it; - unsigned i = 0; - - bool is_owned = owner_[s] == p; - bool wins = !is_owned; - - for (const auto& e: out(s)) + once_more = false; + for (auto it = complement.begin(); it != complement.end();) { - if ((e.acc & max_acc) && subgame.count(e.dst)) + unsigned s = *it; + unsigned i = 0; + + bool is_owned = (*owner)[s] == p; + bool wins = !is_owned; + + for (const auto& e: arena->out(s)) { - if (set.count(e.dst) - || (attr_max && e.acc.max_set() - 1 == max_parity)) + if ((e.acc & max_acc) && subgame.count(e.dst)) { - if (is_owned) + if (set.count(e.dst) + || (attr_max && e.acc.max_set() - 1 == max_parity)) { - 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 + 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 + } } } + ++i; } - ++i; - } - if (wins) - { - // FIXME C++17 extract/insert could be useful here - set.emplace(s); - it = complement.erase(it); - once_more = true; + if (wins) + { + // FIXME C++17 extract/insert could be useful here + set.emplace(s); + it = complement.erase(it); + once_more = true; + } + else + ++it; } - else - ++it; + } while (once_more); + return strategy; + } + + 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; + + // Recursion on max_parity. + region_t u; + auto strat_u = attractor(arena, owner, subgame, u, max_parity, p, true); + + if (max_parity == 0) + { + s[p] = std::move(strat_u); + w[p] = std::move(u); + // FIXME what about w[!p]? + return; } - } while (once_more); - return strategy; -} -void parity_game::solve_rec(region_t& subgame, unsigned max_parity, - region_t (&w)[2], strategy_t (&s)[2]) const -{ - 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; + 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()); - // Recursion on max_parity. - region_t u; - auto strat_u = attractor(subgame, u, max_parity, p, true); + 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; + } - if (max_parity == 0) - { - s[p] = std::move(strat_u); - w[p] = std::move(u); - // FIXME what about w[!p]? - return; + // Recursion on game size. + auto strat_wnp = attractor(arena, owner, + subgame, w0[!p], max_parity, !p, false); + + for (unsigned s: w0[!p]) + subgame.erase(s); + + 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"); + + 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()); } - 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(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()); + } // anonymous - 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; - } + void pg_print(std::ostream& os, const const_twa_graph_ptr& arena) + { + auto owner = ensure_parity_game(arena, "pg_print"); - // Recursion on game size. - auto strat_wnp = attractor(subgame, w0[!p], max_parity, !p); + unsigned ns = arena->num_states(); + unsigned init = arena->get_init_state_number(); + os << "parity " << ns - 1 << ";\n"; + std::vector seen(ns, false); + std::vector todo({init}); + while (!todo.empty()) + { + unsigned src = todo.back(); + todo.pop_back(); + if (seen[src]) + continue; + seen[src] = true; + os << src << ' '; + os << arena->out(src).begin()->acc.max_set() - 1 << ' '; + os << (*owner)[src] << ' '; + bool first = true; + for (auto& e: arena->out(src)) + { + if (!first) + os << ','; + first = false; + os << e.dst; + if (!seen[e.dst]) + todo.push_back(e.dst); + } + if (src == init) + os << " \"INIT\""; + os << ";\n"; + } + } - for (unsigned s: w0[!p]) - subgame.erase(s); + void parity_game_solve(const const_twa_graph_ptr& arena, + region_t (&w)[2], strategy_t (&s)[2]) + { + const std::vector* owner = + ensure_parity_game(arena, "parity_game_solve"); - 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(subgame, max_parity, w1, s1); - if (w1[0].size() + w1[1].size() != subgame.size()) - throw std::runtime_error("size mismatch"); + region_t states_; + unsigned ns = arena->num_states(); + for (unsigned i = 0; i < ns; ++i) + states_.insert(i); - 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()); -} + acc_cond::mark_t m{}; + for (const auto& e: arena->edges()) + m |= e.acc; + solve_rec(arena, owner, states_, m.max_set(), w, s); + } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index aad248404..91c3fbb70 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -31,85 +31,22 @@ namespace spot { - -class SPOT_API parity_game -{ -private: - const const_twa_graph_ptr arena_; - const std::vector owner_; - -public: - /// \a parity_game provides an interface to manipulate a colorized parity - /// automaton as a parity game, including methods to solve the game. - /// The input automaton (arena) should be colorized and have a max-odd parity - /// acceptance condition. - /// - /// \param arena the underlying parity automaton - /// \param owner a vector of Booleans indicating the owner of each state: - /// true stands for Player 1, false stands for Player 0. - parity_game(const twa_graph_ptr& arena, const std::vector& owner); - - unsigned num_states() const - { - return arena_->num_states(); - } - - unsigned get_init_state_number() const - { - return arena_->get_init_state_number(); - } - - internal::state_out - out(unsigned src) const - { - return arena_->out(src); - } - - internal::state_out - out(unsigned src) - { - return arena_->out(src); - } - - bool owner(unsigned src) const - { - return owner_[src]; - } - - unsigned max_parity() const - { - unsigned max_parity = 0; - for (const auto& e: arena_->edges()) - max_parity = std::max(max_parity, e.acc.max_set()); - SPOT_ASSERT(max_parity); - return max_parity - 1; - } - - /// Print the parity game in PGSolver's format. - void print(std::ostream& os); - typedef std::unordered_set region_t; - // Map state number to index of the transition to take. typedef std::unordered_map strategy_t; - /// Compute the winning strategy and winning region of this game for player - /// 1 using Zielonka's recursive algorithm. \cite zielonka.98.tcs - void solve(region_t (&w)[2], strategy_t (&s)[2]) const; - -private: - typedef twa_graph::graph_t::edge_storage_t edge_t; - - // Compute (in place) a set of states from which player can force a visit - // through set, and a strategy to do it. - // if attr_max is true, states that can force a visit through an edge with - // max parity are also counted in. - strategy_t attractor(const region_t& subgame, region_t& set, - unsigned max_parity, int odd, - bool attr_max = false) const; - - // Compute the winning strategy and winning region for both players. - void solve_rec(region_t& subgame, unsigned max_parity, - region_t (&w)[2], strategy_t (&s)[2]) const; -}; + /// \brief solve a parity-game + /// + /// The arena is a deterministic max odd parity automaton with a + /// "state-player" property. + /// + /// This computes the winning strategy and winning region of this + /// game for player 1 using Zielonka's recursive algorithm. + /// \cite zielonka.98.tcs + SPOT_API + void parity_game_solve(const const_twa_graph_ptr& arena, + region_t (&w)[2], strategy_t (&s)[2]); + /// \brief Print a max odd parity game using PG-solver syntax + SPOT_API + void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); }