Package net.maswag.falcaun

Class BlackBoxVerifier<I>

java.lang.Object
net.maswag.falcaun.BlackBoxVerifier<I>
Type Parameters:
I - Type of the input at each step.
public class BlackBoxVerifier<I> extends Object
Verifier of a black-box system with respect to the given properties.
Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

    • EDGE_PARSER

      private static final Function<String,String> EDGE_PARSER

    • memOracle

      de.learnlib.oracle.MembershipOracle.MealyMembershipOracle<String,String> memOracle

    • verifiedSystem

      private final de.learnlib.sul.SUL<String,String> verifiedSystem

    • learnedMealy

      private net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> learnedMealy

    • cexMealy

      private List<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> cexMealy

    • inputAlphabet

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

    • learner

      private final de.learnlib.algorithm.LearningAlgorithm.MealyLearner<String,String> learner

    • eqOracle

      private final de.learnlib.oracle.equivalence.MealyEQOracleChain<String,String> eqOracle

    • properties

      private final AdaptiveSTLUpdater<I> properties

    • cexInput

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

    • cexProperty

      private List<TemporalLogic<I>> cexProperty

    • cexOutput

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

    • modelChecker

      private final net.automatalib.modelchecking.ModelChecker.MealyModelChecker<String,String,String,net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> modelChecker

    • timeoutOracles

      private final List<TimeoutEQOracle<String,String>> timeoutOracles

    • timeout

      private Long timeout

  • Constructor Details

    • BlackBoxVerifier

      public BlackBoxVerifier(de.learnlib.oracle.MembershipOracle.MealyMembershipOracle<String,String> memOracle, de.learnlib.sul.SUL<String,String> verifiedSystem, AdaptiveSTLUpdater<I> properties, net.automatalib.alphabet.Alphabet<String> inputAlphabet)
      Parameters:
      memOracle - The membership oracle
      properties - The LTL properties to be verified. What we verify is the conjunction of the properties.
      inputAlphabet - The input alphabet.

  • Method Details

    • 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 EvaluationCountable.MealyEquivalenceOracle<String,String> 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.

    • addEqOracle

      public void addEqOracle(de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle<String,String> eqOracle)

    • setTimeout

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

    • run

      public boolean run()
      Returns:
      Returns true if and only if the given black-box system 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

    • visualizeCex

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

    • visualizeLearnedMealy

      public void visualizeLearnedMealy()
      Visualize the learned Mealy machine

    • writeETFLearnedMealy

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

    • processMealy

      private boolean processMealy()
      Set the counter example input/output.
      Returns:
      Returns true if and only if the black-box system is verified i.e., no counter example is found for any system.