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.
bool	spot::solve_parity_game (const twa_graph_ptr &arena, bool solve_globally=false)
	solve a parity-game
bool	spot::solve_safety_game (const twa_graph_ptr &game)
	Solve a safety game.
bool	spot::solve_game (const twa_graph_ptr &arena)
	Generic interface for game solving.
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.
void	spot::set_state_player (twa_graph_ptr &arena, unsigned state, bool owner)
	Set the owner of a state.
bool	spot::get_state_player (const const_twa_graph_ptr &arena, unsigned state)
	Get the owner of a state.
void	spot::set_synthesis_outputs (const twa_graph_ptr &arena, const bdd &outs)
	Set all synthesis outputs as a conjunction.
bdd	spot::get_synthesis_outputs (const const_twa_graph_ptr &arena)
	Get all synthesis outputs as a conjunction.
void	spot::set_state_winner (twa_graph_ptr &arena, unsigned state, bool winner)
	Set the winner of a state.
bool	spot::get_state_winner (const const_twa_graph_ptr &arena, unsigned state)
	Get the winner of a state.
std::ostream &	spot::print_pg (std::ostream &os, const const_twa_graph_ptr &arena)
	Print a parity game using PG-solver syntax.
void	spot::pg_print (std::ostream &os, const const_twa_graph_ptr &arena)
	Print a parity game using PG-solver syntax.
void	spot::set_state_players (twa_graph_ptr &arena, const region_t &owners)
	Set the owner for all the states.
void	spot::set_state_players (twa_graph_ptr &arena, region_t &&owners)
	Set the owner for all the states.
const region_t &	spot::get_state_players (const const_twa_graph_ptr &arena)
	Get the owner of all states.
const region_t &	spot::get_state_players (twa_graph_ptr &arena)
	Get the owner of all states.
const strategy_t &	spot::get_strategy (const const_twa_graph_ptr &arena)
	Get or set the strategy.
void	spot::set_strategy (twa_graph_ptr &arena, const strategy_t &strat)
	Get or set the strategy.
void	spot::set_strategy (twa_graph_ptr &arena, strategy_t &&strat)
	Get or set the strategy.
void	spot::set_state_winners (twa_graph_ptr &arena, const region_t &winners)
	Set the winner for all the states.
void	spot::set_state_winners (twa_graph_ptr &arena, region_t &&winners)
	Set the winner for all the states.
const region_t &	spot::get_state_winners (const const_twa_graph_ptr &arena)
	Get the winner of all states.
const region_t &	spot::get_state_winners (twa_graph_ptr &arena)
	Get the winner of all states.

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 const_twa_graph_ptr &	arena,
		unsigned	state )

#include <spot/twaalgos/game.hh>

Get the owner of a state.

References get_state_player().

Referenced by get_state_player().

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.

References get_state_players().

Referenced by get_state_players(), and get_state_players().

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.

References get_state_players().

get_state_winner()

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

#include <spot/twaalgos/game.hh>

Get the winner of a state.

References get_state_winner().

Referenced by get_state_winner().

get_state_winners() [1/2]

const region_t & spot::get_state_winners

(

const const_twa_graph_ptr &

arena

)

#include <spot/twaalgos/game.hh>

Get the winner of all states.

References get_state_winners().

Referenced by get_state_winners().

get_state_winners() [2/2]

const region_t & spot::get_state_winners

(

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.

References get_strategy().

Referenced by get_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.

References get_synthesis_outputs().

Referenced by get_synthesis_outputs().

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.

References highlight_strategy().

Referenced by highlight_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.

References pg_print().

Referenced by pg_print().

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.

References set_state_player().

Referenced by set_state_player().

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.

References set_state_players().

Referenced by set_state_players(), and set_state_players().

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.

References set_state_players().

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.

References set_state_winner().

Referenced by set_state_winner().

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.

References set_state_winners().

Referenced by set_state_winners(), and set_state_winners().

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.

References set_state_winners().

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.

References set_strategy().

Referenced by set_strategy(), and set_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.

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

References set_synthesis_outputs().

Referenced by set_synthesis_outputs().

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,
		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. [zielonka.98.tcs]

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. [vandijk.18.tacas]

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.