Module net.automatalib.api
Package net.automatalib.modelchecking
Interface ModelChecker.MealyModelChecker<I,O,P,R>
- All Superinterfaces:
ModelChecker<I,MealyMachine<?, I, ?, O>, P, R>
- All Known Subinterfaces:
LTSminAlternating<I,,O, R> LTSminIO<I,,O, R> LTSminMealy<I,,O, R> ModelCheckerCache.MealyModelCheckerCache<I,,O, P, R> ModelCheckerLasso.MealyModelCheckerLasso<I,,O, P> ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O, P>
- All Known Implementing Classes:
AbstractLTSminLTLMealy,AbstractLTSminMonitorMealy,LTSminLTLAlternating,LTSminLTLIO,LTSminMonitorAlternating,LTSminMonitorIO,SizeMealyModelCheckerCache,SizeMealyModelCheckerLassoCache
- Enclosing interface:
- ModelChecker<I,
M, P, R>
public static interface ModelChecker.MealyModelChecker<I,O,P,R>
extends ModelChecker<I,MealyMachine<?,I,?,O>,P,R>
A model checker for Mealy machines. Key about the
MealyMachine type here is that it may not be
input-complete. Implementations of MealyMachines should in these cases not return any output for a given
input sequence, i.e., Output.computeOutput(Iterable) should return null when its argument
is not accepted.- See Also:
-
Nested Class Summary
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker
ModelChecker.DFAModelChecker<I,P, R>, ModelChecker.MealyModelChecker<I, O, P, R> -
Method Summary
Modifier and TypeMethodDescriptionCollection<? super O>Returns the outputs for which all transitions should be removed.voidsetSkipOutputs(Collection<? super O> skipOutputs) Sets the outputs which should be skipped.Methods inherited from interface net.automatalib.modelchecking.ModelChecker
findCounterExample
-
Method Details
-
getSkipOutputs
Collection<? super O> getSkipOutputs()Returns the outputs for which all transitions should be removed.That is, before the model checker tries to find a counter example to the automaton every transition which output symbol is in the returned collection is removed.
- Returns:
- the outputs.
-
setSkipOutputs
Sets the outputs which should be skipped.- Parameters:
skipOutputs- the outputs.- See Also:
-