Package ptolemy.vergil.modal.fmv

Vergil Formal Method Verification automata that provide a specialized environment to invoke the NuSMV model checker.

See: Description

Class Summary

Class	Description
FmvAutomatonGraphController	A Graph Controller for Fmv automata models.
FmvAutomatonGraphFrame	Deprecated ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.
FmvAutomatonGraphFrame.SMVFileFilter	A file filter that accepts files that end with ".smv".
FmvAutomatonGraphTableau	Deprecated ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.
FmvAutomatonGraphTableau.Factory	A factory that creates graph editing tableaux for Ptolemy models.
FmvStateIcon	An icon specialized for states of a state machine with reachability and risk analysis.

Package ptolemy.vergil.modal.fmv Description

Vergil Formal Method Verification automata that provide a specialized environment to invoke the NuSMV model checker.

Since:

Ptolemy II 6.1