1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017-2021 Laboratoire de Recherche et Développement 3 // de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <algorithm> 23 #include <memory> 24 #include <ostream> 25 #include <unordered_map> 26 #include <vector> 27 #include <optional> 28 29 #include <bddx.h> 30 #include <spot/misc/optionmap.hh> 31 #include <spot/twa/twagraph.hh> 32 #include <spot/twaalgos/parity.hh> 33 34 namespace spot 35 { 36 /// \addtogroup games Functions related to game solving 37 /// \ingroup twa_algorithms 38 39 /// \ingroup games 40 /// \brief Transform an automaton into a parity game by propagating 41 /// players 42 /// 43 /// This propagate state players, assuming the initial state belong 44 /// to \a first_player, and alternating players on each transitions. 45 /// If an odd cycle is detected, a runtime_exception is raised. 46 /// 47 /// If \a complete0 is set, ensure that states of player 0 are 48 /// complete. 49 SPOT_API 50 void alternate_players(spot::twa_graph_ptr& arena, 51 bool first_player = false, 52 bool complete0 = true); 53 54 55 // false -> env, true -> player 56 typedef std::vector<bool> region_t; 57 // state idx -> global edge number 58 typedef std::vector<unsigned> strategy_t; 59 60 61 /// \ingroup games 62 /// \brief solve a parity-game 63 /// 64 /// The arena is a deterministic max odd parity automaton with a 65 /// "state-player" property. 66 /// 67 /// Player 1 tries to satisfy the acceptance condition, while player 68 /// 0 tries to prevent that. 69 /// 70 /// This computes the winning strategy and winning region using 71 /// Zielonka's recursive algorithm. \cite zielonka.98.tcs 72 /// 73 /// Also includes some inspiration from Oink. 74 /// \cite vandijk.18.tacas 75 /// 76 /// Returns the player winning in the initial state, and sets 77 /// the state-winner and strategy named properties. 78 SPOT_API 79 bool solve_parity_game(const twa_graph_ptr& arena); 80 81 /// \ingroup games 82 /// \brief Solve a safety game. 83 /// 84 /// The arena should be represented by an automaton with true 85 /// acceptance. 86 /// 87 /// Player 1 tries to satisfy the acceptance condition, while player 88 /// 0 tries to prevent that. The only way for player 0 to win is 89 /// to find a way to move the play toward a state without successor. 90 /// If there no state without successors, then the game is necessarily 91 /// winning for player 1. 92 /// 93 /// Returns the player winning in the initial state, and sets 94 /// the state-winner and strategy named properties. 95 SPOT_API 96 bool solve_safety_game(const twa_graph_ptr& game); 97 98 /// \ingroup games 99 /// \brief Generic interface for game solving 100 /// 101 /// Dispatch to solve_safety_game() if the acceptance condition is 102 /// t, or to solve_parity_game() if it is a parity acceptance. Note that 103 /// parity acceptance include Büchi, co-Büchi, Rabin 1, and Streett 1. 104 /// 105 /// Currently unable to solve game with other acceptance conditions 106 /// that are not parity. 107 /// 108 /// Return the winning player for the initial state, and sets 109 /// the state-winner and strategy named properties. 110 SPOT_API bool 111 solve_game(const twa_graph_ptr& arena); 112 113 114 /// \ingroup games 115 /// \brief Print a max odd parity game using PG-solver syntax 116 SPOT_API 117 void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); 118 119 120 /// \ingroup games 121 /// \brief Highlight the edges of a strategy on an automaton. 122 /// 123 /// Pass a negative color to not display the corresponding strategy. 124 SPOT_API 125 twa_graph_ptr highlight_strategy(twa_graph_ptr& arena, 126 int player0_color = 5, 127 int player1_color = 4); 128 129 /// \ingroup games 130 /// \brief Set the owner for all the states. 131 /// @{ 132 SPOT_API 133 void set_state_players(twa_graph_ptr arena, const region_t& owners); 134 SPOT_API 135 void set_state_players(twa_graph_ptr arena, region_t&& owners); 136 /// @} 137 138 /// \ingroup games 139 /// \brief Set the owner of a state. 140 SPOT_API 141 void set_state_player(twa_graph_ptr arena, unsigned state, bool owner); 142 143 /// \ingroup games 144 /// \brief Get the owner of a state. 145 SPOT_API 146 bool get_state_player(const_twa_graph_ptr arena, unsigned state); 147 148 /// \ingroup games 149 /// \brief Get the owner of all states 150 SPOT_API 151 const region_t& get_state_players(const_twa_graph_ptr arena); 152 153 /// \ingroup games 154 /// \brief Get or set the strategy 155 /// @{ 156 SPOT_API 157 const strategy_t& get_strategy(const_twa_graph_ptr arena); 158 SPOT_API 159 void set_strategy(twa_graph_ptr arena, const strategy_t& strat); 160 SPOT_API 161 void set_strategy(twa_graph_ptr arena, strategy_t&& strat); 162 /// @} 163 164 /// \ingroup games 165 /// \brief Set all synthesis outputs as a conjunction 166 SPOT_API 167 void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs); 168 169 /// \ingroup games 170 /// \brief Get all synthesis outputs as a conjunction 171 SPOT_API 172 bdd get_synthesis_outputs(const const_twa_graph_ptr& arena); 173 174 /// \brief Get the vector with the names of the output propositions 175 SPOT_API 176 std::vector<std::string> 177 get_synthesis_output_aps(const const_twa_graph_ptr& arena); 178 179 /// \ingroup games 180 /// \brief Set the winner for all the states. 181 /// @{ 182 SPOT_API 183 void set_state_winners(twa_graph_ptr arena, const region_t& winners); 184 SPOT_API 185 void set_state_winners(twa_graph_ptr arena, region_t&& winners); 186 /// @} 187 188 /// \ingroup games 189 /// \brief Set the winner of a state. 190 SPOT_API 191 void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner); 192 193 /// \ingroup games 194 /// \brief Get the winner of a state. 195 SPOT_API 196 bool get_state_winner(const_twa_graph_ptr arena, unsigned state); 197 198 /// \ingroup games 199 /// \brief Get the winner of all states 200 SPOT_API 201 const region_t& get_state_winners(const_twa_graph_ptr arena); 202 } 203