Package net.automatalib.modelchecking
Interface ModelCheckerLasso<I,A,P,R extends Lasso<I,?>>
-
- Type Parameters:
I
- the input type.A
- the automaton type.P
- the property type.R
- the type of counterexample
- All Superinterfaces:
ModelChecker<I,A,P,R>
- All Known Subinterfaces:
ModelCheckerLasso.DFAModelCheckerLasso<I,P>
,ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
,ModelCheckerLassoCache<I,A,P,R>
,ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>
,ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>
- All Known Implementing Classes:
AbstractLTSminLTL
,AbstractLTSminLTLMealy
,AbstractUnfoldingModelChecker
,LTSminLTLAlternating
,LTSminLTLDFA
,LTSminLTLIO
,SizeDFAModelCheckerLassoCache
,SizeMealyModelCheckerLassoCache
public interface ModelCheckerLasso<I,A,P,R extends Lasso<I,?>> extends ModelChecker<I,A,P,R>
A model checker where the counterexample is a lasso.
-
-
Nested Class Summary
Nested Classes Modifier and Type Interface Description static interface
ModelCheckerLasso.DFAModelCheckerLasso<I,P>
static interface
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>
-
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default int
computeUnfolds(int size)
Compute the number of unfolds according tosize
.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 interface net.automatalib.modelchecking.ModelChecker
findCounterExample
-
-
-
-
Method Detail
-
getMultiplier
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.- Returns:
- the multiplier
-
setMultiplier
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.- Parameters:
multiplier
- the multiplier- Throws:
IllegalArgumentException
- whenmultiplier < 0.0
.
-
getMinimumUnfolds
int getMinimumUnfolds()
Returns the minimum number of times a loop must be unrolled.- Returns:
- the minimum
-
setMinimumUnfolds
void setMinimumUnfolds(int minimumUnfolds)
Set the minimum number of times a loop must be unrolled.- Parameters:
minimumUnfolds
- the minimum- Throws:
IllegalArgumentException
- whenminimumUnfolds < 1
.
-
computeUnfolds
default int computeUnfolds(int size)
Compute the number of unfolds according tosize
.- Parameters:
size
- the number of states in the hypothesis.- Returns:
- the number of times the loop of a lasso has to be unfolded.
-
-