diff --git a/BuchiReachability_8hpp_source.html b/BuchiReachability_8hpp_source.html new file mode 100644 index 0000000..c3862b8 --- /dev/null +++ b/BuchiReachability_8hpp_source.html @@ -0,0 +1,133 @@ + + +
+ + + + +
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
▼NSyft | |
CTLSFArgs | |
CPrinter | |
CBaseRunner | |
CFairnessRunner | |
CGR1Runner | |
CMaxSetRunner | |
CStabilityRunner | |
CSynthesisRunner | |
CParser | A parser for reading LTLf synthesis benchmarks in TLSF format |
CExplicitStateDfa | A DFA with explicit states and symbolic transitions |
CExplicitStateDfaAdd | A DFA with explicit states and symbolic transitions represented in ADDs |
CSymbolicStateDfa | A DFA with symbolic states and transitions |
CBuchiReachability | A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA |
CcoBuchiReachability | A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA |
CcoGR1Reachability | A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA |
CDfaGameSynthesizer | A synthesizer for a game whose arena is a symbolic-state DFA |
CInputOutputPartition | A partition of variables into input and output variables |
CQuantification | Abstract class representing a quantification operation on BDDs |
CNoQuantification | Performs no quantification |
CForall | Performs universal quantification |
CExists | Performs existential quantification |
CForallExists | Performs both universal and existential quantification |
CExistsForall | Performs both universal and existential quantification |
CReachability | A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA |
CReachabilityMaxSet | A maxset-strategy-synthesizer for a reachability game given as a symbolic-state DFA |
CTransducer | A symbolic tranducer representing a winning strategy for a game |
CGR1 | |
CSmtOneStepRealizabilityVisitor | |
CSmtOneStepUnrealizabilityVisitor | |
CStopwatch | Stopwatch for timing executions |
CFairnessLtlfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables |
CGR1LTLfSynthesizer | 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 |
CLTLfMaxSetSynthesizer | A maxset-synthesizer for a reachability game given as a symbolic-state DFA |
CLTLfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA |
CStabilityLtlfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables |
CSynthesisResult | |
CMaxSetSynthesisResult | |
COneStepSynthesisResult | |
CSynthesizer | Abstract class for synthesizers |
CVarMgr | A dictionary that maps variable names to indices and vice versa |
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::BaseRunner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Protected Member Functions | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
+Protected Attributes | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::BuchiReachability, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA. + More...
+ +#include <BuchiReachability.hpp>
+Public Member Functions | |
BuchiReachability (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &Buchi, const CUDD::BDD &state_space) | |
Construct a single-strategy-synthesizer for the given Buchi-reachability game. More... | |
SynthesisResult | run () const final |
Solves the Buchi-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. | |
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.
+Either Buchi condition holds or reachability condition holds.
+Syft::BuchiReachability::BuchiReachability | +( | +const SymbolicStateDfa & | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | const CUDD::BDD & | +goal_states, | +
+ | + | const CUDD::BDD & | +Buchi, | +
+ | + | const CUDD::BDD & | +state_space | +
+ | ) | ++ |
Construct a single-strategy-synthesizer for the given Buchi-reachability game.
+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. |
+
|
+ +finalvirtual | +
Solves the Buchi-reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::DfaGameSynthesizer, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A synthesizer for a game whose arena is a symbolic-state DFA. + More...
+ +#include <DfaGameSynthesizer.h>
+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. | |
A synthesizer for a game whose arena is a symbolic-state DFA.
+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.
+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. |
std::unique_ptr< Transducer > Syft::DfaGameSynthesizer::AbstractSingleStrategy | +( | +const SynthesisResult & | +result | ) | +const | +
Abstract a winning strategy for the game.
+
+
|
+ +protected | +
Check whether the initial state is a winning state.
+winning_states | A set of winning states. |
+
|
+ +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.
winning_states | A set of winning states. |
+
|
+ +protected | +
Project a set of winning moves to a set of winning states.
+Basically quantify all the non-state variables.
winning_moves | A set of winning moves. |
+
|
+ +overridepure virtual | +
Synthesis for the game.
+Implements Syft::Synthesizer< SymbolicStateDfa >.
+ +Implemented in Syft::ReachabilityMaxSet, Syft::Reachability, Syft::coBuchiReachability, and Syft::BuchiReachability.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Exists, including all inherited members.
+apply(const CUDD::BDD &bdd) const override (defined in Syft::Exists) | Syft::Exists | virtual |
Exists(CUDD::BDD existential_variables) (defined in Syft::Exists) | Syft::Exists | |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Performs existential quantification. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+ | Exists (CUDD::BDD existential_variables) |
+CUDD::BDD | apply (const CUDD::BDD &bdd) const override |
Performs existential quantification.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ExistsForall, including all inherited members.
+apply(const CUDD::BDD &bdd) const override (defined in Syft::ExistsForall) | Syft::ExistsForall | virtual |
ExistsForall(CUDD::BDD existential_variables, CUDD::BDD universal_variables) (defined in Syft::ExistsForall) | Syft::ExistsForall | |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Performs both universal and existential quantification. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+ | ExistsForall (CUDD::BDD existential_variables, CUDD::BDD universal_variables) |
+CUDD::BDD | apply (const CUDD::BDD &bdd) const override |
Performs both universal and existential quantification.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ExplicitStateDfa, including all inherited members.
+dfa_complement(ExplicitStateDfa &d) | Syft::ExplicitStateDfa | static |
dfa_minimize(const ExplicitStateDfa &d) | Syft::ExplicitStateDfa | static |
dfa_of_formula(const whitemech::lydia::LTLfFormula &formula) | Syft::ExplicitStateDfa | static |
dfa_print() | Syft::ExplicitStateDfa | |
dfa_product_and(const std::vector< ExplicitStateDfa > &dfa_vector) | Syft::ExplicitStateDfa | static |
dfa_product_or(const std::vector< ExplicitStateDfa > &dfa_vector) | Syft::ExplicitStateDfa | static |
ExplicitStateDfa(DFA *dfa, int nb_variables) | Syft::ExplicitStateDfa | inline |
ExplicitStateDfa(DFA *dfa, const std::vector< std::string > &names) | Syft::ExplicitStateDfa | inline |
ExplicitStateDfa(const ExplicitStateDfa &other) | Syft::ExplicitStateDfa | inline |
get_nb_variables() | Syft::ExplicitStateDfa | inline |
operator=(ExplicitStateDfa other) | Syft::ExplicitStateDfa | inline |
restrict_dfa_with_states(ExplicitStateDfa &d, std::vector< size_t > states) | Syft::ExplicitStateDfa | static |
restrict_dfa_with_transitions(ExplicitStateDfa &d, std::unordered_map< size_t, CUDD::BDD > transitions, std::shared_ptr< VarMgr > var_mgr) | Syft::ExplicitStateDfa | static |
~ExplicitStateDfa() (defined in Syft::ExplicitStateDfa) | Syft::ExplicitStateDfa | inline |
+ LydiaSyft
+
+ |
+
A DFA with explicit states and symbolic transitions. + More...
+ +#include <ExplicitStateDfa.h>
+Public Member Functions | |
ExplicitStateDfa (DFA *dfa, int nb_variables) | |
Create an explicit-state DFA from an Lydia DFA structure and the number of variables. More... | |
ExplicitStateDfa (DFA *dfa, const std::vector< std::string > &names) | |
Create an explicit-state DFA from an Lydia DFA structure and the names of variables. More... | |
+ | ExplicitStateDfa (const ExplicitStateDfa &other) |
Create an explicit-state DFA from an existing one. | |
+ExplicitStateDfa & | operator= (ExplicitStateDfa other) |
Create an explicit-state DFA from an existing one using the opeartor =. | |
+int | get_nb_variables () |
Get the number of variables. | |
+void | dfa_print () |
Print the explicit-state DFA. | |
+Static Public Member Functions | |
static ExplicitStateDfa | dfa_of_formula (const whitemech::lydia::LTLfFormula &formula) |
Construct an explicit-state DFA from a given formula using Lydia. More... | |
static ExplicitStateDfa | dfa_product_and (const std::vector< ExplicitStateDfa > &dfa_vector) |
Take the product AND of a sequence of explicit-state DFAs. More... | |
static ExplicitStateDfa | dfa_product_or (const std::vector< ExplicitStateDfa > &dfa_vector) |
Take the product OR of a sequence of explicit-state DFAs. More... | |
static ExplicitStateDfa | dfa_minimize (const ExplicitStateDfa &d) |
Minimize a given explicit-state DFA. More... | |
static ExplicitStateDfa | restrict_dfa_with_states (ExplicitStateDfa &d, std::vector< size_t > states) |
Restrict an explicit-state DFA with a given set of states. More... | |
static ExplicitStateDfa | restrict_dfa_with_transitions (ExplicitStateDfa &d, std::unordered_map< size_t, CUDD::BDD > transitions, std::shared_ptr< VarMgr > var_mgr) |
Restrict a DFA with a given set of transitions. More... | |
static ExplicitStateDfa | dfa_complement (ExplicitStateDfa &d) |
Complement a DFA. More... | |
A DFA with explicit states and symbolic transitions.
+The LTLf-to-DFA consstruction utilizes Lydia. Giuseppe De Giacomo, Marco Favorito: Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata. ICAPS 2021: 122-130
+
+
|
+ +inline | +
Create an explicit-state DFA from an Lydia DFA structure and the number of variables.
+dfa | A Lydia DFA structure. |
nb_variables | The number of variables in the Lydia DFA. |
+
|
+ +inline | +
Create an explicit-state DFA from an Lydia DFA structure and the names of variables.
+dfa | A Lydia DFA structure. |
names | The names of the variables in the Lydia DFA. |
+
|
+ +static | +
Complement a DFA.
+Basically exchange the accepting states and the non-accepting states.
+d | The DFA to be complemented. |
+
|
+ +static | +
Minimize a given explicit-state DFA.
+d | The DFA to be minimized. |
+
|
+ +static | +
Construct an explicit-state DFA from a given formula using Lydia.
+formula | An LTLf formula. |
+
|
+ +static | +
Take the product AND of a sequence of explicit-state DFAs.
+dfa_vector | The DFAs to be processed. |
+
|
+ +static | +
Take the product OR of a sequence of explicit-state DFAs.
+dfa_vector | The DFAs to be processed. |
+
|
+ +static | +
Restrict an explicit-state DFA with a given set of states.
+Basically restrict a DFA to a set of states from the DFA, and return a minimized one.
+d | The DFA to be restricted. |
states | The set of states to be kept. |
+
|
+ +static | +
Restrict a DFA with a given set of transitions.
+Basically restrict a DFA to a set of transitions, and return a minimized one.
+d | The DFA to be restricted. |
transitions | The set of transitions to be kept. |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ExplicitStateDfaAdd, including all inherited members.
+dump_dot(const std::string &filename) const | Syft::ExplicitStateDfaAdd | |
final_states() const | Syft::ExplicitStateDfaAdd | |
from_dfa_mona(std::shared_ptr< VarMgr > var_mgr, const ExplicitStateDfa &explicit_dfa) | Syft::ExplicitStateDfaAdd | static |
initial_state() const | Syft::ExplicitStateDfaAdd | |
state_count() const | Syft::ExplicitStateDfaAdd | |
transition_function() const | Syft::ExplicitStateDfaAdd | |
var_mgr() const | Syft::ExplicitStateDfaAdd |
+ LydiaSyft
+
+ |
+
A DFA with explicit states and symbolic transitions represented in ADDs. + More...
+ +#include <ExplicitStateDfaAdd.h>
+Public Member Functions | |
+std::shared_ptr< VarMgr > | var_mgr () const |
Returns the variable manager. | |
+std::size_t | initial_state () const |
Returns the initial state of the DFA. | |
+std::size_t | state_count () const |
Returns the number of states in the DFA. | |
+std::vector< std::size_t > | final_states () const |
Returns the list of indices of final states of the DFA. | |
std::vector< CUDD::ADD > | transition_function () const |
Returns the transition function of the DFA as a vector of ADDs. More... | |
void | dump_dot (const std::string &filename) const |
Saves the transition function of the DFA in a .dot file. More... | |
+Static Public Member Functions | |
static ExplicitStateDfaAdd | from_dfa_mona (std::shared_ptr< VarMgr > var_mgr, const ExplicitStateDfa &explicit_dfa) |
Constructs an explicit-state DFA in ADD representation from an explicit-state DFA. More... | |
A DFA with explicit states and symbolic transitions represented in ADDs.
+void Syft::ExplicitStateDfaAdd::dump_dot | +( | +const std::string & | +filename | ) | +const | +
Saves the transition function of the DFA in a .dot file.
+filename | The name of the file to save the transition function to. |
+
|
+ +static | +
Constructs an explicit-state DFA in ADD representation from an explicit-state DFA.
+var_mgr | The variable manager for managing transition variables. |
explicit_dfa | An explicit-state DFA. |
std::vector< CUDD::ADD > Syft::ExplicitStateDfaAdd::transition_function | +( | +) | +const | +
Returns the transition function of the DFA as a vector of ADDs.
+The ADD in index i represents the transition function for state i.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ExplicitStateDfaMona, including all inherited members.
+dfa_complement(ExplicitStateDfaMona &d) | Syft::ExplicitStateDfaMona | static |
dfa_minimize(const ExplicitStateDfaMona &d) | Syft::ExplicitStateDfaMona | static |
dfa_of_formula(const whitemech::lydia::LTLfFormula &formula) | Syft::ExplicitStateDfaMona | static |
dfa_of_formula(const std::string &formula) | Syft::ExplicitStateDfaMona | static |
dfa_print() | Syft::ExplicitStateDfaMona | |
dfa_product_and(const std::vector< ExplicitStateDfaMona > &dfa_vector) | Syft::ExplicitStateDfaMona | static |
dfa_product_or(const std::vector< ExplicitStateDfaMona > &dfa_vector) | Syft::ExplicitStateDfaMona | static |
ExplicitStateDfaMona(DFA *dfa, int nb_variables) (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
ExplicitStateDfaMona(DFA *dfa, const std::vector< std::string > &names) (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
ExplicitStateDfaMona(const ExplicitStateDfaMona &other) (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
get_nb_variables() (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
operator=(ExplicitStateDfaMona other) (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
prune_dfa_with_states(ExplicitStateDfaMona &d, std::vector< size_t > states) | Syft::ExplicitStateDfaMona | static |
prune_dfa_with_transitions(ExplicitStateDfaMona &d, std::unordered_map< size_t, CUDD::BDD > transitions, std::shared_ptr< VarMgr > var_mgr) | Syft::ExplicitStateDfaMona | static |
~ExplicitStateDfaMona() (defined in Syft::ExplicitStateDfaMona) | Syft::ExplicitStateDfaMona | inline |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | ExplicitStateDfaMona (DFA *dfa, int nb_variables) |
+ | ExplicitStateDfaMona (DFA *dfa, const std::vector< std::string > &names) |
+ | ExplicitStateDfaMona (const ExplicitStateDfaMona &other) |
+ExplicitStateDfaMona & | operator= (ExplicitStateDfaMona other) |
+int | get_nb_variables () |
+void | dfa_print () |
Print the DFA. | |
+Static Public Member Functions | |
static ExplicitStateDfaMona | dfa_of_formula (const whitemech::lydia::LTLfFormula &formula) |
Construct DFA from a given formula. More... | |
static ExplicitStateDfaMona | dfa_product_and (const std::vector< ExplicitStateDfaMona > &dfa_vector) |
Take the product AND of a vector of DFAs. More... | |
static ExplicitStateDfaMona | dfa_product_or (const std::vector< ExplicitStateDfaMona > &dfa_vector) |
Take the product AND of a vector of DFAs. More... | |
static ExplicitStateDfaMona | dfa_minimize (const ExplicitStateDfaMona &d) |
Minimize a given DFA. More... | |
static ExplicitStateDfaMona | dfa_of_formula (const std::string &formula) |
Construct DFA from a given formula. More... | |
static ExplicitStateDfaMona | prune_dfa_with_states (ExplicitStateDfaMona &d, std::vector< size_t > states) |
Prune a DFA with given set of states. More... | |
static ExplicitStateDfaMona | prune_dfa_with_transitions (ExplicitStateDfaMona &d, std::unordered_map< size_t, CUDD::BDD > transitions, std::shared_ptr< VarMgr > var_mgr) |
Prune a DFA with given transitions. More... | |
static ExplicitStateDfaMona | dfa_complement (ExplicitStateDfaMona &d) |
Complement a DFA. More... | |
+
|
+ +static | +
Complement a DFA.
+Basically exchange the accepting states and the non-accepting states.
+d | The DFA to be complemented. |
+
|
+ +static | +
Minimize a given DFA.
+d | The DFA to be minimized. |
+
|
+ +static | +
Construct DFA from a given formula.
+formula | An LTLf formula. |
+
|
+ +static | +
Construct DFA from a given formula.
+formula | An LTLf formula. |
+
|
+ +static | +
Take the product AND of a vector of DFAs.
+dfa_vector | The DFAs to be processed. |
+
|
+ +static | +
Take the product AND of a vector of DFAs.
+dfa_vector | The DFAs to be processed. |
+
|
+ +static | +
Prune a DFA with given set of states.
+Basically remove a set of states from the DFA, and return a minimized one.
+d | The DFA to be pruned. |
states | The set of states to be removed. |
+
|
+ +static | +
Prune a DFA with given transitions.
+Basically remove a set of transitions from the DFA, and return a minimized one.
+d | The DFA to be pruned. |
transitions | The set of transitions to be removed. |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::FairReachabilitySynthesizer, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables. + More...
+ +#include <FairReachabilitySynthesizer.h>
+Public Member Functions | |
FairReachabilitySynthesizer (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space, const std::string &assumption_filename) | |
Construct a single-strategy-synthesizer for the given coBuchi-reachability game. More... | |
virtual 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) |
+Protected Member Functions | |
+CUDD::BDD | load_CNF (const std::string &filename) const |
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... | |
+Additional Inherited Members | |
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_ |
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables.
+Syft::FairReachabilitySynthesizer::FairReachabilitySynthesizer | +( | +const SymbolicStateDfa & | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | const CUDD::BDD & | +goal_states, | +
+ | + | const CUDD::BDD & | +state_space, | +
+ | + | const std::string & | +assumption_filename | +
+ | ) | ++ |
Construct a single-strategy-synthesizer for the given coBuchi-reachability game.
+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 set of states that the agent must reach to win. |
state_space | The state space. |
assumption_filename | The file that specifies a Boolean formula \alpha over input variables, denoting the simple Fairness assumption GF\alpha. |
+
|
+ +finalvirtual | +
Solves the coBuchi-reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::FairnessLtlfSynthesizer, including all inherited members.
+FairnessLtlfSynthesizer(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space, const std::string &assumption_filename) | Syft::FairnessLtlfSynthesizer | |
load_CNF(const std::string &filename) const (defined in Syft::FairnessLtlfSynthesizer) | Syft::FairnessLtlfSynthesizer | protected |
run() const | Syft::FairnessLtlfSynthesizer |
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables. + More...
+ +#include <FairnessLtlfSynthesizer.h>
+Public Member Functions | |
FairnessLtlfSynthesizer (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space, const std::string &assumption_filename) | |
Construct a FairnessLtlfSynthesizer. More... | |
SynthesisResult | run () const |
Solves the synthesis problem of LTLf with simple Fairness environment assumption. More... | |
+Protected Member Functions | |
+CUDD::BDD | load_CNF (const std::string &filename) const |
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables.
+Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi: LTLÆ’ Synthesis with Fairness and Stability Assumptions. AAAI 2020: 3088-3095 +
Syft::FairnessLtlfSynthesizer::FairnessLtlfSynthesizer | +( | +const SymbolicStateDfa & | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | const CUDD::BDD & | +goal_states, | +
+ | + | const CUDD::BDD & | +state_space, | +
+ | + | const std::string & | +assumption_filename | +
+ | ) | ++ |
Construct a FairnessLtlfSynthesizer.
+spec | A symbolic-state DFA representing the LTLf formula. |
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 set of states that the agent must reach to win. |
state_space | The state space. |
assumption_filename | The file that specifies a Boolean formula \alpha over input variables, denoting the simple Fairness assumption GF\alpha. |
SynthesisResult Syft::FairnessLtlfSynthesizer::run | +( | +) | +const | +
Solves the synthesis problem of LTLf with simple Fairness environment assumption.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::FairnessRunner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
FairnessRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &assumption_filename, bool print_strategy, bool print_times) (defined in Syft::FairnessRunner) | Syft::FairnessRunner | inline |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
run() const (defined in Syft::FairnessRunner) | Syft::FairnessRunner | |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | FairnessRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &assumption_filename, bool print_strategy, bool print_times) |
+void | run () const |
Public Member Functions inherited from Syft::BaseRunner | |
+ | BaseRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+Additional Inherited Members | |
Protected Member Functions inherited from Syft::BaseRunner | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
Protected Attributes inherited from Syft::BaseRunner | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Forall, including all inherited members.
+apply(const CUDD::BDD &bdd) const override (defined in Syft::Forall) | Syft::Forall | virtual |
Forall(CUDD::BDD universal_variables) (defined in Syft::Forall) | Syft::Forall | |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Performs universal quantification. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+ | Forall (CUDD::BDD universal_variables) |
+CUDD::BDD | apply (const CUDD::BDD &bdd) const override |
Performs universal quantification.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ForallExists, including all inherited members.
+apply(const CUDD::BDD &bdd) const override (defined in Syft::ForallExists) | Syft::ForallExists | virtual |
ForallExists(CUDD::BDD universal_variables, CUDD::BDD existential_variables) (defined in Syft::ForallExists) | Syft::ForallExists | |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Performs both universal and existential quantification. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+ | ForallExists (CUDD::BDD universal_variables, CUDD::BDD existential_variables) |
+CUDD::BDD | apply (const CUDD::BDD &bdd) const override |
Performs both universal and existential quantification.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::GR1LTLfSynthesizer, including all inherited members.
+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) | Syft::GR1LTLfSynthesizer | |
run() const | Syft::GR1LTLfSynthesizer |
+ LydiaSyft
+
+ |
+
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... | |
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
+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.
+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 |
SynthesisResult Syft::GR1LTLfSynthesizer::run | +( | +) | +const | +
Solves the synthesis problem of LTLf with GR(1 environment assumption.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::GR1ReachabilitySynthesizer, including all inherited members.
+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 (defined in Syft::GR1ReachabilitySynthesizer) | Syft::GR1ReachabilitySynthesizer | |
GR1ReachabilitySynthesizer(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) | Syft::GR1ReachabilitySynthesizer | |
run() const | Syft::GR1ReachabilitySynthesizer |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
GR1ReachabilitySynthesizer (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 synthesizer for the given LTLf/GR(1) 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 LTLf/GR(1) game. More... | |
Syft::GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer | +( | +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 synthesizer for the given LTLf/GR(1) game.
+gr1 | A GR(1) formula stating the winning condition. |
env_safety | A symbolic-state DFA representing the environment safety game arena |
agn_reach | A symbolic-state DFA representing the system reachability game arena |
agn_safety | A symbolic-state DFA representing the system safety game arena |
slugs_dir | The root directory of the SLUGS project |
SynthesisResult Syft::GR1ReachabilitySynthesizer::run | +( | +) | +const | +
Solves the LTLf/GR(1) game.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::GR1Runner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
GR1Runner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &path_to_slugs, const std::string &gr1_file, const std::optional< std::string > &env_safety_file, const std::optional< std::string > &agent_safety_file, bool print_strategy, bool print_times) (defined in Syft::GR1Runner) | Syft::GR1Runner | inline |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
run() const (defined in Syft::GR1Runner) | Syft::GR1Runner | |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | GR1Runner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &path_to_slugs, const std::string &gr1_file, const std::optional< std::string > &env_safety_file, const std::optional< std::string > &agent_safety_file, bool print_strategy, bool print_times) |
+void | run () const |
Public Member Functions inherited from Syft::BaseRunner | |
+ | BaseRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+Additional Inherited Members | |
Protected Member Functions inherited from Syft::BaseRunner | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
Protected Attributes inherited from Syft::BaseRunner | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::InputOutputPartition, including all inherited members.
+construct_from_input(const std::vector< std::string > inputs_substr, std::vector< std::string > outputs_substr) | Syft::InputOutputPartition | static |
input_variables (defined in Syft::InputOutputPartition) | Syft::InputOutputPartition | |
InputOutputPartition() | Syft::InputOutputPartition | |
is_input(const std::string &var_name) | Syft::InputOutputPartition | |
is_output(const std::string &var_name) | Syft::InputOutputPartition | |
output_variables (defined in Syft::InputOutputPartition) | Syft::InputOutputPartition | |
read_from_file(const std::string &filename) | Syft::InputOutputPartition | static |
+ LydiaSyft
+
+ |
+
A partition of variables into input and output variables. + More...
+ +#include <InputOutputPartition.h>
+Public Member Functions | |
+ | InputOutputPartition () |
Creates a partition with no variables. | |
+bool | is_input (const std::string &var_name) |
check if a variable is an input variable | |
+bool | is_output (const std::string &var_name) |
check if a variable is an output variable | |
+Static Public Member Functions | |
static InputOutputPartition | read_from_file (const std::string &filename) |
Constructs a partition from a file. More... | |
static InputOutputPartition | construct_from_input (const std::vector< std::string > inputs_substr, std::vector< std::string > outputs_substr) |
Constructs a partition from inputs. More... | |
+Public Attributes | |
+std::vector< std::string > | input_variables |
+std::vector< std::string > | output_variables |
A partition of variables into input and output variables.
+
+
|
+ +static | +
Constructs a partition from inputs.
+inputs_substr | A string vector of input variables. |
outputs_substr | A string vector of output variables. |
+
|
+ +static | +
Constructs a partition from a file.
+The file should look like .inputs: X1 X2 X3 X4 .outputs: Y1 Y2 Y3
+filename | The name of the partition file. + |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::LTLfMaxSetSynthesizer, including all inherited members.
+dump_dot(MaxSetSynthesisResult maxset, const std::string &def_filename, const std::string &nondef_filename) const (defined in Syft::LTLfMaxSetSynthesizer) | Syft::LTLfMaxSetSynthesizer | |
LTLfMaxSetSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | Syft::LTLfMaxSetSynthesizer | |
run() const | Syft::LTLfMaxSetSynthesizer |
+ LydiaSyft
+
+ |
+
A maxset-synthesizer for a reachability game given as a symbolic-state DFA. + More...
+ +#include <LTLfMaxSetSynthesizer.h>
+Public Member Functions | |
LTLfMaxSetSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | |
Construct a MaxSet-LtlfSynthesizer. More... | |
MaxSetSynthesisResult | run () const |
Solves the MaxSet-LTLf synthesis problem. More... | |
+void | dump_dot (MaxSetSynthesisResult maxset, const std::string &def_filename, const std::string &nondef_filename) const |
A maxset-synthesizer for a reachability game given as a symbolic-state DFA.
+Shufang Zhu, Giuseppe De Giacomo: Synthesis of Maximally Permissive Strategies for LTLf Specifications. IJCAI 2022: 2783-2789
+Syft::LTLfMaxSetSynthesizer::LTLfMaxSetSynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space | +
+ | ) | ++ |
Construct a MaxSet-LtlfSynthesizer.
+spec | A symbolic-state DFA representing the LTLf formula. |
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 set of states that the agent must reach to win. |
state_space | The state space. |
MaxSetSynthesisResult Syft::LTLfMaxSetSynthesizer::run | +( | +) | +const | +
Solves the MaxSet-LTLf synthesis problem.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::LTLfSynthesizer, including all inherited members.
+AbstractSingleStrategy(const SynthesisResult &result) const | Syft::LTLfSynthesizer | |
LTLfSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | Syft::LTLfSynthesizer | |
run() const | Syft::LTLfSynthesizer |
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA. + More...
+ +#include <LTLfSynthesizer.h>
+Public Member Functions | |
LTLfSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | |
Construct an LtlfSynthesizer. More... | |
SynthesisResult | run () const |
Solves the LTLf synthesis problem. More... | |
std::unique_ptr< Transducer > | AbstractSingleStrategy (const SynthesisResult &result) const |
Abstract a winning strategy for the agent. More... | |
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA.
+Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi: Symbolic LTLf Synthesis. IJCAI 2017: 1362-1369 +
Syft::LTLfSynthesizer::LTLfSynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space | +
+ | ) | ++ |
Construct an LtlfSynthesizer.
+spec | A symbolic-state DFA representing the LTLf formula. |
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 set of states that the agent must reach to win. |
state_space | The state space. |
std::unique_ptr<Transducer> Syft::LTLfSynthesizer::AbstractSingleStrategy | +( | +const SynthesisResult & | +result | ) | +const | +
Abstract a winning strategy for the agent.
+SynthesisResult Syft::LTLfSynthesizer::run | +( | +) | +const | +
Solves the LTLf synthesis problem.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::MaxSetRunner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
MaxSetRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::MaxSetRunner) | Syft::MaxSetRunner | inline |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
run() (defined in Syft::MaxSetRunner) | Syft::MaxSetRunner | |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | MaxSetRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+void | run () |
Public Member Functions inherited from Syft::BaseRunner | |
+ | BaseRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+Additional Inherited Members | |
Protected Member Functions inherited from Syft::BaseRunner | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
Protected Attributes inherited from Syft::BaseRunner | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::NoQuantification, including all inherited members.
+apply(const CUDD::BDD &bdd) const override (defined in Syft::NoQuantification) | Syft::NoQuantification | virtual |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Performs no quantification. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+CUDD::BDD | apply (const CUDD::BDD &bdd) const override |
Performs no quantification.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Parser, including all inherited members.
+get_formula() const | Syft::Parser | |
get_input_variables() const | Syft::Parser | |
get_output_variables() const | Syft::Parser | |
get_sys_first() const | Syft::Parser | |
Parser() | Syft::Parser | |
read_from_file(const std::string &syfco_location, const std::string &filename) | Syft::Parser | static |
+ LydiaSyft
+
+ |
+
A parser for reading LTLf synthesis benchmarks in TLSF format. + More...
+ +#include <Parser.h>
+Public Member Functions | |
+ | Parser () |
Creates a parser with no items. | |
+std::vector< std::string > | get_input_variables () const |
Return input variables in a vector. | |
+std::vector< std::string > | get_output_variables () const |
Return output variables in a vector. | |
+std::string | get_formula () const |
Return the formula. | |
+bool | get_sys_first () const |
Return true if the target is a Moore machine. | |
+Static Public Member Functions | |
static Parser | read_from_file (const std::string &syfco_location, const std::string &filename) |
Obtain an LTLf formula and construct a partition from a TLSF file. More... | |
A parser for reading LTLf synthesis benchmarks in TLSF format.
+
+
|
+ +static | +
Obtain an LTLf formula and construct a partition from a TLSF file.
+filename | The name of the TLSF file. |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Printer, including all inherited members.
+dump_add_if_enabled(const std::shared_ptr< VarMgr > &var_mgr, const CUDD::ADD &add, const std::string &output_file) const (defined in Syft::Printer) | Syft::Printer | |
dump_maxset_if_enabled(const LTLfMaxSetSynthesizer &maxset_synthesizer, const MaxSetSynthesisResult &maxset_strategy, const std::string &def_strategy_output_file="def_strategy.dot", const std::string &nondef_strategy_output_file="nondef_strategy.dot") const (defined in Syft::Printer) | Syft::Printer | |
dump_transducer_if_enabled(const Transducer &transducer, const std::string &output_file="strategy.dot") const (defined in Syft::Printer) | Syft::Printer | |
print_realizable() const (defined in Syft::Printer) | Syft::Printer | inline |
print_times_if_enabled(const std::string &message, std::chrono::milliseconds time) const (defined in Syft::Printer) | Syft::Printer | |
print_unrealizable() const (defined in Syft::Printer) | Syft::Printer | inline |
Printer(bool print_strategy, bool print_times, std::ostream &out) (defined in Syft::Printer) | Syft::Printer | inline |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | Printer (bool print_strategy, bool print_times, std::ostream &out) |
+void | dump_transducer_if_enabled (const Transducer &transducer, const std::string &output_file="strategy.dot") const |
+void | dump_add_if_enabled (const std::shared_ptr< VarMgr > &var_mgr, const CUDD::ADD &add, const std::string &output_file) const |
+void | dump_maxset_if_enabled (const LTLfMaxSetSynthesizer &maxset_synthesizer, const MaxSetSynthesisResult &maxset_strategy, const std::string &def_strategy_output_file="def_strategy.dot", const std::string &nondef_strategy_output_file="nondef_strategy.dot") const |
+void | print_times_if_enabled (const std::string &message, std::chrono::milliseconds time) const |
+void | print_realizable () const |
+void | print_unrealizable () const |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Quantification, including all inherited members.
+apply(const CUDD::BDD &bdd) const =0 (defined in Syft::Quantification) | Syft::Quantification | pure virtual |
~Quantification() (defined in Syft::Quantification) | Syft::Quantification | inlinevirtual |
+ LydiaSyft
+
+ |
+
Abstract class representing a quantification operation on BDDs. + More...
+ +#include <Quantification.h>
+Public Member Functions | |
+virtual CUDD::BDD | apply (const CUDD::BDD &bdd) const =0 |
Abstract class representing a quantification operation on BDDs.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Reachability, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA. + More...
+ +#include <Reachability.hpp>
+Public Member Functions | |
Reachability (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space) | |
Construct a single-strategy-synthesizer for the given reachability game. More... | |
SynthesisResult | run () const final |
Solves the 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. | |
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA.
+Reachability condition holds.
+Syft::Reachability::Reachability | +( | +const SymbolicStateDfa & | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | const CUDD::BDD & | +goal_states, | +
+ | + | const CUDD::BDD & | +state_space | +
+ | ) | ++ |
Construct a single-strategy-synthesizer for the given reachability game.
+spec | A symbolic-state DFA representing the 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. |
state_space | The state space. |
+
|
+ +finalvirtual | +
Solves the reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ReachabilityMaxSet, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A maxset-strategy-synthesizer for a reachability game given as a symbolic-state DFA. + More...
+ +#include <ReachabilityMaxSet.hpp>
+Public Member Functions | |
ReachabilityMaxSet (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space) | |
Construct a maxset-strategy-synthesizer for the given reachability game. More... | |
MaxSetSynthesisResult | run_maxset () const |
Solves the maxset-reachability game. More... | |
SynthesisResult | run () const final |
Solve standard reachability game. More... | |
+void | dump_dot (MaxSetSynthesisResult maxset, const std::string &def_filename, const std::string &nondef_filename) const |
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. | |
A maxset-strategy-synthesizer for a reachability game given as a symbolic-state DFA.
+Reachability condition holds.
+Syft::ReachabilityMaxSet::ReachabilityMaxSet | +( | +const SymbolicStateDfa & | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | const CUDD::BDD & | +goal_states, | +
+ | + | const CUDD::BDD & | +state_space | +
+ | ) | ++ |
Construct a maxset-strategy-synthesizer for the given reachability game.
+spec | A symbolic-state DFA representing the 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. |
state_space | The state space. |
+
|
+ +finalvirtual | +
Solve standard reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +MaxSetSynthesisResult Syft::ReachabilityMaxSet::run_maxset | +( | +) | +const | +
Solves the maxset-reachability game.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ReachabilityMaxSetSynthesizer, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A maxset-synthesizer for a reachability game given as a symbolic-state DFA. + More...
+ +#include <ReachabilityMaxSetSynthesizer.h>
+Public Member Functions | |
ReachabilityMaxSetSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | |
Construct a maxset-synthesizer for the given reachability game. More... | |
virtual SynthesisResult | run () const final |
Solves the reachability game. More... | |
+MaxSet | AbstractMaxSet (const SynthesisResult &) const |
+void | dump_dot (MaxSet maxset, const std::string &def_filename, const std::string &nondef_filename) const |
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_ |
A maxset-synthesizer for a reachability game given as a symbolic-state DFA.
+Syft::ReachabilityMaxSetSynthesizer::ReachabilityMaxSetSynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space | +
+ | ) | ++ |
Construct a maxset-synthesizer for the given reachability game.
+spec | A symbolic-state DFA representing the reachability game. |
starting_player | The player that moves first each turn. |
goal_states | The set of states that the agent must reach to win. |
+
|
+ +finalvirtual | +
Solves the reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::ReachabilitySynthesizer, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA. + More...
+ +#include <ReachabilitySynthesizer.h>
+Public Member Functions | |
ReachabilitySynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space) | |
Construct a single-strategy-synthesizer for the given reachability game. More... | |
virtual SynthesisResult | run () const final |
Solves the 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_ |
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA.
+Syft::ReachabilitySynthesizer::ReachabilitySynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space | +
+ | ) | ++ |
Construct a single-strategy-synthesizer for the given reachability game.
+spec | A symbolic-state DFA representing the 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 set of states that the agent must reach to win. |
state_space | The state space. |
+
|
+ +finalvirtual | +
Solves the reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::SmtOneStepRealizabilityVisitor, including all inherited members.
+
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | SmtOneStepRealizabilityVisitor (const InputOutputPartition &partition, const Syft::VarMgr &var_mgr, z3::context &z3_context, z3::solver &solver) |
+void | visit (const whitemech::lydia::LTLfTrue &) override |
+void | visit (const whitemech::lydia::LTLfFalse &) override |
+void | visit (const whitemech::lydia::LTLfAtom &) override |
+void | visit (const whitemech::lydia::LTLfNot &) override |
+void | visit (const whitemech::lydia::LTLfAnd &) override |
+void | visit (const whitemech::lydia::LTLfOr &) override |
+void | visit (const whitemech::lydia::LTLfNext &) override |
+void | visit (const whitemech::lydia::LTLfWeakNext &) override |
+void | visit (const whitemech::lydia::LTLfUntil &) override |
+void | visit (const whitemech::lydia::LTLfRelease &) override |
+void | visit (const whitemech::lydia::LTLfEventually &) override |
+void | visit (const whitemech::lydia::LTLfAlways &) override |
+z3::expr | apply (const whitemech::lydia::LTLfFormula &f) |
+Public Attributes | |
+InputOutputPartition | partition |
+const VarMgr & | var_mgr |
+z3::context & | z3_context |
+z3::solver & | solver |
+z3::expr | result |
+std::set< std::string > | uncontrollableVars |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::SmtOneStepUnrealizabilityVisitor, including all inherited members.
+
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | SmtOneStepUnrealizabilityVisitor (const InputOutputPartition &partition, const Syft::VarMgr &var_mgr, z3::context &z3_context, z3::solver &solver, Syft::Player starting_player) |
+void | visit (const whitemech::lydia::LTLfTrue &) override |
+void | visit (const whitemech::lydia::LTLfFalse &) override |
+void | visit (const whitemech::lydia::LTLfAtom &) override |
+void | visit (const whitemech::lydia::LTLfNot &) override |
+void | visit (const whitemech::lydia::LTLfAnd &) override |
+void | visit (const whitemech::lydia::LTLfOr &) override |
+void | visit (const whitemech::lydia::LTLfNext &) override |
+void | visit (const whitemech::lydia::LTLfWeakNext &) override |
+void | visit (const whitemech::lydia::LTLfUntil &) override |
+void | visit (const whitemech::lydia::LTLfRelease &) override |
+void | visit (const whitemech::lydia::LTLfEventually &) override |
+void | visit (const whitemech::lydia::LTLfAlways &) override |
+z3::expr | apply (const whitemech::lydia::LTLfFormula &f) |
+Public Attributes | |
+InputOutputPartition | partition |
+const VarMgr & | var_mgr |
+z3::context & | z3_context |
+z3::solver & | solver |
+z3::expr | result |
+Syft::Player | starting_player |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::StabilityLtlfSynthesizer, including all inherited members.
+load_CNF(const std::string &filename) const (defined in Syft::StabilityLtlfSynthesizer) | Syft::StabilityLtlfSynthesizer | protected |
run() const | Syft::StabilityLtlfSynthesizer | |
StabilityLtlfSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space, std::string &assumption_filename) | Syft::StabilityLtlfSynthesizer |
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables. + More...
+ +#include <StabilityLtlfSynthesizer.h>
+Public Member Functions | |
StabilityLtlfSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space, std::string &assumption_filename) | |
Construct an StabilityLtlfSynthesizer. More... | |
SynthesisResult | run () const |
Solves the synthesis problem of LTLf with simple Stability environment assumption. More... | |
+Protected Member Functions | |
+CUDD::BDD | load_CNF (const std::string &filename) const |
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables.
+Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi: LTLÆ’ Synthesis with Fairness and Stability Assumptions. AAAI 2020: 3088-3095 +
Syft::StabilityLtlfSynthesizer::StabilityLtlfSynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space, | +
+ | + | std::string & | +assumption_filename | +
+ | ) | ++ |
Construct an StabilityLtlfSynthesizer.
+spec | A symbolic-state DFA representing the LTLf formula. |
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 set of states that the agent must reach to win. |
state_space | The state space. |
assumption_filename | The file that specifies a Boolean formula \alpha over input variables, denoting the simple Stability assumption FG\alpha. |
SynthesisResult Syft::StabilityLtlfSynthesizer::run | +( | +) | +const | +
Solves the synthesis problem of LTLf with simple Stability environment assumption.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::StabilityRunner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
run() (defined in Syft::StabilityRunner) | Syft::StabilityRunner | |
StabilityRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &assumption_filename, bool print_strategy, bool print_times) (defined in Syft::StabilityRunner) | Syft::StabilityRunner | inline |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | StabilityRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, const std::string &assumption_filename, bool print_strategy, bool print_times) |
+void | run () |
Public Member Functions inherited from Syft::BaseRunner | |
+ | BaseRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+Additional Inherited Members | |
Protected Member Functions inherited from Syft::BaseRunner | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
Protected Attributes inherited from Syft::BaseRunner | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::StableReachabilitySynthesizer, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA. + More...
+ +#include <StableReachabilitySynthesizer.h>
+Public Member Functions | |
StableReachabilitySynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space, std::string &assumption_filename) | |
Construct a single-strategy-synthesizer for the given Buchi-reachability game. More... | |
virtual 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) |
+Protected Member Functions | |
+CUDD::BDD | load_CNF (const std::string &filename) const |
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... | |
+Additional Inherited Members | |
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_ |
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.
+Syft::StableReachabilitySynthesizer::StableReachabilitySynthesizer | +( | +SymbolicStateDfa | +spec, | +
+ | + | Player | +starting_player, | +
+ | + | Player | +protagonist_player, | +
+ | + | CUDD::BDD | +goal_states, | +
+ | + | CUDD::BDD | +state_space, | +
+ | + | std::string & | +assumption_filename | +
+ | ) | ++ |
Construct a single-strategy-synthesizer for the given Buchi-reachability game.
+spec | A symbolic-state DFA representing the Buchi-reachability game. |
starting_player | The player that moves first each turn. |
goal_states | The set of states that the agent must reach to win. |
+
|
+ +finalvirtual | +
Solves the coBuchi-reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Stopwatch, including all inherited members.
+start() | Syft::Stopwatch | |
stop() | Syft::Stopwatch | |
Stopwatch() | Syft::Stopwatch |
+ LydiaSyft
+
+ |
+
Stopwatch for timing executions. + More...
+ +#include <Stopwatch.h>
+Public Member Functions | |
+ | Stopwatch () |
Create a stopwatch without starting it. | |
+void | start () |
Start the stopwatch. | |
std::chrono::milliseconds | stop () |
Stop the stopwatch. More... | |
Stopwatch for timing executions.
+std::chrono::milliseconds Syft::Stopwatch::stop | +( | +) | ++ |
Stop the stopwatch.
+Throws an exception if stopwatch hasn't been started since the last time it was stopped.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::SymbolicStateDfa, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A DFA with symbolic states and transitions. + More...
+ +#include <SymbolicStateDfa.h>
+Public Member Functions | |
+std::shared_ptr< VarMgr > | var_mgr () const |
Returns the variable manager. | |
std::size_t | automaton_id () const |
Returns the automaton ID. More... | |
+std::vector< int > | initial_state () const |
Returns the bitvector representing the initial state of the DFA. | |
+CUDD::BDD | initial_state_bdd () const |
Returns the BDD representing the initial state of the DFA. | |
+CUDD::BDD | final_states () const |
Returns the BDD encoding the set of final states. | |
std::vector< CUDD::BDD > | transition_function () const |
Returns the transition function of the DFA as a vector of BDDs. More... | |
void | restrict_dfa_with_states (const CUDD::BDD &valid_states) |
Restrict a symbolic DFA with a given set of states. More... | |
void | restrict_dfa_with_transitions (const CUDD::BDD &feasible_moves) |
Restrict a symbolic DFA with a set of feasible moves. More... | |
void | dump_dot (const std::string &filename) const |
Saves the symbolic representation of the DFA in a .dot file. More... | |
void | new_sink_states (const CUDD::BDD &sink_states) |
Shrink a set of states to a sink state. More... | |
+Static Public Member Functions | |
static SymbolicStateDfa | from_explicit (const ExplicitStateDfaAdd &explicit_dfa) |
Converts an explicit DFA to a symbolic representation. More... | |
static SymbolicStateDfa | from_predicates (std::shared_ptr< VarMgr > var_mgr, std::vector< CUDD::BDD > predicates) |
Creates a simple automaton that remembers the value of predicates. More... | |
static SymbolicStateDfa | product_AND (const std::vector< SymbolicStateDfa > &dfa_vector) |
Returns a product AND of two symbolic DFAs. More... | |
static std::vector< int > | state_to_binary (std::size_t state, std::size_t bit_count) |
Returns the binary encoding of a given state index. More... | |
static SymbolicStateDfa | product_OR (const std::vector< SymbolicStateDfa > &dfa_vector) |
Returns a product AND of two symbolic DFAs. More... | |
static SymbolicStateDfa | complement (const SymbolicStateDfa dfa) |
Returns the complement of a symbolic DFA. More... | |
A DFA with symbolic states and transitions.
+Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi: Symbolic LTLf Synthesis. IJCAI 2017: 1362-1369
+std::size_t Syft::SymbolicStateDfa::automaton_id | +( | +) | +const | +
Returns the automaton ID.
+This ID can be used to retrieve the associated state variables from the variable manager.
+ +
+
|
+ +static | +
Returns the complement of a symbolic DFA.
+dfa | The DFA to be complemented. |
void Syft::SymbolicStateDfa::dump_dot | +( | +const std::string & | +filename | ) | +const | +
Saves the symbolic representation of the DFA in a .dot file.
+The file includes both the BDDs representing the transition function and the BDD representing the final states.
+filename | The name of the file to save the symbolic DFA to. |
+
|
+ +static | +
Converts an explicit DFA to a symbolic representation.
+Encodes the state space of the DFA in a logarithmic number of state variables, using BDDs to represent the transition function and the set of final states.
+explicit_dfa | The explicit DFA to be converted. |
+
|
+ +static | +
Creates a simple automaton that remembers the value of predicates.
+var_mgr | The variable manager to use to create the state variables. |
predicates | A vector of BDDs over named variables representing the predicates to remember. |
void Syft::SymbolicStateDfa::new_sink_states | +( | +const CUDD::BDD & | +sink_states | ) | ++ |
Shrink a set of states to a sink state.
+sink_states | The set of states to shrink. |
+
|
+ +static | +
Returns a product AND of two symbolic DFAs.
+first_dfa | The first DFA. |
second_dfa | The second DFA. |
+
|
+ +static | +
Returns a product AND of two symbolic DFAs.
+first_dfa | The first DFA. |
second_dfa | The second DFA. |
void Syft::SymbolicStateDfa::restrict_dfa_with_states | +( | +const CUDD::BDD & | +valid_states | ) | ++ |
Restrict a symbolic DFA with a given set of states.
+Basically restrict a DFA to a set of states from the DFA.
+valid_states | The set of states to be kept. |
void Syft::SymbolicStateDfa::restrict_dfa_with_transitions | +( | +const CUDD::BDD & | +feasible_moves | ) | ++ |
Restrict a symbolic DFA with a set of feasible moves.
+feasible_moves | The set of feasible moves to be kept. |
+
|
+ +static | +
Returns the binary encoding of a given state index.
+state | The state index. |
bit_count | The number of bits in the binary encoding DFA. |
std::vector< CUDD::BDD > Syft::SymbolicStateDfa::transition_function | +( | +) | +const | +
Returns the transition function of the DFA as a vector of BDDs.
+The BDD in index i computes the value of state variable i in the next step, given the current values of the state and alphabet variables.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::SynthesisRunner, including all inherited members.
+args_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
BaseRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::BaseRunner) | Syft::BaseRunner | inline |
do_dfa_construction_() const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
driver_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
formula_file_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_preprocessing_result_(const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
handle_synthesis_result_(const SynthesisResult &result) const (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
path_to_syfco_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
printer_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
run() (defined in Syft::SynthesisRunner) | Syft::SynthesisRunner | |
SynthesisRunner(const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) (defined in Syft::SynthesisRunner) | Syft::SynthesisRunner | inline |
var_mgr_ (defined in Syft::BaseRunner) | Syft::BaseRunner | protected |
+ LydiaSyft
+
+ |
+
+Public Member Functions | |
+ | SynthesisRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+void | run () |
Public Member Functions inherited from Syft::BaseRunner | |
+ | BaseRunner (const std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > &driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, bool print_times) |
+Additional Inherited Members | |
Protected Member Functions inherited from Syft::BaseRunner | |
+bool | handle_preprocessing_result_ (const OneStepSynthesisResult &one_step_result, Stopwatch &total_time_stopwatch) const |
+void | handle_synthesis_result_ (const DfaGameSynthesizer &synthesizer, const SynthesisResult &result) const |
+void | handle_synthesis_result_ (const SynthesisResult &result) const |
+SymbolicStateDfa | do_dfa_construction_ () const |
Protected Attributes inherited from Syft::BaseRunner | |
+const std::string | formula_file_ |
+const std::string | path_to_syfco_ |
+const TLSFArgs | args_ |
+const std::shared_ptr< Syft::VarMgr > | var_mgr_ |
+const Printer | printer_ |
+std::shared_ptr< whitemech::lydia::parsers::ltlf::LTLfDriver > | driver_ |
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Synthesizer< Spec >, including all inherited members.
+run() const =0 | Syft::Synthesizer< Spec > | pure virtual |
spec_ | Syft::Synthesizer< Spec > | protected |
Synthesizer(Spec spec) (defined in Syft::Synthesizer< Spec >) | Syft::Synthesizer< Spec > | inline |
~Synthesizer() (defined in Syft::Synthesizer< Spec >) | Syft::Synthesizer< Spec > | inlinevirtual |
+ LydiaSyft
+
+ |
+
Abstract class for synthesizers. + More...
+ +#include <Synthesizer.h>
+Public Member Functions | |
+ | Synthesizer (Spec spec) |
virtual SynthesisResult | run () const =0 |
Solves the synthesis problem of the specification. More... | |
+Protected Attributes | |
+Spec | spec_ |
The game arena. | |
Abstract class for synthesizers.
+Can be inherited to implement synthesizers for different specification types.
+
+
|
+ +pure virtual | +
Solves the synthesis problem of the specification.
+Implemented in Syft::DfaGameSynthesizer, Syft::ReachabilityMaxSet, Syft::Reachability, Syft::coBuchiReachability, and Syft::BuchiReachability.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::Transducer, including all inherited members.
+dump_dot(const std::string &filename) const | Syft::Transducer | |
Transducer(const std::shared_ptr< VarMgr > &var_mgr, const std::vector< int > &initial_vector, const std::unordered_map< int, CUDD::BDD > &output_function, const std::vector< CUDD::BDD > &transition_function, Player starting_player, Player protagonist_player=Player::Agent) (defined in Syft::Transducer) | Syft::Transducer |
+ LydiaSyft
+
+ |
+
A symbolic tranducer representing a winning strategy for a game. + More...
+ +#include <Transducer.h>
+Public Member Functions | |
+ | Transducer (const std::shared_ptr< VarMgr > &var_mgr, const std::vector< int > &initial_vector, const std::unordered_map< int, CUDD::BDD > &output_function, const std::vector< CUDD::BDD > &transition_function, Player starting_player, Player protagonist_player=Player::Agent) |
+void | dump_dot (const std::string &filename) const |
Saves the output function of the transducer in a .dot file. | |
A symbolic tranducer representing a winning strategy for a game.
+May be either a Moore or Mealy machine.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::VarMgr, including all inherited members.
+automaton_num() const | Syft::VarMgr | |
bdd_to_string(const CUDD::BDD &bdd) const | Syft::VarMgr | |
create_complement_state_space(const std::size_t automaton_id) | Syft::VarMgr | |
create_named_variables(const std::vector< std::string > &variable_names) | Syft::VarMgr | |
create_product_state_space(const std::vector< std::size_t > &automaton_ids) | Syft::VarMgr | |
create_state_variables(std::size_t variable_count) | Syft::VarMgr | |
cudd_mgr() const | Syft::VarMgr | |
dump_dot(const CUDD::ADD &add, const std::string &filename) const | Syft::VarMgr | |
dump_dot(const std::vector< CUDD::ADD > &adds, const std::vector< std::string > &function_labels, const std::string &filename) const | Syft::VarMgr | |
index_to_name(int index) const | Syft::VarMgr | |
input_cube() const | Syft::VarMgr | |
input_variable_count() const | Syft::VarMgr | |
input_variable_labels() const | Syft::VarMgr | |
make_compose_vector(std::size_t automaton_id, const std::vector< CUDD::BDD > &state_bdds) const | Syft::VarMgr | |
make_eval_vector(std::size_t automaton_id, const std::vector< int > &state_vector) const | Syft::VarMgr | |
make_state_eval_vector(std::size_t automaton_id, const std::vector< int > &state_vector) const | Syft::VarMgr | |
name_to_variable(const std::string &name) const | Syft::VarMgr | |
output_cube() const | Syft::VarMgr | |
output_variable_count() const | Syft::VarMgr | |
output_variable_labels() const | Syft::VarMgr | |
partition_variables(const std::vector< std::string > &input_names, const std::vector< std::string > &output_names) | Syft::VarMgr | |
state_variable(std::size_t automaton_id, std::size_t i) const | Syft::VarMgr | |
state_variable_count(std::size_t automaton_id) const | Syft::VarMgr | |
state_variable_labels(std::size_t automaton_id) const | Syft::VarMgr | |
state_variables_cube(std::size_t automaton_id) const | Syft::VarMgr | |
state_vector_to_bdd(std::size_t automaton_id, const std::vector< int > &state_vector) const | Syft::VarMgr | |
total_state_variable_count() const | Syft::VarMgr | |
total_variable_count() const | Syft::VarMgr | |
variable_labels() const | Syft::VarMgr | |
VarMgr() | Syft::VarMgr |
+ LydiaSyft
+
+ |
+
A dictionary that maps variable names to indices and vice versa. + More...
+ +#include <VarMgr.h>
+Public Member Functions | |
+ | VarMgr () |
Constructs a VarMgr with no variables. | |
void | create_named_variables (const std::vector< std::string > &variable_names) |
Creates BDD variables and associates each with a name. More... | |
std::size_t | create_state_variables (std::size_t variable_count) |
Creates and stores state variables. More... | |
std::size_t | create_product_state_space (const std::vector< std::size_t > &automaton_ids) |
Registers a new automaton ID associated with a product state space. More... | |
+CUDD::BDD | state_variable (std::size_t automaton_id, std::size_t i) const |
Returns the i-th state variable for a given automaton. | |
CUDD::BDD | state_vector_to_bdd (std::size_t automaton_id, const std::vector< int > &state_vector) const |
Converts a state vector to a BDD. More... | |
void | partition_variables (const std::vector< std::string > &input_names, const std::vector< std::string > &output_names) |
Partitions the named variables between inputs and outputs. More... | |
+std::shared_ptr< CUDD::Cudd > | cudd_mgr () const |
Returns the CUDD manager used to create the variables. | |
+CUDD::BDD | name_to_variable (const std::string &name) const |
Returns the index of the variable with the given name. | |
+std::string | index_to_name (int index) const |
Returns the name of the variable at index index. | |
+std::size_t | total_variable_count () const |
Returns the total number of variables, including named and state. | |
+std::size_t | total_state_variable_count () const |
Returns the total number of state variables. | |
+std::size_t | state_variable_count (std::size_t automaton_id) const |
Returns the number of state variables for a given automaton. | |
+std::size_t | input_variable_count () const |
Returns the number of input variables. | |
+std::size_t | output_variable_count () const |
Returns the number of output variables. | |
+CUDD::BDD | input_cube () const |
Returns a BDD formed by the conjunction of all input variables. | |
+CUDD::BDD | output_cube () const |
Returns a BDD formed by the conjunction of all output variables. | |
+CUDD::BDD | state_variables_cube (std::size_t automaton_id) const |
Returns a BDD formed by the conjunction of all state variables of automaton automaton_id. | |
std::vector< int > | make_eval_vector (std::size_t automaton_id, const std::vector< int > &state_vector) const |
Creates a valid input to CUDD::BDD::Eval. More... | |
std::vector< int > | make_state_eval_vector (std::size_t automaton_id, const std::vector< int > &state_vector) const |
Creates a valid input to CUDD::BDD::Eval. More... | |
std::vector< CUDD::BDD > | make_compose_vector (std::size_t automaton_id, const std::vector< CUDD::BDD > &state_bdds) const |
Creates a valid input to CUDD::BDD::VectorCompose. More... | |
std::vector< std::string > | variable_labels () const |
Returns a vector with a label for each variable. More... | |
std::vector< std::string > | input_variable_labels () const |
Returns a vector with a label for each input variable. More... | |
std::vector< std::string > | output_variable_labels () const |
Returns a vector with a label for each output variable. More... | |
std::vector< std::string > | state_variable_labels (std::size_t automaton_id) const |
Returns a vector with a label for each state variable. More... | |
void | dump_dot (const CUDD::ADD &add, const std::string &filename) const |
Saves an ADD in a .dot file. More... | |
void | dump_dot (const std::vector< CUDD::ADD > &adds, const std::vector< std::string > &function_labels, const std::string &filename) const |
Saves ADDs to a .dot file with corresponding labels. More... | |
+std::size_t | automaton_num () const |
Returns the number of DFAs the manager handles. | |
std::string | bdd_to_string (const CUDD::BDD &bdd) const |
Prints a BDD as a Boolean formula, where each variable has a specific label. More... | |
+std::size_t | create_complement_state_space (const std::size_t automaton_id) |
Create the state space when complementing a DFA. | |
A dictionary that maps variable names to indices and vice versa.
+std::string Syft::VarMgr::bdd_to_string | +( | +const CUDD::BDD & | +bdd | ) | +const | +
Prints a BDD as a Boolean formula, where each variable has a specific label.
+A | given BDD. |
void Syft::VarMgr::create_named_variables | +( | +const std::vector< std::string > & | +variable_names | ) | ++ |
Creates BDD variables and associates each with a name.
+variable_names | The names of the variables to create. A new variable is only created if a variable by that name does not already exist. |
std::size_t Syft::VarMgr::create_product_state_space | +( | +const std::vector< std::size_t > & | +automaton_ids | ) | ++ |
Registers a new automaton ID associated with a product state space.
+This function does not create new state variables. Instead, the variables associated with the new ID are the union of all variables for the automata that form the product.
+automaton_ids | A vector of automaton IDs all of which must already exist in the manager. |
std::size_t Syft::VarMgr::create_state_variables | +( | +std::size_t | +variable_count | ) | ++ |
Creates and stores state variables.
+Multiple calls of this function create separate groups of state variables. The call generates an ID for the automaton whose state space the variables represent, so that the correct group of variables can be retrieved later.
+variable_count | The number of state variables to create. |
void Syft::VarMgr::dump_dot | +( | +const CUDD::ADD & | +add, | +
+ | + | const std::string & | +filename | +
+ | ) | +const | +
Saves an ADD in a .dot file.
+Uses ADD for better visualization in the .dot file. To call with a BDD, use dump_dot(bdd.Add(), filename).
+An | ADD add and filename. |
void Syft::VarMgr::dump_dot | +( | +const std::vector< CUDD::ADD > & | +adds, | +
+ | + | const std::vector< std::string > & | +function_labels, | +
+ | + | const std::string & | +filename | +
+ | ) | +const | +
Saves ADDs to a .dot file with corresponding labels.
+adds | A vector of ADDs to be saved to file. |
function_labels | A vector such that function_labels[i] contains the label for adds[i]. The labels appear above the corresponding ADD in the file. |
filename | The name of the .dot file. |
std::vector< std::string > Syft::VarMgr::input_variable_labels | +( | +) | +const | +
Returns a vector with a label for each input variable.
+To be used with CUDD::Cudd::DumpDot.
+std::vector< CUDD::BDD > Syft::VarMgr::make_compose_vector | +( | +std::size_t | +automaton_id, | +
+ | + | const std::vector< CUDD::BDD > & | +state_bdds | +
+ | ) | +const | +
Creates a valid input to CUDD::BDD::VectorCompose.
+automaton_id | The ID of the automaton whose variables to use. |
state_bdds | A vector containing one BDD for each state variable of the automaton. |
std::vector< int > Syft::VarMgr::make_eval_vector | +( | +std::size_t | +automaton_id, | +
+ | + | const std::vector< int > & | +state_vector | +
+ | ) | +const | +
Creates a valid input to CUDD::BDD::Eval.
+automaton_id | The ID of the automaton whose variables to use. |
state_vector | A vector of 1s and 0s encoding a state's binary representation. |
std::vector< int > Syft::VarMgr::make_state_eval_vector | +( | +std::size_t | +automaton_id, | +
+ | + | const std::vector< int > & | +state_vector | +
+ | ) | +const | +
Creates a valid input to CUDD::BDD::Eval.
+automaton_id | The ID of the automaton whose variables to use. |
state_vector | A vector of 1s and 0s encoding a state's binary representation. |
std::vector< std::string > Syft::VarMgr::output_variable_labels | +( | +) | +const | +
Returns a vector with a label for each output variable.
+To be used with CUDD::Cudd::DumpDot.
+void Syft::VarMgr::partition_variables | +( | +const std::vector< std::string > & | +input_names, | +
+ | + | const std::vector< std::string > & | +output_names | +
+ | ) | ++ |
Partitions the named variables between inputs and outputs.
+input_names | The names of the variables that should be considered inputs. |
output_names | The names of the variables that should be considered outputs. |
std::vector< std::string > Syft::VarMgr::state_variable_labels | +( | +std::size_t | +automaton_id | ) | +const | +
Returns a vector with a label for each state variable.
+To be used with CUDD::Cudd::DumpDot.
+CUDD::BDD Syft::VarMgr::state_vector_to_bdd | +( | +std::size_t | +automaton_id, | +
+ | + | const std::vector< int > & | +state_vector | +
+ | ) | +const | +
Converts a state vector to a BDD.
+automaton_id | The ID of the automaton whose variables to use. |
state_vector | A vector of 1s and 0s encoding a state's binary representation. |
std::vector< std::string > Syft::VarMgr::variable_labels | +( | +) | +const | +
Returns a vector with a label for each variable.
+To be used with CUDD::Cudd::DumpDot.
+
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::coBuchiReachability, including all inherited members.
+
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA. + More...
+ +#include <coBuchiReachability.hpp>
+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. | |
A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA.
+Either coBuchi condition holds or reachability condition holds.
+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.
+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. |
+
|
+ +finalvirtual | +
Solves the coBuchi-reachability game.
+Implements Syft::DfaGameSynthesizer.
+ +
+ LydiaSyft
+
+ |
+
This is the complete list of members for Syft::coGR1Reachability, including all inherited members.
+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) | Syft::coGR1Reachability | |
coGR1Reachability(SymbolicStateDfa dfa, Player player, Player player1, CUDD::BDD bdd, CUDD::BDD bdd1, CUDD::BDD bdd2) (defined in Syft::coGR1Reachability) | Syft::coGR1Reachability | |
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 (defined in Syft::coGR1Reachability) | Syft::coGR1Reachability | |
run() const | Syft::coGR1Reachability |
+ LydiaSyft
+
+ |
+
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA. + More...
+ +#include <coGR1Reachability.hpp>
+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) |
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.
+Either Buchi condition holds or reachability condition holds.
+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.
+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.
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
▼ src | |
▼ cli | |
base.hpp | |
fairness.hpp | |
gr1.hpp | |
maxset.hpp | |
stability.hpp | |
synthesis.hpp | |
▼ parser | |
Parser.h | |
▼ synthesis | |
▼ header | |
▼ automata | |
ExplicitStateDfa.h | |
ExplicitStateDfaAdd.h | |
SymbolicStateDfa.h | |
▼ game | |
BuchiReachability.hpp | |
coBuchiReachability.hpp | |
coGR1Reachability.hpp | |
DfaGameSynthesizer.h | |
InputOutputPartition.h | |
Quantification.h | |
Reachability.hpp | |
ReachabilityMaxSet.hpp | |
Transducer.h | |
▼ synthesizer | |
FairnessLtlfSynthesizer.h | |
GR1LTLfSynthesizer.h | |
LTLfMaxSetSynthesizer.h | |
LTLfSynthesizer.h | |
StabilityLtlfSynthesizer.h | |
GR1.h | |
OneStepRealizability.h | |
OneStepUnrealizability.h | |
Player.h | |
Preprocessing.h | |
Stopwatch.h | |
Synthesizer.h | |
VarMgr.h | |
▼ utils | |
string_utilities.h |
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
+ LydiaSyft
+
+ |
+
This page explains how to interpret the graphs that are generated by doxygen.
+Consider the following example:
This will result in the following graph:
+The boxes in the above graph have the following meaning:
+The arrows have the following meaning:
+
+ LydiaSyft
+
+ |
+
▼CSyft::BaseRunner | |
CSyft::FairnessRunner | |
CSyft::GR1Runner | |
CSyft::MaxSetRunner | |
CSyft::StabilityRunner | |
CSyft::SynthesisRunner | |
CSyft::coGR1Reachability | A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA |
CSyft::ExplicitStateDfaAdd | A DFA with explicit states and symbolic transitions represented in ADDs |
CSyft::FairnessLtlfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Fairness assumption. The simple Fairness assumption is in the form of GF\alpha, where \alpha is a Boolean formula over environment variables |
CSyft::GR1 | |
CSyft::GR1LTLfSynthesizer | 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 |
CSyft::InputOutputPartition | A partition of variables into input and output variables |
CSyft::LTLfMaxSetSynthesizer | A maxset-synthesizer for a reachability game given as a symbolic-state DFA |
CSyft::LTLfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA |
CSyft::MaxSetSynthesisResult | |
▼Cwhitemech::lydia::mona_dfa | |
CSyft::ExplicitStateDfa | A DFA with explicit states and symbolic transitions |
CSyft::OneStepSynthesisResult | |
CSyft::Parser | A parser for reading LTLf synthesis benchmarks in TLSF format |
CSyft::Printer | |
▼CSyft::Quantification | Abstract class representing a quantification operation on BDDs |
CSyft::Exists | Performs existential quantification |
CSyft::ExistsForall | Performs both universal and existential quantification |
CSyft::Forall | Performs universal quantification |
CSyft::ForallExists | Performs both universal and existential quantification |
CSyft::NoQuantification | Performs no quantification |
CSyft::StabilityLtlfSynthesizer | A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables |
CSyft::Stopwatch | Stopwatch for timing executions |
CSyft::SymbolicStateDfa | A DFA with symbolic states and transitions |
CSyft::SynthesisResult | |
CSyft::Synthesizer< Spec > | Abstract class for synthesizers |
▼CSyft::Synthesizer< SymbolicStateDfa > | |
▼CSyft::DfaGameSynthesizer | A synthesizer for a game whose arena is a symbolic-state DFA |
CSyft::BuchiReachability | A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA |
CSyft::Reachability | A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA |
CSyft::ReachabilityMaxSet | A maxset-strategy-synthesizer for a reachability game given as a symbolic-state DFA |
CSyft::coBuchiReachability | A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA |
CSyft::TLSFArgs | |
CSyft::Transducer | A symbolic tranducer representing a winning strategy for a game |
CSyft::VarMgr | A dictionary that maps variable names to indices and vice versa |
▼Cwhitemech::lydia::Visitor | |
CSyft::SmtOneStepRealizabilityVisitor | |
CSyft::SmtOneStepUnrealizabilityVisitor |
+ LydiaSyft
+
+ |
+
We assume the software will be built on a Ubuntu 22.04 machine.
+First, install the following system-wide dependencies:
+0.1 Make sure CUDD is installed. CUDD can be found at:
https://github.com/KavrakiLab/cudd.git +
0.2 Install CUDD:
./configure --enable-silent-rules --enable-obj --enable-dddmp --prefix=[install location] +sudo make install + +If you get an error about aclocal, this might be due to either +a. Not having automake: + sudo apt-get install automake +b. Needing to reconfigure, do this before configuring: + autoreconf -i +
0.3 Install flex and bison:
sudo apt-get install flex bison +
The tool requires the installation of Lydia, which will be triggered by the CMake configuration.
+However, if you want to install Lydia manually, you can co into submodules/lydia
and follow the installation instructions in the README.md
.
By default, the CMake configuration will fetch z3 automatically from the GitHub repository. In order to disable this behaviour, you can configure the project by setting -DZ3_FETCH=OFF.
+In that case, you have to have the library installed on your system. To link the static library of z3, you have to install z3 manually:
+For the graphical features (automata and strategy visualization), graphviz need to be installed:
+4.1. For solving LTLf synthesis with GR(1) conditions, please install slugs
following submodules/slugs/README.md
Usage:
+To see the options of each subcommand, run:
+Examples (run commands from the root directory of the project):
+The documentation is built using Doxygen. First, install doxygen
:
Then:
+
+ LydiaSyft
+
+ |
+
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ + |
+ LydiaSyft
+
+ |
+