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 this ModelChecker, 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.