Commit 760bde09 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

python: add some parity-game bindings

* python/spot/impl.i: Process game.hh.
* spot/misc/game.cc, spot/misc/game.hh: Make the output of
parity_game_solve() a solved_game object for easier manipulation in
Python.
* bin/ltlsynt.cc: Adjust usage.
* tests/python/paritygame.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention these bindings.
parent 9e8a8429
Pipeline #21504 passed with stages
in 569 minutes and 32 seconds
...@@ -79,6 +79,11 @@ New in spot 2.9.4.dev (not yet released) ...@@ -79,6 +79,11 @@ New in spot 2.9.4.dev (not yet released)
- print_dot() will display states from player 1 using a diamond - print_dot() will display states from player 1 using a diamond
shape. shape.
Python:
- Bindings for functions related to parity games.
See https://spot.lrde.epita.fr/ipynb/paritygame.html for examples.
New in spot 2.9.4 (2020-09-07) New in spot 2.9.4 (2020-09-07)
Bugs fixed: Bugs fixed:
......
...@@ -216,11 +216,10 @@ namespace ...@@ -216,11 +216,10 @@ namespace
static spot::twa_graph_ptr static spot::twa_graph_ptr
strat_to_aut(const spot::const_twa_graph_ptr& pg, strat_to_aut(const spot::const_twa_graph_ptr& pg,
const spot::strategy_t& strat, const spot::strategy_t& strat,
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(pg->get_dict());
aut->copy_ap_of(dpa); aut->copy_ap_of(pg);
unsigned pg_init = pg->get_init_state_number(); unsigned pg_init = pg->get_init_state_number();
std::vector<unsigned> todo{pg_init}; std::vector<unsigned> todo{pg_init};
std::vector<int> pg2aut(pg->num_states(), -1); std::vector<int> pg2aut(pg->num_states(), -1);
...@@ -230,10 +229,10 @@ namespace ...@@ -230,10 +229,10 @@ namespace
{ {
unsigned s = todo.back(); unsigned s = todo.back();
todo.pop_back(); todo.pop_back();
for (auto& e1: dpa->out(s)) for (auto& e1: pg->out(s))
{ {
unsigned i = 0; unsigned i = 0;
for (auto& e2: dpa->out(e1.dst)) for (auto& e2: pg->out(e1.dst))
{ {
bool self_loop = false; bool self_loop = false;
if (e1.dst == s || e2.dst == e1.dst) if (e1.dst == s || e2.dst == e1.dst)
...@@ -520,18 +519,16 @@ namespace ...@@ -520,18 +519,16 @@ namespace
return 0; return 0;
} }
spot::strategy_t strategy[2];
spot::region_t winning_region[2];
if (want_time) if (want_time)
sw.start(); sw.start();
parity_game_solve(dpa, winning_region, strategy); auto solution = parity_game_solve(dpa);
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 = dpa->num_states(); nb_states_parity_game = dpa->num_states();
timer.stop(); timer.stop();
if (winning_region[1].count(dpa->get_init_state_number())) if (solution.player_winning_at(1, dpa->get_init_state_number()))
{ {
std::cout << "REALIZABLE\n"; std::cout << "REALIZABLE\n";
if (!opt_real) if (!opt_real)
...@@ -539,7 +536,7 @@ namespace ...@@ -539,7 +536,7 @@ namespace
if (want_time) if (want_time)
sw.start(); sw.start();
auto strat_aut = auto strat_aut =
strat_to_aut(dpa, strategy[1], dpa, all_outputs); strat_to_aut(dpa, solution.winning_strategy[1], all_outputs);
if (want_time) if (want_time)
strat2aut_time = sw.stop(); strat2aut_time = sw.stop();
......
...@@ -72,6 +72,7 @@ real notebooks instead. ...@@ -72,6 +72,7 @@ real notebooks instead.
automata automata
- [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata
in Python in Python
- [[https://spot.lrde.epita.fr/ipynb/paritygame.html][=paritygame.ipynb=]] illustrates support for parity games
- [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata
in Python in Python
- [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]]
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009-2019 Laboratoire de Recherche et Développement // Copyright (C) 2009-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
...@@ -164,6 +164,8 @@ ...@@ -164,6 +164,8 @@
#include <spot/parseaut/public.hh> #include <spot/parseaut/public.hh>
#include <spot/misc/game.hh>
#include <spot/kripke/fairkripke.hh> #include <spot/kripke/fairkripke.hh>
#include <spot/kripke/kripke.hh> #include <spot/kripke/kripke.hh>
#include <spot/kripke/kripkegraph.hh> #include <spot/kripke/kripkegraph.hh>
...@@ -690,6 +692,8 @@ def state_is_accepting(self, src) -> "bool": ...@@ -690,6 +692,8 @@ def state_is_accepting(self, src) -> "bool":
%include <spot/twaalgos/complement.hh> %include <spot/twaalgos/complement.hh>
%include <spot/misc/game.hh>
%include <spot/kripke/fairkripke.hh> %include <spot/kripke/fairkripke.hh>
%include <spot/kripke/kripke.hh> %include <spot/kripke/kripke.hh>
%include <spot/kripke/kripkegraph.hh> %include <spot/kripke/kripkegraph.hh>
......
...@@ -230,9 +230,11 @@ namespace spot ...@@ -230,9 +230,11 @@ namespace spot
} }
} }
void parity_game_solve(const const_twa_graph_ptr& arena, solved_game parity_game_solve(const const_twa_graph_ptr& arena)
region_t (&w)[2], strategy_t (&s)[2])
{ {
solved_game result;
result.arena = arena;
const std::vector<bool>* owner = const std::vector<bool>* owner =
ensure_parity_game(arena, "parity_game_solve"); ensure_parity_game(arena, "parity_game_solve");
...@@ -245,7 +247,10 @@ namespace spot ...@@ -245,7 +247,10 @@ namespace spot
for (const auto& e: arena->edges()) for (const auto& e: arena->edges())
m |= e.acc; m |= e.acc;
solve_rec(arena, owner, states_, m.max_set(), w, s); solve_rec(arena, owner, states_, m.max_set(),
result.winning_region, result.winning_strategy);
return result;
} }
void propagate_players(spot::twa_graph_ptr& arena, void propagate_players(spot::twa_graph_ptr& arena,
...@@ -304,4 +309,44 @@ namespace spot ...@@ -304,4 +309,44 @@ namespace spot
arena->set_named_prop("state-player", owner); arena->set_named_prop("state-player", owner);
} }
twa_graph_ptr
highlight_strategy(twa_graph_ptr& aut, const strategy_t& s,
unsigned color)
{
unsigned ns = aut->num_states();
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
("highlight-edges");
for (auto [src, n]: s)
{
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;
}
}
return aut;
}
twa_graph_ptr
solved_game::highlight_strategy(unsigned player, unsigned color)
{
auto aut = std::const_pointer_cast<twa_graph>(arena);
auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>
("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);
}
} }
...@@ -50,6 +50,24 @@ namespace spot ...@@ -50,6 +50,24 @@ namespace spot
typedef std::unordered_set<unsigned> region_t; typedef std::unordered_set<unsigned> region_t;
typedef std::unordered_map<unsigned, unsigned> strategy_t; typedef std::unordered_map<unsigned, unsigned> 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 /// \brief solve a parity-game
/// ///
/// The arena is a deterministic max odd parity automaton with a /// The arena is a deterministic max odd parity automaton with a
...@@ -59,10 +77,16 @@ namespace spot ...@@ -59,10 +77,16 @@ namespace spot
/// game for player 1 using Zielonka's recursive algorithm. /// game for player 1 using Zielonka's recursive algorithm.
/// \cite zielonka.98.tcs /// \cite zielonka.98.tcs
SPOT_API SPOT_API
void parity_game_solve(const const_twa_graph_ptr& arena, solved_game 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 /// \brief Print a max odd parity game using PG-solver syntax
SPOT_API SPOT_API
void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
/// \brief Highlight the edges of a strategy on an automaton.
SPOT_API
twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
const strategy_t& s,
unsigned color);
} }
...@@ -362,6 +362,7 @@ TESTS_ipython = \ ...@@ -362,6 +362,7 @@ TESTS_ipython = \
python/ltsmin-dve.ipynb \ python/ltsmin-dve.ipynb \
python/ltsmin-pml.ipynb \ python/ltsmin-pml.ipynb \
python/parity.ipynb \ python/parity.ipynb \
python/paritygame.ipynb \
python/product.ipynb \ python/product.ipynb \
python/randaut.ipynb \ python/randaut.ipynb \
python/randltl.ipynb \ python/randltl.ipynb \
......
This diff is collapsed.
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