Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES
SUMMARY:  INNER | FIELD | CONSTR | METHOD DETAIL:  FIELD | CONSTR | METHOD

Class FlatDocumentWriter

java.lang.Object
  |
  +--DocumentReader
        |
        +--DocumentWriter
              |
              +--FlatDocumentWriter
public class FlatDocumentWriter
extends DocumentWriter

This class is used to abstract away from dtd changes when creating the flat document (in uppaalDTD grammar).

Usage

All changes and additions to the document are done via method calls to The main method is complete(), that

Version:
Vanilla-1 Mon Apr 9 15:40:40 2001
Author:
M. Oliver Möller

Field Summary
private  boolean completed
          Keeping track, whether the full-translation is already done
private  org.w3c.dom.Element declaration
           
(package private) static java.lang.StringBuffer declarationText
          Text inserted in the (flat) declaration label.

Contains original global variables plus flattening slack like newly introduced channels etc.
private static java.util.Hashtable hashIDsToNewLocationElements
          Store all newly generated (flat) locations.
Requires the use of the methods inventLocation(java.lang.String) and changeLocationID(org.w3c.dom.Element, java.lang.String) in order to work properly.
private  org.w3c.dom.Element instantiation
           
(package private) static java.lang.StringBuffer instantiationText
          Text describing the Instantiations of templates used for the system.
static boolean inventNewGoegraphicalLocations
          If true, ignore the x/y-information given in the (hierarchical) templates and use a default-layout.

This is possible, if using only the method inventLocation(java.lang.String) for creation of new locations.
 java.lang.String kickOffDoneID
          Id of kickoff location, where every direct child of the root is activated.

Needed for global exits.
 org.w3c.dom.Element kickOffTemplate
          Store kickoff template Element, once crated...
(package private)  Layouter layouter
          Module for Layout (Re-)Computations (post-processing)
private  org.w3c.dom.Element root
          Root of DocumentWriter.doc
(package private) static java.util.Stack slackInstantiations
          A vector of Strings that are to be added to the (global) instantiation
private  org.w3c.dom.Element system
           
protected  java.util.Stack systemComponents
          Store all (instantiated) component of the system by the name String
private  java.lang.StringBuffer systemText
          Text declaring the flat system.
Accumulates all the timed automata executed in parallel.
protected  java.util.Stack templates
          Templates that are to be instantiated at some point
(package private) static java.lang.String uppaalDTD
          Version of the flat uppaal grammar that is used.
(package private) static java.lang.String uppaalDTD_URI
          Used DTD for flat Uppaal documents.
Give the http:// or file:/ location
(package private) static boolean useLabelConstruct
          Determines whether translations uses the <label> construct or not.

From uppaal-1.4 / uppaal-3-1-39 on, this should be true.
(package private) static boolean useLabelForInvariants
          Determines whether grammar uses the <label> construct also for invariants.
 
Fields inherited from class DocumentWriter
CHANNEL_SEPARATOR, debug, doc, geoCount, geoXOffset, geoYOffset, globalGeoXOffset, globalGeoYOffset, idNameCount, locationNameCount, locNameXOffset, locNameYOffset, NAME_SEPARATOR_CHAR, SAFE_SEPARATOR_CHAR, sanityChecks, synchronisationNameCount, templateNameCount
 
Fields inherited from class DocumentReader
hashOriginalIDsToElements, origDoc
 
Constructor Summary
FlatDocumentWriter()
          Default Constructor
 
Method Summary
protected  org.w3c.dom.Element addAssignmentToTransition(org.w3c.dom.Element el)
          Add an assigment to a transition (as a child).
Returns the assignment Element.
protected  org.w3c.dom.Element addAssignmentToTransition(org.w3c.dom.Element el, java.lang.String assText)
          Add an assigment to a transition (as a child), including some initial text
Returns the assignment Element.
 void addDeclaration(java.lang.String s)
          Add just a declaration (e.g.
 void addDeclarationText(java.lang.String s)
          Append some declaration (purely textual)
protected  org.w3c.dom.Element addGuardToTransition(org.w3c.dom.Element el)
          Add a guard to a transition (as a child).
Returns the guard Element.
protected  org.w3c.dom.Element addGuardToTransition(org.w3c.dom.Element el, java.lang.String guardText)
          Add a guard to a transition (as a child), including some guard text
Returns the guard Element.
 void addInformationAboutTranslation(InstantiationTree tree)
           
 void addInstantiation(TextualInstantiation tinst)
          Arrange that a new instantiation is created.
This means, that the template (if not present) is added and the instantiations and the system are updated.
 void addLocationToTemplate(org.w3c.dom.Element loc, org.w3c.dom.Element template)
          Add a location at the right place.

Throws Exception, if the second argument is not a template.
 org.w3c.dom.Element addNameToTemplate(org.w3c.dom.Element name, org.w3c.dom.Element template)
          Add a name element at the right place.

Throws Exception, if the second argument is not a template or a name element exits.

Returns the name Element.
 void addParameterToTemplate(org.w3c.dom.Element par, org.w3c.dom.Element template)
          Add a parameter element at the right place.

Throws Exception, if the second argument is not a template or a parameter element exits.
protected  void addReceiveSynchronisationToTransition(java.lang.String channelName, org.w3c.dom.Element el)
          Add a ?-synchronisation (without caring about graphical information)

Assumes that the argument is a transition
protected  void addSendSynchronisationToTransition(java.lang.String channelName, org.w3c.dom.Element el)
          Add a !-synchronisation (without caring about graphical information)

Assumes that the argument is a transition
 void addSourceToTransition(org.w3c.dom.Element source, org.w3c.dom.Element transition)
          Add a source to a transition in the right place.
protected  org.w3c.dom.Element addSynchronisationToTransition(org.w3c.dom.Element el)
          Add a synchronisation to a transition (as a child).
Returns the synchronisation Element.
protected  org.w3c.dom.Element addSynchronisationToTransition(java.lang.String syncText, org.w3c.dom.Element el)
          Add a synchronisation to a transition (as a child), including some initial text.
Returns the synchronisation Element.
 void addTargetToTransition(org.w3c.dom.Element target, org.w3c.dom.Element transition)
          Add a target to a transition in the right place.
private  void addTemplate(org.w3c.dom.Element template)
          Add a new template
 void addTextualInvariantToLocation(org.w3c.dom.Element loc, java.lang.String invariantText)
          Add an (textual) invariant at the right place.
If an invariant already existsm conjunct it logically.
 void addTransitionToTemplate(org.w3c.dom.Element transition, org.w3c.dom.Element template)
          Append a transition to the template as a child at the right place
 void appendTextToTextualContentOfElement(org.w3c.dom.Element el, java.lang.String text)
          Appends some text to the #PCDATA, that is associated with this element (i.e in between <element></element>).
Relies on method "normalize" to join adjacent child text nodes.
protected  void changeLocationID(org.w3c.dom.Element el, java.lang.String newID)
          Changes the id-attribute of the location, but also updates the hashtable hashIDsToNewLocationElements
protected  void changeSyncTextAtTransition(org.w3c.dom.Element transition, java.lang.String newText)
          Change synchronization text of a transtion.
 void cleanupTransitionLabels()
          Browse through all transitions (the ones already in the document),
and remove empty labels sort labels in guard-sync-assignment
 org.w3c.dom.Element cloneTransition(org.w3c.dom.Element transition)
          Create a clone of a transition Element and add it in the appropriate template.
Returns the clone.
 void complete()
          Main Method
 void conjunctTextualAssignmentToTransition(org.w3c.dom.Element transition, java.lang.String text)
          Adds some assignment text to a transition, i.e.
 void conjunctTextualGuardToTransition(org.w3c.dom.Element transition, java.lang.String text)
          Adds some guard text to a transition, i.e.
 void copyChannelDeclaration(java.lang.String oldChanName, java.lang.String newChanName)
          Search declarations (Existing text) for declaration of a channel old (chan or urgent chan) and declare a channel of the same type, with new name.

Throws exception, if declaration of the old channel is not found.
protected  org.w3c.dom.Element createAssignment()
          Creates an assignment Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="assignment"

actual choice depends on useLabelConstruct.
protected  org.w3c.dom.Element createAssignmentInheritingCoordinates(org.w3c.dom.Element transition)
          Create and append an assignment Element to a transition.
Return this Element
protected  org.w3c.dom.Element createDeclaration(java.lang.String declarationText)
          Create a new declaration element
If the argument is empty, the element will be empty
protected  org.w3c.dom.Element createElement(java.lang.String type)
          Create an element particular to the flat hierarchical document
protected  org.w3c.dom.Element createGuard()
          Creates a guard Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="guard"

actual choice depends on useLabelConstruct.
protected  org.w3c.dom.Element createGuardInheritingCoordinates(org.w3c.dom.Element transition)
          Create and append an guard Element to a transition.
Return this Element
 void createHurryDummy()
          Create a dummy automaton trying constantly to synchronize on an urgent channel
protected  org.w3c.dom.Element createInvariant()
          Creates a invariant Element.

From some later uppaal versions on, this might be a label with attribute

kind="invariant"

!LABEL!, see useLabelForInvariants.
 org.w3c.dom.Element createKickTemplate(java.util.Vector rootEntrySignals)
          Create the kickoff-templates, that starts the global process.
protected  org.w3c.dom.Element createNameElement(java.lang.String name)
          Returns a Element that is a name tag with specified content
protected  org.w3c.dom.Element createParameter(java.util.Vector parameters)
          Create a new parameter element
The argument is a Vector of Strings -
protected  org.w3c.dom.Element createSource(java.lang.String locID)
          Creates a (flat document) source Element and sets the attribute ref.

The attriubte exitref remains unset.
protected  org.w3c.dom.Element createSynchronisation()
          Creates a synchronisation Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="synchronisation"

actual choice depends on useLabelConstruct.
protected  org.w3c.dom.Element createSynchronisationInheritingCoordinates(org.w3c.dom.Element transition)
          Create and append an synchronisation Element to a transition.
Return this Element
protected  org.w3c.dom.Element createTarget(org.w3c.dom.Element locationOrComponent)
          Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.
protected  org.w3c.dom.Element createTarget(java.lang.String locID)
          Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.
 org.w3c.dom.Element createTemplate()
          Returns a (fresh) template node and insert it in the list of known templates.
protected  org.w3c.dom.Element createTransition(java.lang.String sourceID, java.lang.String targetID)
          Returns a basic transition, given source and target id
protected  org.w3c.dom.Element createTransitionChildInheritingCoordinates(org.w3c.dom.Element transition, java.lang.String childType)
          Create and append a child Element to a transition.
Return this Element
 org.w3c.dom.Element createTransitionInTemplate(org.w3c.dom.Element template)
          Returns a (fresh) template node and insert it in the list of known templates.
private  void generateEndTemplateSemaphores()
          Insert a comment line at the end of every template.

(To be called after completion).
 java.util.Vector getAllTransitionsLeadingToLocation(org.w3c.dom.Element loc)
          Returns a Vector, where all the (immediate) transitions to a specific location are stored.

Should be called only after all transitions are created!
 java.util.Vector getAllTransitionsStartingAtLocation(org.w3c.dom.Element loc)
          Returns a Vector, where all the (immediate) transitions from a specific location are stored.

Should be called only after all transitions are created!
 org.apache.crimson.tree.XmlDocument getDoc()
          Return the (completed) XMLDocument
static org.w3c.dom.Element getTheChildThatIsAssignmentIfExists(org.w3c.dom.Element transition)
          Return the child label Element, that is an assignment.
static org.w3c.dom.Element getTheChildThatIsGuardIfExists(org.w3c.dom.Element transition)
          Return the child label Element, that is an guard.
static org.w3c.dom.Element getTheChildThatIsInvariantIfExists(org.w3c.dom.Element location)
          Return the child label Element, that is an invariant.
static org.w3c.dom.Element getTheChildThatIsSynchronisationIfExists(org.w3c.dom.Element transition)
          Return the child label Element, that is an synchronisation.
protected  org.w3c.dom.Element inventLocation()
          Create a new unique location without caring about the name (Exception is never really thrown)
protected  org.w3c.dom.Element inventLocation(java.lang.String name)
          Create a new unique location with a specified name
 org.w3c.dom.Element inventLocationInTemplate(org.w3c.dom.Element template)
          Invent a new location and append it to the specified (flat) template.
 org.w3c.dom.Element inventLocationInTemplate(java.lang.String name, org.w3c.dom.Element template)
          Invent a new named location and append it to the specified (flat) template.
static boolean isAssignment(org.w3c.dom.Element el)
          Test, whether this is an assignment Element.

Depends on useLabelConstruct.
static boolean isGuard(org.w3c.dom.Element el)
          Test, whether this is an guard Element.

Depends on useLabelConstruct.
static boolean isInvariant(org.w3c.dom.Element el)
          Test, whether this is an invariant Element.

Depends on useLabelForInvariants.
static boolean isSynchronisation(org.w3c.dom.Element el)
          Test, whether this is an synchronisation Element.

Depends on useLabelConstruct.
protected  void makeLocationCommitted(org.w3c.dom.Element el)
          Add a committed element
Throws an exception, if the element is not a location.

(might cause problems if called at the wrong time, for the order of child nodes matters in the uppaalDTD)
protected  void makeLocationInitial(org.w3c.dom.Element loc)
          NOTE: Only works, if location has been inserted in a template element alread!
private  boolean notACommentedLine(java.lang.String s)
          Check in String, whether the first line is a commented line (in terms of Uppaal Declarations)
Currently, every line where the first non-whitespace character is a '/' is consiered a comment line.
 void recomputeAllTemplateLayouts()
          Browse through all templates (the ones already in the documnent),
and call the Layouter method on them
static java.lang.String textuallyConjunctInvariants(java.lang.String inv1, java.lang.String inv2)
          Returns (texualy) a logical and of two invariant texts.
(does not manipulate the texts themselves)
 void writeToFile(java.lang.String fileName)
          Output the (current) flat document to a given file.
Old file contents, if any, are destroyed.
 
Methods inherited from class DocumentWriter
addCoordinatesToElement, addCoordinatesToElement, addDefaultLocationCoordinates, addIDToElement, addNameToElement, addTextualContentToElement, appendComment, freshLocationName, freshSynchronisationName, freshTemplateName, inventFreshID, makeIDSafe, makeNameSafe, makeSignalSafe, resetDefaultLayout, testGeoCordinates
 
Methods inherited from class DocumentReader
getAllChildrenWithLabel, getCdataOfElement, getElementByID, getElementID, getElementName, getFirstChildWithLabel, getFirstChildWithLabelIfExists, getTheChildWithLabel, getTheChildWithLabelIfExists, getXCoordinate, getYCoordinate, max, max, max3, max4, max5, memorizeIDsOfOriginalDocument, min
 
Methods inherited from class java.lang.Object
, clone, equals, finalize, getClass, hashCode, notify, notifyAll, registerNatives, toString, wait, wait, wait
 

Field Detail

useLabelConstruct

static final boolean useLabelConstruct
Determines whether translations uses the <label> construct or not.

From uppaal-1.4 / uppaal-3-1-39 on, this should be true.

useLabelForInvariants

static final boolean useLabelForInvariants
Determines whether grammar uses the <label> construct also for invariants.
For uppaal-1.4, this is false.

uppaalDTD

static final java.lang.String uppaalDTD
Version of the flat uppaal grammar that is used.

uppaalDTD_URI

static final java.lang.String uppaalDTD_URI
Used DTD for flat Uppaal documents.
Give the http:// or file:/ location

layouter

Layouter layouter
Module for Layout (Re-)Computations (post-processing)

root

private org.w3c.dom.Element root
Root of DocumentWriter.doc

declaration

private org.w3c.dom.Element declaration

instantiation

private org.w3c.dom.Element instantiation

system

private org.w3c.dom.Element system

inventNewGoegraphicalLocations

public static boolean inventNewGoegraphicalLocations
If true, ignore the x/y-information given in the (hierarchical) templates and use a default-layout.

This is possible, if using only the method inventLocation(java.lang.String) for creation of new locations. call DocumentWriter.resetDefaultLayout() when starting a new template

completed

private boolean completed
Keeping track, whether the full-translation is already done

(Currently, after a full translation, is is not possible any more to call a add-method)

templates

protected java.util.Stack templates
Templates that are to be instantiated at some point

systemText

private java.lang.StringBuffer systemText
Text declaring the flat system.
Accumulates all the timed automata executed in parallel. During construction, they are stored in systemComponents.

systemComponents

protected java.util.Stack systemComponents
Store all (instantiated) component of the system by the name String

slackInstantiations

static java.util.Stack slackInstantiations
A vector of Strings that are to be added to the (global) instantiation

!! might switch to more sophisticated data structure as content !!

See Also:
TextualInstantiation

instantiationText

static java.lang.StringBuffer instantiationText
Text describing the Instantiations of templates used for the system.

Currently, every template is instantiated exactly once

declarationText

static java.lang.StringBuffer declarationText
Text inserted in the (flat) declaration label.

Contains original global variables plus flattening slack like newly introduced channels etc.

kickOffTemplate

public org.w3c.dom.Element kickOffTemplate
Store kickoff template Element, once crated...

kickOffDoneID

public java.lang.String kickOffDoneID
Id of kickoff location, where every direct child of the root is activated.

Needed for global exits.

hashIDsToNewLocationElements

private static java.util.Hashtable hashIDsToNewLocationElements
Store all newly generated (flat) locations.
Requires the use of the methods inventLocation(java.lang.String) and changeLocationID(org.w3c.dom.Element, java.lang.String) in order to work properly.
Constructor Detail

FlatDocumentWriter

public FlatDocumentWriter()
Default Constructor
Method Detail

complete

public void complete()
              throws java.lang.Exception

Main Method

Triggers the translation of all added components.

getDoc

public org.apache.crimson.tree.XmlDocument getDoc()
                                           throws java.lang.Exception
Return the (completed) XMLDocument

addDeclarationText

public void addDeclarationText(java.lang.String s)
                        throws java.lang.Exception
Append some declaration (purely textual)

!! This might be more sophisticated at some point

addDeclaration

public void addDeclaration(java.lang.String s)
                    throws java.lang.Exception
Add just a declaration (e.g. "chan x")

copyChannelDeclaration

public void copyChannelDeclaration(java.lang.String oldChanName,
                                   java.lang.String newChanName)
                            throws java.lang.Exception
Search declarations (Existing text) for declaration of a channel old (chan or urgent chan) and declare a channel of the same type, with new name.

Throws exception, if declaration of the old channel is not found. !!! BUG: also finds 
/* ...
commented declarations !!!

notACommentedLine

private boolean notACommentedLine(java.lang.String s)
Check in String, whether the first line is a commented line (in terms of Uppaal Declarations)
Currently, every line where the first non-whitespace character is a '/' is consiered a comment line.
Assumes that the first line contains characters other than whitespace

addTemplate

private void addTemplate(org.w3c.dom.Element template)
                  throws java.lang.Exception
Add a new template

addInstantiation

public void addInstantiation(TextualInstantiation tinst)
                      throws java.lang.Exception
Arrange that a new instantiation is created.
This means, that the template (if not present) is added and the instantiations and the system are updated.

changeSyncTextAtTransition

protected void changeSyncTextAtTransition(org.w3c.dom.Element transition,
                                          java.lang.String newText)
                                   throws java.lang.Exception
Change synchronization text of a transtion.

addSendSynchronisationToTransition

protected void addSendSynchronisationToTransition(java.lang.String channelName,
                                                  org.w3c.dom.Element el)
                                           throws java.lang.Exception
Add a !-synchronisation (without caring about graphical information)

Assumes that the argument is a transition

!! Might be augmented with positioning information at some point

addReceiveSynchronisationToTransition

protected void addReceiveSynchronisationToTransition(java.lang.String channelName,
                                                     org.w3c.dom.Element el)
                                              throws java.lang.Exception
Add a ?-synchronisation (without caring about graphical information)

Assumes that the argument is a transition

!! Might be augmented with positioning information at some point

addAssignmentToTransition

protected org.w3c.dom.Element addAssignmentToTransition(org.w3c.dom.Element el)
                                                 throws java.lang.Exception
Add an assigment to a transition (as a child).
Returns the assignment Element.

addAssignmentToTransition

protected org.w3c.dom.Element addAssignmentToTransition(org.w3c.dom.Element el,
                                                        java.lang.String assText)
                                                 throws java.lang.Exception
Add an assigment to a transition (as a child), including some initial text
Returns the assignment Element.

addGuardToTransition

protected org.w3c.dom.Element addGuardToTransition(org.w3c.dom.Element el)
                                            throws java.lang.Exception
Add a guard to a transition (as a child).
Returns the guard Element.

addGuardToTransition

protected org.w3c.dom.Element addGuardToTransition(org.w3c.dom.Element el,
                                                   java.lang.String guardText)
                                            throws java.lang.Exception
Add a guard to a transition (as a child), including some guard text
Returns the guard Element.

addSynchronisationToTransition

protected org.w3c.dom.Element addSynchronisationToTransition(org.w3c.dom.Element el)
                                                      throws java.lang.Exception
Add a synchronisation to a transition (as a child).
Returns the synchronisation Element.

addSynchronisationToTransition

protected org.w3c.dom.Element addSynchronisationToTransition(java.lang.String syncText,
                                                             org.w3c.dom.Element el)
                                                      throws java.lang.Exception
Add a synchronisation to a transition (as a child), including some initial text.
Returns the synchronisation Element.

makeLocationCommitted

protected void makeLocationCommitted(org.w3c.dom.Element el)
                              throws java.lang.Exception
Add a committed element
Throws an exception, if the element is not a location.

(might cause problems if called at the wrong time, for the order of child nodes matters in the uppaalDTD)

makeLocationInitial

protected void makeLocationInitial(org.w3c.dom.Element loc)
                            throws java.lang.Exception
NOTE: Only works, if location has been inserted in a template element alread!

conjunctTextualGuardToTransition

public void conjunctTextualGuardToTransition(org.w3c.dom.Element transition,
                                             java.lang.String text)
                                      throws java.lang.Exception
Adds some guard text to a transition, i.e. builds the logical AND with its existing guard.
If no guard Element exists jet, one is created.

conjunctTextualAssignmentToTransition

public void conjunctTextualAssignmentToTransition(org.w3c.dom.Element transition,
                                                  java.lang.String text)
                                           throws java.lang.Exception
Adds some assignment text to a transition, i.e. append it to the (possibly empty) textual list of existing assignments.
If no assignement Element exists jet, one is created.

appendTextToTextualContentOfElement

public void appendTextToTextualContentOfElement(org.w3c.dom.Element el,
                                                java.lang.String text)
                                         throws java.lang.Exception
Appends some text to the #PCDATA, that is associated with this element (i.e in between <element></element>).
Relies on method "normalize" to join adjacent child text nodes.
See Also:
Node

addTransitionToTemplate

public void addTransitionToTemplate(org.w3c.dom.Element transition,
                                    org.w3c.dom.Element template)
Append a transition to the template as a child at the right place

cloneTransition

public org.w3c.dom.Element cloneTransition(org.w3c.dom.Element transition)
                                    throws java.lang.Exception
Create a clone of a transition Element and add it in the appropriate template.
Returns the clone.

Throws exception, if attempted to clone something different.

addSourceToTransition

public void addSourceToTransition(org.w3c.dom.Element source,
                                  org.w3c.dom.Element transition)
Add a source to a transition in the right place.

addTargetToTransition

public void addTargetToTransition(org.w3c.dom.Element target,
                                  org.w3c.dom.Element transition)
                           throws java.lang.Exception
Add a target to a transition in the right place.

addLocationToTemplate

public void addLocationToTemplate(org.w3c.dom.Element loc,
                                  org.w3c.dom.Element template)
                           throws java.lang.Exception
Add a location at the right place.

Throws Exception, if the second argument is not a template.

addParameterToTemplate

public void addParameterToTemplate(org.w3c.dom.Element par,
                                   org.w3c.dom.Element template)
                            throws java.lang.Exception
Add a parameter element at the right place.

Throws Exception, if the second argument is not a template or a parameter element exits.

addNameToTemplate

public org.w3c.dom.Element addNameToTemplate(org.w3c.dom.Element name,
                                             org.w3c.dom.Element template)
                                      throws java.lang.Exception
Add a name element at the right place.

Throws Exception, if the second argument is not a template or a name element exits.

Returns the name Element.

addTextualInvariantToLocation

public void addTextualInvariantToLocation(org.w3c.dom.Element loc,
                                          java.lang.String invariantText)
                                   throws java.lang.Exception
Add an (textual) invariant at the right place.
If an invariant already existsm conjunct it logically.
Throws Exception, if the first argument is not a location.

createTemplate

public org.w3c.dom.Element createTemplate()
                                   throws java.lang.Exception
Returns a (fresh) template node and insert it in the list of known templates.

Throws exception, if already finalized.

createTransitionInTemplate

public org.w3c.dom.Element createTransitionInTemplate(org.w3c.dom.Element template)
                                               throws java.lang.Exception
Returns a (fresh) template node and insert it in the list of known templates.

Throws exception, if already finalized.

createTransitionChildInheritingCoordinates

protected org.w3c.dom.Element createTransitionChildInheritingCoordinates(org.w3c.dom.Element transition,
                                                                         java.lang.String childType)
                                                                  throws java.lang.Exception
Create and append a child Element to a transition.
Return this Element

createAssignmentInheritingCoordinates

protected org.w3c.dom.Element createAssignmentInheritingCoordinates(org.w3c.dom.Element transition)
                                                             throws java.lang.Exception
Create and append an assignment Element to a transition.
Return this Element

createGuardInheritingCoordinates

protected org.w3c.dom.Element createGuardInheritingCoordinates(org.w3c.dom.Element transition)
                                                        throws java.lang.Exception
Create and append an guard Element to a transition.
Return this Element

createSynchronisationInheritingCoordinates

protected org.w3c.dom.Element createSynchronisationInheritingCoordinates(org.w3c.dom.Element transition)
                                                                  throws java.lang.Exception
Create and append an synchronisation Element to a transition.
Return this Element

createAssignment

protected org.w3c.dom.Element createAssignment()
Creates an assignment Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="assignment"

actual choice depends on useLabelConstruct.

createGuard

protected org.w3c.dom.Element createGuard()
Creates a guard Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="guard"

actual choice depends on useLabelConstruct.

createSynchronisation

protected org.w3c.dom.Element createSynchronisation()
Creates a synchronisation Element.

From uppaal-1.4.dtd on, this is a <label> with attribute

kind="synchronisation"

actual choice depends on useLabelConstruct.

createInvariant

protected org.w3c.dom.Element createInvariant()
Creates a invariant Element.

From some later uppaal versions on, this might be a label with attribute

kind="invariant"

!LABEL!, see useLabelForInvariants.

createDeclaration

protected org.w3c.dom.Element createDeclaration(java.lang.String declarationText)
Create a new declaration element
If the argument is empty, the element will be empty

!! This might be more sophisticated at some point

createParameter

protected org.w3c.dom.Element createParameter(java.util.Vector parameters)
Create a new parameter element
The argument is a Vector of Strings -

!! This might be more sophisticated at some point

createElement

protected org.w3c.dom.Element createElement(java.lang.String type)
                                     throws java.lang.Exception
Create an element particular to the flat hierarchical document

createNameElement

protected org.w3c.dom.Element createNameElement(java.lang.String name)
Returns a Element that is a name tag with specified content

!! Could contain optional argument for placement at some point !!

Overrides:
createNameElement in class DocumentWriter

createTransition

protected org.w3c.dom.Element createTransition(java.lang.String sourceID,
                                               java.lang.String targetID)
Returns a basic transition, given source and target id

!! Might be augmented with coordinates/nails

createSource

protected org.w3c.dom.Element createSource(java.lang.String locID)
Creates a (flat document) source Element and sets the attribute ref.

The attriubte exitref remains unset.

createTarget

protected org.w3c.dom.Element createTarget(java.lang.String locID)
Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.

createTarget

protected org.w3c.dom.Element createTarget(org.w3c.dom.Element locationOrComponent)
                                    throws java.lang.Exception
Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.

inventLocation

protected org.w3c.dom.Element inventLocation(java.lang.String name)
                                      throws java.lang.Exception
Create a new unique location with a specified name

!! could contain coordinate information at some point !!

(Exception is never really thrown)

inventLocation

protected org.w3c.dom.Element inventLocation()
                                      throws java.lang.Exception
Create a new unique location without caring about the name (Exception is never really thrown)

inventLocationInTemplate

public org.w3c.dom.Element inventLocationInTemplate(org.w3c.dom.Element template)
                                             throws java.lang.Exception
Invent a new location and append it to the specified (flat) template.

inventLocationInTemplate

public org.w3c.dom.Element inventLocationInTemplate(java.lang.String name,
                                                    org.w3c.dom.Element template)
                                             throws java.lang.Exception
Invent a new named location and append it to the specified (flat) template.

changeLocationID

protected void changeLocationID(org.w3c.dom.Element el,
                                java.lang.String newID)
                         throws java.lang.Exception
Changes the id-attribute of the location, but also updates the hashtable hashIDsToNewLocationElements

writeToFile

public void writeToFile(java.lang.String fileName)
                 throws java.io.IOException
Output the (current) flat document to a given file.
Old file contents, if any, are destroyed.

isAssignment

public static boolean isAssignment(org.w3c.dom.Element el)
Test, whether this is an assignment Element.

Depends on useLabelConstruct.

isGuard

public static boolean isGuard(org.w3c.dom.Element el)
Test, whether this is an guard Element.

Depends on useLabelConstruct.

isSynchronisation

public static boolean isSynchronisation(org.w3c.dom.Element el)
Test, whether this is an synchronisation Element.

Depends on useLabelConstruct.

isInvariant

public static boolean isInvariant(org.w3c.dom.Element el)
Test, whether this is an invariant Element.

Depends on useLabelForInvariants.

createHurryDummy

public void createHurryDummy()
                      throws java.lang.Exception
Create a dummy automaton trying constantly to synchronize on an urgent channel

createKickTemplate

public org.w3c.dom.Element createKickTemplate(java.util.Vector rootEntrySignals)
                                       throws java.lang.Exception
Create the kickoff-templates, that starts the global process.
The parameter is a vector of strings, i.e., the signals to enter the global components.
Returns the name of the instantiation

addInformationAboutTranslation

public void addInformationAboutTranslation(InstantiationTree tree)

generateEndTemplateSemaphores

private void generateEndTemplateSemaphores()
                                    throws java.lang.Exception
Insert a comment line at the end of every template.

(To be called after completion).

textuallyConjunctInvariants

public static java.lang.String textuallyConjunctInvariants(java.lang.String inv1,
                                                           java.lang.String inv2)
Returns (texualy) a logical and of two invariant texts.
(does not manipulate the texts themselves)

recomputeAllTemplateLayouts

public void recomputeAllTemplateLayouts()
                                 throws java.lang.Exception
Browse through all templates (the ones already in the documnent),
and call the Layouter method on them

cleanupTransitionLabels

public void cleanupTransitionLabels()
                             throws java.lang.Exception
Browse through all transitions (the ones already in the document),
and

getAllTransitionsLeadingToLocation

public java.util.Vector getAllTransitionsLeadingToLocation(org.w3c.dom.Element loc)
                                                    throws java.lang.Exception
Returns a Vector, where all the (immediate) transitions to a specific location are stored.

Should be called only after all transitions are created!

getAllTransitionsStartingAtLocation

public java.util.Vector getAllTransitionsStartingAtLocation(org.w3c.dom.Element loc)
                                                     throws java.lang.Exception
Returns a Vector, where all the (immediate) transitions from a specific location are stored.

Should be called only after all transitions are created!

getTheChildThatIsAssignmentIfExists

public static org.w3c.dom.Element getTheChildThatIsAssignmentIfExists(org.w3c.dom.Element transition)
                                                               throws java.lang.Exception
Return the child label Element, that is an assignment. If it does not exist, then return null.

If not called on a transition, or it has more than one label of kind assignment, then an exception is thrown.

getTheChildThatIsGuardIfExists

public static org.w3c.dom.Element getTheChildThatIsGuardIfExists(org.w3c.dom.Element transition)
                                                          throws java.lang.Exception
Return the child label Element, that is an guard. If it does not exist, then return null.

If not called on a transition, or it has more than one label of kind guard, then an exception is thrown.

getTheChildThatIsSynchronisationIfExists

public static org.w3c.dom.Element getTheChildThatIsSynchronisationIfExists(org.w3c.dom.Element transition)
                                                                    throws java.lang.Exception
Return the child label Element, that is an synchronisation. If it does not exist, then return null.

If not called on a transition, or it has more than one label of kind synchronisation, then an exception is thrown.

getTheChildThatIsInvariantIfExists

public static org.w3c.dom.Element getTheChildThatIsInvariantIfExists(org.w3c.dom.Element location)
                                                              throws java.lang.Exception
Return the child label Element, that is an invariant. If it does not exist, then return null.

If not called on a location, or it has more than one label of kind invariant, then an exception is thrown.
 Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES
SUMMARY:  INNER | FIELD | CONSTR | METHOD DETAIL:  FIELD | CONSTR | METHOD