public static interface ModelChecker.MealyModelChecker<I,O,P,R> extends ModelChecker<I,MealyMachine<?,I,?,O>,P,R>
MealyMachine
type here is that it may not be
input-complete. Implementations of MealyMachine
s should in these cases not return any output for a given
input sequence. I.e. DetSuffixOutputAutomaton.computeOutput(Iterable)
should return null when its argument is not
accepted.ModelChecker
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Method and Description |
---|---|
Collection<? super O> |
getSkipOutputs()
Returns the outputs for which all transitions should be removed.
|
void |
setSkipOutputs(Collection<? super O> skipOutputs)
Sets the outputs which should be skipped.
|
findCounterExample
Collection<? super O> getSkipOutputs()
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.
void setSkipOutputs(Collection<? super O> skipOutputs)
skipOutputs
- the outputs.getSkipOutputs()
Copyright © 2019. All rights reserved.