ptolemy.domains.fsm.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.fsm.kernel.FSMActor
ptolemy.domains.fsm.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:
- Proposed Rating:
Fields inherited from class ptolemy.kernel.util.NamedObj |
_changeListeners, _changeLock, _changeRequests, _debugging, _debugListeners, _elementName, _isPersistent, _verbose, _workspace, ATTRIBUTES, CLASSNAME, COMPLETE, CONTENTS, DEEP, FULLNAME, LINKS |
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.fsm.kernel.FSMActor |
_addEntity, _addRelation, _commitLastChosenTransition, _isRefinementOutput, _readInputs, _setCurrentConnectionMap, addInitializable, attributeChanged, chooseTransition, clone, createReceivers, currentState, enabledTransitions, exportSubmodel, fire, getCausalityInterface, getContext, getDirector, getExecutiveDirector, getInitialState, 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.util.NamedObj |
_addAttribute, _adjustOverride, _attachText, _cloneFixAttributeFields, _debug, _debug, _debug, _debug, _debug, _getIndentPrefix, _isMoMLSuppressed, _markContentsDerived, _propagateValue, _removeAttribute, _splitName, _stripNumericSuffix, addChangeListener, addDebugListener, 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 |
_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
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.
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.