Module de.learnlib.oracle.property

Package de.learnlib.oracle.property

Class LoggingPropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

java.lang.Object

de.learnlib.oracle.property.LoggingPropertyOracle<I,A,P,D>

Type Parameters:

I - the input type

A - the automaton type

P - the property type

D - the output type

All Implemented Interfaces:

EquivalenceOracle<A,I,D>, InclusionOracle<A,I,D>, PropertyOracle<I,A,P,D>

Direct Known Subclasses:

LoggingPropertyOracle.DFALoggingPropertyOracle, LoggingPropertyOracle.MealyLoggingPropertyOracle

public class LoggingPropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>
extends Object
implements PropertyOracle<I,A,P,D>

A PropertyOracle that performs logging.

This class will log whenever the property is disproved, or when a counterexample to an automaton is found (i.e. a spurious counterexample is found).

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	LoggingPropertyOracle.DFALoggingPropertyOracle<I,P>
static class	LoggingPropertyOracle.MealyLoggingPropertyOracle<I,O,P>

Nested classes/interfaces inherited from interface de.learnlib.oracle.EquivalenceOracle

EquivalenceOracle.DFAEquivalenceOracle<I>, EquivalenceOracle.MealyEquivalenceOracle<I,O>, EquivalenceOracle.MooreEquivalenceOracle<I,O>

Nested classes/interfaces inherited from interface de.learnlib.oracle.InclusionOracle

InclusionOracle.DFAInclusionOracle<I>, InclusionOracle.MealyInclusionOracle<I,O>

Nested classes/interfaces inherited from interface de.learnlib.oracle.PropertyOracle

PropertyOracle.DFAPropertyOracle<I,P>, PropertyOracle.MealyPropertyOracle<I,O,P>

Constructor Summary

Constructors

Constructor	Description
LoggingPropertyOracle(PropertyOracle<I,A,P,D> propertyOracle)	Constructs a new LoggingPropertyOracle.

Method Summary

Modifier and Type	Method	Description
@Nullable DefaultQuery<I,D>	disprove(A hypothesis, Collection<? extends I> inputs)	Try to disprove this propertyOracle, and log whenever it is disproved.
@Nullable DefaultQuery<I,D>	doFindCounterExample(A hypothesis, Collection<? extends I> inputs)	Try to find a counterexample to the given hypothesis, and log whenever such a spurious counterexample is found.
@Nullable DefaultQuery<I,D>	getCounterExample()	Returns the counterexample for the property if PropertyOracle.isDisproved(), null otherwise.
P	getProperty()	Returns the property.
boolean	isDisproved()	Returns whether the property is disproved.
String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.learnlib.oracle.InclusionOracle

isCounterExample

Methods inherited from interface de.learnlib.oracle.PropertyOracle

findCounterExample

Constructor Detail

LoggingPropertyOracle

public LoggingPropertyOracle(PropertyOracle<I,A,P,D> propertyOracle)

Constructs a new LoggingPropertyOracle.

Parameters:

propertyOracle - the PropertyOracle to wrap around.

Method Detail

isDisproved

public boolean isDisproved()

Description copied from interface: PropertyOracle

Returns whether the property is disproved.

Specified by:

isDisproved in interface PropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

Returns:

whether the property is disproved.

getProperty

public P getProperty()

Description copied from interface: PropertyOracle

Returns the property.

Specified by:

getProperty in interface PropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

Returns:

the property.

getCounterExample

public @Nullable DefaultQuery<I,D> getCounterExample()

Description copied from interface: PropertyOracle

Returns the counterexample for the property if PropertyOracle.isDisproved(), null otherwise.

If this method does not return null, a previous call to PropertyOracle.disprove(Output, Collection) must have returned a DefaultQuery.

Specified by:

getCounterExample in interface PropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

Returns:

the counterexample for the property if PropertyOracle.isDisproved(), null otherwise.

disprove

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

Try to disprove this propertyOracle, and log whenever it is disproved.

Specified by:

disprove in interface PropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

Parameters:

hypothesis - the hypothesis

inputs - the inputs

Returns:

the DefaultQuery that is a counterexample to the property, or null, if the property could not be disproved.

See Also:

PropertyOracle.disprove(Output, Collection)

doFindCounterExample

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

Try to find a counterexample to the given hypothesis, and log whenever such a spurious counterexample is found.

Specified by:

doFindCounterExample in interface PropertyOracle<I,A extends net.automatalib.automaton.concept.Output<I,D>,P,D>

Parameters:

hypothesis - the hypothesis to find a counterexample to

inputs - the input symbols to consider for finding a counterexample

Returns:

a counterexample for the current hypothesis. May be null of none can be found

See Also:

PropertyOracle.findCounterExample(Output, Collection)

toString

public String toString()

Overrides:

toString in class Object