ModelCheckerLasso (AutomataLib 0.11.0 API)

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 to `size`.
`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 - when multiplier < 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 - when minimumUnfolds < 1.
  - computeUnfolds
```
default int computeUnfolds(int size)
```
    Compute the number of unfolds according to size.
    
    Parameters:
    
    size - the number of states in the hypothesis.
    
    Returns:
    
    the number of times the loop of a lasso has to be unfolded.