Package de.upb.swt.mcie.mc

This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker.

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.
 

Package de.upb.swt.mcie.mc Description

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.

See Also:
de.upb.swt.mcie.formulas, de.upb.swt.mcie.parser, de.upb.swt.mcie.robdds