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 |
---|---|
DFA<?,I> |
findCounterExample(DFA<?,I> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
DFA . |
getExtraCommandLineOptions, getMinimumRequiredVersion
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
automaton2ETF, dfa2ETF
getString2Input, isKeepFiles
@Nullable public DFA<?,I> findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property) throws ModelCheckingException
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.ModelCheckingException
- when this model checker can not check the property.ModelChecker.findCounterExample(Object, Collection, Object)
Copyright © 2019. All rights reserved.