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:
  • 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

      void setSkipOutputs(Collection<? super O> skipOutputs)
      Sets the outputs which should be skipped.
      Parameters:
      skipOutputs - the outputs.
      See Also: