Package ptolemy.domains.modal.kernel.fmv

Class FmvState

java.lang.Object

ptolemy.kernel.util.NamedObj

ptolemy.kernel.InstantiableNamedObj

ptolemy.kernel.Entity<T>

ptolemy.kernel.ComponentEntity

ptolemy.domains.modal.kernel.State

ptolemy.domains.modal.kernel.fmv.FmvState

All Implemented Interfaces:

java.lang.Cloneable, ConfigurableEntity, Changeable, Configurable, Debuggable, DebugListener, Derivable, DropTargetHandler, Flowable, Instantiable, ModelErrorHandler, MoMLExportable, Moveable, Nameable

public class FmvState
extends State

A Formal Method Verification (FMV) State. It supports graphical specification generation for safety or reachability analysis.

Since:

Ptolemy II 8.0

Version:

$Id$

Author:

Chihhong Patrick Cheng

Pt.AcceptedRating:

Red (patrickj)

Pt.ProposedRating:

Red (patrickj)

Nested Class Summary

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

Entity.ContainedObjectsIterator

Field Summary

Fields

Modifier and Type	Field	Description
Parameter	isReachabilityAnalysisState	A boolean parameter indicating whether this state is a reachability analysis state.
Parameter	isRiskAnalysisState	A boolean parameter indicating that this state is a risk state.

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

incomingPort, isFinalState, isInitialState, outgoingPort, refinementName, saveRefinementsInConfigurer

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

Constructor Summary

Constructors

Constructor	Description
FmvState(CompositeEntity container, java.lang.String name)	Create an FmvState in the specified container with the specified name.

Method Summary

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

_exportMoMLContents, attributeChanged, clone, configure, dropObject, errorTransitionList, getConfigurer, getConfigureSource, getConfigureText, getIncomingPort, getObjectInRefinement, getOutgoingPort, getRefinement, nonErrorNonTerminationTransitionList, nonpreemptiveTransitionList, preemptiveTransitionList, terminationTransitionList

Methods inherited from class ptolemy.kernel.ComponentEntity

_adjustDeferrals, _checkContainer, _getContainedObject, _propagateExistence, getContainer, instantiate, isAtomic, isOpaque, moveDown, moveToFirst, moveToIndex, moveToLast, moveUp, newPort, propagateExistence, setContainer, setName

Methods inherited from class ptolemy.kernel.Entity

_addPort, _description, _removePort, _validateSettables, connectedPortList, connectedPorts, connectionsChanged, containedObjectsIterator, getAttribute, getPort, getPorts, linkedRelationList, linkedRelations, portList, removeAllPorts, setClassDefinition, uniqueName

Methods inherited from class ptolemy.kernel.InstantiableNamedObj

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

Methods inherited from class ptolemy.kernel.util.NamedObj

_addAttribute, _adjustOverride, _attachText, _cloneFixAttributeFields, _containedDecorators, _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, handleModelError, 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.Derivable

getDerivedLevel, getDerivedList, propagateValue

Methods inherited from interface ptolemy.kernel.util.Nameable

description, getDisplayName, getFullName, getName, getName

Field Detail

isRiskAnalysisState

public Parameter isRiskAnalysisState

A boolean parameter indicating that this state is a risk state. The default value is false.

isReachabilityAnalysisState

public Parameter isReachabilityAnalysisState

A boolean parameter indicating whether this state is a reachability analysis state. The default value is false.

Constructor Detail

FmvState

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

Create an FmvState 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.