I
- the input typepublic class LTSminLTLDFA<I> extends AbstractLTSminLTL<I,DFA<?,I>,Lasso.DFALasso<I>> implements ModelCheckerLasso.DFAModelCheckerLasso<I,String>, LTSminDFA<I,Lasso.DFALasso<I>>
AbstractLTSminLTL.BuilderDefaults
ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
Modifier and Type | Field and Description |
---|---|
static String |
LABEL_NAME
The index in the FSM state vector for accept/reject.
|
static String |
LABEL_VALUE
The value in the state vector for acceptance.
|
REQUIRED_VERSION
Constructor and Description |
---|
LTSminLTLDFA(boolean keepFiles,
Function<String,I> string2Input,
int minimumUnfolds,
double multiplier) |
Modifier and Type | Method and Description |
---|---|
Lasso.DFALasso<I> |
findCounterExample(DFA<?,I> automaton,
Collection<? extends I> inputs,
String property)
Converts the FSM file to a
Lasso.DFALasso . |
getExtraCommandLineOptions, getMinimumRequiredVersion, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
findCounterExampleFSM, getString2Input, isKeepFiles
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier
automaton2ETF, dfa2ETF
getString2Input, isKeepFiles
public static final String LABEL_NAME
public static final String LABEL_VALUE
@Nullable public Lasso.DFALasso<I> findCounterExample(DFA<?,I> automaton, Collection<? extends I> inputs, String property) throws ModelCheckingException
Lasso.DFALasso
.findCounterExample
in interface ModelChecker<I,DFA<?,I>,String,Lasso.DFALasso<I>>
automaton
- the DFA used to compute the number of loop unrolls.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.