ptolemy.verification.kernel.maude
Class RTMaudeUtility

java.lang.Object
  ptolemy.verification.kernel.maude.RTMaudeUtility

public class RTMaudeUtility
extends java.lang.Object

This is an utility function for Ptolemy II models. It performs a systematic traversal of the system and generate Realtime Maude model file

Since:

Ptolemy II 8.0

Version:

$Id: RTMaudeUtility.java 57046 2010-01-27 23:35:53Z cxh $

Author:

Kyungmin Bae

Accepted Rating:

Red (kbae4)

Proposed Rating:

Red (kbae4)

Field Summary

private static java.lang.String

SEMANTIC_FILE_PATH

Constructor Summary

RTMaudeUtility()

Method Summary

private static void	_generateFormula(java.lang.StringBuffer returnRTMFormat, java.lang.String formula)
private static void	_generateModelBody(java.lang.StringBuffer returnRTMFormat, java.lang.String modelName, RTMList topconf)
private static void	_loadSemanticFiles(java.lang.StringBuffer buffer, boolean inline)
private static RTMObject	_translateActor(Actor act)
private static RTMList	_translateCompositeEntity(CompositeEntity cent, java.util.HashSet<Actor> exc)
private static RTMObject	_translatePort(Port port)
private static RTMTerm	_translateTransition(Transition tr)
static java.lang.StringBuffer	generateRTMDescription(java.io.BufferedReader template, CompositeActor model, java.lang.String formula) Return a StringBuffer that contains the converted .maude format of the system.
static java.lang.StringBuffer	generateRTMDescription(CompositeActor model, java.lang.String formula, boolean inlineFilesIfPossible) Return a StringBuffer that contains the converted .maude format of the system.
private static RTMTerm	portName(NamedObj upper, Port p)
private static RTMTerm	procRefinements(java.lang.String name, Actor[] rfs, java.lang.String identifier, java.util.HashSet<Actor> inact)

Methods inherited from class java.lang.Object

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

Field Detail

SEMANTIC_FILE_PATH

private static final java.lang.String SEMANTIC_FILE_PATH

See Also:

Constant Field Values

Constructor Detail

RTMaudeUtility

public RTMaudeUtility()

Method Detail

generateRTMDescription

public static java.lang.StringBuffer generateRTMDescription(CompositeActor model,
                                                            java.lang.String formula,
                                                            boolean inlineFilesIfPossible)
                                                     throws IllegalActionException,
                                                            NameDuplicationException

Return a StringBuffer that contains the converted .maude format of the system.

Parameters:

model - The system under analysis.

formula -

Returns:

The converted .maude format of the system.

Throws:

IllegalActionException

NameDuplicationException

generateRTMDescription

public static java.lang.StringBuffer generateRTMDescription(java.io.BufferedReader template,
                                                            CompositeActor model,
                                                            java.lang.String formula)
                                                     throws IllegalActionException,
                                                            NameDuplicationException

Return a StringBuffer that contains the converted .maude format of the system.

Parameters:

model - The system under analysis.

formula -

Returns:

The converted .maude format of the system.

Throws:

IllegalActionException

NameDuplicationException

_generateFormula

private static void _generateFormula(java.lang.StringBuffer returnRTMFormat,
                                     java.lang.String formula)

_generateModelBody

private static void _generateModelBody(java.lang.StringBuffer returnRTMFormat,
                                       java.lang.String modelName,
                                       RTMList topconf)

_loadSemanticFiles

private static void _loadSemanticFiles(java.lang.StringBuffer buffer,
                                       boolean inline)
                                throws IllegalActionException

Throws:

IllegalActionException

_translateActor

private static RTMObject _translateActor(Actor act)
                                  throws IllegalActionException

Throws:

IllegalActionException

_translateCompositeEntity

private static RTMList _translateCompositeEntity(CompositeEntity cent,
                                                 java.util.HashSet<Actor> exc)
                                          throws IllegalActionException

Throws:

IllegalActionException

_translatePort

private static RTMObject _translatePort(Port port)

_translateTransition

private static RTMTerm _translateTransition(Transition tr)
                                     throws IllegalActionException

Throws:

IllegalActionException

portName

private static RTMTerm portName(NamedObj upper,
                                Port p)

procRefinements

private static RTMTerm procRefinements(java.lang.String name,
                                       Actor[] rfs,
                                       java.lang.String identifier,
                                       java.util.HashSet<Actor> inact)
                                throws IllegalActionException

Throws:

IllegalActionException