net.automatalib.modelchecking

Interface ModelChecker<I,A,P,R>

Type Parameters:

I - the input type

A - the automaton type

P - the property type

R - the type of a counterexample

All Known Subinterfaces:

LTSmin<I,A,R>, LTSminAlternating<I,O,R>, LTSminDFA<I,R>, LTSminIO<I,O,R>, LTSminMealy<I,O,R>, ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>, ModelCheckerCache<I,A,P,R>, ModelCheckerCache.DFAModelCheckerCache<I,P,R>, ModelCheckerCache.MealyModelCheckerCache<I,O,P,R>, ModelCheckerLasso<I,A,P,R>, ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>, ModelCheckerLassoCache<I,A,P,R>, ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>, ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>

All Known Implementing Classes:

AbstractLTSmin, AbstractLTSminLTL, AbstractLTSminLTLMealy, AbstractLTSminMonitor, AbstractLTSminMonitorMealy, AbstractUnfoldingModelChecker, LTSminLTLAlternating, LTSminLTLDFA, LTSminLTLIO, LTSminMonitorAlternating, LTSminMonitorDFA, LTSminMonitorIO, SizeDFAModelCheckerCache, SizeDFAModelCheckerLassoCache, SizeMealyModelCheckerCache, SizeMealyModelCheckerLassoCache

public interface ModelChecker<I,A,P,R>

A model checker checks whether a given automaton satisfies a given property. If the property can not be satisfied it provides counter examples. In fact, the counter examples is an automaton which language is a subset of the language of the given automaton.

Author:

Jeroen Meijer

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static interface	ModelChecker.DFAModelChecker<I,P,R>
static interface	ModelChecker.MealyModelChecker<I,O,P,R> A model checker for Mealy machines.

Method Summary

Modifier and Type	Method and Description
R	findCounterExample(A automaton, Collection<? extends I> inputs, P property) Try to find counter examples for the given property and automaton.

Method Detail

findCounterExample

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

Try to find counter examples for the given property and automaton.

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.

Throws:

ModelCheckingException - when this model checker can not check the property.