All Classes Interface Summary Class Summary Exception Summary
Class |
Description |
AbstractLTSmin<I,A,R> |
An LTL model checker using LTSmin.
|
AbstractLTSminLTL<I,A,L extends Lasso<I,?>> |
An LTSmin model checker for full LTL.
|
AbstractLTSminLTLMealy<I,O> |
An LTL model checker using LTSmin for Mealy machines.
|
AbstractLTSminMonitor<I,A,R> |
An LTSmin model checker for monitors.
|
AbstractLTSminMonitorMealy<I,O> |
A monitor model checker using LTSmin for Mealy machines.
|
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.
|
LTSminLTLAlternating<I,O> |
An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.
|
LTSminLTLAlternatingBuilder<I,O> |
|
LTSminLTLDFA<I> |
An LTL model checker using LTSmin for DFAs.
|
LTSminLTLDFABuilder<I> |
|
LTSminLTLIO<I,O> |
An LTL model checker using LTSmin for Mealy machines using synchronous edge semantics.
|
LTSminLTLIOBuilder<I,O> |
|
LTSminLTLParser |
A parser that verifies the syntax of LTL formulae of LTSmin.
|
LTSminMealy<I,O,R> |
A feature of this ModelChecker , is that one can remove particular output
symbols from the given MealyMachine hypothesis.
|
LTSminMonitorAlternating<I,O> |
A monitor model checker using LTSmin for Mealy machines using alternating edge semantics.
|
LTSminMonitorAlternatingBuilder<I,O> |
|
LTSminMonitorDFA<I> |
A monitor model checker using LTSmin for DFAs.
|
LTSminMonitorDFABuilder<I> |
|
LTSminMonitorIO<I,O> |
A monitor model checker using LTSmin for Mealy machines using synchronous edge semantics.
|
LTSminMonitorIOBuilder<I,O> |
|
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.
|
ParseException |
This exception is thrown when parse errors are encountered.
|