Package net.automatalib.modelchecking
Interface ModelChecker<I,A,P,R>
-
- Type Parameters:
I
- the input typeA
- the automaton typeP
- the property typeR
- the type of 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
,ADDSolver
,BDDSolver
,LTSminLTLAlternating
,LTSminLTLDFA
,LTSminLTLIO
,LTSminMonitorAlternating
,LTSminMonitorDFA
,LTSminMonitorIO
,SizeDFAModelCheckerCache
,SizeDFAModelCheckerLassoCache
,SizeMealyModelCheckerCache
,SizeMealyModelCheckerLassoCache
,StringADDSolver
,StringBDDSolver
,TypedADDSolver
,TypedBDDSolver
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.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
ModelChecker.DFAModelChecker<I,P,R>
static interface
ModelChecker.MealyModelChecker<I,O,P,R>
A model checker for Mealy machines.
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description @Nullable R
findCounterExample(A automaton, Collection<? extends I> inputs, P property)
Try to find counter examples for the givenproperty
andautomaton
.
-
-
-
Method Detail
-
findCounterExample
@Nullable R findCounterExample(A automaton, Collection<? extends I> inputs, P property)
Try to find counter examples for the givenproperty
andautomaton
.- 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.
-
-