spot 2.11.6.dev
Loading...
Searching...
No Matches
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
34namespace 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
83 SPOT_API
84 bool solve_parity_game(const twa_graph_ptr& arena,
85 bool solve_globally = false);
86
101 SPOT_API
102 bool solve_safety_game(const twa_graph_ptr& game);
103
116 SPOT_API bool
117 solve_game(const twa_graph_ptr& arena);
118
119
134 SPOT_API
135 std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena);
136
137 SPOT_DEPRECATED("use print_pg() instead")
138 SPOT_API
139 void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
141
146 SPOT_API
147 twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
148 int player0_color = 5,
149 int player1_color = 4);
150
154 SPOT_API
155 void set_state_players(twa_graph_ptr arena, const region_t& owners);
156 SPOT_API
157 void set_state_players(twa_graph_ptr arena, region_t&& owners);
159
162 SPOT_API
163 void set_state_player(twa_graph_ptr arena, unsigned state, bool owner);
164
167 SPOT_API
168 bool get_state_player(const_twa_graph_ptr arena, unsigned state);
169
173 SPOT_API
174 const region_t& get_state_players(const const_twa_graph_ptr& arena);
175 SPOT_API
176 const region_t& get_state_players(twa_graph_ptr& arena);
178
182 SPOT_API
183 const strategy_t& get_strategy(const const_twa_graph_ptr& arena);
184 SPOT_API
185 void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
186 SPOT_API
187 void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
189
192 SPOT_API
193 void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
194
197 SPOT_API
198 bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
199
201 SPOT_API
202 std::vector<std::string>
203 get_synthesis_output_aps(const const_twa_graph_ptr& arena);
204
208 SPOT_API
209 void set_state_winners(twa_graph_ptr arena, const region_t& winners);
210 SPOT_API
211 void set_state_winners(twa_graph_ptr arena, region_t&& winners);
213
216 SPOT_API
217 void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
218
221 SPOT_API
222 bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
223
226 SPOT_API
227 const region_t& get_state_winners(const const_twa_graph_ptr& arena);
228}
Abstract class for states.
Definition twa.hh:51
const region_t & get_state_winners(const const_twa_graph_ptr &arena)
Get the winner of all states.
bool get_state_winner(const_twa_graph_ptr arena, unsigned state)
Get the winner of a state.
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.
const strategy_t & get_strategy(const const_twa_graph_ptr &arena)
Get or set the strategy.
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.
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.
std::ostream & print_pg(std::ostream &os, const const_twa_graph_ptr &arena)
Print a parity game using PG-solver syntax.
const region_t & get_state_players(const const_twa_graph_ptr &arena)
Get the owner of all states.
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: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.8