spot  2.11.6
game.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2017-2023 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 {
38 
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 
78  SPOT_API
79  bool solve_parity_game(const twa_graph_ptr& arena);
80 
95  SPOT_API
96  bool solve_safety_game(const twa_graph_ptr& game);
97 
110  SPOT_API bool
111  solve_game(const twa_graph_ptr& arena);
112 
113 
128  SPOT_API
129  std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena);
130 
131  SPOT_DEPRECATED("use print_pg() instead")
132  SPOT_API
133  void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
135 
140  SPOT_API
141  twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
142  int player0_color = 5,
143  int player1_color = 4);
144 
148  SPOT_API
149  void set_state_players(twa_graph_ptr arena, const region_t& owners);
150  SPOT_API
151  void set_state_players(twa_graph_ptr arena, region_t&& owners);
153 
156  SPOT_API
157  void set_state_player(twa_graph_ptr arena, unsigned state, bool owner);
158 
161  SPOT_API
162  bool get_state_player(const_twa_graph_ptr arena, unsigned state);
163 
167  SPOT_API
168  const region_t& get_state_players(const const_twa_graph_ptr& arena);
169  SPOT_API
170  const region_t& get_state_players(twa_graph_ptr& arena);
172 
176  SPOT_API
177  const strategy_t& get_strategy(const const_twa_graph_ptr& arena);
178  SPOT_API
179  void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
180  SPOT_API
181  void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
183 
186  SPOT_API
187  void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
188 
191  SPOT_API
192  bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
193 
195  SPOT_API
196  std::vector<std::string>
197  get_synthesis_output_aps(const const_twa_graph_ptr& arena);
198 
202  SPOT_API
203  void set_state_winners(twa_graph_ptr arena, const region_t& winners);
204  SPOT_API
205  void set_state_winners(twa_graph_ptr arena, region_t&& winners);
207 
210  SPOT_API
211  void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
212 
215  SPOT_API
216  bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
217 
220  SPOT_API
221  const region_t& get_state_winners(const const_twa_graph_ptr& arena);
222 }
Abstract class for states.
Definition: twa.hh:51
bool get_state_winner(const_twa_graph_ptr arena, unsigned state)
Get the winner of a state.
const region_t & get_state_players(const const_twa_graph_ptr &arena)
Get the owner of all states.
const strategy_t & get_strategy(const const_twa_graph_ptr &arena)
Get or set the strategy.
std::ostream & print_pg(std::ostream &os, const const_twa_graph_ptr &arena)
Print a parity game using PG-solver syntax.
void set_strategy(twa_graph_ptr arena, const strategy_t &strat)
Get or set the strategy.
void pg_print(std::ostream &os, const const_twa_graph_ptr &arena)
Print a parity game using PG-solver syntax.
void set_state_players(twa_graph_ptr arena, const region_t &owners)
Set the owner for all the states.
bool solve_safety_game(const twa_graph_ptr &game)
Solve a safety game.
bdd get_synthesis_outputs(const const_twa_graph_ptr &arena)
Get all synthesis outputs as a conjunction.
bool solve_parity_game(const twa_graph_ptr &arena)
solve a parity-game
bool solve_game(const twa_graph_ptr &arena)
Generic interface for game solving.
twa_graph_ptr highlight_strategy(twa_graph_ptr &arena, int player0_color=5, int player1_color=4)
Highlight the edges of a strategy on an automaton.
void set_state_player(twa_graph_ptr arena, unsigned state, bool owner)
Set the owner of a state.
const region_t & get_state_winners(const const_twa_graph_ptr &arena)
Get the winner of all states.
void set_state_winners(twa_graph_ptr arena, const region_t &winners)
Set the winner for all the states.
void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner)
Set the winner of a state.
void set_synthesis_outputs(const twa_graph_ptr &arena, const bdd &outs)
Set all synthesis outputs as a conjunction.
bool get_state_player(const_twa_graph_ptr arena, unsigned state)
Get the owner of a state.
void alternate_players(spot::twa_graph_ptr &arena, bool first_player=false, bool complete0=true)
Transform an automaton into a parity game by propagating players.
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
Definition: automata.hh:27
std::vector< std::string > get_synthesis_output_aps(const const_twa_graph_ptr &arena)
Get the vector with the names of the output propositions.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1