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,A,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. DetSuffixOutputAutomaton.computeOutput(Iterable) should return null when its argument is not accepted.

See Also:

ModelChecker

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 Type	Method	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.

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

Method Detail

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

void setSkipOutputs(Collection<? super O> skipOutputs)

Sets the outputs which should be skipped.

Parameters:

skipOutputs - the outputs.

See Also:

getSkipOutputs()