Package net.maswag.falcaun

Class SimulinkSULVerifier

java.lang.Object

net.maswag.falcaun.NumericSULVerifier

net.maswag.falcaun.SimulinkSULVerifier

public class SimulinkSULVerifier
extends NumericSULVerifier

Field Summary

Fields inherited from class net.maswag.falcaun.NumericSULVerifier

rawSUL, simulink

Constructor Summary

Constructors

Constructor	Description
SimulinkSULVerifier(String initScript, List<String> paramName, double signalStep, double simulinkSimulationStep, AdaptiveSTLUpdater<List<Double>> properties, NumericSULMapper mapper)	Constructor for SimulinkVerifier.

Method Summary

Modifier and Type	Method	Description
void	setSimulationStep(double simulinkSimulationStep)	Modify the simulation step of Simulink.

Methods inherited from class net.maswag.falcaun.NumericSULVerifier

addBFOracle, addCompleteExplorationEQOracle, addCornerCaseEQOracle, addGAEQOracle, addGAEQOracleAll, addHillClimbingEQOracle, addHillClimbingEQOracle, addHillClimbingEQOracleAll, addMutateSelectEQOracle, addRandomWalkEQOracle, addRandomWordEQOracle, addSAEQOracle, addSAEQOracleAll, addSimulinkEqOracle, addWpMethodEQOracle, close, getCexAbstractInput, getCexConcreteInput, getCexOutput, getCexProperty, getProperties, getSimulationTimeSecond, getSimulinkCount, getSimulinkCountForEqTest, run, setTimeout, visualizeCex, visualizeLearnedMealy, writeDOTCex, writeDOTLearnedMealy, writeETFLearnedMealy

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

SimulinkSULVerifier

public SimulinkSULVerifier(String initScript,
 List<String> paramName,
 double signalStep,
 double simulinkSimulationStep,
 AdaptiveSTLUpdater<List<Double>> properties,
 NumericSULMapper mapper)
                    throws Exception

Constructor for SimulinkVerifier.

Parameters:

initScript - The MATLAB script called at first. You have to define mdl in the script.

paramName - The list of input parameters.

signalStep - The signal step in the simulation

properties - The LTL properties to be verified

mapper - The I/O mapepr between abstract/concrete Simulink models.

Throws:

Exception - It can be thrown from the constructor of SimulinkSUL.

Method Details

setSimulationStep

public void setSimulationStep(double simulinkSimulationStep)

Modify the simulation step of Simulink.

Parameters:

simulinkSimulationStep - The fixed simulation step of Simulink. If this value is too large, Simulink can abort due to an computation error.