Module net.automatalib.modelchecker.ltsmin

Package net.automatalib.modelchecker.ltsmin.ltl

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

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:

keepFiles - whether to keep the files generated during model checking

string2Input - the input parsing function

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 class AbstractLTSmin<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 class AbstractLTSmin<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 interface ModelCheckerLasso<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 interface ModelCheckerLasso<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 interface ModelCheckerLasso<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 interface ModelCheckerLasso<I,A,String,L extends Lasso<I,?>>

Parameters:

minimumUnfolds - the minimum