Syft::GR1LTLfSynthesizer Class Reference

A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment GR(1) assumption. Additionally, one can also add safety conditions to both the environment and the agent, utilizing LTLf formulas. More...

#include <GR1LTLfSynthesizer.h>

Public Member Functions
	GR1LTLfSynthesizer (const std::shared_ptr< VarMgr > &var_mgr, const GR1 &gr1, const SymbolicStateDfa &env_safety, const SymbolicStateDfa &agn_reach, const SymbolicStateDfa &agn_safety, const std::string &slugs_dir, const std::string &benchmark_name)
	Construct a GR(1)LtlfSynthesizer. More...
SynthesisResult	run () const
	Solves the synthesis problem of LTLf with GR(1 environment assumption. More...

Detailed Description

A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment GR(1) assumption. Additionally, one can also add safety conditions to both the environment and the agent, utilizing LTLf formulas.

Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu: Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. IJCAI 2021: 1852-1858

Constructor & Destructor Documentation

GR1LTLfSynthesizer()

Syft::GR1LTLfSynthesizer::GR1LTLfSynthesizer	(	const std::shared_ptr< VarMgr > &	var_mgr,
		const GR1 &	gr1,
		const SymbolicStateDfa &	env_safety,
		const SymbolicStateDfa &	agn_reach,
		const SymbolicStateDfa &	agn_safety,
		const std::string &	slugs_dir,
		const std::string &	benchmark_name
	)

Construct a GR(1)LtlfSynthesizer.

Parameters

gr1	The GR(1) environment assumption.
env_safety	A symbolic-state DFA representing the LTLf formula indicating the environment safety condition
agn_reach	A symbolic-state DFA representing the LTLf formula indicating the system reachability condition
agn_safety	A symbolic-state DFA representing the LTLf formula indicating the system safety condition
slugs_dir	The root directory of SLUGS

Member Function Documentation

run()

SynthesisResult Syft::GR1LTLfSynthesizer::run

(

)

const

Solves the synthesis problem of LTLf with GR(1 environment assumption.

Returns

The synthesis result.

---

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

• src/synthesis/header/synthesizer/GR1LTLfSynthesizer.h
• src/synthesis/source/synthesizer/GR1LTLfSynthesizer.cpp