Package net.maswag.falcaun

Class SimulinkRandomTester

java.lang.Object

net.maswag.falcaun.SimulinkRandomTester

public class SimulinkRandomTester
extends Object

Pure Random Tester of a Simulink model

Author:

Masaki Waga

Field Summary

Fields

Modifier and Type	Field	Description
private final net.automatalib.alphabet.Alphabet<String>	abstractInputAlphabet
private List<net.automatalib.word.Word<String>>	cexInput
private List<net.automatalib.word.Word<String>>	cexOutput
private List<TemporalLogic.STLCost>	cexProperty
private final List<TemporalLogic.STLCost>	costFunc
private final int	length
private static final org.slf4j.Logger	LOGGER
private final NumericSULMapper	mapper
private final List<String>	properties
private final Random	random
private final SimulinkSUL	rawSimulink
private final double	signalStep
protected de.learnlib.sul.SUL<List<Double>,IOSignalPiece<List<Double>>>	simulink
private long	timeout

Constructor Summary

Constructors

Constructor	Description
SimulinkRandomTester(String initScript, List<String> paramName, int length, double signalStep, List<String> properties, List<TemporalLogic.STLCost> costFunc, NumericSULMapper mapper)

Method Summary

Modifier and Type	Method	Description
private net.automatalib.word.Word<String>	generateTestWord(List<? extends String> symbolList)	Generate one word of length length randomly
(package private) List<Signal>	getCexConcreteInput()
boolean	run()
(package private) void	setTimeout(long timeout)	Set timeout to the equivalence oracle added next time.

Methods inherited from class java.lang.Object

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

Field Details

simulink

protected de.learnlib.sul.SUL<List<Double>,IOSignalPiece<List<Double>>> simulink

rawSimulink

private final SimulinkSUL rawSimulink

abstractInputAlphabet

private final net.automatalib.alphabet.Alphabet<String> abstractInputAlphabet

mapper

private final NumericSULMapper mapper

costFunc

private final List<TemporalLogic.STLCost> costFunc

timeout

private long timeout

cexInput

private List<net.automatalib.word.Word<String>> cexInput

cexProperty

private List<TemporalLogic.STLCost> cexProperty

cexOutput

private List<net.automatalib.word.Word<String>> cexOutput

length

private final int length

random

private final Random random

properties

private final List<String> properties

signalStep

private final double signalStep

LOGGER

private static final org.slf4j.Logger LOGGER

Constructor Details

SimulinkRandomTester

public SimulinkRandomTester(String initScript,
 List<String> paramName,
 int length,
 double signalStep,
 List<String> properties,
 List<TemporalLogic.STLCost> costFunc,
 NumericSULMapper mapper)
                     throws Exception

Parameters:

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

paramName - The list of input parameters.

length - The length of the sampled signals.

signalStep - The signal step in the simulation

properties - The LTL properties to be verified

costFunc - The STL 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

setTimeout

void setTimeout(long timeout)

Set timeout to the equivalence oracle added next time.

Parameters:

timeout - timeout in seconds.

getCexConcreteInput

List<Signal> getCexConcreteInput()

run

public boolean run()

Returns:

Returns true if and only if the Simulink model is verified i.e., no counter example is found.

generateTestWord

private net.automatalib.word.Word<String> generateTestWord(List<? extends String> symbolList)

Generate one word of length length randomly

Parameters:

symbolList - The list of the possible symbols

Returns:

the generated word