Package de.learnlib.oracle

Interface AutomatonOracle<A extends 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

public interface AutomatonOracle<A extends DeterministicAutomaton<?,I,?>,I,D>

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

Nested Class Summary

Nested Classes

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

Method Summary

Modifier and Type	Method	Description
boolean	accepts(A hypothesis, Iterable<? extends I> input)	Returns whether the given input is accepted by the given hypothesis.
void	addWord(Word<I> input)	Add a new input word.
default void	addWords(A hypothesis, Collection<? extends I> inputs, Word<I> prefix)	Adds words to a datastructure.
default @Nullable DefaultQuery<I,D>	findCounterExample(A hypothesis, Collection<? extends I> inputs)	Finds a counter example to the given hypothesis.
default @Nullable 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.
@Nullable 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, Word<I> input)	Processes the given input.
void	setMultiplier(double multiplier)

Method Detail

isCounterExample

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.

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 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 there is no next input.

addWord

void addWord(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,
                                     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,
                      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)

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

Parameters:

hypothesis - the hypothesis automaton.

input - the input.

Returns:

whether the given input is accepted.

findCounterExample

default @Nullable 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

default @Nullable 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