|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
See:
Description
Class Summary | |
---|---|
FairModel | Implements a fair model based on some other model. |
Kripkestructure | Implements a Kripke structure. |
Model | Abstract class for a model on which model checking should be performed. |
Procedures | This class implements some general procedures which might be used in some model checking algorithms. |
Transitionsystem | Implements a transition system. |
Exception Summary | |
---|---|
AbortException | Exception that indicates that a model checking operation on a model was explicitly aborted. |
IncorrectUseException | Exception that results from an incorrect use of the model checking procedures, the models, or their extensions. |
This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker. Special model are Kripke structures and transition systems as well their fair extensions.
The model checking procedures use the methods for operations on ROBDDs
implemented in the package de.upb.swt.mcie.robdds
.
de.upb.swt.mcie.formulas
,
de.upb.swt.mcie.parser
,
de.upb.swt.mcie.robdds
|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |