public abstract class AbstractLTSminLTL<I,A,L extends Lasso<I,?>> extends AbstractLTSmin<I,A,L> implements ModelCheckerLasso<I,A,String,L>
AbstractLTSmin
Modifier and Type | Class and Description |
---|---|
static class |
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 LTSminVersion |
REQUIRED_VERSION |
Modifier | Constructor and Description |
---|---|
protected |
AbstractLTSminLTL(boolean keepFiles,
Function<String,I> string2Input,
int minimumUnfolds,
double multiplier)
Constructs a new AbstractLTSminLTL.
|
Modifier and Type | Method and Description |
---|---|
protected List<String> |
getExtraCommandLineOptions()
Returns the extra command line options that should be given to the etf2lts-mc binary.
|
protected LTSminVersion |
getMinimumRequiredVersion()
Returns the minimum required version of LTSmin.
|
int |
getMinimumUnfolds()
Returns the minimum number of times a loop must be unrolled.
|
double |
getMultiplier()
Return the multiplier for the number of times a loop of the lasso must be unrolled, relative to the size of the
hypothesis.
|
void |
setMinimumUnfolds(int minimumUnfolds)
Set the minimum number of times a loop must be unrolled.
|
void |
setMultiplier(double multiplier)
Set the multiplier for the number of times a loop of the lasso must be unrolled, relative to the size of the
hypothesis.
|
findCounterExampleFSM, getString2Input, isKeepFiles, verifyFormula
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
computeUnfolds
findCounterExample
automaton2ETF
public static final LTSminVersion REQUIRED_VERSION
protected AbstractLTSminLTL(boolean keepFiles, Function<String,I> string2Input, int minimumUnfolds, double multiplier)
multiplier
- the multiplier.minimumUnfolds
- the minimum number of unfolds.AbstractLTSmin.AbstractLTSmin(boolean, Function)
protected LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(value=AbstractLTSmin.class) AbstractLTSminLTL<I,A,L extends Lasso<I,?>> this)
AbstractLTSmin
getMinimumRequiredVersion
in class AbstractLTSmin<I,A,L extends Lasso<I,?>>
protected List<String> getExtraCommandLineOptions()
AbstractLTSmin
getExtraCommandLineOptions
in class AbstractLTSmin<I,A,L extends Lasso<I,?>>
public double getMultiplier()
ModelCheckerLasso
getMultiplier
in interface ModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
public void setMultiplier(double multiplier)
ModelCheckerLasso
setMultiplier
in interface ModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
multiplier
- the multiplierpublic int getMinimumUnfolds()
ModelCheckerLasso
getMinimumUnfolds
in interface ModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
public void setMinimumUnfolds(int minimumUnfolds)
ModelCheckerLasso
setMinimumUnfolds
in interface ModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
minimumUnfolds
- the minimumCopyright © 2020. All rights reserved.