Package net.automatalib.modelchecking
-
Interface Summary Interface Description Lasso<I,D> A lasso is a single infinite word.Lasso.DFALasso<I> A DFALasso is a lasso forDFA
s.Lasso.MealyLasso<I,O> A MealyLasso is a lasso forMealyMachine
s.ModelChecker<I,A,P,R> A model-checker checks whether a given automaton satisfies a given property.ModelChecker.DFAModelChecker<I,P,R> ModelChecker.MealyModelChecker<I,O,P,R> A model checker for Mealy machines.ModelCheckerCache<I,A,P,R> A model checker that caches calls toModelChecker.findCounterExample(Object, Collection, Object)
.ModelCheckerCache.DFAModelCheckerCache<I,P,R> ModelCheckerCache.MealyModelCheckerCache<I,O,P,R> ModelCheckerLasso<I,A,P,R extends Lasso<I,?>> A model checker where the counterexample is a lasso.ModelCheckerLasso.DFAModelCheckerLasso<I,P> ModelCheckerLasso.MealyModelCheckerLasso<I,O,P> ModelCheckerLassoCache<I,A,P,R extends Lasso<I,?>> ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P> ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P> -
Class Summary Class Description AbstractLasso<I,D> AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>> AnModelCheckerLasso
that can unfold loops of lassos.DFALassoImpl<I> A DFALasso is a lasso forDFA
s.MealyLassoImpl<I,O> A MealyLasso is a lasso forMealyMachine
s.SizeDFAModelCheckerCache<I,P,R> A DFAModelCheckerCache that invalidates the cached counter examples whenModelChecker.findCounterExample(Object, Collection, Object)
is called with a DFA with a size different, and an input alphabet different from the previous call.SizeDFAModelCheckerLassoCache<I,P> SizeMealyModelCheckerCache<I,O,P,R> SizeMealyModelCheckerLassoCache<I,O,P>