Package net.maswag.falcaun

Class AbstractSelectEQOracle

java.lang.Object
net.maswag.falcaun.AbstractSelectEQOracle
All Implemented Interfaces:
EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, EquivalenceOracle.MealyEquivalenceOracle<String,String>, EvaluationCountable, EvaluationCountable.MealyEquivalenceOracle<String,String>
Direct Known Subclasses:
HillClimbingEQOracle, MutateSelectEQOracle
public abstract class AbstractSelectEQOracle extends Object implements EquivalenceOracle.MealyEquivalenceOracle<String,String>, EvaluationCountable.MealyEquivalenceOracle<String,String>
Abstract class for implementing equivalence oracles that select test cases based on a cost function. This class serves as a foundational framework for generating and evaluating test cases aimed at finding counterexamples in Mealy machines. It is designed to be extended by specific implementations that define the logic for selecting test cases and evaluating their costs.
Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

    • LOGGER

      private static final org.slf4j.Logger LOGGER
      Logger instance for this class, used for logging debug and error information during the execution of the equivalence oracle.

    • random

      protected Random random
      Random number generator used for generating random test cases to ensure diversity in the test suite.

    • generationSize

      protected int generationSize
      The number of initial test cases generated to start the evaluation process. This parameter determines the diversity and coverage of the initial set of test cases.

    • childrenSize

      protected int childrenSize
      The number of child test cases generated from each successful (good) sample. This parameter controls the diversity and depth of the test case generation process.

    • symbolList

      protected List<? extends String> symbolList
      A list containing all possible input symbols that can be used in the test cases. This list defines the alphabet of inputs for the Mealy machine being tested.

    • memOracle

      protected NumericMembershipOracleCost memOracle
      The membership oracle responsible for evaluating the generated test cases against the Mealy machine. It provides the cost associated with each test case and determines whether it is a counterexample.

    • length

      private int length
      The length of each generated test word. This parameter defines how long each test case will be, affecting the complexity and coverage of the tests.

    • maxTests

      private int maxTests
      The maximum number of test cases to evaluate before terminating the search for counterexamples. This parameter prevents infinite loops and ensures that the process does not run indefinitely.

    • resetWord

      protected boolean resetWord
      A flag that indicates whether the word generation process should be reset. If set to true, it will clear and regenerate the initial set of test cases.

    • currentSamples

      private List<net.automatalib.word.Word<String>> currentSamples
      A list containing the current set of test cases that are being evaluated. This list is updated as new generations of test cases are generated and evaluated.

    • ltlOracle

      private PropertyOracle.MealyPropertyOracle<String,String,String> ltlOracle
      The property oracle responsible for checking whether a specific property (e.g., an LTL formula) is disproved by the generated test cases. If provided, it overrides the cost-based evaluation mechanism.

    • evaluateCount

      private int evaluateCount
      A counter that keeps track of the total number of test cases evaluated during the search process. This helps in monitoring the progress and performance of the equivalence oracle.

    • minCost

      private double minCost
      Minimum cost observed during the evaluation process.

  • Constructor Details

    • AbstractSelectEQOracle

      AbstractSelectEQOracle(NumericMembershipOracleCost memOracle, int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord)
      Constructs an instance of AbstractSelectEQOracle with the specified parameters. This constructor initializes the equivalence oracle without a property oracle, relying solely on the cost function provided by the membership oracle to evaluate test cases.
      Parameters:
      memOracle - The membership oracle used to evaluate test cases and provide costs.
      length - The length of each generated test word.
      random - Random number generator for generating diverse test cases.
      maxTests - Maximum number of test cases to evaluate before terminating the search process.
      generationSize - Size of the initial set of test cases generated at the start.
      childrenSize - Number of child test cases generated from each successful (good) sample.
      resetWord - Flag indicating whether to reset the word generation process, clearing and regenerating the initial set of test cases if true.

    • AbstractSelectEQOracle

      AbstractSelectEQOracle(NumericMembershipOracleCost memOracle, int length, Random random, int maxTests, int generationSize, int childrenSize, boolean resetWord, PropertyOracle.MealyPropertyOracle<String,String,String> ltlOracle)
      Constructs an instance of AbstractSelectEQOracle with the specified parameters, including a property oracle. This constructor initializes the equivalence oracle with both a membership oracle and a property oracle, allowing it to evaluate test cases based on both cost functions and specific properties (e.g., LTL formulas).
      Parameters:
      memOracle - The membership oracle used to evaluate test cases and provide costs.
      length - The length of each generated test word.
      random - Random number generator for generating diverse test cases.
      maxTests - Maximum number of test cases to evaluate before terminating the search process.
      generationSize - Size of the initial set of test cases generated at the start.
      childrenSize - Number of child test cases generated from each successful (good) sample.
      resetWord - Flag indicating whether to reset the word generation process, clearing and regenerating the initial set of test cases if true.
      ltlOracle - The property oracle used to check if a specific property is disproved by the generated test cases. If provided, it overrides the cost-based evaluation mechanism.

  • Method Details

    • resetSamples

      private void resetSamples()
      Resets the list of current samples by clearing it and generating a new set of random test words. This method is used to refresh the initial set of test cases when necessary.

    • isDisproved

      private boolean isDisproved()
      Checks if a property has been disproved by evaluating the minimum observed cost. If a property oracle is provided, it checks whether the property is disproved using the oracle; otherwise, it checks if the minimum observed cost is less than zero.
      Returns:
      true if the property is disproved, false otherwise.

    • findCounterExample

      @Nullable public @Nullable DefaultQuery<String,net.automatalib.word.Word<String>> findCounterExample(net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> hypothesis, Collection<? extends String> inputs)
      Finds a counterexample to the given hypothesis Mealy machine using the specified set of input symbols. This method generates and evaluates test cases to determine if there is any input that causes the hypothesis to produce an output different from the expected output.
      Specified by:
      findCounterExample in interface EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>
      Parameters:
      hypothesis - The Mealy machine hypothesis to be tested.
      inputs - A collection of possible input symbols for generating test cases.
      Returns:
      A DefaultQuery representing a counterexample if found, or null if no counterexample is discovered within the specified constraints.

    • generateTestWord

      private net.automatalib.word.Word<String> generateTestWord(List<? extends String> symbolList)
      Generates a random test word of the specified length using the provided list of possible input symbols. This method is used to create initial test cases for evaluation.
      Parameters:
      symbolList - A list containing all possible input symbols that can be used in the test cases.
      Returns:
      A randomly generated Word of the specified length.

    • createNextGeneration

      abstract List<net.automatalib.word.Word<String>> createNextGeneration(List<net.automatalib.word.Word<String>> goodSamples)
      Generates the next set of test cases based on the provided list of successful (good) samples. This method is responsible for creating new test cases that are derived from the current set of successful samples, ensuring a diverse and evolving set of test cases.
      Parameters:
      goodSamples - A list of successful test cases used as the basis for generating the next generation of test cases.
      Returns:
      A list of newly generated test cases for the next evaluation cycle.