net.automatalib.modelchecking.modelchecker

Class AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>

java.lang.Object

net.automatalib.modelchecking.modelchecker.AbstractUnfoldingModelChecker<I,A,P,L>

Type Parameters:

I - the input type

A - the automaton type

P - the property type

L - the Lasso type

All Implemented Interfaces:

ModelChecker<I,A,P,L>, ModelCheckerLasso<I,A,P,L>

public abstract class AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>
extends Object
implements ModelCheckerLasso<I,A,P,L>

An ModelCheckerLasso that can unfold loops of lassos.

Unfolding a lasso is done according to two conditions: 1. the lasso has to be unfolded a minimum number of times (getMinimumUnfolds(). 2. the lasso has to be unfolded relative to the number of states in an hypothesis, multiplied by some double (getMultiplier().

Note that one can unfold a lasso a fixed number of times if the multiplier is set to 0.0. Also note that a lasso needs to be unfolded at least once, and the multiplier can not be negative.

Nested Class Summary

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker

ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractUnfoldingModelChecker(int minimumUnfolds, double multiplier) Constructs a new AbstractUnfoldingModelChecker.

Method Summary

Modifier and Type	Method and Description
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 java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

computeUnfolds

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

Constructor Detail

AbstractUnfoldingModelChecker

protected AbstractUnfoldingModelChecker(int minimumUnfolds,
                                        double multiplier)

Constructs a new AbstractUnfoldingModelChecker.

Parameters:

minimumUnfolds - the minimum number of unfolds.

multiplier - the multiplier

Throws:

IllegalArgumentException - when minimumUnfolds < 1 || multiplier < 0.0.

Method Detail

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,P,L extends Lasso<I,?>>

Returns:

the minimum

setMinimumUnfolds

public void setMinimumUnfolds(@UnknownInitialization AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>> this,
                              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,P,L extends Lasso<I,?>>

Parameters:

minimumUnfolds - the minimum

setMultiplier

public void setMultiplier(@UnknownInitialization AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>> this,
                          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,P,L extends Lasso<I,?>>

Parameters:

multiplier - the multiplier

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,P,L extends Lasso<I,?>>

Returns:

the multiplier