Package ptolemy.verification.kernel

This package includes core Functions that provides a specialized environment to convert existing Ptolemy II models into SMV format and invoke the NuSMV model checker.

See:
Description

Class Summary

MathematicalModelConverter
REDUtility	This is an utility for Ptolemy model conversion.
REDUtility.REDModuleNameInitialBean
REDUtility.REDSingleEntityBean
REDUtility.REDTransitionBean
REDUtility.VariableInfo
SMVUtility	This is an utility function for Ptolemy II models.
SMVUtility.VariableInfo
SMVUtility.VariableTransitionInfo

Enum Summary

MathematicalModelConverter.FormulaType
MathematicalModelConverter.ModelType
MathematicalModelConverter.OutputType

Package ptolemy.verification.kernel Description

This package includes core Functions that provides a specialized environment to convert existing Ptolemy II models into SMV format and invoke the NuSMV model checker.

Since:

Ptolemy II 7.0