A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA. More...

Inheritance diagram for Syft::coBuchiReachability:

Collaboration diagram for Syft::coBuchiReachability:

Public Member Functions
	coBuchiReachability (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &coBuchi, const CUDD::BDD &state_space)
	Construct a single-strategy-synthesizer for the given coBuchi-reachability game. More...

SynthesisResult	run () const final
	Solves the coBuchi-reachability game. More...

Public Member Functions inherited from Syft::DfaGameSynthesizer
	DfaGameSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player)
	Construct a synthesizer for a given DFA 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)

Additional Inherited Members
Protected Member Functions inherited from Syft::DfaGameSynthesizer
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 inherited from Syft::DfaGameSynthesizer
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 single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA.

Either coBuchi condition holds or reachability condition holds.

Constructor & Destructor Documentation

Syft::coBuchiReachability::coBuchiReachability	(	const SymbolicStateDfa &	spec,
		Player	starting_player,
		Player	protagonist_player,
		const CUDD::BDD &	goal_states,
		const CUDD::BDD &	coBuchi,
		const CUDD::BDD &	state_space
	)

Construct a single-strategy-synthesizer for the given coBuchi-reachability game.

Parameters

spec	A symbolic-state DFA representing the coBuchi-reachability game arena.
starting_player	The player that moves first each turn.
protagonist_player	The player for which we aim to find the winning strategy.
goal_states	The reachability condition.
coBuchi	The coBuchi condition represented as a Boolean formula \beta over input variables, denoting the coBuchi condition FG\beta.
state_space	The state space.

SynthesisResult Syft::coBuchiReachability::run ( ) const

finalvirtual

Solves the coBuchi-reachability game.

Returns: The result consists of realizability a set of agent winning states a transducer representing a winning strategy or nullptr if the game is unrealizable.

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