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.
|
protected void |
verifyFormula(String formula)
This method must verify that the given formula adheres to the expected syntax of the chosen serialization format
for hypotheses of
this model-checker. |
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.protected void verifyFormula(String formula)
AbstractLTSmin
this
model-checker.
If the formula does not adhere to the expected syntax, this method should throw a IllegalArgumentException
, possibly containing nested causes that further elaborate on why the formula couldn't
be verified.
verifyFormula
in class AbstractLTSminLTLMealy<I,O>
formula
- the formula to verifyCopyright © 2020. All rights reserved.