ptolemy.verification.kernel
Class SMVUtility

java.lang.Object
  ptolemy.verification.kernel.SMVUtility

public class SMVUtility
extends java.lang.Object

This is an utility function for Ptolemy II models. It performs a systematic traversal of the system and generate NuSMV (or Cadence SMV) acceptable files for model checking.

FIXME: A new version for users to specify the integer bound without using abstraction of "LS" and "GT" should be implemented to support complicated update functions. Note that this has already been implemented in REDUtility.java since the format of RED 7.0 does not support these features.

Since:

Ptolemy II 8.0

Version:

$Id: SMVUtility.java 59167 2010-09-21 17:08:02Z cxh $

Author:

Chih-Hong Cheng, Contributor: Edward A. Lee, Christopher Brooks

Accepted Rating:

Red (patrickj)

Proposed Rating:

Red (patrickj)

Nested Class Summary

private static class	SMVUtility.VariableInfo
private static class	SMVUtility.VariableTransitionInfo

Field Summary

private static java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.String>>	_globalSignalDistributionInfo
private static java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>>	_globalSignalNestedRetrivalInfo
private static java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>>	_globalSignalRetrivalInfo
private static java.util.HashMap<java.lang.String,SMVUtility.VariableInfo>	_variableInfo
private static java.util.HashMap<java.lang.String,java.util.LinkedList<SMVUtility.VariableTransitionInfo>>	_variableTransitionInfo
private static int	DOMAIN_GT
private static int	DOMAIN_LS

Constructor Summary

SMVUtility()

Method Summary

private static java.util.HashSet<java.lang.String>	_decideGuardSignalVariableSet(FSMActor actor) This private function first decides signals used in the guard expression of an actor.
private static java.util.HashSet<java.lang.String>	_decideSignalVariableSet(FSMActor actor) This private function first decides signal variables that is emitted from the actor.
private static java.util.HashSet<java.lang.String>	_decideStateVariableSet(FSMActor actor, int numSpan) This private function first decides state variables (or called inner variables) that would be used in the Kripke structure.
private static java.util.HashSet<State>	_enumerateStateSet(FSMActor actor) Perform an enumeration of the state in this FmvAutomaton and return a HashSet of states.
private static void	_generateAllVariableTransitions(FSMActor actor, java.util.HashSet<java.lang.String> variableSet) Generate all premise-action pairs regarding this automaton.
private static java.util.HashSet<java.lang.String>	_generateGraphicalSpecificationRecursiveStep(CompositeActor model, java.lang.String specType, java.lang.StringBuffer upperLevelStatement)
private static 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 static void	_generatePremiseAndResultEachTransitionRecursiveStep(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 static java.util.ArrayList<java.lang.StringBuffer>	_generateSMVDescriptionModalModelWithRefinement(ModalModel modalmodel, java.lang.String span, java.lang.String upperStateName) This function generates the Kripke structure acceptable by NuSMV from a ModalModel in Ptolemy II.
private static java.lang.StringBuffer	_generateSMVDescriptionSubSystem(CompositeActor model, java.lang.String span, java.lang.String upperStateName) This private function generates the system description of a subsystem which has a ModalModel controller as its upper-layer.
private static java.util.ArrayList<java.lang.String>	_prescanSystemSignal(CompositeActor model, java.lang.String span) Perform a systematic pre-scan to obtain information regarding the visibility of a signal.
private static java.util.ArrayList<java.lang.StringBuffer>	_retrieveSubSystemModuleNameParameterInfo(FSMActor controller) This function is trying to generate the definition for modules contained in a controller.
private static java.util.HashMap<java.lang.String,java.lang.String>	_retrieveVariableInitialValue(FSMActor actor, java.util.HashSet<java.lang.String> variableSet) A private function used as to generate variable initial values for the initial variable set.
private static java.lang.StringBuffer	_translateSingleFSMActor(FSMActor actor, java.lang.String span, boolean isController, java.lang.String refinementStateName) Translate a single FSMActor into the format acceptable by model checker.
static java.lang.String	generateGraphicalSpecification(CompositeActor model, java.lang.String specType) This function generates the reachability/risk specification of a system by scanning through the subsystem, and extract states which have special risk or reachability labels.
static java.lang.StringBuffer	generateSMVDescription(CompositeActor model, java.lang.String pattern, java.lang.String choice, java.lang.String span) Return a StringBuffer that contains the converted .smv format of the system.
static boolean	isValidModelForVerification(CompositeActor model) This function decides if the director of the current actor is SR.

Methods inherited from class java.lang.Object

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

Field Detail

_globalSignalDistributionInfo

private static java.util.HashMap<java.lang.String,java.util.ArrayList<java.lang.String>> _globalSignalDistributionInfo

_globalSignalRetrivalInfo

private static java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> _globalSignalRetrivalInfo

_globalSignalNestedRetrivalInfo

private static java.util.HashMap<java.lang.String,java.util.HashSet<java.lang.String>> _globalSignalNestedRetrivalInfo

_variableInfo

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

_variableTransitionInfo

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

DOMAIN_GT

private static int DOMAIN_GT

DOMAIN_LS

private static int DOMAIN_LS

Constructor Detail

SMVUtility

public SMVUtility()

Method Detail

generateGraphicalSpecification

public static java.lang.String generateGraphicalSpecification(CompositeActor model,
                                                              java.lang.String specType)
                                                       throws IllegalActionException

This function generates the reachability/risk specification of a system by scanning through the subsystem, and extract states which have special risk or reachability labels.

Parameters:

model - The system model under analysis.

specType - The type of the graphical specification, it may be either "Risk" or "Reachability"

Returns:

A string indicating the CTL formula for risk/reachability analysis.

Throws:

IllegalActionException

generateSMVDescription

public static java.lang.StringBuffer generateSMVDescription(CompositeActor model,
                                                            java.lang.String pattern,
                                                            java.lang.String choice,
                                                            java.lang.String span)
                                                     throws IllegalActionException,
                                                            NameDuplicationException

Return a StringBuffer that contains the converted .smv format of the system. Current algorithm uses a modular approach for construction, enabling us to deal with hierarchical systems. Also recognition of Boolean tokens is supported.

For previous implementation, no matter what token is sent through the channel, the receiver only senses the existence of the token by the guard expression XX_isPresent. We now support Boolean token recognition.

In order to introduce this mechanism, for each signal XX, two boolean variables are introduced:
1) XX_isPresent: indicating whether the signal is present or not.
2) XX_value: indicating the value of the signal.

Therefore, now in the guard expression, it may be possible to have
1) XX_isPresent (in Ptolemy) ==> XX_isPresent (in SMV)
2) XX == 0 (in Ptolemy) ==> XX_isPresent && XX_value == 0 (in SMV)
3) XX == 1 (in Ptolemy) ==> XX_isPresent && XX_value == 1 (in SMV)

If XX_isPresent is false, then the value of XX_value is not valid.

In SMV, there is no distinguishing between boolean T, F and numerical values 1, 0. So for the sender side, we only need to check if a sender sends a token whose value is not 0 or 1.

Parameters:

model - The system under analysis.

pattern - 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 domain of the variable.

Returns:

The converted .smv format of the system.

Throws:

IllegalActionException

NameDuplicationException

isValidModelForVerification

public static boolean isValidModelForVerification(CompositeActor model)

This function decides if the director of the current actor is SR. If not, return false. This is because our current analysis is only valid when the director is SR.

Parameters:

model - Model used for testing.

Returns:

a boolean value indicating if the director is SR.

_decideGuardSignalVariableSet

private static java.util.HashSet<java.lang.String> _decideGuardSignalVariableSet(FSMActor actor)
                                                                          throws IllegalActionException

This private function first decides signals used in the guard expression of an actor. Those signals should be of the format XX_isPresent. If it is of the format XX == const, we need to check if XX is in the initial parameter list. If yes, then it is a state variable; if not, then it is a signal variable, then use "X_isPresent" or "X_value" to represent it.

Parameters:

actor - The actor under analysis.

Returns:

The set of signals used in the guard expression of the actor.

Throws:

IllegalActionException

_decideSignalVariableSet

private static java.util.HashSet<java.lang.String> _decideSignalVariableSet(FSMActor actor)
                                                                     throws IllegalActionException

This private function first decides signal variables that is emitted from the actor. Note that signal variables only appears in outputActions. In order to keep the signal "X" compatible with the appearance in the guard expression "X_isPresent" shown in other actors, we need to attach "_isPresent" with the signal.

MODIFICATION 2008.07.21: We need to have "X_isPresent" and "X_value" to represent a variable for new features (supporting boolean tokens).

Parameters:

actor - The actor under analysis

Returns:

A set containing names of the signal

Throws:

IllegalActionException

_decideStateVariableSet

private static java.util.HashSet<java.lang.String> _decideStateVariableSet(FSMActor actor,
                                                                           int numSpan)
                                                                    throws IllegalActionException

This private function first decides state variables (or called inner variables) that would be used in the Kripke structure. It would first perform a system prescan to have a rough domain for each variable. Then it expands the domain by using the constant span.

Parameters:

actor - The actor under analysis

numSpan - The size to expand the original domain

Returns:

The state variable set.

Throws:

IllegalActionException

_enumerateStateSet

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

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

Parameters:

actor - The actor under analysis

Returns:

A HashSet of states of a particular FSMActor

Throws:

IllegalActionException

_generateAllVariableTransitions

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

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

Parameters:

actor - The actor under analysis

variableSet - The set of variables used

Throws:

IllegalActionException

_generateGraphicalSpecificationRecursiveStep

private static java.util.HashSet<java.lang.String> _generateGraphicalSpecificationRecursiveStep(CompositeActor model,
                                                                                                java.lang.String specType,
                                                                                                java.lang.StringBuffer upperLevelStatement)
                                                                                         throws IllegalActionException

Throws:

IllegalActionException

_generatePremiseAndResultEachTransition

private static 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()

Parameters:

statePrecondition -

valueDomain -

lValue -

offset -

operatingSign -

Throws:

IllegalActionException

_generatePremiseAndResultEachTransitionRecursiveStep

private static void _generatePremiseAndResultEachTransitionRecursiveStep(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

_generateSMVDescriptionModalModelWithRefinement

private static java.util.ArrayList<java.lang.StringBuffer> _generateSMVDescriptionModalModelWithRefinement(ModalModel modalmodel,
                                                                                                           java.lang.String span,
                                                                                                           java.lang.String upperStateName)
                                                                                                    throws IllegalActionException,
                                                                                                           NameDuplicationException

This function generates the Kripke structure acceptable by NuSMV from a ModalModel in Ptolemy II. Here modular approach is applied to eliminate complexity of the conversion process.

Parameters:

modalmodel - ModalModel under analysis

span - The size to expand the original domain

upperStateName -

Throws:

IllegalActionException

NameDuplicationException

_generateSMVDescriptionSubSystem

private static java.lang.StringBuffer _generateSMVDescriptionSubSystem(CompositeActor model,
                                                                       java.lang.String span,
                                                                       java.lang.String upperStateName)
                                                                throws IllegalActionException,
                                                                       NameDuplicationException

This private function generates the system description of a subsystem which has a ModalModel controller as its upper-layer.

Parameters:

model - The subsystem which is the refinement of a state.

span - The size of span to expand the domain of variable.

upperStateName - The name of the upper level model name. This upper state has the model as refinement.

Returns:

The StringBuffer description of the subsystem acceptable by the model checker.

Throws:

IllegalActionException

NameDuplicationException

_prescanSystemSignal

private static java.util.ArrayList<java.lang.String> _prescanSystemSignal(CompositeActor model,
                                                                          java.lang.String span)
                                                                   throws IllegalActionException,
                                                                          NameDuplicationException

Perform a systematic pre-scan to obtain information regarding the visibility of a signal. See the description in the source code for technical details.

Parameters:

model - The whole system under analysis

span - The number to expand the domain of a variable. Note that it is in fact irrelevant to the signal generation. It is only used for the reuse of existing functions.

Returns:

An array of Strings that contains the pre-scan results.

Throws:

IllegalActionException

NameDuplicationException

_retrieveSubSystemModuleNameParameterInfo

private static java.util.ArrayList<java.lang.StringBuffer> _retrieveSubSystemModuleNameParameterInfo(FSMActor controller)
                                                                                              throws IllegalActionException

This function is trying to generate the definition for modules contained in a controller. It need to check whether a signal is visible by the controller. If not, then this signal should be passed from outside, and the required signal set (extended by guard signals) for the controller should add up this signal. If a signal is visible by the controller, then we know that this signal is only passed between modules of the controller. We can list out the location of the signal.

Parameters:

controller - The controller which contains those modules

Returns:

An ArrayList containing all submodule definitions

Throws:

IllegalActionException - Undefined behavior happens.

_retrieveVariableInitialValue

private static java.util.HashMap<java.lang.String,java.lang.String> _retrieveVariableInitialValue(FSMActor actor,
                                                                                                  java.util.HashSet<java.lang.String> variableSet)
                                                                                           throws IllegalActionException

A private function used as to generate variable initial values for the initial variable set. The current approach is to retrieve from the parameter specified in the actor.

Parameters:

actor - The actor under analysis

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

Returns:

A HashMap indicating the pair (variable name, initial value).

Throws:

IllegalActionException

_translateSingleFSMActor

private static java.lang.StringBuffer _translateSingleFSMActor(FSMActor actor,
                                                               java.lang.String span,
                                                               boolean isController,
                                                               java.lang.String refinementStateName)
                                                        throws IllegalActionException

Translate a single FSMActor into the format acceptable by model checker. New functionalities for supporting boolean-token recognition are added.

Parameters:

actor - The FSMActor under analysis.

span - The constant span for expanding the integer domain for state (inner) variables

isController - Whether the FSMActor is the controller of a ModalModel

refinementStateName - The name of the refinement state

Returns:

The translated actor in a format suitable for the model checker.

Throws:

IllegalActionException