ptolemy.verification.kernel

Class REDUtility

java.lang.Object

ptolemy.verification.kernel.REDUtility

Deprecated.

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

@Deprecated
public class REDUtility
extends java.lang.Object

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: REDUtility.java 70402 2014-10-23 00:52:20Z cxh $

Author:

Chih-Hong Cheng, Contributor: Edward A. Lee

Accepted Rating:

Red (patrickj)

Proposed Rating:

Red (patrickj)

Constructor Summary

Constructors

Constructor and Description
REDUtility() Deprecated.

Method Summary

Modifier and Type	Method and Description
static CompositeActor	generateEquivalentSystemWithoutHierarchy(CompositeActor originalCompositeActor) Deprecated. This function generates an equivalent system which is flattened.
static java.lang.StringBuffer	generateREDDescription(CompositeActor PreModel, java.lang.String pattern, MathematicalModelConverter.FormulaType choice, int span, int bufferSizeDelayActor) Deprecated. This is the main function which generates the system description which is acceptable by the tool RED (Regional Encoding Diagram).
static boolean	isValidModelForVerification(CompositeActor model) Deprecated. This function decides if the director of the current actor is DE.

Methods inherited from class java.lang.Object

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

Constructor Detail

REDUtility

public REDUtility()

Deprecated.

Method Detail

generateEquivalentSystemWithoutHierarchy

public static CompositeActor generateEquivalentSystemWithoutHierarchy(CompositeActor originalCompositeActor)
                                                               throws NameDuplicationException,
                                                                      IllegalActionException,
                                                                      java.lang.CloneNotSupportedException

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:

NameDuplicationException

IllegalActionException

java.lang.CloneNotSupportedException

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:

IllegalActionException

NameDuplicationException

java.lang.CloneNotSupportedException

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.