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.
|
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
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
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 AbstractLTSminMonitorMealy<I,O>
formula
- the formula to verifyCopyright © 2020. All rights reserved.