From 9a17f5676c03e61770b73ce13166521871c9faaf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Dec 2020 17:18:20 +0100 Subject: [PATCH] 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. --- NEWS | 4 +- doc/org/tut.org | 2 +- spot/twaalgos/game.cc | 117 ++- spot/twaalgos/game.hh | 28 +- tests/Makefile.am | 2 +- tests/python/except.py | 23 +- .../python/{paritygame.ipynb => games.ipynb} | 695 +++++++++++++++++- 7 files changed, 784 insertions(+), 87 deletions(-) rename tests/python/{paritygame.ipynb => games.ipynb} (53%) diff --git a/NEWS b/NEWS index 42b2cf712..a524e91ec 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/doc/org/tut.org b/doc/org/tut.org index 67f1eae92..ba8f893b5 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -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=]] diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 03fca1bea..1f47da445 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -19,7 +19,6 @@ #include "config.h" -#include #include #include #include @@ -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 seen(game->num_states(), false); - std::vector 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 transposed; + // Reverse the automaton, compute the out degree of + // each state, and save dead-states in queue. + transposed.new_states(ns); + std::vector out_degree; + out_degree.reserve(ns); + std::vector queue; + for (unsigned s = 0; s < ns; ++s) { - for (const auto& e : edges) - todo.push_back(e.dst); - seen[cur] = true; - } - else - { - todo.pop_back(); - bool player = owners[cur]; - - auto it = std::find_if(edges.begin(), edges.end(), - [&winners, player](auto& e) + unsigned deg = 0; + for (auto& e: game->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; - } - } + 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); + } + } + // 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()) + { + unsigned s = queue.back(); + queue.pop_back(); + for (auto& e: transposed.out(s)) + { + 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()]; } diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index 9e125de53..58adfeb14 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -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); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 0bb285224..cd3d3c01a 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/python/except.py b/tests/python/except.py index f911474e8..fdd1cf64a 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -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() diff --git a/tests/python/paritygame.ipynb b/tests/python/games.ipynb similarity index 53% rename from tests/python/paritygame.ipynb rename to tests/python/games.ipynb index 597e3d5ee..2da7d8a03 100644 --- a/tests/python/paritygame.ipynb +++ b/tests/python/games.ipynb @@ -7,6 +7,7 @@ "outputs": [], "source": [ "import spot\n", + "from buddy import bddtrue\n", "spot.setup()" ] }, @@ -14,14 +15,653 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Support for parity games\n", + "# Support for games\n", "\n", - "The support for parity games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n", + "The support for games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n", "\n", - "In essence, a parity game is just a parity automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1.\n", + "In essence, agame is just an ω-automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1. The player owning a state can decide what the next transition from this state should be. The goal for player 1 is to force the play to be infinite and to satisfy the acceptance condition of the automaton, while the goal for player 0 is to prevent it by either forcing a finite play, or forcing an infinite play that does not satisfy the acceptance condition.\n", "\n", - "Player 1 is winning if it has a strategy to satisfy the acceptance condition regardless of player 0's moves.\n", - "Player 0 is winning if it has a strategy to not satisfy the acceptance codition regardless of player 1's moves." + "The support is currently restricted to games that use:\n", + "- `t` acceptance: all infinite run are accepting, and player 0 can only win if it manages to force a finite play (this requires reaching states without successors).\n", + "- max odd parity acceptance: player 0 can win if the maximal value seen infinitely often is even" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Creating games from scratch\n", + "\n", + "Games can be [created like any automaton](https://spot.lrde.epita.fr/tut22.html). \n", + "Using `set_state_players()` will fix the state owners." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\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", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "bdict = spot.make_bdd_dict();\n", + "game = spot.make_twa_graph(bdict)\n", + "game.new_states(9)\n", + "for (s, d) in ((0,1), (0, 3), \n", + " (1, 0), (1, 2),\n", + " (2, 1), (2, 5),\n", + " (3, 2), (3, 4), (3, 6),\n", + " (6, 7),\n", + " (7, 6), (7, 8),\n", + " (8, 5)):\n", + " game.new_edge(s, d, bddtrue)\n", + "spot.set_state_players(game, [True, False, True, False, True, True, True, False, False])\n", + "game.show('.g') # Use \"g\" to hide the irrelevant edge labels." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `set_state_players()` function takes a list of owner for each of the states in the automaton. In the output,\n", + "states from player 0 use circles, ellispes, or rectangle with rounded corners (mnemonic: 0 is round) while states from player 1 have a losanse shape (1 has only straight lines). \n", + "\n", + "\n", + "State ownership can also be manipulated by the following functions:" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(True, False, True, False, True, True, True, False, False)" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.get_state_players(game)" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "1" + ] + }, + "execution_count": 4, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.get_state_player(game, 4)" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\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", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.set_state_player(game, 4, False)\n", + "game.show('.g')" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Solving a game\n", + "\n", + "Solving a game is done my calling `solve_safety_game()` or `solve_parity_game()`. This will attach two additional vectors into the game automaton: one vector stores the winner of each state, and one vector stores (memory-less) strategy for each state, i.e., the transition that should always be taken by the owner of this state in order to win. \n", + "\n", + "The return value of those function is simply the winner for the initial state." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.solve_safety_game(game)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Calling the `highlight_strategy()` function can be used to decorate the `game` automaton using the winning regions and strategies. Below, green represent the winning region/strategy for player 1 and red those for player 0." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\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", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8->5\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "spot.highlight_strategy(game)\n", + "game.show('.g')" ] }, { @@ -35,7 +675,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -272,10 +912,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f9bf8477330> >" + " *' at 0x7fa3979355d0> >" ] }, - "execution_count": 2, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -296,7 +936,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 9, "metadata": {}, "outputs": [ { @@ -353,19 +993,12 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Solving games" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "The `solve_parity_game()` function returns the player winning from the initial state (`False` for player 0, and `True` for player 1)." + "Here is the solution of this particular game." ] }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 10, "metadata": {}, "outputs": [ { @@ -374,7 +1007,7 @@ "True" ] }, - "execution_count": 4, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -383,18 +1016,9 @@ "spot.solve_parity_game(game)" ] }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "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": 5, + "execution_count": 11, "metadata": {}, "outputs": [ { @@ -631,10 +1255,10 @@ "\n" ], "text/plain": [ - " *' at 0x7f9bf83e1060> >" + " *' at 0x7fa37f087db0> >" ] }, - "execution_count": 5, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } @@ -642,6 +1266,13 @@ "source": [ "spot.highlight_strategy(game)" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -660,7 +1291,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.6rc1" + "version": "3.9.1rc1" } }, "nbformat": 4,