I
- the input typeO
- the output typepublic class LTSminMonitorAlternating<I,O> extends AbstractLTSminMonitorMealy<I,O> implements LTSminAlternating<I,O,MealyMachine<?,I,?,O>>
AbstractLTSmin.BuilderDefaults
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
REQUIRED_VERSION
Constructor and Description |
---|
LTSminMonitorAlternating(boolean keepFiles,
Function<String,I> string2Input,
Function<String,O> string2Output,
Collection<? super O> skipOutputs) |
Modifier and Type | Method and Description |
---|---|
boolean |
requiresOriginalAutomaton()
Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.
|
findCounterExample, getSkipOutputs, getString2Output, setSkipOutputs
getExtraCommandLineOptions, getMinimumRequiredVersion
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
fsm2Mealy, mealy2ETF
automaton2ETF, getString2Output
getSkipOutputs, setSkipOutputs
getString2Input, isKeepFiles
findCounterExample
public boolean requiresOriginalAutomaton()
LTSminAlternating
requiresOriginalAutomaton
in interface LTSminAlternating<I,O,MealyMachine<?,I,?,O>>
true
, because there could be undefined outputs in FSMs.FSM2MealyParserAlternating
Copyright © 2019. All rights reserved.