Class AbstractLTSminLTL<I,A,L extends Lasso<I,?>>
- java.lang.Object
-
- net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,L>
-
- net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL<I,A,L>
-
- All Implemented Interfaces:
LTSmin<I,A,L>
,ModelChecker<I,A,String,L>
,ModelCheckerLasso<I,A,String,L>
- Direct Known Subclasses:
AbstractLTSminLTLMealy
,LTSminLTLDFA
public abstract class AbstractLTSminLTL<I,A,L extends Lasso<I,?>> extends AbstractLTSmin<I,A,L> implements ModelCheckerLasso<I,A,String,L>
An LTSmin model checker for full LTL.- See Also:
- man etf2lts-mc,
AbstractLTSmin
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker
ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>
-
Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLasso
ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
-
-
Field Summary
Fields Modifier and Type Field Description static LTSminVersion
REQUIRED_VERSION
-
Constructor Summary
Constructors Modifier Constructor Description protected
AbstractLTSminLTL(boolean keepFiles, Function<String,I> string2Input, int minimumUnfolds, double multiplier)
Constructs a new AbstractLTSminLTL.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method 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.-
Methods inherited from class net.automatalib.modelchecker.ltsmin.AbstractLTSmin
findCounterExampleFSM, getString2Input, isKeepFiles, verifyFormula
-
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
-
Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSmin
automaton2ETF
-
Methods inherited from interface net.automatalib.modelchecking.ModelChecker
findCounterExample
-
Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso
computeUnfolds
-
-
-
-
Field Detail
-
REQUIRED_VERSION
public static final LTSminVersion REQUIRED_VERSION
-
-
Constructor Detail
-
AbstractLTSminLTL
protected AbstractLTSminLTL(boolean keepFiles, Function<String,I> string2Input, int minimumUnfolds, double multiplier)
Constructs a new AbstractLTSminLTL.- Parameters:
multiplier
- the multiplier.minimumUnfolds
- the minimum number of unfolds.- See Also:
AbstractLTSmin(boolean, Function)
-
-
Method Detail
-
getMinimumRequiredVersion
protected LTSminVersion getMinimumRequiredVersion(@UnknownInitialization(AbstractLTSmin.class) AbstractLTSminLTL<I,A,L extends Lasso<I,?>> this)
Description copied from class:AbstractLTSmin
Returns the minimum required version of LTSmin.- Specified by:
getMinimumRequiredVersion
in classAbstractLTSmin<I,A,L extends Lasso<I,?>>
- Returns:
- the major version.
-
getExtraCommandLineOptions
protected List<String> getExtraCommandLineOptions()
Description copied from class:AbstractLTSmin
Returns the extra command line options that should be given to the etf2lts-mc binary.- Specified by:
getExtraCommandLineOptions
in classAbstractLTSmin<I,A,L extends Lasso<I,?>>
- Returns:
- the extra command line options.
-
getMultiplier
public double getMultiplier()
Description copied from interface:ModelCheckerLasso
Return the multiplier for the number of times a loop of the lasso must be unrolled, relative to the size of the hypothesis.- Specified by:
getMultiplier
in interfaceModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
- Returns:
- the multiplier
-
setMultiplier
public void setMultiplier(double multiplier)
Description copied from interface:ModelCheckerLasso
Set the multiplier for the number of times a loop of the lasso must be unrolled, relative to the size of the hypothesis.- Specified by:
setMultiplier
in interfaceModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
- Parameters:
multiplier
- the multiplier
-
getMinimumUnfolds
public int getMinimumUnfolds()
Description copied from interface:ModelCheckerLasso
Returns the minimum number of times a loop must be unrolled.- Specified by:
getMinimumUnfolds
in interfaceModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
- Returns:
- the minimum
-
setMinimumUnfolds
public void setMinimumUnfolds(int minimumUnfolds)
Description copied from interface:ModelCheckerLasso
Set the minimum number of times a loop must be unrolled.- Specified by:
setMinimumUnfolds
in interfaceModelCheckerLasso<I,A,String,L extends Lasso<I,?>>
- Parameters:
minimumUnfolds
- the minimum
-
-