Class DocumentWriter

java.lang.Object
  |
  +--DocumentReader
        |
        +--DocumentWriter

Direct Known Subclasses:

FlatDocumentWriter

public class DocumentWriter

extends DocumentReader

Constructor Class

This class serves as a wrapper do construct XML documents.

Though a lot of variations of this theme exist, these are the ones specific to Uppaal Documents.

This class contains

• Separator Chars
• Graphical Layout Routines
• Fresh Name Mechanisms
• Auxillary Mechnisms for adding attributes to elements

It inherits the general accessors from DocumentReader.

Version:

Vanilla-1 Mon Mar 19 13:12:52 2001

Author:

M. Oliver Möller

See Also:

DocumentReader

Field Summary

(package private) static java.lang.String	CHANNEL_SEPARATOR Separator sequence used in Uppaal channel names
boolean	debug Spam out debuggin information, if debug is true
protected org.apache.crimson.tree.XmlDocument	doc XML document where the written version is constructed
long	geoCount Parameter for default layout computatation
long	geoXOffset
long	geoYOffset
long	globalGeoXOffset x-Distance from upper left corner
long	globalGeoYOffset y-Distance from upper left corner
(package private) static long	idNameCount Counter to make introduced ID names unique
(package private) static long	locationNameCount Counter to make introduced location names unique
static long	locNameXOffset
static long	locNameYOffset
(package private) static char	NAME_SEPARATOR_CHAR Separator that can be used in <name> elements
(package private) static char	SAFE_SEPARATOR_CHAR Separator that can be used everywhere
(package private) static boolean	sanityChecks Do (possibly time-consuming) sanity checks, if true
(package private) static long	synchronisationNameCount Counter to make introduced channel names unique
(package private) static long	templateNameCount Counter to make introduced template names unique

Fields inherited from class DocumentReader

hashOriginalIDsToElements, origDoc

Constructor Summary

DocumentWriter()
Default Constructor: Creates the (global) document

Method Summary

protected static void	addCoordinatesToElement(org.w3c.dom.Element el) Set x and y to some value.
protected static void	addCoordinatesToElement(org.w3c.dom.Element el, long x, long y) Set x and y to specified values.
protected void	addDefaultLocationCoordinates(org.w3c.dom.Element location)
protected static void	addIDToElement(org.w3c.dom.Element el) Invent a fresh unique ID for this element.
protected org.w3c.dom.Element	addNameToElement(org.w3c.dom.Element el, java.lang.String name) Insert a child node containing a supplided name by default, add coordinates next to el; can be changed afterwards if required. Relies on the fact, that a name element is always the first child. Returns name Element.
protected void	addTextualContentToElement(org.w3c.dom.Element el, java.lang.String text) Add textual content to an Element
void	appendComment(org.w3c.dom.Node node, java.lang.String text) Append comment text as last child of a Node
private org.w3c.dom.Element	createNameElement(java.lang.String name) Returns a Element that is a name tag with specified content
protected static java.lang.String	freshLocationName() Return a new, unique location name
protected static java.lang.String	freshSynchronisationName() Return a new, unique channel name (without !/?)
protected static java.lang.String	freshTemplateName() Return a new, unique template name
protected static java.lang.String	inventFreshID() Return a unique ID string
static java.lang.String	makeIDSafe(java.lang.String name) Transform the ID (Attribute value) to a safe version, i.e.
static java.lang.String	makeNameSafe(java.lang.String name) Transform the name (cdata content of a Element) to a safe version, i.e.
static java.lang.String	makeSignalSafe(java.lang.String name) Transform the signal (i.e.
protected void	resetDefaultLayout() Start coordinate-counting anew
void	testGeoCordinates(long upto)

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

CHANNEL_SEPARATOR

static final java.lang.String CHANNEL_SEPARATOR

Separator sequence used in Uppaal channel names

SAFE_SEPARATOR_CHAR

static final char SAFE_SEPARATOR_CHAR

Separator that can be used everywhere

NAME_SEPARATOR_CHAR

static final char NAME_SEPARATOR_CHAR

Separator that can be used in <name> elements

debug

public boolean debug

Spam out debuggin information, if debug is true

sanityChecks

static boolean sanityChecks

Do (possibly time-consuming) sanity checks, if true

locationNameCount

static long locationNameCount

Counter to make introduced location names unique

synchronisationNameCount

static long synchronisationNameCount

Counter to make introduced channel names unique

idNameCount

static long idNameCount

Counter to make introduced ID names unique

templateNameCount

static long templateNameCount

Counter to make introduced template names unique

doc

protected org.apache.crimson.tree.XmlDocument doc

XML document where the written version is constructed

globalGeoXOffset

public long globalGeoXOffset

x-Distance from upper left corner

globalGeoYOffset

public long globalGeoYOffset

y-Distance from upper left corner

geoXOffset

public long geoXOffset

geoYOffset

public long geoYOffset

locNameXOffset

public static long locNameXOffset

locNameYOffset

public static long locNameYOffset

geoCount

public long geoCount

Parameter for default layout computatation

Constructor Detail

DocumentWriter

public DocumentWriter()

Default Constructor: Creates the (global) document

Method Detail

freshTemplateName

protected static java.lang.String freshTemplateName()

Return a new, unique template name

freshLocationName

protected static java.lang.String freshLocationName()
                                             throws java.lang.Exception

Return a new, unique location name

freshSynchronisationName

protected static java.lang.String freshSynchronisationName()

Return a new, unique channel name (without !/?)

inventFreshID

protected static java.lang.String inventFreshID()

Return a unique ID string

!! might enter the ID in some list at some point !!

makeNameSafe

public static java.lang.String makeNameSafe(java.lang.String name)

Transform the name (cdata content of a Element) to a safe version, i.e. one that is accepted by Uppaal

makeSignalSafe

public static java.lang.String makeSignalSafe(java.lang.String name)

Transform the signal (i.e. a channel name) to a safe version, i.e. one that is accepted by Uppaal

makeIDSafe

public static java.lang.String makeIDSafe(java.lang.String name)

Transform the ID (Attribute value) to a safe version, i.e. one that is accepted by Uppaal

resetDefaultLayout

protected void resetDefaultLayout()

Start coordinate-counting anew

addDefaultLocationCoordinates

protected void addDefaultLocationCoordinates(org.w3c.dom.Element location)
                                      throws java.lang.Exception

testGeoCordinates

public void testGeoCordinates(long upto)

addCoordinatesToElement

protected static void addCoordinatesToElement(org.w3c.dom.Element el)

Set x and y to some value.

!! Can be the default layout at some point !!

(Currently, everything is "0")

addCoordinatesToElement

protected static void addCoordinatesToElement(org.w3c.dom.Element el,
                                              long x,
                                              long y)

Set x and y to specified values.

addIDToElement

protected static void addIDToElement(org.w3c.dom.Element el)

Invent a fresh unique ID for this element.

!! Could take an optional argument, hinting at the origin

addNameToElement

protected org.w3c.dom.Element addNameToElement(org.w3c.dom.Element el,
                                               java.lang.String name)

Insert a child node containing a supplided name
by default, add coordinates next to el; can be changed afterwards if required.

Relies on the fact, that a name element is always the first child.

Returns name Element.

addTextualContentToElement

protected void addTextualContentToElement(org.w3c.dom.Element el,
                                          java.lang.String text)

Add textual content to an Element

appendComment

public void appendComment(org.w3c.dom.Node node,
                          java.lang.String text)

Append comment text as last child of a Node

createNameElement

private 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 !!