Commit 25c75c55 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 6379d988
...@@ -63,6 +63,10 @@ New in spot 2.9.4.dev (not yet released) ...@@ -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 be simplied to {0}, but the oppose rewriting can be useful as
well. (Issue #418.) 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) New in spot 2.9.4 (2020-09-07)
Bugs fixed: Bugs fixed:
......
...@@ -185,7 +185,7 @@ namespace ...@@ -185,7 +185,7 @@ namespace
// Ensures that the game is complete for player 0. // Ensures that the game is complete for player 0.
// Also computes the owner of each state (false for player 0, i.e. env). // 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. // Initial state belongs to Player 0 and the game is turn-based.
static std::vector<bool> static std::vector<bool>*
complete_env(spot::twa_graph_ptr& arena) complete_env(spot::twa_graph_ptr& arena)
{ {
unsigned sink_env = arena->new_state(); unsigned sink_env = arena->new_state();
...@@ -198,10 +198,11 @@ namespace ...@@ -198,10 +198,11 @@ namespace
arena->new_edge(sink_env, sink_con, bddtrue, um.second); arena->new_edge(sink_env, sink_con, bddtrue, um.second);
std::vector<bool> seen(arena->num_states(), false); std::vector<bool> seen(arena->num_states(), false);
std::vector<unsigned> todo({arena->get_init_state_number()}); unsigned init = arena->get_init_state_number();
std::vector<bool> owner(arena->num_states(), false); std::vector<unsigned> todo({init});
owner[arena->get_init_state_number()] = false; auto owner = new std::vector<bool>(arena->num_states(), false);
owner[sink_env] = true; (*owner)[init] = false;
(*owner)[sink_env] = true;
while (!todo.empty()) while (!todo.empty())
{ {
unsigned src = todo.back(); unsigned src = todo.back();
...@@ -210,16 +211,16 @@ namespace ...@@ -210,16 +211,16 @@ namespace
bdd missing = bddtrue; bdd missing = bddtrue;
for (const auto& e: arena->out(src)) for (const auto& e: arena->out(src))
{ {
if (!owner[src]) if (!(*owner)[src])
missing -= e.cond; missing -= e.cond;
if (!seen[e.dst]) if (!seen[e.dst])
{ {
owner[e.dst] = !owner[src]; (*owner)[e.dst] = !(*owner)[src];
todo.push_back(e.dst); todo.push_back(e.dst);
} }
} }
if (!owner[src] && missing != bddfalse) if (!(*owner)[src] && missing != bddfalse)
arena->new_edge(src, sink_con, missing, um.second); arena->new_edge(src, sink_con, missing, um.second);
} }
...@@ -254,17 +255,18 @@ namespace ...@@ -254,17 +255,18 @@ namespace
// accessible. Also merge back pairs of p --(i)--> q --(o)--> r // accessible. Also merge back pairs of p --(i)--> q --(o)--> r
// transitions to p --(i&o)--> r. // transitions to p --(i&o)--> r.
static spot::twa_graph_ptr static spot::twa_graph_ptr
strat_to_aut(const spot::parity_game& pg, strat_to_aut(const spot::const_twa_graph_ptr& pg,
const spot::parity_game::strategy_t& strat, const spot::strategy_t& strat,
const spot::twa_graph_ptr& dpa, const spot::twa_graph_ptr& dpa,
bdd all_outputs) bdd all_outputs)
{ {
auto aut = spot::make_twa_graph(dpa->get_dict()); auto aut = spot::make_twa_graph(dpa->get_dict());
aut->copy_ap_of(dpa); aut->copy_ap_of(dpa);
std::vector<unsigned> todo{pg.get_init_state_number()}; unsigned pg_init = pg->get_init_state_number();
std::vector<int> pg2aut(pg.num_states(), -1); std::vector<unsigned> todo{pg_init};
std::vector<int> pg2aut(pg->num_states(), -1);
aut->set_init_state(aut->new_state()); 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()) while (!todo.empty())
{ {
unsigned s = todo.back(); unsigned s = todo.back();
...@@ -541,7 +543,7 @@ namespace ...@@ -541,7 +543,7 @@ namespace
if (want_time) if (want_time)
sw.start(); sw.start();
auto owner = complete_env(dpa); auto owner = complete_env(dpa);
auto pg = spot::parity_game(dpa, owner); dpa->set_named_prop("state-player", owner);
if (want_time) if (want_time)
bgame_time = sw.stop(); bgame_time = sw.stop();
if (verbose) if (verbose)
...@@ -550,22 +552,22 @@ namespace ...@@ -550,22 +552,22 @@ namespace
if (opt_print_pg) if (opt_print_pg)
{ {
timer.stop(); timer.stop();
pg.print(std::cout); pg_print(std::cout, dpa);
return 0; return 0;
} }
spot::parity_game::strategy_t strategy[2]; spot::strategy_t strategy[2];
spot::parity_game::region_t winning_region[2]; spot::region_t winning_region[2];
if (want_time) if (want_time)
sw.start(); sw.start();
pg.solve(winning_region, strategy); parity_game_solve(dpa, winning_region, strategy);
if (want_time) if (want_time)
solve_time = sw.stop(); solve_time = sw.stop();
if (verbose) if (verbose)
std::cerr << "parity game solved in " << solve_time << " seconds\n"; 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(); 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"; std::cout << "REALIZABLE\n";
if (!opt_real) if (!opt_real)
...@@ -573,7 +575,7 @@ namespace ...@@ -573,7 +575,7 @@ namespace
if (want_time) if (want_time)
sw.start(); sw.start();
auto strat_aut = auto strat_aut =
strat_to_aut(pg, strategy[1], dpa, all_outputs); strat_to_aut(dpa, strategy[1], dpa, all_outputs);
if (want_time) if (want_time)
strat2aut_time = sw.stop(); strat2aut_time = sw.stop();
......
...@@ -1144,6 +1144,7 @@ Here is a list of named properties currently used inside Spot: ...@@ -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 | | ~rejected-word~ | ~std::string~ | a word rejected by the automaton |
| ~simulated-states~ | ~std::vector<unsigned>~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions | | ~simulated-states~ | ~std::vector<unsigned>~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions |
| ~state-names~ | ~std::vector<std::string>~ | vector naming each state of the automaton, for display purpose | | ~state-names~ | ~std::vector<std::string>~ | vector naming each state of the automaton, for display purpose |
| ~state-player~ | ~std::vector<bool>~ | 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) | | ~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 Objects referenced via named properties are automatically destroyed
......
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -24,198 +24,227 @@ ...@@ -24,198 +24,227 @@
namespace spot namespace spot
{ {
namespace
{
parity_game::parity_game(const twa_graph_ptr& arena, static const std::vector<bool>*
const std::vector<bool>& owner) ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname)
: 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<bool> seen(num_states(), false);
std::vector<unsigned> todo({get_init_state_number()});
while (!todo.empty())
{ {
unsigned src = todo.back(); bool max, odd;
todo.pop_back(); arena->acc().is_parity(max, odd, true);
if (seen[src]) if (!(max && odd))
continue; throw std::runtime_error
seen[src] = true; (std::string(fnname) +
os << src << ' '; ": arena must have max-odd acceptance condition");
os << out(src).begin()->acc.max_set() - 1 << ' ';
os << owner(src) << ' '; for (const auto& e : arena->edges())
bool first = true; if (!e.acc)
for (auto& e: out(src)) throw std::runtime_error
{ (std::string(fnname) + ": arena must be colorized");
if (!first)
os << ','; auto owner = arena->get_named_prop<std::vector<bool>>("state-player");
first = false; if (!owner)
os << e.dst; throw std::runtime_error
if (!seen[e.dst]) (std::string(fnname) + ": automaton should define \"state-player\"");
todo.push_back(e.dst);
} return owner;
if (src == get_init_state_number())
os << " \"INIT\"";
os << ";\n";
} }
}
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 strategy_t attractor(const const_twa_graph_ptr& arena,
parity_game::attractor(const region_t& subgame, region_t& set, const std::vector<bool>* owner,
unsigned max_parity, int p, bool attr_max) const const region_t& subgame, region_t& set,
{ unsigned max_parity, int p,
strategy_t strategy; bool attr_max)
std::set<unsigned> complement(subgame.begin(), subgame.end()); {
for (unsigned s: set) strategy_t strategy;
complement.erase(s); std::set<unsigned> complement(subgame.begin(), subgame.end());
for (unsigned s: set)
complement.erase(s);
acc_cond::mark_t max_acc({}); acc_cond::mark_t max_acc({});
for (unsigned i = 0; i <= max_parity; ++i) for (unsigned i = 0; i <= max_parity; ++i)
max_acc.set(i); max_acc.set(i);
bool once_more; bool once_more;
do do
{
once_more = false;
for (auto it = complement.begin(); it != complement.end();)
{ {
unsigned s = *it; once_more = false;
unsigned i = 0; for (auto it = complement.begin(); it != complement.end();)
{
unsigned s = *it;
unsigned i = 0;
bool is_owned = owner_[s] == p; bool is_owned = (*owner)[s] == p;
bool wins = !is_owned; bool wins = !is_owned;
for (const auto& e: out(s)) for (const auto& e: arena->out(s))
{
if ((e.acc & max_acc) && subgame.count(e.dst))
{ {
if (set.count(e.dst) if ((e.acc & max_acc) && subgame.count(e.dst))
|| (attr_max && e.acc.max_set() - 1 == max_parity))
{ {
if (is_owned) if (set.count(e.dst)
|| (attr_max && e.acc.max_set() - 1 == max_parity))
{ {
strategy[s] = i; if (is_owned)
wins = true; {
break; // no need to check all edges strategy[s] = i;
wins = true;
break; // no need to check all edges
}
} }
} else
else
{
if (!is_owned)
{ {
wins = false; if (!is_owned)
break; // no need to check all edges {
wins = false;
break; // no need to check all edges
}
} }
} }
++i;
} }
++i;
}
if (wins) if (wins)
{ {
// FIXME C++17 extract/insert could be useful here // FIXME C++17 extract/insert could be useful here
set.emplace(s); set.emplace(s);
it = complement.erase(it); it = complement.erase(it);
once_more = true; once_more = true;
}
else
++it;
} }
else } while (once_more);
++it; return strategy;
}
} 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;
// Recursion on max_parity.
region_t u;
auto strat_u = attractor(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;
} }
for (unsigned s: u) void solve_rec(const const_twa_graph_ptr& arena,
subgame.erase(s); const std::vector<bool>* owner,
region_t w0[2]; // Player's winning region in the first recursive call. region_t& subgame, unsigned max_parity,
strategy_t s0[2]; // Player's winning strategy in the first recursive call. region_t (&w)[2], strategy_t (&s)[2])
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());
if (w0[p].size() + u.size() == subgame.size())
{ {
s[p] = std::move(strat_u); assert(w[0].empty());
s[p].insert(s0[p].begin(), s0[p].end()); assert(w[1].empty());
w[p].insert(subgame.begin(), subgame.end()); assert(s[0].empty());
return; 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;
}
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());
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;
}
// Recursion on game size. // Recursion on game size.
auto strat_wnp = attractor(subgame, w0[!p], max_parity, !p); auto strat_wnp = attractor(arena, owner,
subgame, w0[!p], max_parity, !p, false);
for (unsigned s: w0[!p]) for (unsigned s: w0[!p])
subgame.erase(s); subgame.erase(s);
region_t w1[2]; // Odd's winning region in the second recursive call. 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. strategy_t s1[2]; // Odd's winning strategy in the second recursive call.
solve_rec(subgame, max_parity, w1, s1); solve_rec(arena, owner, subgame, max_parity, w1, s1);
if (w1[0].size() + w1[1].size() != subgame.size()) if (w1[0].size() + w1[1].size() != subgame.size())
throw std::runtime_error("size mismatch"); throw std::runtime_error("size mismatch");
w[p] = std::move(w1[p]); w[p] = std::move(w1[p]);
s[p] = std::move(s1[p]); s[p] = std::move(s1[p]);
w[!p] = std::move(w1[!p]); w[!p] = std::move(w1[!p]);
w[!p].insert(w0[!p].begin(), w0[!p].end()); w[!p].insert(w0[!p].begin(), w0[!p].end());
s[!p] = std::move(strat_wnp); s[!p] = std::move(strat_wnp);
s[!p].insert(s0[!p].begin(), s0[!p].end()); s[!p].insert(s0[!p].begin(), s0[!p].end());
s[!p].insert(s1[!p].begin(), s1[!p].end()); s[!p].insert(s1[!p].begin(), s1[!p].end());
subgame.insert(w0[!p].begin(), w0[!p].end()); subgame.insert(w0[!p].begin(), w0[!p].end());
} }
} // anonymous
void pg_print(std::ostream& os, const const_twa_graph_ptr& arena)
{
auto owner = ensure_parity_game(arena, "pg_print");
unsigned ns = arena->num_states();
unsigned init = arena->get_init_state_number();
os << "parity " << ns - 1 << ";\n";
std::vector<bool> seen(ns, false);
std::vector<unsigned> 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";
}
}
void parity_game_solve(const const_twa_graph_ptr& arena,
region_t (&w)[2], strategy_t (&s)[2])
{
const std::vector<bool>* 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(), w, s);
}
} }
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).