Commit 9a17f567 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

game: rewrite, document, and rename solve_reachability_game

* spot/twaalgos/game.hh, spot/twaalgos/game.cc: Rename
solve_reachability_game() as solve_safety_game(), rewrite it (the old
implementation incorrectly marked dead states as winning for their
owner).
* tests/python/paritygame.ipynb: Rename as...
* tests/python/games.ipynb: ... this, and illustrate
solve_safety_game().
* tests/Makefile.am, NEWS, doc/org/tut.org: Adjust.
* tests/python/except.py: Add more tests.
parent 05449a42
Pipeline #24195 passed with stages
in 193 minutes and 59 seconds
......@@ -148,8 +148,8 @@ New in spot 2.9.5.dev (not yet released)
Python:
- Bindings for functions related to parity games.
See https://spot.lrde.epita.fr/ipynb/paritygame.html for examples.
- Bindings for functions related to games.
See https://spot.lrde.epita.fr/ipynb/games.html for examples.
Bugs fixed:
......
......@@ -72,7 +72,7 @@ real notebooks instead.
automata
- [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata
in Python
- [[https://spot.lrde.epita.fr/ipynb/paritygame.html][=paritygame.ipynb=]] illustrates support for parity games
- [[https://spot.lrde.epita.fr/ipynb/games.html][=games.ipynb=]] illustrates support for games
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
in Python
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
......
......@@ -19,7 +19,6 @@
#include "config.h"
#include <cmath>
#include <spot/twaalgos/game.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh>
......@@ -958,53 +957,91 @@ namespace spot
return (*owners)[state] ? 1 : 0;
}
bool solve_reachability_game(twa_graph_ptr game)
bool solve_safety_game(twa_graph_ptr game)
{
if (!game->acc().is_t())
throw std::runtime_error
("solve_safety_game(): arena should have true acceptance");
auto owners = get_state_players(game);
auto winners = new region_t(game->num_states(), true);
unsigned ns = game->num_states();
auto winners = new region_t(ns, true);
game->set_named_prop("state-winner", winners);
auto strategy = new strategy_t(game->num_states(), 0);
auto strategy = new strategy_t(ns, 0);
game->set_named_prop("strategy", strategy);
std::vector<bool> seen(game->num_states(), false);
std::vector<unsigned> todo;
todo.reserve(game->num_states());
auto& g = game->get_graph();
todo.push_back(game->get_init_state_number());
while (!todo.empty())
{
unsigned cur = todo.back();
auto edges = game->out(cur);
if (!seen[cur])
// transposed is a reversed copy of game to compute predecessors
// more easily. It also keep track of the original edge iindex.
struct edge_data {
unsigned edgeidx;
};
digraph<void, edge_data> transposed;
// Reverse the automaton, compute the out degree of
// each state, and save dead-states in queue.
transposed.new_states(ns);
std::vector<unsigned> out_degree;
out_degree.reserve(ns);
std::vector<unsigned> queue;
for (unsigned s = 0; s < ns; ++s)
{
for (const auto& e : edges)
todo.push_back(e.dst);
seen[cur] = true;
unsigned deg = 0;
for (auto& e: game->out(s))
{
transposed.new_edge(e.dst, e.src, game->edge_number(e));
++deg;
}
out_degree.push_back(deg);
if (deg == 0)
{
(*winners)[s] = false;
queue.push_back(s);
}
}
else
// queue is initially filled with dead-states, which are winning
// for player 0. Any predecessor owned by player 0 is therefore
// winning as well (check 1), and any predecessor owned by player
// 1 that has all its successors winning for player 0 (check 2) is
// also winning. Use queue to propagate everything.
// For the second check, we decrease out_degree by each edge leading
// to a state winning for player 0, so if out_degree reaches 0,
// we have ensured that all outgoing transitions are winning for 0.
//
// We use queue as a stack, to propagate bad states in DFS.
// However it would be ok to replace the vector by a std::deque
// to implement a BFS and build shorter strategies for player 0.
// Right no we are assuming that strategies for player 0 have
// limited uses, so we just avoid the overhead of std::deque in
// favor of the simpler std::vector.
while (!queue.empty())
{
todo.pop_back();
bool player = owners[cur];
auto it = std::find_if(edges.begin(), edges.end(),
[&winners, player](auto& e)
unsigned s = queue.back();
queue.pop_back();
for (auto& e: transposed.out(s))
{
return (*winners)[e.dst] == player;
});
if (it != edges.end())
{
(*strategy)[cur] = g.index_of_edge(*it);
(*winners)[cur] = player;
}
else
(*winners)[cur] = !player;
}
}
unsigned pred = e.dst;
if (!(*winners)[pred])
continue;
// check 1 || check 2
bool check1 = owners[pred] == false;
if (check1 || --out_degree[pred] == 0)
{
(*winners)[pred] = false;
queue.push_back(pred);
if (check1)
(*strategy)[pred] = e.edgeidx;
}
}
}
// Let's fill in the strategy for Player 1.
for (unsigned s = 0; s < ns; ++s)
if (owners[s] && (*winners)[s])
for (auto& e: game->out(s))
if ((*winners)[e.dst])
{
(*strategy)[s] = game->edge_number(e);
break;
}
return (*winners)[game->get_init_state_number()];
}
......
......@@ -58,9 +58,11 @@ namespace spot
/// 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
/// Player 1 tries to satisfy the acceptance condition, while player
/// 0 tries to prevent that.
///
/// This computes the winning strategy and winning region using
/// Zielonka's recursive algorithm. \cite zielonka.98.tcs
///
/// Also includes some inspiration from Oink.
/// \cite vandijk.18.tacas
......@@ -70,6 +72,22 @@ namespace spot
SPOT_API
bool solve_parity_game(const twa_graph_ptr& arena);
/// \brief Solve a safety game.
///
/// The arena should be represented by an automaton with true
/// acceptance.
///
/// Player 1 tries to satisfy the acceptance condition, while player
/// 0 tries to prevent that. The only way for player 0 to win is
/// to find a way to move the play toward a state without successor.
/// If there no state without successors, then the game is necessarily
/// winning for player 1.
///
/// Returns the player winning in the initial state, and sets
/// the state-winner and strategy named properties.
SPOT_API
bool solve_safety_game(twa_graph_ptr game);
/// \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);
......@@ -100,8 +118,4 @@ namespace spot
/// \brief Get the owner of a state.
SPOT_API
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
/// \brief Solve a reachability game.
SPOT_API
bool solve_reachability_game(twa_graph_ptr game);
}
......@@ -357,12 +357,12 @@ TESTS_ipython = \
python/contains.ipynb \
python/decompose.ipynb \
python/formulas.ipynb \
python/games.ipynb \
python/gen.ipynb \
python/highlighting.ipynb \
python/ltsmin-dve.ipynb \
python/ltsmin-pml.ipynb \
python/parity.ipynb \
python/paritygame.ipynb \
python/product.ipynb \
python/randaut.ipynb \
python/randltl.ipynb \
......
......@@ -196,24 +196,39 @@ assert spot.is_deterministic(a2)
try:
spot.product_xor(a1, a2)
except RuntimeError as e:
assert "product_xor() only works with deterministic automata"
assert "product_xor() only works with deterministic automata" in str(e)
else:
report_missing_exception()
try:
spot.product_xor(a2, a1)
except RuntimeError as e:
assert "product_xor() only works with deterministic automata"
assert "product_xor() only works with deterministic automata" in str(e)
else:
report_missing_exception()
try:
spot.product_xnor(a1, a2)
except RuntimeError as e:
assert "product_xnor() only works with deterministic automata"
assert "product_xnor() only works with deterministic automata" in str(e)
else:
report_missing_exception()
try:
spot.product_xnor(a2, a1)
except RuntimeError as e:
assert "product_xnor() only works with deterministic automata"
assert "product_xnor() only works with deterministic automata" in str(e)
else:
report_missing_exception()
try:
spot.solve_safety_game(a1)
except RuntimeError as e:
assert "solve_safety_game(): arena should have true acceptance" in str(e)
else:
report_missing_exception()
try:
spot.solve_parity_game(a1)
except RuntimeError as e:
assert "solve_parity_game(): arena must have max-odd acceptance condition" \
in str(e)
else:
report_missing_exception()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment