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

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() [1/2]

const region_t& spot::get_state_players

(

const const_twa_graph_ptr &

arena

)

#include <spot/twaalgos/game.hh>

Get the owner of all states.

get_state_players() [2/2]

const region_t& spot::get_state_players

(

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