Modifier and Type | Interface and Description |
---|---|
interface |
LTSmin<I,A,R>
An LTSmin model checker.
|
interface |
LTSminAlternating<I,O,R>
A model checker using LTSmin for Mealy machines using alternating edge semantics.
|
interface |
LTSminDFA<I,R>
A model checker using LTSmin for DFAs.
|
interface |
LTSminIO<I,O,R>
An model checker using LTSmin for Mealy machines using synchronous edge semantics.
|
interface |
LTSminMealy<I,O,R>
A feature of this
ModelChecker , is that one can remove particular output
symbols from the a given MealyMachine hypothesis. |
Modifier and Type | Class and Description |
---|---|
class |
AbstractLTSmin<I,A,R>
An LTL model checker using LTSmin.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractLTSminLTL<I,A,L extends Lasso<I,?>>
An LTSmin model checker for full LTL.
|
class |
AbstractLTSminLTLMealy<I,O>
An LTL model checker using LTSmin for Mealy machines.
|
class |
LTSminLTLAlternating<I,O>
An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.
|
class |
LTSminLTLDFA<I>
An LTL model checker using LTSmin for DFAs.
|
class |
LTSminLTLIO<I,O>
An LTL model checker using LTSmin for Mealy machines using synchronous edge semantics.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractLTSminMonitor<I,A,R>
An LTSmin model checker for monitors.
|
class |
AbstractLTSminMonitorMealy<I,O>
An monitor model checker using LTSmin for Mealy machines.
|
class |
LTSminMonitorAlternating<I,O>
A monitor model checker using LTSmin for Mealy machines using alternating edge semantics.
|
class |
LTSminMonitorDFA<I>
A monitor model checker using LTSmin for DFAs.
|
class |
LTSminMonitorIO<I,O>
A monitor model checker using LTSmin for Mealy machines using synchronous edge semantics.
|
Modifier and Type | Interface and Description |
---|---|
static interface |
ModelChecker.DFAModelChecker<I,P,R> |
static interface |
ModelChecker.MealyModelChecker<I,O,P,R>
A model checker for Mealy machines.
|
interface |
ModelCheckerCache<I,A,P,R>
A model checker that caches calls to
findCounterExample(Object, Collection, Object) . |
static interface |
ModelCheckerCache.DFAModelCheckerCache<I,P,R> |
static interface |
ModelCheckerCache.MealyModelCheckerCache<I,O,P,R> |
interface |
ModelCheckerLasso<I,A,P,R extends Lasso<I,?>>
A model checker where the counterexample is a lasso.
|
static interface |
ModelCheckerLasso.DFAModelCheckerLasso<I,P> |
static interface |
ModelCheckerLasso.MealyModelCheckerLasso<I,O,P> |
interface |
ModelCheckerLassoCache<I,A,P,R extends Lasso<I,?>> |
static interface |
ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P> |
static interface |
ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P> |
Modifier and Type | Class and Description |
---|---|
class |
AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>
An
ModelCheckerLasso that can unfold loops of lassos. |
Modifier and Type | Class and Description |
---|---|
class |
SizeDFAModelCheckerCache<I,P,R>
A DFAModelCheckerCache that invalidates the cached counter examples when
findCounterExample(Object, Collection, Object) is called with a DFA with a size different, and
an input alphabet different than the previous call. |
class |
SizeDFAModelCheckerLassoCache<I,P> |
class |
SizeMealyModelCheckerCache<I,O,P,R> |
class |
SizeMealyModelCheckerLassoCache<I,O,P> |
Copyright © 2019. All rights reserved.