Package net.maswag.falcaun

Class NumericSULVerifier

java.lang.Object
net.maswag.falcaun.NumericSULVerifier
Direct Known Subclasses:
SimulinkSULVerifier
public class NumericSULVerifier extends Object
Verifier of a NumericSUL
Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

  • Constructor Details

    • NumericSULVerifier

      public NumericSULVerifier(NumericSUL rawSUL, double signalStep, AdaptiveSTLUpdater<List<Double>> properties, NumericSULMapper mapper)

      Constructor for SimulinkVerifier.

      Parameters:
      rawSUL - The system under test.
      signalStep - The signal step in the simulation
      properties - The LTL properties to be verified
      mapper - The I/O mapper between abstract/concrete Simulink models.

  • Method Details

    • getCexProperty

      public List<TemporalLogic<List<Double>>> getCexProperty()
      Returns the falsified STL formulas in the string representation.

    • addSimulinkEqOracle

      void addSimulinkEqOracle(Function<IOSignal<List<Double>>,Double> costFunc, Function<NumericMembershipOracleCost,? extends EvaluationCountable.MealyEquivalenceOracle<String,String>> constructor)

    • addWpMethodEQOracle

      public void addWpMethodEQOracle(int maxDepth)

    • addBFOracle

      public void addBFOracle(double multiplier)

    • addRandomWordEQOracle

      public void addRandomWordEQOracle(int minLength, int maxLength, int maxTests, Random random, int batchSize)

    • addRandomWalkEQOracle

      public void addRandomWalkEQOracle(double restartProbability, long maxSteps, Random random)

    • addCompleteExplorationEQOracle

      public void addCompleteExplorationEQOracle(int minDepth, int maxDepth, int batchSize)

    • addCornerCaseEQOracle

      public void addCornerCaseEQOracle(int length, int minStep)
      Add a corner case equivalence oracle.

      This oracle tries the corner case input, i.e., the inputs with the same values

      Parameters:
      length - The length of the input.
      minStep - The minimum step of the corner case.

    • setTimeout

      public void setTimeout(long timeout)
      Set timeout to the equivalence oracle added next time.
      Parameters:
      timeout - timeout in seconds.

    • addHillClimbingEQOracle

      public void addHillClimbingEQOracle(TemporalLogic.STLCost costFunc, int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord)

    • addHillClimbingEQOracle

      public void addHillClimbingEQOracle(Function<IOSignal<List<Double>>,Double> costFunc, int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord, de.learnlib.oracle.PropertyOracle.MealyPropertyOracle<String,String,String> ltlOracle)

      addHillClimbingEQOracle.

      Parameters:
      costFunc - a Function object.
      length - a int.
      random - a Random object.
      maxTests - a int.
      generationSize - a int.
      childrenSize - a int.
      resetWord - a boolean.
      ltlOracle - a PropertyOracle.MealyPropertyOracle object.

    • addHillClimbingEQOracleAll

      public void addHillClimbingEQOracleAll(int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord)

    • addSAEQOracle

      public void addSAEQOracle(Function<IOSignal<List<Double>>,Double> costFunc, int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord, double alpha, de.learnlib.oracle.PropertyOracle.MealyPropertyOracle<String,String,String> ltlOracle)

      addSAEQOracle.

      Parameters:
      costFunc - a Function object.
      length - a int.
      random - a Random object.
      maxTests - a int.
      generationSize - a int.
      childrenSize - a int.
      resetWord - a boolean.
      alpha - a double.
      ltlOracle - a PropertyOracle.MealyPropertyOracle object.

    • addMutateSelectEQOracle

      void addMutateSelectEQOracle(Function<IOSignal<List<Double>>,Double> costFunc, int length, Random random, int maxTests, int generationSize, int childrenSize, int changeSize, boolean resetWord)

    • addGAEQOracle

      public void addGAEQOracle(Function<IOSignal<List<Double>>,Double> costFunc, int length, int maxTests, ArgParser.GASelectionKind selectionKind, int generationSize, double crossoverProb, double mutationProbability, de.learnlib.oracle.PropertyOracle.MealyPropertyOracle<String,String,String> ltlOracle)
      add a Genetic algorithm-based equivalence oracle
      Parameters:
      costFunc - The cost function assigning a Double to each OutputSignal. This is typically an STL formula.
      length - length of the generated signals
      maxTests - maximum test size
      selectionKind - kind of the selection method
      generationSize - size of each generation. This must be an even number.
      crossoverProb - probability to have crossover
      mutationProbability - probability to have mutation
      ltlOracle - the LTL formula

    • getCexAbstractInput

      public List<net.automatalib.word.Word<String>> getCexAbstractInput()

    • getCexConcreteInput

      public List<Signal> getCexConcreteInput()

    • getCexOutput

      public List<net.automatalib.word.Word<String>> getCexOutput()

    • run

      public boolean run()

      run.

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

    • writeDOTCex

      public void writeDOTCex(int index, Appendable a) throws IOException
      Wirte the DOT of the found counter example.
      Parameters:
      a - Write the DOT to a
      Throws:
      IOException - The exception by GraphDOT.write

    • writeDOTLearnedMealy

      public void writeDOTLearnedMealy(Appendable a) throws IOException
      Wirte the DOT of the learned Mealy machine
      Parameters:
      a - Write the DOT to a
      Throws:
      IOException - The exception by GraphDOT.write

    • writeETFLearnedMealy

      public void writeETFLearnedMealy(OutputStream os)
      Write the ETF of the learned Mealy machine.
      Parameters:
      os - Write the ETF to os

    • visualizeCex

      public void visualizeCex(int index)
      Visualize the found counter example.

    • visualizeLearnedMealy

      public void visualizeLearnedMealy()
      Visualize the learned Mealy machine

    • getSimulinkCount

      public int getSimulinkCount()
      Returns:
      the number of the Simulink executions

    • getSimulinkCountForEqTest

      public int getSimulinkCountForEqTest()

    • getProperties

      public AdaptiveSTLUpdater<List<Double>> getProperties()

    • addSAEQOracleAll

      public void addSAEQOracleAll(int length, Random random, int maxTest, int generationSize, int childrenSize, boolean resetWord, double alpha)

    • addGAEQOracleAll

      public void addGAEQOracleAll(int length, int maxTest, ArgParser.GASelectionKind selectionKind, int populationSize, double crossoverProb, double mutationProb)

    • close

      public void close() throws Exception
      Close the MATLAB engine. This method must be called when the object is no longer used.
      Throws:
      Exception

    • getSimulationTimeSecond

      public double getSimulationTimeSecond()