spot  2.10.6
Functions
Functions related to game solving

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...
 

Detailed Description

Function Documentation

◆ alternate_players()

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.

◆ get_state_player()

bool spot::get_state_player ( const_twa_graph_ptr  arena,
unsigned  state 
)

#include <spot/twaalgos/game.hh>

Get the owner of a state.

◆ get_state_players()

const region_t& spot::get_state_players ( const_twa_graph_ptr  arena)

#include <spot/twaalgos/game.hh>

Get the owner of all states.

◆ get_state_winner()

bool spot::get_state_winner ( const_twa_graph_ptr  arena,
unsigned  state 
)

#include <spot/twaalgos/game.hh>

Get the winner of a state.

◆ get_state_winners()

const region_t& spot::get_state_winners ( const_twa_graph_ptr  arena)

#include <spot/twaalgos/game.hh>

Get the winner of all states.

◆ get_strategy()

const strategy_t& spot::get_strategy ( const_twa_graph_ptr  arena)

#include <spot/twaalgos/game.hh>

Get or set the strategy.

◆ get_synthesis_outputs()

bdd spot::get_synthesis_outputs ( const const_twa_graph_ptr &  arena)

#include <spot/twaalgos/game.hh>

Get all synthesis outputs as a conjunction.

◆ highlight_strategy()

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.

◆ pg_print()

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.

◆ set_state_player()

void spot::set_state_player ( twa_graph_ptr  arena,
unsigned  state,
bool  owner 
)

#include <spot/twaalgos/game.hh>

Set the owner of a state.

◆ set_state_players() [1/2]

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.

◆ set_state_players() [2/2]

void spot::set_state_players ( twa_graph_ptr  arena,
region_t &&  owners 
)

#include <spot/twaalgos/game.hh>

Set the owner for all the states.

◆ set_state_winner()

void spot::set_state_winner ( twa_graph_ptr  arena,
unsigned  state,
bool  winner 
)

#include <spot/twaalgos/game.hh>

Set the winner of a state.

◆ set_state_winners() [1/2]

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.

◆ set_state_winners() [2/2]

void spot::set_state_winners ( twa_graph_ptr  arena,
region_t &&  winners 
)

#include <spot/twaalgos/game.hh>

Set the winner for all the states.

◆ set_strategy() [1/2]

void spot::set_strategy ( twa_graph_ptr  arena,
const strategy_t &  strat 
)

#include <spot/twaalgos/game.hh>

Get or set the strategy.

◆ set_strategy() [2/2]

void spot::set_strategy ( twa_graph_ptr  arena,
strategy_t &&  strat 
)

#include <spot/twaalgos/game.hh>

Get or set the strategy.

◆ set_synthesis_outputs()

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.

◆ solve_game()

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.

◆ solve_parity_game()

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. [54]

Also includes some inspiration from Oink. [53]

Returns the player winning in the initial state, and sets the state-winner and strategy named properties.

◆ solve_safety_game()

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.


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.1