All Classes and Interfaces
Class
Description
Abstract class for potentially adaptive set of STL formulas
Abstract AbstractSelectEQOracle class.
Abstract TemporalLogic class.
This class provides an empty implementation of
AbstractTemporalLogicListener
,
which can be extended to create a listener which only needs to handle a subset
of the available methods.This class provides an empty implementation of
AbstractTemporalLogicVisitor
,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.This interface defines a complete listener for a parse tree produced by
AbstractTemporalLogicParser
.This interface defines a complete generic visitor for a parse tree produced
by
AbstractTemporalLogicParser
.Adaptive updater of STL/LTL formulas
Interface for potentially adaptive set of STL formulas
Verifier of a black-box system with respect to the given properties.
Continuous-time systems under learning with numerical I/O.
SimulinkGenerationalGeneticAlgorithm class.
EQSearchProblem class.
SimulinkSteadyStateGeneticAlgorithm class.
A pair of input and output signals at one time step potentially with some previous output signals.
Class to construct pseudo signals from concrete signals
This class provides an empty implementation of
ExtendedSignalMapperListener
,
which can be extended to create a listener which only needs to handle a subset
of the available methods.This class provides an empty implementation of
ExtendedSignalMapperVisitor
,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.This interface defines a complete listener for a parse tree produced by
ExtendedSignalMapperParser
.This interface defines a complete generic visitor for a parse tree produced
by
ExtendedSignalMapperParser
.ExtendedSignalMapperVisitorImpl class.
FalCAuN class.
Equivalence query using genetic algorithm
HillClimbingEQOracle class.
This class implements a random mutation operator for integer solution.
Uniform crossover for integers
A signal with continuous output values.
A discrete-time signal with both input and output values.
A signal with both input and output values.
A pair of input and output signals at one time step.
The atomic propositions in LTL formulas
This class provides an empty implementation of
LTLListener
,
which can be extended to create a listener which only needs to handle a subset
of the available methods.This class provides an empty implementation of
LTLVisitor
,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.This interface defines a complete listener for a parse tree produced by
LTLParser
.This interface defines a complete generic visitor for a parse tree produced
by
LTLParser
.LTLVisitorImpl class.
Equivalence oracle that uses a fixed set of samples.
MutateSelectEQOracle class.
The membership oracle for a Simulink model
Systems under learning with numerical I/O.
I/O Mapper between abstract/concrete NumericSUL.
Verifier of a NumericSUL
The RoSI class representing a robust satisfaction interval (RoSI).
Answer the Equivalence query by simulated annealing
Signal of Simulink
Interface to construct pseudo signals from concrete signals
This class provides an empty implementation of
SignalMapperListener
,
which can be extended to create a listener which only needs to handle a subset
of the available methods.This class provides an empty implementation of
SignalMapperVisitor
,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.This interface defines a complete listener for a parse tree produced by
SignalMapperParser
.This interface defines a complete generic visitor for a parse tree produced
by
SignalMapperParser
.STLVisitorImpl class.
Class to construct pseudo signals from concrete signals
SimulinkAbstractAlphabetDomain class.
Raw Simulink model.
Enum for the interpolation methods of the input signal
Pure Random Tester of a Simulink model
The System Under Learning implemented by a Simulink.
List of STL/LTL formulas without update
STLAtomic class.
This class provides an empty implementation of
STLListener
,
which can be extended to create a listener which only needs to handle a subset
of the available methods.This class provides an empty implementation of
STLVisitor
,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.STLAtomic class.
This interface defines a complete listener for a parse tree produced by
STLParser
.STLAtomic class.
This interface defines a complete generic visitor for a parse tree produced
by
STLParser
.STLVisitorImpl class.
Wraps an equivalence oracle so that the equivalence oracle is skipped if all the LTL oracles are disproved.
The class representing the AND operator of temporal logic.
STLEventually class.
STLGlobal class.
STLImply class.
Interface of a TemporalLogic formula.
Specifies the type of the formula.
STLNext class.
STLTemporalNot class.
The class representing the OR operator of temporal logic.
STLRelease class.
STLUntil class.
Am equivalence oracle to add timeout in addition to the original oracle.
A pair of time and values.