ptolemy.domains.modal.kernel.fmv

Class FmvAutomaton

java.lang.Object

ptolemy.kernel.util.NamedObj

ptolemy.kernel.InstantiableNamedObj

ptolemy.kernel.Entity<T>

ptolemy.kernel.ComponentEntity

ptolemy.kernel.CompositeEntity

ptolemy.domains.modal.kernel.FSMActor

ptolemy.domains.modal.kernel.fmv.FmvAutomaton

All Implemented Interfaces:

java.lang.Cloneable, Actor, Executable, Initializable, TypedActor, ExplicitChangeContext, Changeable, Debuggable, DebugListener, Derivable, Instantiable, ModelErrorHandler, MoMLExportable, Moveable, Nameable

Deprecated.

ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.

@Deprecated
public class FmvAutomaton
extends FSMActor

A Formal Method Verification (FMV) Automaton. An FmvAutomaton is not different from a regular FSM, but the class definition provides a specialized environment to convert into format acceptable by model checker NuSMV. Also, the state insertion of FmvAutomaton supports the inserting of FmvState, where these specialized states are able to have property indicating whether it is a risk state.

Since:

Ptolemy II 8.0

Version:

$Id$

Author:

Chihhong Patrick Cheng, Contributor: Edward A. Lee

See Also:

State, Transition, FmvState

Pt.AcceptedRating:

Red (patrickj)

Pt.ProposedRating:

Red (patrickj)

Nested Class Summary

Nested classes/interfaces inherited from class ptolemy.domains.modal.kernel.FSMActor

FSMActor.PortScope

Nested classes/interfaces inherited from class ptolemy.kernel.CompositeEntity

CompositeEntity.ContainedObjectsIterator

Field Summary

Fields inherited from class ptolemy.domains.modal.kernel.FSMActor

_currentState, _disabledRefinements, _initializables, _inputTokenMap, _lastChosenTransition, _lastChosenTransitions, _lastTakenTransitions, _stateRefinementsToPostfire, _stopRequested, errorCause, errorClass, errorMessage, finalStateNames, initialStateName, probability, resetOnEachRun, seed, stateDependentCausality, timeout

Fields inherited from class ptolemy.kernel.CompositeEntity

_levelCrossingLinks

Fields inherited from class ptolemy.kernel.util.NamedObj

_changeListeners, _changeLock, _changeRequests, _debugging, _debugListeners, _deferChangeRequests, _elementName, _isPersistent, _verbose, _workspace, ATTRIBUTES, CLASSNAME, COMPLETE, CONTENTS, DEEP, FULLNAME, LINKS

Fields inherited from interface ptolemy.actor.Executable

COMPLETED, NOT_READY, STOP_ITERATING

Constructor Summary

Constructors

Constructor and Description
FmvAutomaton() Deprecated. Construct an FmvAutomaton in the default workspace with an empty string as its name.
FmvAutomaton(CompositeEntity container, java.lang.String name) Deprecated. Create an FmvAutomaton in the specified container with the specified name.
FmvAutomaton(Workspace workspace) Deprecated. Construct an FmvAutomaton in the specified workspace with an empty string as its name.

Method Summary

Modifier and Type	Method and Description
java.lang.StringBuffer	convertToSMVFormat(java.lang.String formula, MathematicalModelConverter.FormulaType choice, int span) Deprecated. Return an StringBuffer that contains the .smv format of the FmvAutomaton.

Methods inherited from class ptolemy.domains.modal.kernel.FSMActor

_addEntity, _addRelation, _areAllImmediateTransitionsDisabled, _chooseTransitions, _destinationState, _getChannelForIdentifier, _getPortForIdentifier, _getStateRefinementsToPostfire, _getTransitionRefinementsToPostfire, _init, _initializeRefinements, _isRefinementOutput, _isSafeToClear, _readInputs, _schedule, _setCurrentConnectionMap, _setTimeForRefinement, addChosenTransition, addInitializable, attributeChanged, clone, createReceivers, currentState, enabledTransitions, exportSubmodel, fire, foundUnknown, getCausalityInterface, getContext, getDirector, getExecutiveDirector, getInitialState, getLastChosenTransition, getLastChosenTransitions, getLastTakenTransitions, getManager, getModifiedVariables, getPortScope, handleModelError, hasInput, hasInput, initialize, inputPortList, isBackwardTypeInferenceEnabled, isFireFunctional, isOpaque, isStrict, iterate, newPort, newReceiver, newRelation, outputPortList, postfire, prefire, preinitialize, readInputs, readOutputsFromRefinement, removeInitializable, reset, setLastChosenTransition, setNewIteration, setSupportMultirate, stop, stopFire, terminate, typeConstraints, wasTransitionTaken, wrapup

Methods inherited from class ptolemy.kernel.CompositeEntity

_adjustDeferrals, _containedDecorators, _deepOpaqueEntityList, _description, _exportMoMLContents, _finishedAddEntity, _removeEntity, _removeRelation, _validateSettables, allAtomicEntityList, allowLevelCrossingConnect, classDefinitionList, connect, connect, containedObjectsIterator, deepCompositeEntityList, deepEntityList, deepGetEntities, deepNamedObjList, deepOpaqueEntityList, deepRelationSet, entityList, entityList, exportLinks, exportMoML, getAttribute, getEntities, getEntity, getPort, getRelation, getRelations, isAtomic, lazyAllAtomicEntityList, lazyAllCompositeEntityList, lazyAllCompositeTransparentAndOpaqueEntityList, lazyClassDefinitionList, lazyDeepEntityList, lazyEntityList, lazyRelationList, numberOfEntities, numberOfRelations, numEntities, numRelations, relationList, removeAllEntities, removeAllRelations, setClassDefinition, setContainer, statistics, uniqueName

Methods inherited from class ptolemy.kernel.ComponentEntity

_checkContainer, _getContainedObject, _propagateExistence, getContainer, instantiate, moveDown, moveToFirst, moveToIndex, moveToLast, moveUp, propagateExistence, setName

Methods inherited from class ptolemy.kernel.Entity

_addPort, _removePort, connectedPortList, connectedPorts, connectionsChanged, getPorts, linkedRelationList, linkedRelations, portList, removeAllPorts

Methods inherited from class ptolemy.kernel.InstantiableNamedObj

_setParent, getChildren, getElementName, getParent, getPrototypeList, isClassDefinition, isWithinClassDefinition

Methods inherited from class ptolemy.kernel.util.NamedObj

_addAttribute, _adjustOverride, _attachText, _cloneFixAttributeFields, _copyChangeRequestList, _debug, _debug, _debug, _debug, _debug, _executeChangeRequests, _getIndentPrefix, _isMoMLSuppressed, _markContentsDerived, _notifyHierarchyListenersAfterChange, _notifyHierarchyListenersBeforeChange, _propagateValue, _removeAttribute, _splitName, _stripNumericSuffix, addChangeListener, addDebugListener, addHierarchyListener, attributeDeleted, attributeList, attributeList, attributeTypeChanged, clone, decorators, deepContains, depthInHierarchy, description, description, event, executeChangeRequests, exportMoML, exportMoML, exportMoML, exportMoML, exportMoMLPlain, getAttribute, getAttributes, getChangeListeners, getClassName, getDecoratorAttribute, getDecoratorAttributes, getDerivedLevel, getDerivedList, getDisplayName, getFullName, getModelErrorHandler, getName, getName, getSource, isDeferringChangeRequests, isOverridden, isPersistent, lazyContainedObjectsIterator, message, notifyOfNameChange, propagateValue, propagateValues, removeAttribute, removeChangeListener, removeDebugListener, removeHierarchyListener, requestChange, setClassName, setDeferringChangeRequests, setDerivedLevel, setDisplayName, setModelErrorHandler, setPersistent, setSource, sortContainedObjects, toplevel, toString, validateSettables, workspace

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface ptolemy.kernel.util.Nameable

description, getContainer, getDisplayName, getFullName, getName, getName, setName

Methods inherited from interface ptolemy.kernel.util.Derivable

getDerivedLevel, getDerivedList, propagateValue

Constructor Detail

FmvAutomaton

public FmvAutomaton()

Deprecated.

Construct an FmvAutomaton in the default workspace with an empty string as its name. Add the actor to the workspace directory. Increment the version number of the workspace.

FmvAutomaton

public FmvAutomaton(Workspace workspace)

Deprecated.

Construct an FmvAutomaton in the specified workspace with an empty string as its name. The name can be changed later with setName(). If the workspace argument is null, then use the default workspace. Add the actor to the workspace directory. Increment the version number of the workspace.

Parameters:

workspace - The workspace that will list the actor.

FmvAutomaton

public FmvAutomaton(CompositeEntity container,
                    java.lang.String name)
             throws IllegalActionException,
                    NameDuplicationException

Deprecated.

Create an FmvAutomaton in the specified container with the specified name. The name must be unique within the container or an exception is thrown. The container argument must not be null, or a NullPointerException will be thrown.

Parameters:

container - The container.

name - The name of this automaton within the container.

Throws:

IllegalActionException - If the entity cannot be contained by the proposed container.

NameDuplicationException - If the name coincides with an entity already in the container.

Method Detail

convertToSMVFormat

public java.lang.StringBuffer convertToSMVFormat(java.lang.String formula,
                                                 MathematicalModelConverter.FormulaType choice,
                                                 int span)
                                          throws IllegalActionException

Deprecated.

Return an StringBuffer that contains the .smv format of the FmvAutomaton.

Parameters:

formula - The temporal formula used to be attached in the .smv file.

choice - The type of the formula. It may be either a CTL or LTL formula.

span - A constant used to expand the size of the rough domain.

Returns:

The .smv format of the FmvAutomaton.

Throws:

IllegalActionException - If there is a problem with the conversion.