Package de.learnlib.oracle.property
Class PropertyOracleChain<I,A extends Output<I,D>,P,D>
- java.lang.Object
-
- de.learnlib.oracle.property.PropertyOracleChain<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:
DFAPropertyOracleChain
,MealyPropertyOracleChain
public class PropertyOracleChain<I,A extends Output<I,D>,@Nullable P,D> extends Object implements PropertyOracle<I,A,P,D>
A chain of property oracles. Useful when combining multiple model checking strategies to disprove a property, or when finding counter examples to hypotheses.For example, you may want to construct a chain that first uses a model checker for monitors, and next, one that uses a model checker for full LTL. This strategy tends to give shorter counter examples for properties, and these counter examples can be found more quickly (as in smaller hypothesis size and less learning queries).
-
-
Nested Class Summary
-
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 PropertyOracleChain(PropertyOracle<I,? super A,@Nullable P,D>... oracles)
PropertyOracleChain(Collection<? extends PropertyOracle<I,? super A,@Nullable P,D>> oracles)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
addOracle(PropertyOracle<I,? super A,@Nullable P,D> oracle)
@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.@Nullable DefaultQuery<I,D>
getCounterExample()
Returns the counterexample for the property ifPropertyOracle.isDisproved()
,null
otherwise.P
getProperty()
Returns the property.void
setProperty(@Nullable P property)
Set the property.-
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
-
Methods inherited from interface de.learnlib.oracle.InclusionOracle
isCounterExample
-
Methods inherited from interface de.learnlib.oracle.PropertyOracle
findCounterExample, isDisproved
-
-
-
-
Constructor Detail
-
PropertyOracleChain
@SafeVarargs public PropertyOracleChain(PropertyOracle<I,? super A,@Nullable P,D>... oracles)
-
PropertyOracleChain
public PropertyOracleChain(Collection<? extends PropertyOracle<I,? super A,@Nullable P,D>> oracles)
-
-
Method Detail
-
addOracle
public void addOracle(PropertyOracle<I,? super A,@Nullable P,D> oracle)
-
doFindCounterExample
public @Nullable DefaultQuery<I,D> doFindCounterExample(A hypothesis, Collection<? extends I> inputs)
Description copied from interface:PropertyOracle
Unconditionally find a counterexample, i.e. regardless of whether the property can be disproved. In fact,PropertyOracle.disprove(Output, Collection)
is not even be called.- Specified by:
doFindCounterExample
in interfacePropertyOracle<I,A extends Output<I,D>,P,D>
- See Also:
PropertyOracle.findCounterExample(Output, Collection)
-
disprove
public @Nullable DefaultQuery<I,D> disprove(A hypothesis, Collection<? extends I> inputs)
Description copied from interface:PropertyOracle
Try to disprove the property with the givenhypothesis
.- Specified by:
disprove
in interfacePropertyOracle<I,A extends Output<I,D>,P,D>
- Parameters:
hypothesis
- the hypothesis.inputs
- the inputs- Returns:
- the
DefaultQuery
that is a counterexample the property, ornull
, if the property could not be disproved.
-
setProperty
public void setProperty(@Nullable P property)
Description copied from interface:PropertyOracle
Set the property.- Specified by:
setProperty
in interfacePropertyOracle<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 interfacePropertyOracle<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 ifPropertyOracle.isDisproved()
,null
otherwise.If this method does not return
null
, a previous call toPropertyOracle.disprove(Output, Collection)
must have returned aDefaultQuery
.- Specified by:
getCounterExample
in interfacePropertyOracle<I,A extends Output<I,D>,P,D>
- Returns:
- the counterexample for the property if
PropertyOracle.isDisproved()
,null
otherwise.
-
-