Package de.learnlib.oracle.property
Class MealyFinitePropertyOracle<I,O,P>
- java.lang.Object
-
- de.learnlib.oracle.property.MealyFinitePropertyOracle<I,O,P>
-
- Type Parameters:
I
- the input typeO
- the output typeP
- the property type
- All Implemented Interfaces:
EquivalenceOracle<MealyMachine<?,I,?,O>,I,Word<O>>
,EquivalenceOracle.MealyEquivalenceOracle<I,O>
,InclusionOracle<MealyMachine<?,I,?,O>,I,Word<O>>
,InclusionOracle.MealyInclusionOracle<I,O>
,PropertyOracle<I,MealyMachine<?,I,?,O>,P,Word<O>>
,PropertyOracle.MealyPropertyOracle<I,O,P>
public class MealyFinitePropertyOracle<I,O,P> extends Object implements PropertyOracle.MealyPropertyOracle<I,O,P>
A property oracle for Mealy Machines where it is fine to only check finite words from the model checker.
-
-
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 MealyFinitePropertyOracle(P property, InclusionOracle.MealyInclusionOracle<I,O> inclusionOracle, EmptinessOracle.MealyEmptinessOracle<I,O> emptinessOracle, ModelChecker.MealyModelChecker<I,O,P,MealyMachine<?,I,?,O>> modelChecker)
-
Method Summary
All Methods Instance Methods Concrete 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.@Nullable DefaultQuery<I,D>
getCounterExample()
Returns the counterexample for the property ifPropertyOracle.isDisproved()
,null
otherwise.P
getProperty()
Returns the property.protected MealyMachine<?,I,?,O>
modelCheck(MealyMachine<?,I,?,O> hypothesis, Collection<? extends I> inputs)
protected @Nullable DefaultQuery<I,D>
setCounterExample(@Nullable DefaultQuery<I,D> counterExample)
void
setProperty(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
disprove, doFindCounterExample, findCounterExample, getCounterExample, getProperty, isDisproved, setProperty
-
-
-
-
Constructor Detail
-
MealyFinitePropertyOracle
public MealyFinitePropertyOracle(P property, InclusionOracle.MealyInclusionOracle<I,O> inclusionOracle, EmptinessOracle.MealyEmptinessOracle<I,O> emptinessOracle, ModelChecker.MealyModelChecker<I,O,P,MealyMachine<?,I,?,O>> modelChecker)
-
-
Method Detail
-
modelCheck
protected MealyMachine<?,I,?,O> modelCheck(MealyMachine<?,I,?,O> hypothesis, Collection<? extends I> inputs)
-
setCounterExample
protected @Nullable DefaultQuery<I,D> setCounterExample(@Nullable DefaultQuery<I,D> counterExample)
-
setProperty
public void setProperty(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.
-
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.
-
-