I
- the input typepublic class LTSminMonitorDFA<I> extends AbstractLTSminMonitor<I,DFA<?,I>,DFA<?,I>> implements LTSminDFA<I,DFA<?,I>>
AbstractLTSmin.BuilderDefaults
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
REQUIRED_VERSION
LABEL_NAME, LABEL_VALUE
Constructor and Description |
---|
LTSminMonitorDFA(boolean keepFiles,
Function<String,I> string2Input) |
Modifier and Type | Method and Description |
---|---|
@Nullable DFA<?,I> |
findCounterExample(DFA<?,I> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
DFA . |
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. |
getExtraCommandLineOptions, getMinimumRequiredVersion
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
automaton2ETF, dfa2ETF
getString2Input, isKeepFiles
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 AbstractLTSmin<I,DFA<?,I>,DFA<?,I>>
formula
- the formula to verifypublic @Nullable DFA<?,I> findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property)
DFA
.findCounterExample
in interface ModelChecker<I,DFA<?,I>,String,DFA<?,I>>
automaton
- the automaton to check the property on.inputs
- the alphabet.property
- the property.null
if no counter examples exist.ModelChecker.findCounterExample(Object, Collection, Object)
Copyright © 2020. All rights reserved.