Module de.learnlib.oracle.property

Package de.learnlib.oracle.property

Class MealyLassoPropertyOracle<I,O,P>

java.lang.Object

de.learnlib.oracle.property.MealyLassoPropertyOracle<I,O,P>

Type Parameters:

I - the input type

O - the output type

P - the property type

All Implemented Interfaces:

EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,I,?,O>,I,net.automatalib.word.Word<O>>, EquivalenceOracle.MealyEquivalenceOracle<I,O>, InclusionOracle<net.automatalib.automaton.transducer.MealyMachine<?,I,?,O>,I,net.automatalib.word.Word<O>>, InclusionOracle.MealyInclusionOracle<I,O>, PropertyOracle<I,net.automatalib.automaton.transducer.MealyMachine<?,I,?,O>,P,net.automatalib.word.Word<O>>, PropertyOracle.MealyPropertyOracle<I,O,P>

public class MealyLassoPropertyOracle<I,O,P>
extends Object
implements PropertyOracle.MealyPropertyOracle<I,O,P>

A property oracle for Mealy machines that can check lassos 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
MealyLassoPropertyOracle(P property, InclusionOracle.MealyInclusionOracle<I,O> inclusionOracle, LassoEmptinessOracle.MealyLassoEmptinessOracle<I,O> emptinessOracle, net.automatalib.modelchecking.ModelCheckerLasso.MealyModelCheckerLasso<I,O,P> modelChecker)

Method Summary

Modifier and Type	Method	Description
@Nullable DefaultQuery<I,D>	disprove(A hypothesis, Collection<? extends I> inputs)	Try to disprove the property with the given hypothesis.
@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 if PropertyOracle.isDisproved(), null otherwise.
P	getProperty()	Returns the property.
protected @Nullable net.automatalib.modelchecking.Lasso.MealyLasso<I,O>	modelCheck(net.automatalib.automaton.transducer.MealyMachine<?,I,?,O> hypothesis, Collection<? extends I> inputs)
protected @Nullable DefaultQuery<I,D>	setCounterExample(@Nullable DefaultQuery<I,D> counterExample)

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

Constructor Detail

MealyLassoPropertyOracle

public MealyLassoPropertyOracle(P property,
                                InclusionOracle.MealyInclusionOracle<I,O> inclusionOracle,
                                LassoEmptinessOracle.MealyLassoEmptinessOracle<I,O> emptinessOracle,
                                net.automatalib.modelchecking.ModelCheckerLasso.MealyModelCheckerLasso<I,O,P> modelChecker)

Method Detail

modelCheck

protected @Nullable net.automatalib.modelchecking.Lasso.MealyLasso<I,O> modelCheck(net.automatalib.automaton.transducer.MealyMachine<?,I,?,O> hypothesis,
                                                                                         Collection<? extends I> inputs)

setCounterExample

protected @Nullable DefaultQuery<I,D> setCounterExample(@Nullable DefaultQuery<I,D> counterExample)

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.

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 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)

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 given hypothesis.

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.