Package net.automatalib.modelchecker.ltsmin
This package (and sub-packages) provides the integration of the model checker LTSmin as described in the paper Sound Black-Box Checking in the LearnLib by Jeroen Meijer
and Jaco van de Pol.
Note that this implementation requires a local installation of the LTSmin binaries which are not explicitly included in this artifact due to packaging reasons.
-
Interface Summary Interface Description LTSmin<I,A,R> An LTSmin model checker.LTSminAlternating<I,O,R> A model checker using LTSmin for Mealy machines using alternating edge semantics.LTSminDFA<I,R> A model checker using LTSmin for DFAs.LTSminIO<I,O,R> A model checker using LTSmin for Mealy machines using synchronous edge semantics.LTSminMealy<I,O,R> A feature of thisModelChecker
, is that one can remove particular output symbols from the given MealyMachine hypothesis. -
Class Summary Class Description AbstractLTSmin<I,A,R> An LTL model checker using LTSmin.LTSminLTLParser A parser that verifies the syntax of LTL formulae of LTSmin.LTSminUtil A utility class that encapsulates certain technical aspects of LTSmin (e.g. accessibility of the binary, etc.)LTSminVersion A class for describing LTSmin version. -
Exception Summary Exception Description ParseException This exception is thrown when parse errors are encountered.