spot 2.12.2
|
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, bool solve_globally=false) |
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... | |
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 const_twa_graph_ptr &arena, unsigned state) |
Get the owner of a state. 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 const_twa_graph_ptr &arena, unsigned state) |
Get the winner of a state. More... | |
std::ostream & | spot::print_pg (std::ostream &os, const const_twa_graph_ptr &arena) |
Print a parity game using PG-solver syntax. More... | |
void | spot::pg_print (std::ostream &os, const const_twa_graph_ptr &arena) |
Print a parity game using PG-solver syntax. 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 region_t & | spot::get_state_players (const const_twa_graph_ptr &arena) |
Get the owner of all states. More... | |
const region_t & | spot::get_state_players (twa_graph_ptr &arena) |
Get the owner of all states. More... | |
const strategy_t & | spot::get_strategy (const 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... | |
const region_t & | spot::get_state_winners (const const_twa_graph_ptr &arena) |
Get the winner of all states. More... | |
const region_t & | spot::get_state_winners (twa_graph_ptr &arena) |
Get the winner of all 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 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 const_twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Get the owner of all states.
const region_t & spot::get_state_players | ( | twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Get the owner of all states.
bool spot::get_state_winner | ( | const 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 const_twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Get the winner of all states.
const region_t & spot::get_state_winners | ( | twa_graph_ptr & | arena | ) |
#include <spot/twaalgos/game.hh>
Get the winner of all states.
const strategy_t & spot::get_strategy | ( | const 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 parity game using PG-solver syntax.
The input automaton should have parity acceptance and should define state owner. Since the PG solver format want player 1 to solve a max odd condition, the acceptance condition will be adapted to max odd if necessary.
The output will list the initial state as first state (because that is the convention of our parser), and list only reachable states.
If states are named, the names will be output as well.
std::ostream & spot::print_pg | ( | std::ostream & | os, |
const const_twa_graph_ptr & | arena | ||
) |
#include <spot/twaalgos/game.hh>
Print a parity game using PG-solver syntax.
The input automaton should have parity acceptance and should define state owner. Since the PG solver format want player 1 to solve a max odd condition, the acceptance condition will be adapted to max odd if necessary.
The output will list the initial state as first state (because that is the convention of our parser), and list only reachable states.
If states are named, the names will be output as well.
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, |
bool | solve_globally = false |
||
) |
#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. [60]
By default only a 'local' strategy is computed: Only the part of the arena reachable from the init state is considered. If you want to compute a strategy for ALL states, set solve_globally to true
Also includes some inspiration from Oink. [59]
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.