Class REDUtility


  • @Deprecated
    public class REDUtility
    extends java.lang.Object
    Deprecated.
    ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.
    This is an utility for Ptolemy model conversion. It performs a systematic traversal of the system and convert the Ptolemy model into communicating timed automata (CTA) with the format acceptable by model checker RED (Regional Encoding Diagram Verification Engine, v.7.0).

    The conversion mechanism roughly is based on the technical report UCB/EECS-2008-41 with some modifications. Basically, the token would not be accumulated in the port of the FSMActor - therefore buffer overflow property would no longer exist in this implementation; it would only happen in the TimedDelay or NondeterministicTimedDelay actor.

    For a successful conversion, we simply disallow a system to have super dense time tag with the format (\tau, i), where i>0. In our context this only happens when there is a TimedDelay actor with its parameter equals to zero. For systems with super dense time tag with the format (\tau, i), where i>0, the system can still be converted. However, please note that the semantics might no longer be preserved.

    One important feature in our converted model is the use of "complementary" edges. This is used to handle the situation where the FSMActor must react to an arrival of token in the incoming port, but the token can not trigger any transition. For this case, the 'present' token should turn to be 'absent' as time advances. To avoid including any unnecessary behavior we add one "invalid" transition, mentioning that the FSMActor will perform a "stable" move, and at the same time the token will be bring to absent state.

    For the tool RED, all time constants should be an integer. This is not a problem because the unit is actually not specified by the timed automata. Therefore, we expect users to use integer values to specify their delay or period.

    Limitations: Simply following the statement in the technical report, we restate limitations of the conversion. The designer must understand the boundary of variable domain for the model under conversion. Also, due to the use of complementary edges, complex guard conditions are currently not supported.

    Since:
    Ptolemy II 8.0
    Version:
    $Id$
    Author:
    Chih-Hong Cheng, Contributor: Edward A. Lee
    Pt.AcceptedRating:
    Red (patrickj)
    Pt.ProposedRating:
    Red (patrickj)
    • Constructor Detail

      • REDUtility

        public REDUtility()
        Deprecated.
    • Method Detail

      • generateEquivalentSystemWithoutHierarchy

        public static CompositeActor generateEquivalentSystemWithoutHierarchy​(CompositeActor originalCompositeActor)
                                                                       throws java.lang.CloneNotSupportedException,
                                                                              IllegalActionException,
                                                                              NameDuplicationException
        Deprecated.
        This function generates an equivalent system which is flattened. It would perform a rewriting of each ModalModel with hierarchy to an FSMActor. Note that in our current implementation the rewriting only supports 'state refinements'.
        Parameters:
        originalCompositeActor - original system under processing
        Returns:
        a flattened equivalent system.
        Throws:
        java.lang.CloneNotSupportedException - If thrown while rewriting the modal model with state refinements to a FSMActor.
        IllegalActionException - If thrown while rewriting the modal model with state refinements to a FSMActor.
        NameDuplicationException - If thrown while rewriting the modal model with state refinements to a FSMActor.
      • generateREDDescription

        public static java.lang.StringBuffer generateREDDescription​(CompositeActor PreModel,
                                                                    java.lang.String pattern,
                                                                    MathematicalModelConverter.FormulaType choice,
                                                                    int span,
                                                                    int bufferSizeDelayActor)
                                                             throws IllegalActionException,
                                                                    NameDuplicationException,
                                                                    java.lang.CloneNotSupportedException
        Deprecated.
        This is the main function which generates the system description which is acceptable by the tool RED (Regional Encoding Diagram).

        For hierarchical conversion, here we are able to deal with cases where state refinement exists. For a modalmodel with state refinement, we first rewrite it into an equivalent FSMActor.

        Parameters:
        PreModel - The original model in Ptolemy II
        pattern - The temporal formula in TCTL
        choice - Specify the type of formula: buffer overflow detection or general TCTL formula
        span - The size of the span used for domain analysis.
        bufferSizeDelayActor - The buffer size of the TimedDelay actor.
        Returns:
        A Communicating Timed Automata system description of the original system
        Throws:
        java.lang.CloneNotSupportedException - If thrown while generating an equivalent system without hierarchy.
        IllegalActionException - If there is a problem generating the RED description.
        NameDuplicationException - If thrown while generating an equivalent system without hierarchy.
      • isValidModelForVerification

        public static boolean isValidModelForVerification​(CompositeActor model)
        Deprecated.
        This function decides if the director of the current actor is DE. If not, return false. This is because our current conversion to CTA is only valid when the director is DE.
        Parameters:
        model - Model used for testing.
        Returns:
        boolean value indicating if the director is DE.