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.