de.learnlib.api.oracle

Interface AutomatonOracle<A extends net.automatalib.automata.DeterministicAutomaton<?,I,?>,I,D>

Type Parameters:

A - the automaton type

I - the input type

D - the output type

All Known Subinterfaces:

AutomatonOracle.DFAOracle<I>, AutomatonOracle.MealyOracle<I,O>

All Known Implementing Classes:

AbstractBFInclusionOracle, AbstractBFOracle, DFABFEmptinessOracle, DFABFInclusionOracle, MealyBFEmptinessOracle, MealyBFInclusionOracle

@ParametersAreNonnullByDefault
public interface AutomatonOracle<A extends net.automatalib.automata.DeterministicAutomaton<?,I,?>,I,D>

Finds counterexamples (to particular claims) to an hypothesis, while generating words that are in the given hypothesis.

Author:

Jeroen Meijer

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static interface	AutomatonOracle.DFAOracle<I>
static interface	AutomatonOracle.MealyOracle<I,O>

Method Summary

Modifier and Type	Method and Description
boolean	accepts(A hypothesis, Iterable<? extends I> input, int length) Returns whether the given input is accepted by the given hypothesis.
void	addWord(net.automatalib.words.Word<I> input) Add a new input word.
default void	addWords(A hypothesis, Collection<? extends I> inputs, net.automatalib.words.Word<I> prefix) Adds words to a datastructure.
default DefaultQuery<I,D>	findCounterExample(A hypothesis, Collection<? extends I> inputs) Finds a counter example to the given hypothesis.
default DefaultQuery<I,D>	findCounterExample(A hypothesis, Collection<? extends I> inputs, int maxQueries) Find a counterexample for a given hypothesis.
double	getMultiplier() Returns the multiplier used to compute the number of queries this automaton oracle should perform to decide whether a given hypothesis is a counter example.
boolean	isCounterExample(A hypothesis, Iterable<? extends I> inputs, D output) Returns whether the given input and output is a counter example for the given hypothesis.
net.automatalib.words.Word<I>	nextInput() Returns the next input word, or null if there is no next input.
void	pre() Setup method which is called immediately before findCounterExample(DeterministicAutomaton, Collection, int) is called.
DefaultQuery<I,D>	processInput(A hypothesis, net.automatalib.words.Word<I> input) Processes the given input.
void	setMultiplier(double multiplier)

Method Detail

isCounterExample

boolean isCounterExample(A hypothesis,
                         Iterable<? extends I> inputs,
                         @Nullable
                         D output)

Returns whether the given input and output is a counter example for the given hypothesis.

Parameters:

hypothesis - the hypothesis

inputs - the input sequence

output - the output corresponding to the input.

Returns:

whether the given input and output is a counter example.

nextInput

@Nullable
net.automatalib.words.Word<I> nextInput()

Returns the next input word, or null if there is no next input.

Implementations could for example return words in a breadth-first, or depth-first manner.

Returns:

the next input word, or null if t here is no next input.

addWord

void addWord(net.automatalib.words.Word<I> input)

Add a new input word.

Implementations could add words to e.g. a Stack, or Queue.

Parameters:

input - the input word to add.

pre

void pre()

Setup method which is called immediately before findCounterExample(DeterministicAutomaton, Collection, int) is called.

getMultiplier

double getMultiplier()

Returns the multiplier used to compute the number of queries this automaton oracle should perform to decide whether a given hypothesis is a counter example.

Returns:

the multiplier

setMultiplier

void setMultiplier(double multiplier)

Parameters:

multiplier - the multiplier

See Also:

getMultiplier()

processInput

DefaultQuery<I,D> processInput(A hypothesis,
                               net.automatalib.words.Word<I> input)

Processes the given input. Implementations could use membership oracles to process the query.

Parameters:

hypothesis - the hypothesis.

input - the input to process.

Returns:

the processed query.

addWords

default void addWords(A hypothesis,
                      Collection<? extends I> inputs,
                      net.automatalib.words.Word<I> prefix)

Adds words to a datastructure. The key part of the implementation is that undefined inputs will be skipped.

Parameters:

hypothesis - the automaton to add words for.

inputs - the input alphabet.

prefix - the current prefix to extend.

accepts

boolean accepts(A hypothesis,
                Iterable<? extends I> input,
                int length)

Returns whether the given input is accepted by the given hypothesis.

Parameters:

hypothesis - the hypothesis automaton.

input - the input.

length - the length of the input.

Returns:

whether the given input is accepted.

findCounterExample

@Nullable
default DefaultQuery<I,D> findCounterExample(A hypothesis,
                                                       Collection<? extends I> inputs,
                                                       int maxQueries)

Find a counterexample for a given hypothesis.

Parameters:

hypothesis - the hypothesis to find a counter example to.

inputs - the alphabet.

maxQueries - the maximum number of queries.

Returns:

the counterexample, or null if a counter example does not exist.

findCounterExample

@Nullable
default DefaultQuery<I,D> findCounterExample(A hypothesis,
                                                       Collection<? extends I> inputs)

Finds a counter example to the given hypothesis. By default the maximum number of queries performed are hypothesis.size() * getMultiplier().

Parameters:

hypothesis - the hypothesis automaton.

inputs - the input alphabet.

Returns:

the counter example, or null if a counter example does not exist