Package net.automatalib.modelchecking

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

  • 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 a 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.

    • 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

      • 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