spot 2.11.3.dev
game.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2017-2022 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
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
166 SPOT_API
167 const region_t& get_state_players(const_twa_graph_ptr arena);
168
172 SPOT_API
173 const strategy_t& get_strategy(const_twa_graph_ptr arena);
174 SPOT_API
175 void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
176 SPOT_API
177 void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
179
182 SPOT_API
183 void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
184
187 SPOT_API
188 bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
189
191 SPOT_API
192 std::vector<std::string>
193 get_synthesis_output_aps(const const_twa_graph_ptr& arena);
194
198 SPOT_API
199 void set_state_winners(twa_graph_ptr arena, const region_t& winners);
200 SPOT_API
201 void set_state_winners(twa_graph_ptr arena, region_t&& winners);
203
206 SPOT_API
207 void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
208
211 SPOT_API
212 bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
213
216 SPOT_API
217 const region_t& get_state_winners(const_twa_graph_ptr arena);
218}
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_twa_graph_ptr arena)
Get the owner of all states.
void set_strategy(twa_graph_ptr arena, const strategy_t &strat)
Get or set the strategy.
const strategy_t & get_strategy(const_twa_graph_ptr arena)
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.
const region_t & get_state_winners(const_twa_graph_ptr arena)
Get the winner of all states.
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.
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.
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.4