Functions related to game solving

Classes
class	spot::backprop_graph
	Graph used for backward propagation of winning conditions in parity games. More...

Typedefs
typedef std::vector< bool >	spot::region_t
	Winning region: false = player 0 (env), true = player 1.
typedef std::vector< unsigned >	spot::strategy_t
	Strategy: maps each state index to the chosen global edge number.

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

Typedef Documentation

region_t

typedef std::vector<bool> spot::region_t

#include <spot/twaalgos/game.hh>

Winning region: false = player 0 (env), true = player 1.

strategy_t

typedef std::vector<unsigned> spot::strategy_t

#include <spot/twaalgos/game.hh>

Strategy: maps each state index to the chosen global edge number.

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 propagates state players, assuming the initial state belongs to first_player, and alternating players on each transition. 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.

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

#include <spot/twaalgos/game.hh>

Get the winner of a state.

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.

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.

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 a 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 must have a transition-based parity acceptance and a "state-player" property. The solver accepts all four parity variants (max/min, odd/even) and normalizes them internally. Choices are made by the owner of each state; determinism of transition labels is not required by the solver, but callers such as synthesis may require mutually exclusive labels. States without successors are not supported by parity games and should be removed or completed by the caller.

Player 1 tries to satisfy the acceptance condition, while player 0 tries to prevent that.

This computes a winning region (stored in the "state-winner" property) and a positional winning strategy (stored in the "strategy" property). The strategy is meaningful only for states whose owner is the winner; its entry is a global edge number leading to a state with the same winner. Other entries are unspecified and currently represented by 0; zero can nevertheless be a valid global edge number, so callers must check the owner and winner before using an entry.

By default only a 'local' strategy is computed: only the part of the arena reachable from the initial state is considered. Unreachable states consequently have no solved winner or strategy guarantee. If you want winners and strategies for all states, set solve_globally to true. In either mode, solving is done from scratch, and named properties from an earlier solve are replaced.

The implementation currently uses Zielonka's recursive algorithm, with optimizations inspired by Oink. These implementation details are not part of the strategy-selection contract. [zielonka.98.tcs] [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 successors. If there is 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.