Package net.automatalib.modelchecking

Class SizeDFAModelCheckerCache<I,P,R>

java.lang.Object

net.automatalib.modelchecking.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 from 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.ModelChecker

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

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

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

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	Description
void	clear()	Clears the cache.
@Nullable 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.ModelChecker

findCounterExample

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerCache

clear

Constructor Detail

SizeDFAModelCheckerCache

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

Method Detail

findCounterExample

public @Nullable 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>