ptolemy.verification.kernel

Class SMVUtility

java.lang.Object

ptolemy.verification.kernel.SMVUtility

Deprecated.

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

@Deprecated
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$

Author:

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

Pt.AcceptedRating:

Red (patrickj)

Pt.ProposedRating:

Red (patrickj)

Constructor Summary

Constructors

Constructor and Description
SMVUtility() Deprecated.

Method Summary

Modifier and Type	Method and Description
static java.lang.String	generateGraphicalSpecification(CompositeActor model, java.lang.String specType) Deprecated. 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) Deprecated. Return a StringBuffer that contains the converted .smv format of the system.
static boolean	isValidModelForVerification(CompositeActor model) Deprecated. 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

Constructor Detail

SMVUtility

public SMVUtility()

Deprecated.

Method Detail

generateGraphicalSpecification

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

Deprecated.

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

Deprecated.

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)

Deprecated.

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.