spot
2.10.2.dev
|
Functions | |
void | spot::alternate_players (spot::twa_graph_ptr &arena, bool first_player=false, bool complete0=true) |
Transform an automaton into a parity game by propagating players. More... | |
bool | spot::solve_parity_game (const twa_graph_ptr &arena) |
solve a parity-game More... | |
bool | spot::solve_safety_game (const twa_graph_ptr &game) |
Solve a safety game. More... | |
bool | spot::solve_game (const twa_graph_ptr &arena) |
Generic interface for game solving. More... | |
void | spot::pg_print (std::ostream &os, const const_twa_graph_ptr &arena) |
Print a max odd parity game using PG-solver syntax. More... | |
twa_graph_ptr | spot::highlight_strategy (twa_graph_ptr &arena, int player0_color=5, int player1_color=4) |
Highlight the edges of a strategy on an automaton. More... | |
void | spot::set_state_player (twa_graph_ptr arena, unsigned state, bool owner) |
Set the owner of a state. More... | |
bool | spot::get_state_player (const_twa_graph_ptr arena, unsigned state) |
Get the owner of a state. More... | |
const region_t & | spot::get_state_players (const_twa_graph_ptr arena) |
Get the owner of all states. More... | |
void | spot::set_synthesis_outputs (const twa_graph_ptr &arena, const bdd &outs) |
Set all synthesis outputs as a conjunction. More... | |
bdd | spot::get_synthesis_outputs (const const_twa_graph_ptr &arena) |
Get all synthesis outputs as a conjunction. More... | |
void | spot::set_state_winner (twa_graph_ptr arena, unsigned state, bool winner) |
Set the winner of a state. More... | |
bool | spot::get_state_winner (const_twa_graph_ptr arena, unsigned state) |
Get the winner of a state. More... | |
const region_t & | spot::get_state_winners (const_twa_graph_ptr arena) |
Get the winner of all states. More... | |
void | spot::set_state_players (twa_graph_ptr arena, const region_t &owners) |
Set the owner for all the states. More... | |
void | spot::set_state_players (twa_graph_ptr arena, region_t &&owners) |
Set the owner for all the states. More... | |
const strategy_t & | spot::get_strategy (const_twa_graph_ptr arena) |
Get or set the strategy. More... | |
void | spot::set_strategy (twa_graph_ptr arena, const strategy_t &strat) |
Get or set the strategy. More... | |
void | spot::set_strategy (twa_graph_ptr arena, strategy_t &&strat) |
Get or set the strategy. More... | |
void | spot::set_state_winners (twa_graph_ptr arena, const region_t &winners) |
Set the winner for all the states. More... | |
void | spot::set_state_winners (twa_graph_ptr arena, region_t &&winners) |
Set the winner for all the states. More... | |
void spot::alternate_players | ( | spot::twa_graph_ptr & | arena, |
bool | first_player = false , |
||
bool | complete0 = true |
||
) |
#include <spot/twaalgos/game.hh>
Transform an automaton into a parity game by propagating players.
This propagate state players, assuming the initial state belong to first_player, and alternating players on each transitions. If an odd cycle is detected, a runtime_exception is raised.
If complete0 is set, ensure that states of player 0 are complete.
bool spot::get_state_player | ( | const_twa_graph_ptr | arena, |
unsigned | state | ||
) |
#include <spot/twaalgos/game.hh>
Get the owner of a state.
const region_t& spot::get_state_players | ( | const_twa_graph_ptr | arena | ) |
#include <spot/twaalgos/game.hh>
Get the owner of all states.
bool spot::get_state_winner | ( | const_twa_graph_ptr | arena, |
unsigned | state | ||
) |
#include <spot/twaalgos/game.hh>
Get the winner of a state.
const region_t& spot::get_state_winners | ( | const_twa_graph_ptr | arena | ) |
#include <spot/twaalgos/game.hh>
Get the winner of all states.
const strategy_t& spot::get_strategy | ( | const_twa_graph_ptr | arena | ) |
#include <spot/twaalgos/game.hh>
Get or set the strategy.
bdd spot::get_synthesis_outputs | ( | const const_twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Get all synthesis outputs as a conjunction.
twa_graph_ptr spot::highlight_strategy | ( | twa_graph_ptr & | arena, |
int | player0_color = 5 , |
||
int | player1_color = 4 |
||
) |
#include <spot/twaalgos/game.hh>
Highlight the edges of a strategy on an automaton.
Pass a negative color to not display the corresponding strategy.
void spot::pg_print | ( | std::ostream & | os, |
const const_twa_graph_ptr & | arena | ||
) |
#include <spot/twaalgos/game.hh>
Print a max odd parity game using PG-solver syntax.
void spot::set_state_player | ( | twa_graph_ptr | arena, |
unsigned | state, | ||
bool | owner | ||
) |
#include <spot/twaalgos/game.hh>
Set the owner of a state.
void spot::set_state_players | ( | twa_graph_ptr | arena, |
const region_t & | owners | ||
) |
#include <spot/twaalgos/game.hh>
Set the owner for all the states.
void spot::set_state_players | ( | twa_graph_ptr | arena, |
region_t && | owners | ||
) |
#include <spot/twaalgos/game.hh>
Set the owner for all the states.
void spot::set_state_winner | ( | twa_graph_ptr | arena, |
unsigned | state, | ||
bool | winner | ||
) |
#include <spot/twaalgos/game.hh>
Set the winner of a state.
void spot::set_state_winners | ( | twa_graph_ptr | arena, |
const region_t & | winners | ||
) |
#include <spot/twaalgos/game.hh>
Set the winner for all the states.
void spot::set_state_winners | ( | twa_graph_ptr | arena, |
region_t && | winners | ||
) |
#include <spot/twaalgos/game.hh>
Set the winner for all the states.
void spot::set_strategy | ( | twa_graph_ptr | arena, |
const strategy_t & | strat | ||
) |
#include <spot/twaalgos/game.hh>
Get or set the strategy.
void spot::set_strategy | ( | twa_graph_ptr | arena, |
strategy_t && | strat | ||
) |
#include <spot/twaalgos/game.hh>
Get or set the strategy.
void spot::set_synthesis_outputs | ( | const twa_graph_ptr & | arena, |
const bdd & | outs | ||
) |
#include <spot/twaalgos/game.hh>
Set all synthesis outputs as a conjunction.
bool spot::solve_game | ( | const twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Generic interface for game solving.
Dispatch to solve_safety_game() if the acceptance condition is t, or to solve_parity_game() if it is a parity acceptance. Note that parity acceptance include Büchi, co-Büchi, Rabin 1, and Streett 1.
Currently unable to solve game with other acceptance conditions that are not parity.
Return the winning player for the initial state, and sets the state-winner and strategy named properties.
bool spot::solve_parity_game | ( | const twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
solve a parity-game
The arena is a deterministic max odd parity automaton with a "state-player" property.
Player 1 tries to satisfy the acceptance condition, while player 0 tries to prevent that.
This computes the winning strategy and winning region using Zielonka's recursive algorithm. [52]
Also includes some inspiration from Oink. [51]
Returns the player winning in the initial state, and sets the state-winner and strategy named properties.
bool spot::solve_safety_game | ( | const twa_graph_ptr & | game | ) |
#include <spot/twaalgos/game.hh>
Solve a safety game.
The arena should be represented by an automaton with true acceptance.
Player 1 tries to satisfy the acceptance condition, while player 0 tries to prevent that. The only way for player 0 to win is to find a way to move the play toward a state without successor. If there no state without successors, then the game is necessarily winning for player 1.
Returns the player winning in the initial state, and sets the state-winner and strategy named properties.