net.automatalib.modelchecking.modelchecker.cache

Class SizeDFAModelCheckerLassoCache<I,P>

java.lang.Object

net.automatalib.modelchecking.modelchecker.cache.SizeDFAModelCheckerLassoCache<I,P>

All Implemented Interfaces:

ModelChecker<I,DFA<?,I>,P,Lasso.DFALasso<I>>, InternalModelCheckerDelegator.ModelCheckerLassoDelegator<ModelCheckerLasso.DFAModelCheckerLasso<I,P>,I,DFA<?,I>,P,Lasso.DFALasso<I>>, ModelChecker.DFAModelChecker<I,P,Lasso.DFALasso<I>>, ModelCheckerCache<I,DFA<?,I>,P,Lasso.DFALasso<I>>, ModelCheckerCache.DFAModelCheckerCache<I,P,Lasso.DFALasso<I>>, ModelCheckerLasso<I,DFA<?,I>,P,Lasso.DFALasso<I>>, ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLassoCache<I,DFA<?,I>,P,Lasso.DFALasso<I>>, ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>

public class SizeDFAModelCheckerLassoCache<I,P>
extends Object
implements ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>, InternalModelCheckerDelegator.ModelCheckerLassoDelegator<ModelCheckerLasso.DFAModelCheckerLasso<I,P>,I,DFA<?,I>,P,Lasso.DFALasso<I>>

See Also:

SizeDFAModelCheckerCache

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	InternalModelCheckerDelegator.MealyModelCheckerDelegator<MC extends ModelChecker.MealyModelChecker<I,O,P,R>,I,O,P,R> Specialization of InternalModelCheckerDelegator.
static interface	InternalModelCheckerDelegator.MealyModelCheckerLassoDelegator<MC extends ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>,I,O,P> Specialization of InternalModelCheckerDelegator.
static interface	InternalModelCheckerDelegator.ModelCheckerLassoDelegator<MC extends ModelCheckerLasso<I,A,P,R>,I,A,P,R extends Lasso<I,?>> Specialization of InternalModelCheckerDelegator.

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLassoCache

ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>, ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerCache

ModelCheckerCache.DFAModelCheckerCache<I,P,R>, ModelCheckerCache.MealyModelCheckerCache<I,O,P,R>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker

ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>

Constructor Summary

Constructors

Constructor and Description
SizeDFAModelCheckerLassoCache(ModelCheckerLasso.DFAModelCheckerLasso<I,P> modelChecker)

Method Summary

Modifier and Type	Method and Description
void	clear() Clears the cache.
R	findCounterExample(A automaton, Collection<? extends I> inputs, P property) The cached implementation for finding counter examples.
ModelCheckerLasso.DFAModelCheckerLasso<I,P>	getModelChecker()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerCache

clear

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

Methods inherited from interface net.automatalib.modelchecking.modelchecker.cache.InternalModelCheckerDelegator.ModelCheckerLassoDelegator

getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Constructor Detail

SizeDFAModelCheckerLassoCache

public SizeDFAModelCheckerLassoCache(ModelCheckerLasso.DFAModelCheckerLasso<I,P> modelChecker)

Method Detail

getModelChecker

public ModelCheckerLasso.DFAModelCheckerLasso<I,P> getModelChecker()

findCounterExample

@Nullable
public R findCounterExample(A automaton,
                                      Collection<? extends I> inputs,
                                      P property)

The cached implementation for finding counter examples.

Specified by:

findCounterExample in interface ModelChecker<I,A extends SimpleAutomaton<?,I>,P,R>

Parameters:

automaton - the automaton to check the property on.

inputs - the alphabet.

property - the property.

Returns:

the counter examples, or null if no counter examples exist.

See Also:

ModelChecker.findCounterExample(Object, Collection, Object)

clear

public void clear()

Description copied from interface: ModelCheckerCache

Clears the cache.

Specified by:

clear in interface ModelCheckerCache<I,A extends SimpleAutomaton<?,I>,P,R>