net.automatalib.modelchecking.modelchecker.cache

Class SizeDFAModelCheckerCache<I,P,R>

java.lang.Object

net.automatalib.modelchecking.modelchecker.cache.SizeDFAModelCheckerCache<I,P,R>

Type Parameters:

I - the input type

P - the property type

All Implemented Interfaces:

ModelChecker<I,DFA<?,I>,P,R>, ModelChecker.DFAModelChecker<I,P,R>, ModelCheckerCache<I,DFA<?,I>,P,R>, ModelCheckerCache.DFAModelCheckerCache<I,P,R>

public class SizeDFAModelCheckerCache<I,P,R>
extends Object
implements ModelCheckerCache.DFAModelCheckerCache<I,P,R>

A DFAModelCheckerCache that invalidates the cached counter examples when ModelChecker.findCounterExample(Object, Collection, Object) is called with a DFA with a size different, and an input alphabet different than the previous call.

In active learning the automaton increases in size with every proper counter example. Hence these caches are useful in between calls to disproving properties and finding counter examples to hypotheses.

Nested Class Summary

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.ModelChecker

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

Constructor Summary

Constructors

Constructor and Description
SizeDFAModelCheckerCache(ModelChecker.DFAModelChecker<I,P,R> 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.

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.ModelChecker

findCounterExample

Constructor Detail

SizeDFAModelCheckerCache

public SizeDFAModelCheckerCache(ModelChecker.DFAModelChecker<I,P,R> modelChecker)

Method Detail

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>