All Classes and Interfaces
Class
Description
Abstract class representing a potentially adaptive set of Signal Temporal Logic (STL) formulas.
Abstract class representing an Input-Output (IO) signal.
Abstract class for reading and parsing mapper data from files.
Abstract class for implementing equivalence oracles that select test cases based on a cost function.
Abstract base class for temporal logic formulas.
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 a potentially adaptive set of Signal Temporal Logic (STL) formulas.
Utility class for constructing abstract atomic propositions.
Verifies a black-box system against specified properties using various equivalence oracles and model checking techniques.
Continuous-time systems under learning with numerical I/O.
This class provides construction of Mealy machine from DOT file
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.
Equivalence query using genetic algorithm
Enumeration of selection methods used in Genetic Algorithm (GA) equivalence queries.
HillClimbingEQOracle class.
A class that represents a mapping from characters to double values.
Deprecated.
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.
Represents a pair of input and output signals at one time step in a system's behavior.
Represents the atomic propositions (APs) for LTL formulas.
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 class provides a method to parse an LTL (Linear Temporal Logic) formula.
Base class for LTL formula implementations that provides common functionality
for atomic propositions management using composition instead of inheritance.
Helper class for LTL formula operations.
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
A membership oracle that computes the cost of input-output signals using a specified cost function.
Systems under learning with numerical I/O.
I/O Mapper between abstract/concrete NumericSUL.
Output Mapper for NumericSUL based on Specification-Guided Abstraction.
Verifies a Numeric System Under Learning (NumericSUL) against specified properties using various equivalence oracles and model checking techniques.
A class for mapping output values to characters.
Deprecated.
Use
OutputMapper instead.SignalDiscretizer post-composed with an SULMapper.
SignalDiscretizer pre-composed with an SULMapper
The RoSI class representing a robust satisfaction interval (RoSI).
Answer the Equivalence query by simulated annealing
Output Mapper for Mealy machine based on Specification-Guided Abstraction.
Signal is a sequence of values, each associated with an increasing timestamp.
I/O Mapper between abstract/concrete signals using InputMapper and OutputMapper.
Signal derivation mapper that uses SignalMapper to derive signals from concrete I/O signals.
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
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.This class represents an atomic formula in STL for input signals.
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.
TemporalGlobally 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.
TemporalRelease class.
TemporalUntil class.
Time measurement utility for tracking elapsed time in nanoseconds.
Am equivalence oracle to add timeout in addition to the original oracle.
A sequence of values each associated with an increasing timestamp.
Equivalence Oracle using the actual model of SUL.
InputMapperinstead.