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

Public Member Functions
	coGR1Reachability (const std::shared_ptr< VarMgr > &var_mgr, const GR1 &gr1, const SymbolicStateDfa &arena, const CUDD::BDD &state_space, const CUDD::BDD &initial_condition, const std::string &slugs_dir, const std::string &benchmark_name)
	Construct a single-strategy-synthesizer for the given Buchi-reachability game. More...

const std::string	exec_slugs (const std::string &slugs, const std::string &slugs_input_file, const std::string &slugs_res_file, const std::string &slugs_strategy_file) const

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

	coGR1Reachability (SymbolicStateDfa dfa, Player player, Player player1, CUDD::BDD bdd, CUDD::BDD bdd1, CUDD::BDD bdd2)

Detailed Description

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

Either Buchi condition holds or reachability condition holds.

Constructor & Destructor Documentation

Syft::coGR1Reachability::coGR1Reachability	(	const std::shared_ptr< VarMgr > &	var_mgr,
		const GR1 &	gr1,
		const SymbolicStateDfa &	arena,
		const CUDD::BDD &	state_space,
		const CUDD::BDD &	initial_condition,
		const std::string &	slugs_dir,
		const std::string &	benchmark_name
	)

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

Parameters

spec	A symbolic-state DFA representing the Buchi-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.
Buchi	The Buchi condition represented as a Boolean formula \beta over input variables, denoting the Buchi condition FG\beta.
state_space	The state space.

SynthesisResult Syft::coGR1Reachability::run ( ) const

Solves the Buchi-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: