Syft::DfaGameSynthesizer Class Reference

A synthesizer for a game whose arena is a symbolic-state DFA. More...

#include <DfaGameSynthesizer.h>

Inheritance diagram for Syft::DfaGameSynthesizer:

Collaboration diagram for Syft::DfaGameSynthesizer:

Public Member Functions
	DfaGameSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player)
	Construct a synthesizer for a given DFA game. More...
virtual SynthesisResult	run () const override=0
	Synthesis for the game. More...
std::unique_ptr< Transducer >	AbstractSingleStrategy (const SynthesisResult &result) const
	Abstract a winning strategy for the game. More...
Public Member Functions inherited from Syft::Synthesizer< SymbolicStateDfa >
	Synthesizer (SymbolicStateDfa spec)

Protected Member Functions
CUDD::BDD	preimage (const CUDD::BDD &winning_states) const
	Compute a set of winning moves. More...
CUDD::BDD	project_into_states (const CUDD::BDD &winning_moves) const
	Project a set of winning moves to a set of winning states. More...
bool	includes_initial_state (const CUDD::BDD &winning_states) const
	Check whether the initial state is a winning state. More...

Protected Attributes
std::shared_ptr< VarMgr >	var_mgr_
	Variable manager.
Player	starting_player_
	The player that moves first each turn.
Player	protagonist_player_
	The player for which we aim to find the winning strategy.
std::vector< int >	initial_vector_
	The initial state of the game arena.
std::vector< CUDD::BDD >	transition_vector_
	The transition function of the game arena.
std::unique_ptr< Quantification >	quantify_independent_variables_
	Quantification on the variables that the protagonist player does not depend on.
std::unique_ptr< Quantification >	quantify_non_state_variables_
	Quantification on non-state variables.
Protected Attributes inherited from Syft::Synthesizer< SymbolicStateDfa >
SymbolicStateDfa	spec_
	The game arena.

Detailed Description

A synthesizer for a game whose arena is a symbolic-state DFA.

Constructor & Destructor Documentation

DfaGameSynthesizer()

Syft::DfaGameSynthesizer::DfaGameSynthesizer	(	SymbolicStateDfa	spec,
		Player	starting_player,
		Player	protagonist_player
	)

Construct a synthesizer for a given DFA game.

The winning condition is unspecified and should be defined by the subclass.

Parameters

spec	A symbolic-state DFA representing the game's arena.
starting_player	The player that moves first each turn.
protagonist_player	The player for which we aim to find the winning strategy.

Member Function Documentation

AbstractSingleStrategy()

std::unique_ptr< Transducer > Syft::DfaGameSynthesizer::AbstractSingleStrategy

(

const SynthesisResult &

result

)

const

Abstract a winning strategy for the game.

Returns

A winning strategy represented as a transducer.

includes_initial_state()

bool Syft::DfaGameSynthesizer::includes_initial_state ( const CUDD::BDD &  winning_states ) const

protected

Check whether the initial state is a winning state.

Parameters

winning_states

A set of winning states.

Returns

True if the initial state is a winning state.

preimage()

CUDD::BDD Syft::DfaGameSynthesizer::preimage ( const CUDD::BDD &  winning_states ) const

protected

Compute a set of winning moves.

Basically first collect the transitions that move into a winning state, and then quantify all variables that the protagonist player doesn't depend on.

Parameters

winning_states

A set of winning states.

Returns

The preimage.

project_into_states()

CUDD::BDD Syft::DfaGameSynthesizer::project_into_states ( const CUDD::BDD &  winning_moves ) const

protected

Project a set of winning moves to a set of winning states.

Basically quantify all the non-state variables.

Parameters

winning_moves

A set of winning moves.

Returns

A set of winning states.

run()

virtual SynthesisResult Syft::DfaGameSynthesizer::run ( ) const

overridepure virtual

Synthesis for the game.

Returns

The synthesis result, consisting of realizability, the set of winning states and the set of winning moves.

Implements Syft::Synthesizer< SymbolicStateDfa >.

Implemented in Syft::ReachabilityMaxSet, Syft::Reachability, Syft::coBuchiReachability, and Syft::BuchiReachability.

---

The documentation for this class was generated from the following files:

• src/synthesis/header/game/DfaGameSynthesizer.h
• src/synthesis/source/game/DfaGameSynthesizer.cpp