Package de.learnlib.oracle.property

Class LoggingPropertyOracle<I,A extends 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 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.
void	setProperty(P property)	Set the property.
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 Output<I,D>,P,D>

Returns:

whether the property is disproved.

setProperty

public void setProperty(P property)

Description copied from interface: PropertyOracle

Set the property.

Specified by:

setProperty in interface PropertyOracle<I,A extends Output<I,D>,P,D>

Parameters:

property - the property to set.

getProperty

public P getProperty()

Description copied from interface: PropertyOracle

Returns the property.

Specified by:

getProperty in interface PropertyOracle<I,A extends 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 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 Output<I,D>,P,D>

Parameters:

hypothesis - the hypothesis.

inputs - the inputs

Returns:

the DefaultQuery that is a counterexample 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 Output<I,D>,P,D>

See Also:

PropertyOracle.findCounterExample(Output, Collection)

toString

public String toString()

Overrides:

toString in class Object