Package net.automatalib.modelchecker.ltsmin

Class AbstractLTSmin<I,​A,​R>

  • Type Parameters:
    I - the input type.
    A - the automaton type.
    R - the type of counterexample
    All Implemented Interfaces:
    LTSmin<I,​A,​R>, ModelChecker<I,​A,​String,​R>
    Direct Known Subclasses:
    AbstractLTSminLTL, AbstractLTSminMonitor
    public abstract class AbstractLTSmin<I,​A,​R>
extends Object
implements ModelChecker<I,​A,​String,​R>, LTSmin<I,​A,​R>
    An LTL model checker using LTSmin.

    The user must install LTSmin in order for AbstractLTSmin to run without exceptions. Once LTSmin is installed the user may specify the path to the installed LTSmin binaries with the property automatalib.ltsmin.path. If this property is not set the binaries will be run as usual (e.g. simply by invoking etf2lts-mc, and ltsmin-convert), which means the user can also specify the location of the binaries in the PATH environment variable.

    This model checker is implemented as follows. The hypothesis automaton is first written to an LTS in ETF AbstractETFWriter file, which serves as input for the etf2lts-mc binary. Then the etf2lts-mc binary is run, which will write an LTS in GCF format. This LTS will be a subset of the language of the given hypothesis. Next, the GCF is converted to FSM using the ltsmin-convert binary. Lastly, the FSM is read back into an automaton using an AbstractFSMParser.

    See Also:
    http://ltsmin.utwente.nl, AbstractFSMParser, AbstractETFWriter, AutomataLibSettings

    • Constructor Detail

      • AbstractLTSmin

        protected AbstractLTSmin​(boolean keepFiles,
                         Function<String,​I> string2Input)
        Constructs a new AbstractLTSmin.
        Parameters:
        keepFiles - whether to keep intermediate files, (e.g. etfs, gcfs etc.).
        string2Input - a function that transforms edges in FSM files to actual input.
        Throws:
        ModelCheckingException - when the LTSmin binaries can not be run successfully.
        See Also:
        AbstractLTSmin

    • Method Detail

      • getExtraCommandLineOptions

        protected abstract List<String> getExtraCommandLineOptions()
        Returns the extra command line options that should be given to the etf2lts-mc binary.
        Returns:
        the extra command line options.

      • verifyFormula

        protected abstract void verifyFormula​(String formula)
        This method must verify that the given formula adheres to the expected syntax of the chosen serialization format for hypotheses of this model-checker.

        If the formula does not adhere to the expected syntax, this method should throw a IllegalArgumentException, possibly containing nested causes that further elaborate on why the formula couldn't be verified.

        Parameters:
        formula - the formula to verify

      • isKeepFiles

        public boolean isKeepFiles()
        Description copied from interface: LTSmin
        Returns whether intermediate files should be kept, e.g. etfs, gcfs, etc.
        Specified by:
        isKeepFiles in interface LTSmin<I,​A,​R>
        Returns:
        the boolean

      • getString2Input

        public Function<String,​I> getString2Input()
        Description copied from interface: LTSmin
        Returns the function that transforms edges in FSM files to actual input.
        Specified by:
        getString2Input in interface LTSmin<I,​A,​R>
        Returns:
        the Function.

      • findCounterExampleFSM

        protected final @Nullable File findCounterExampleFSM​(A hypothesis,
                                                     Collection<? extends I> inputs,
                                                     String formula)
        Finds a counterexample for the given formula, and given hypothesis in FSM format.
        Parameters:
        hypothesis - the hypothesis to check
        inputs - the inputs which should be regarded for checking
        formula - the formula that should be checked
        Returns:
        a file containing the FSM representation for the found counterexample, or null if no such counterexample could be found.
        See Also:
        AbstractLTSmin