ptolemy.domains.modal.kernel.fmv
Class FmvAutomaton

java.lang.Object
  ptolemy.kernel.util.NamedObj
      ptolemy.kernel.InstantiableNamedObj
          ptolemy.kernel.Entity
              ptolemy.kernel.ComponentEntity
                  ptolemy.kernel.CompositeEntity
                      ptolemy.domains.modal.kernel.FSMActor
                          ptolemy.domains.modal.kernel.fmv.FmvAutomaton

All Implemented Interfaces:

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

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: FmvAutomaton.java 57044 2010-01-27 22:41:05Z cxh $

Author:

Chihhong Patrick Cheng, Contributor: Edward A. Lee

See Also:

State, Transition, FmvState, Serialized Form

Accepted Rating:

Red (patrickj)

Proposed Rating:

Red (patrickj)

Nested Class Summary

private static class	FmvAutomaton.VariableInfo
private static class	FmvAutomaton.VariableTransitionInfo

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

private java.util.HashMap<java.lang.String,FmvAutomaton.VariableInfo>	_variableInfo
private java.util.HashMap<java.lang.String,java.util.LinkedList<FmvAutomaton.VariableTransitionInfo>>	_variableTransitionInfo
private static int	DOMAIN_GT
private static int	DOMAIN_LS

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

_currentState, _initializables, _inputTokenMap, _lastChosenTransition, _stopRequested, finalStateNames, initialStateName, stateDependentCausality

Fields inherited from class ptolemy.kernel.CompositeEntity

_levelCrossingLinks

Fields inherited from class ptolemy.kernel.util.NamedObj

_changeListeners, _changeLock, _changeRequests, _debugging, _debugListeners, _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

FmvAutomaton()
Construct an FmvAutomaton in the default workspace with an empty string as its name.

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

FmvAutomaton(Workspace workspace)
Construct an FmvAutomaton in the specified workspace with an empty string as its name.

Method Summary

private java.util.HashSet<java.lang.String>	_decideVariableSet(int numSpan) This private function first decides variables that would be used in the Kripke structure.
private java.util.HashSet<State>	_enumerateStateSet() Perform an enumeration of the state in this FmvAutomaton and return a HashSet of states.
private void	_generateAllVariableTransitions(java.util.HashSet<java.lang.String> variableSet) Generate all premise-action pairs regarding this FmvAutomaton.
private void	_generatePremiseAndResultEachTransition(java.lang.String statePrecondition, java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.Integer>> valueDomain, java.lang.String lValue, java.lang.String offset, java.lang.String operatingSign) This function is used to generate detailed pre-conditions and post-conditions in .smv format.
private void	_recursiveStepGeneratePremiseAndResultEachTransition(java.lang.String currentPremise, int index, int maxIndex, java.lang.String[] keySetArray, java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.Integer>> valueDomain, java.lang.String lValue, java.lang.String newVariableValue, java.lang.String operatingSign) A private function used as a recursive step to generate all premises for enabling transition in .smv file.
private java.util.HashMap<java.lang.String,java.lang.String>	_retrieveVariableInitialValue(java.util.HashSet<java.lang.String> variableSet) A private function used as to generate variable initial values for the initial variable set.
java.lang.StringBuffer	convertToSMVFormat(java.lang.String formula, MathematicalModelConverter.FormulaType choice, int span) Return an StringBuffer that contains the .smv format of the FmvAutomaton.

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

_addEntity, _addRelation, _commitLastChosenTransition, _getChannelForIdentifier, _getPortForIdentifier, _isRefinementOutput, _readInputs, _setCurrentConnectionMap, addInitializable, chooseTransition, clone, createReceivers, currentState, enabledTransitions, exportSubmodel, fire, foundUnknown, getCausalityInterface, getContext, getDirector, getExecutiveDirector, getInitialState, getLastChosenTransition, getManager, getModifiedVariables, getPortScope, hasInput, hasInput, initialize, inputPortList, isFireFunctional, isOpaque, isStrict, iterate, newPort, newReceiver, newRelation, outputPortList, postfire, prefire, preinitialize, readInputs, readOutputsFromRefinement, removeInitializable, reset, setLastChosenTransition, setNewIteration, setSupportMultirate, stop, stopFire, terminate, typeConstraints, wrapup

Methods inherited from class ptolemy.kernel.CompositeEntity

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

Methods inherited from class ptolemy.kernel.ComponentEntity

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

Methods inherited from class ptolemy.kernel.Entity

_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, _debug, _debug, _debug, _debug, _debug, _getIndentPrefix, _isMoMLSuppressed, _markContentsDerived, _propagateValue, _removeAttribute, _splitName, _stripNumericSuffix, addChangeListener, addDebugListener, attributeChanged, attributeList, attributeList, attributeTypeChanged, clone, 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, propagateValue, propagateValues, removeChangeListener, removeDebugListener, 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

Field Detail

_variableInfo

private java.util.HashMap<java.lang.String,FmvAutomaton.VariableInfo> _variableInfo

_variableTransitionInfo

private java.util.HashMap<java.lang.String,java.util.LinkedList<FmvAutomaton.VariableTransitionInfo>> _variableTransitionInfo

DOMAIN_GT

private static int DOMAIN_GT

DOMAIN_LS

private static int DOMAIN_LS

Constructor Detail

FmvAutomaton

public FmvAutomaton()

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)

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

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

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.

_decideVariableSet

private java.util.HashSet<java.lang.String> _decideVariableSet(int numSpan)
                                                        throws IllegalActionException

This private function first decides variables that would be used in the Kripke structure. Once when it is decided, it performs step 1 and 2 of the variable domain generation process.

Parameters:

numSpan - The size of the span used to expand the domain of a variable.

Returns:

a set indicating the variable used in this automaton

Throws:

IllegalActionException

_enumerateStateSet

private java.util.HashSet<State> _enumerateStateSet()
                                             throws IllegalActionException

Perform an enumeration of the state in this FmvAutomaton and return a HashSet of states.

Returns:

A HashSet of states of a particular FmvAutomaton

Throws:

IllegalActionException

_generateAllVariableTransitions

private void _generateAllVariableTransitions(java.util.HashSet<java.lang.String> variableSet)
                                      throws IllegalActionException

Generate all premise-action pairs regarding this FmvAutomaton. For example, this method may generate (state=red)&&(count=1):{grn}. This can only be applied when the domain of variable is decided.

Throws:

IllegalActionException

_generatePremiseAndResultEachTransition

private void _generatePremiseAndResultEachTransition(java.lang.String statePrecondition,
                                                     java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.Integer>> valueDomain,
                                                     java.lang.String lValue,
                                                     java.lang.String offset,
                                                     java.lang.String operatingSign)
                                              throws IllegalActionException

This function is used to generate detailed pre-conditions and post-conditions in .smv format. It is used by the function _generateAllVariableTransitions()

Throws:

IllegalActionException

_recursiveStepGeneratePremiseAndResultEachTransition

private void _recursiveStepGeneratePremiseAndResultEachTransition(java.lang.String currentPremise,
                                                                  int index,
                                                                  int maxIndex,
                                                                  java.lang.String[] keySetArray,
                                                                  java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.Integer>> valueDomain,
                                                                  java.lang.String lValue,
                                                                  java.lang.String newVariableValue,
                                                                  java.lang.String operatingSign)
                                                           throws IllegalActionException

A private function used as a recursive step to generate all premises for enabling transition in .smv file. In variable valueDomain, it specifies that for a particular transition, the set of all possible values to invoke the transition. Thus it is the duty of this recursive step function to generate all possible combinations. The function would try to attach correct premise and update correct new value for the variable set by the transition based on the original value.

Parameters:

currentPremise - Current precondition for the transition. It is not completed unless parameter index == maxIndex.

index - Current depth for the recursive function. It would stop when it reaches maxIndex.

maxIndex -

keySetArray - keySetArray stores all variable names that is used in this transition.

valueDomain - valueDomain specifies for a particular transition, for each variable, the set of all possible values to invoke the transition.

lValue - lValue specifies the variable name that would be set after the transition.

newVariableValue - newVariableValue can have different meanings based on different value of variable operatingSign. When operatingSign is +,-,*,/ it represents the offset. Remember in the set-action, each sub-statement has formats either var = var operatingSign offset or var = rValue. When operatingSign is S or N, it represents the rValue of the system.

operatingSign -

Throws:

IllegalActionException

_retrieveVariableInitialValue

private java.util.HashMap<java.lang.String,java.lang.String> _retrieveVariableInitialValue(java.util.HashSet<java.lang.String> variableSet)

A private function used as to generate variable initial values for the initial variable set. This is achieved using a scan on all transitions in edges (equalities/ inequalities) and retrieve all integer values in the system. Currently the span is not taken into consideration.

Parameters:

variableSet - Set of variables that expect to find initial values.