Package de.learnlib.oracle.equivalence

Class CExFirstOracle<A extends Output<I,​D>,​I,​D>

  • Type Parameters:
    A - the automaton type
    I - the input type
    D - the output type
    All Implemented Interfaces:
    BlackBoxOracle<A,​I,​D>, EquivalenceOracle<A,​I,​D>, InclusionOracle<A,​I,​D>
    Direct Known Subclasses:
    DFACExFirstOracle, MealyCExFirstOracle
    public class CExFirstOracle<A extends Output<I,​D>,​I,​D>
extends Object
implements BlackBoxOracle<A,​I,​D>
    The strategy of this black-box oracle is to first try out a property, to see if it can be disproved. If it can not be disproved it tries the same property to find a counter example to the hypothesis, before continuing with the next property.

    This implementation may be used when refining a hypothesis is inexpensive compared to disproving propertyOracles.

    See Also:
    DisproveFirstOracle

    • Constructor Detail

      • CExFirstOracle

        public CExFirstOracle()

      • CExFirstOracle

        public CExFirstOracle​(PropertyOracle<I,​? super A,​?,​D> propertyOracle)

    • Method Detail

      • findCounterExample

        public @Nullable DefaultQuery<I,​D> findCounterExample​(A hypothesis,
                                                            Collection<? extends I> inputs)
        Description copied from interface: EquivalenceOracle
        Searches for a counterexample disproving the subjected hypothesis. A counterexample is query which, when performed on the SUL, yields a different output than what was predicted by the hypothesis. If no counterexample could be found (this does not necessarily mean that none exists), null is returned.
        Specified by:
        findCounterExample in interface EquivalenceOracle<A extends Output<I,​D>,​I,​D>
        Parameters:
        hypothesis - the conjecture
        inputs - the set of inputs to consider, this should be a subset of the input alphabet of the provided hypothesis
        Returns:
        a query exposing different behavior, or null if no counterexample could be found. In case a non-null value is returned, the output field in the DefaultQuery contains the SUL output for the respective query.