Package de.learnlib.oracle
Interface PropertyOracle<I,A extends Output<I,D>,P,D>
-
- Type Parameters:
I
- the input typeA
- the automaton typeP
- the property typeD
- the output type
- All Superinterfaces:
EquivalenceOracle<A,I,D>
,InclusionOracle<A,I,D>
- All Known Subinterfaces:
PropertyOracle.DFAPropertyOracle<I,P>
,PropertyOracle.MealyPropertyOracle<I,O,P>
- All Known Implementing Classes:
DFAFinitePropertyOracle
,DFALassoPropertyOracle
,DFAPropertyOracleChain
,LoggingPropertyOracle
,LoggingPropertyOracle.DFALoggingPropertyOracle
,LoggingPropertyOracle.MealyLoggingPropertyOracle
,MealyFinitePropertyOracle
,MealyLassoPropertyOracle
,MealyPropertyOracleChain
,PropertyOracleChain
public interface PropertyOracle<I,A extends Output<I,D>,P,D> extends InclusionOracle<A,I,D>
APropertyOracle
can disprove a property, and used to find a counter example to a hypothesis.Note that a property oracle is also an
InclusionOracle
and thus anEquivalenceOracle
, hence it can be use used to find counterexamples to hypotheses.An implementation should keep track of whether the property is already disproved.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
PropertyOracle.DFAPropertyOracle<I,P>
static interface
PropertyOracle.MealyPropertyOracle<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>
-
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description @Nullable DefaultQuery<I,D>
disprove(A hypothesis, Collection<? extends I> inputs)
Try to disprove the property with the givenhypothesis
.@Nullable DefaultQuery<I,D>
doFindCounterExample(A hypothesis, Collection<? extends I> inputs)
Unconditionally find a counterexample, i.e. regardless of whether the property can be disproved.default @Nullable DefaultQuery<I,D>
findCounterExample(A hypothesis, Collection<? extends I> inputs)
Try to find a counterexample to the givenhypothesis
if the property can not be disproved.@Nullable DefaultQuery<I,D>
getCounterExample()
Returns the counterexample for the property ifisDisproved()
,null
otherwise.P
getProperty()
Returns the property.default boolean
isDisproved()
Returns whether the property is disproved.void
setProperty(P property)
Set the property.-
Methods inherited from interface de.learnlib.oracle.InclusionOracle
isCounterExample
-
-
-
-
Method Detail
-
isDisproved
default boolean isDisproved()
Returns whether the property is disproved.- Returns:
- whether the property is disproved.
-
setProperty
void setProperty(P property)
Set the property.- Parameters:
property
- the property to set.
-
getProperty
@Pure P getProperty()
Returns the property.- Returns:
- the property.
-
getCounterExample
@Nullable DefaultQuery<I,D> getCounterExample()
Returns the counterexample for the property ifisDisproved()
,null
otherwise.If this method does not return
null
, a previous call todisprove(Output, Collection)
must have returned aDefaultQuery
.- Returns:
- the counterexample for the property if
isDisproved()
,null
otherwise.
-
disprove
@Nullable DefaultQuery<I,D> disprove(A hypothesis, Collection<? extends I> inputs)
Try to disprove the property with the givenhypothesis
.- Parameters:
hypothesis
- the hypothesis.inputs
- the inputs- Returns:
- the
DefaultQuery
that is a counterexample the property, ornull
, if the property could not be disproved.
-
findCounterExample
default @Nullable DefaultQuery<I,D> findCounterExample(A hypothesis, Collection<? extends I> inputs)
Try to find a counterexample to the givenhypothesis
if the property can not be disproved.- Specified by:
findCounterExample
in interfaceEquivalenceOracle<I,A extends Output<I,D>,P>
- Parameters:
hypothesis
- the hypothesis to find a counterexample to.inputs
- the input alphabet.- Returns:
- the
DefaultQuery
that is a counterexample to the givenhypothesis
, ornull
, a counterexample could not be found or the property could be disproved.
-
doFindCounterExample
@Nullable DefaultQuery<I,D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs)
Unconditionally find a counterexample, i.e. regardless of whether the property can be disproved. In fact,disprove(Output, Collection)
is not even be called.- See Also:
findCounterExample(Output, Collection)
-
-