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

◆ print_pg()

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.

◆ 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. [58]

Also includes some inspiration from Oink. [57]

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