25 #include <unordered_map>
30 #include <spot/misc/optionmap.hh>
31 #include <spot/twa/twagraph.hh>
32 #include <spot/twaalgos/parity.hh>
51 bool first_player =
false,
52 bool complete0 =
true);
56 typedef std::vector<bool> region_t;
58 typedef std::vector<unsigned> strategy_t;
129 std::ostream&
print_pg(std::ostream& os,
const const_twa_graph_ptr& arena);
133 void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
142 int player0_color = 5,
143 int player1_color = 4);
196 std::vector<std::
string>
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.
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.