I
- the input typeO
- the output typepublic class LTSminLTLAlternating<I,O> extends AbstractLTSminLTLMealy<I,O> implements LTSminAlternating<I,O,Lasso.MealyLasso<I,O>>
AbstractLTSminLTL.BuilderDefaults
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
REQUIRED_VERSION
Constructor and Description |
---|
LTSminLTLAlternating(boolean keepFiles,
Function<String,I> string2Input,
Function<String,O> string2Output,
int minimumUnfolds,
double multiplier,
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, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
fsm2Mealy, mealy2ETF
automaton2ETF, getString2Output
getSkipOutputs, setSkipOutputs
getString2Input, isKeepFiles
findCounterExample
computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
public boolean requiresOriginalAutomaton()
LTSminAlternating
requiresOriginalAutomaton
in interface LTSminAlternating<I,O,Lasso.MealyLasso<I,O>>
false
, because only lassos should be read from FSMs.Copyright © 2019. All rights reserved.