spot  2.12
game.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <algorithm>
22 #include <memory>
23 #include <ostream>
24 #include <unordered_map>
25 #include <vector>
26 #include <optional>
27 
28 #include <bddx.h>
29 #include <spot/misc/optionmap.hh>
30 #include <spot/twa/twagraph.hh>
31 #include <spot/twaalgos/parity.hh>
32 
33 namespace spot
34 {
37 
48  SPOT_API
49  void alternate_players(spot::twa_graph_ptr& arena,
50  bool first_player = false,
51  bool complete0 = true);
52 
53 
54  // false -> env, true -> player
55  typedef std::vector<bool> region_t;
56  // state idx -> global edge number
57  typedef std::vector<unsigned> strategy_t;
58 
59 
82  SPOT_API
83  bool solve_parity_game(const twa_graph_ptr& arena,
84  bool solve_globally = false);
85 
100  SPOT_API
101  bool solve_safety_game(const twa_graph_ptr& game);
102 
115  SPOT_API bool
116  solve_game(const twa_graph_ptr& arena);
117 
118 
133  SPOT_API
134  std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena);
135 
136  SPOT_DEPRECATED("use print_pg() instead")
137  SPOT_API
138  void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
140 
145  SPOT_API
146  twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
147  int player0_color = 5,
148  int player1_color = 4);
149 
153  SPOT_API
154  void set_state_players(twa_graph_ptr arena, const region_t& owners);
155  SPOT_API
156  void set_state_players(twa_graph_ptr arena, region_t&& owners);
158 
161  SPOT_API
162  void set_state_player(twa_graph_ptr arena, unsigned state, bool owner);
163 
166  SPOT_API
167  bool get_state_player(const_twa_graph_ptr arena, unsigned state);
168 
172  SPOT_API
173  const region_t& get_state_players(const const_twa_graph_ptr& arena);
174  SPOT_API
175  const region_t& get_state_players(twa_graph_ptr& arena);
177 
181  SPOT_API
182  const strategy_t& get_strategy(const const_twa_graph_ptr& arena);
183  SPOT_API
184  void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
185  SPOT_API
186  void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
188 
191  SPOT_API
192  void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
193 
196  SPOT_API
197  bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
198 
200  SPOT_API
201  std::vector<std::string>
202  get_synthesis_output_aps(const const_twa_graph_ptr& arena);
203 
207  SPOT_API
208  void set_state_winners(twa_graph_ptr arena, const region_t& winners);
209  SPOT_API
210  void set_state_winners(twa_graph_ptr arena, region_t&& winners);
212 
215  SPOT_API
216  void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
217 
220  SPOT_API
221  bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
222 
225  SPOT_API
226  const region_t& get_state_winners(const const_twa_graph_ptr& arena);
227 }
Abstract class for states.
Definition: twa.hh:47
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.
bool solve_parity_game(const twa_graph_ptr &arena, bool solve_globally=false)
solve a parity-game
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_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.
Definition: automata.hh:26
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