Class List

Here are the classes, structs, unions and interfaces with brief descriptions:

[detail level 12]

▼NSyft
CPrinter
CBaseRunner	Base class for running a synthesis algorithm
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	Implementation of the one-step realizability check using Z3
CSmtOneStepUnrealizabilityVisitor	Implementation of the one-step unrealizability check using Z3
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
CTLSFArgs
CVarMgr	A dictionary that maps variable names to indices and vice versa