Package ptolemy.verification.kernel

Class SMVUtility

  • @Deprecated
public class SMVUtility
extends java.lang.Object
    Deprecated.
    ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.
    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 Description
      SMVUtility()
      Deprecated.
       

    • Method Summary

      All Methods Static Methods Concrete Methods Deprecated Methods 
      Modifier and Type Method 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.