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:
- Proposed Rating:
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 |
SEMANTIC_FILE_PATH
private static final java.lang.String SEMANTIC_FILE_PATH
- See Also:
- Constant Field Values
RTMaudeUtility
public RTMaudeUtility()
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