A B C D E F G H I K L M N O P R S T U V W X Y

A

activator - Variable in class TextualInstantiation

The channel the translation of this template depends on.
The translation of this part of the system remains in a special state _idle_(number), until the signal [activator]! is sent.

addAssignmentToTransition(Element) - Method in class FlatDocumentWriter

Add an assigment to a transition (as a child).
Returns the assignment Element.

addAssignmentToTransition(Element, String) - Method in class FlatDocumentWriter

Add an assigment to a transition (as a child), including some initial text
Returns the assignment Element.

addChild(InstantiationTree) - Method in class InstantiationTree

Add a child

addConflict(String, Element, TextualInstantiation) - Method in class ChannelRegistry

Adds the synchronization from a global join, that might cause a conflict.

Note that the TextualInstantiaton handed over is not where the transition lives in, but the tinst of the component, where it originates from.

addConflictsForNewSync(String, String) - Method in class ChannelRegistry

Go through the conflicts;

If there was a conflict entry for oldSync, add a new conflict entry for newSync

(Necessary, see ChannelManager Handnotes)

addCoordinatesToElement(Element) - Static method in class DocumentWriter

Set x and y to some value.

addCoordinatesToElement(Element, long, long) - Static method in class DocumentWriter

Set x and y to specified values.

addDeclaration(String) - Method in class FlatDocumentWriter

Add just a declaration (e.g.

addDeclarationText(String) - Method in class FlatDocumentWriter

Append some declaration (purely textual)

addDefaultLocationCoordinates(Element) - Method in class DocumentWriter

addDefaultLocationCoordinates(Element) - Method in class SimpleLayouter

addDefaultLocationCoordinates(Element) - Method in class SkewedGridLayouter

addGuardsAndAssignmentsOfConnectionInContext(Element, Vector, Vector, Object) - Method in class HierarchicalDocumentReader

The TexualInstantiaion is handed over for context information (i.e.

addGuardToTransition(Element) - Method in class FlatDocumentWriter

Add a guard to a transition (as a child).
Returns the guard Element.

addGuardToTransition(Element, String) - Method in class FlatDocumentWriter

Add a guard to a transition (as a child), including some guard text
Returns the guard Element.

addIDAndElementToHashTable(String, Element) - Method in class HierarchicalDocumentReader

Make hash table entries for Elements that are not accessible in the original document

Used to retrieve components with fake IDs.

addIDToElement(Element) - Static method in class DocumentWriter

Invent a fresh unique ID for this element.

addInformationAboutTranslation(InstantiationTree) - Method in class FlatDocumentWriter

addInstantiation(TextualInstantiation) - Method in class FlatDocumentWriter

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.

addLocationToTemplate(Element, Element) - Method in class FlatDocumentWriter

Add a location at the right place.

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

addNameToElement(Element, String) - Method in class DocumentWriter

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.

addNameToTemplate(Element, Element) - Method in class FlatDocumentWriter

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.

addNode(Node) - Method in class MutableNodeListImpl

Insert a node at the end of the list.

addParameterToTemplate(Element, Element) - Method in class FlatDocumentWriter

Add a parameter element at the right place.

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

addReceiveSynchronisationToTransition(String, Element) - Method in class FlatDocumentWriter

Add a ?-synchronisation (without caring about graphical information)

Assumes that the argument is a transition

addRegisteredReceiveSynchronisationToTransition(String, Element, TextualInstantiation) - Static method in class Flatten

Add RECEIVE synchronization and provide registration in {@see ChannelRegistry}

Returns the synchronisation Element

(only necessary for original (hierarchical) synchronizations)
??? necessary ???

addRegisteredSendSynchronisationToTransition(String, Element, TextualInstantiation) - Static method in class Flatten

Add SEND synchronization and provide registration in {@see ChannelRegistry}

Returns the synchronisation Element

(only necessary for original (hierarchical) synchronizations)

??? necessary ???

addRegisteredSynchronisationToTransition(String, Element, TextualInstantiation) - Static method in class Flatten

Add synchronization and provide registration in {@see ChannelRegistry}

Returns the synchronisation Element

(only necessary for original (hierarchical) synchronizations)

addSendSynchronisationToTransition(String, Element) - Method in class FlatDocumentWriter

Add a !-synchronisation (without caring about graphical information)

Assumes that the argument is a transition

addSourceToTransition(Element, Element) - Method in class FlatDocumentWriter

Add a source to a transition in the right place.

addSynchronisationToTransition(Element) - Method in class FlatDocumentWriter

Add a synchronisation to a transition (as a child).
Returns the synchronisation Element.

addSynchronisationToTransition(String, Element) - Method in class FlatDocumentWriter

Add a synchronisation to a transition (as a child), including some initial text.
Returns the synchronisation Element.

addTargetToTransition(Element, Element) - Method in class FlatDocumentWriter

Add a target to a transition in the right place.

addTemplate(Element) - Method in class FlatDocumentWriter

Add a new template

addTextualContentToElement(Element, String) - Method in class DocumentWriter

Add textual content to an Element

addTextualInvariantToLocation(Element, String) - Method in class FlatDocumentWriter

Add an (textual) invariant at the right place.
If an invariant already existsm conjunct it logically.

addTransitionToTemplate(Element, Element) - Method in class FlatDocumentWriter

Append a transition to the template as a child at the right place

adjustLocation(Element) - Method in class SkewedGridLayouter

Adjust a location:

adjustTransition(Element) - Method in class SimpleLayouter

Adjust a transition:

adjustTransition(Element) - Method in class SkewedGridLayouter

Adjust a transition:

allAssignments - Variable in class GlobalJoin

Vector containing all assignments as textual String (with the proper renaiming), including the one of the root-transition (if present).

allEntriesAreCreated - Static variable in class LocationMapper

allGlobalJoins - Static variable in class GlobalJoin

The (global) Vector, all joins are collected in

This is where the additional join is planted to, if the GlobalJoin.clone() method is called.

allGuards - Variable in class GlobalJoin

Vector containing all guards as textual String (with the proper renaiming), including the one of the root-transition (if present).

allHierarchicalStartLocations - Variable in class GlobalJoin

The (growing) collection of all the (hierarchical) basic locations, from where the join might start.
The entries of this Vector are TinstElementPairs.

allTransitionsWithSyncInTinst(String, TextualInstantiation) - Method in class ChannelRegistry

Return vector of entires, of empty vector if there are none.

appendComment(Node, String) - Method in class DocumentWriter

Append comment text as last child of a Node

appendTextToTextualContentOfElement(Element, String) - Method in class FlatDocumentWriter

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.

assignment - Static variable in class Flatten

assignmentXOffset - Static variable in class SimpleLayouter

assignmentXOffset - Static variable in class SkewedGridLayouter

assignmentXShift - Static variable in class SimpleLayouter

assignmentXShift - Static variable in class SkewedGridLayouter

assignmentYOffset - Static variable in class SimpleLayouter

assignmentYOffset - Static variable in class SkewedGridLayouter

assignmentYShift - Static variable in class SimpleLayouter

assignmentYShift - Static variable in class SkewedGridLayouter

attIndent - Static variable in class Flatten

Additional Indentation for attributes

B

blanks - Static variable in class Flatten

C

changeLocationID(Element, String) - Method in class FlatDocumentWriter

Changes the id-attribute of the location, but also updates the hashtable FlatDocumentWriter.hashIDsToNewLocationElements

changeSyncTextAtTransition(Element, String) - Method in class FlatDocumentWriter

Change synchronization text of a transtion.

CHANNEL_SEPARATOR - Static variable in class DocumentWriter

Separator sequence used in Uppaal channel names

channelCopyCounter - Static variable in class ChannelRegistry

Counter used for @{link newPostfix}

ChannelRegistry - class ChannelRegistry.

This class stores information about cannel communication, that is needed for Phase III of translation, i.e., duplication of channels if necessary.

ChannelRegistry(InstantiationTree) - Constructor for class ChannelRegistry

Default Constructor: Needs references

chanOfSync(String) - Static method in class ChannelRegistry

Return channel of sync (handshake)
Throw Exception, if the input is not a sync.

children - Variable in class InstantiationTree

All child instantiatino trees.

cleanupTransitionLabels() - Method in class FlatDocumentWriter

Browse through all transitions (the ones already in the document),
and remove empty labels sort labels in guard-sync-assignment

clone() - Method in class GlobalJoin

Returns a copy of this object, i.e.

cloneStackOfPointers(Stack) - Static method in class GlobalJoin

Clones a stack of pointers, preserving the order.

Assumes that a stack is sorted, starting with position 0 as the bottommost element.

cloneTransition(Element) - Method in class FlatDocumentWriter

Create a clone of a transition Element and add it in the appropriate template.
Returns the clone.

cloneVectorOfPointers(Vector) - Static method in class GlobalJoin

Returns a new Vector containing all (pointers to) objects of the Vector in the same order.

cloneVectorOfStrings(Vector) - Method in class GlobalJoin

Returns a new Vector containing all the strings of the old one (intentionally, but not necessarily in the same order).

cm - Static variable in class Flatten

An entity that translates pairs (hierarchial component, textual instantiation) to the textual instantiation of this compenent.

cm - Static variable in class GlobalJoin

ComponentMapper to help access.
The entries in it are created by Flatten.

collectedInstantiations - Static variable in class Flatten

collectGlobalJoinsStartingBelowHere(Vector) - Method in class InstantiationTree

Adds the global joins starting in a descendand to the argument Vector

collectGlobalJoinsStartingHERE(Vector) - Method in class InstantiationTree

Add the global joins, that have their root transition in the textual instantiation.

collectGuardsAndAssignmentsOfTarget(Element, Vector, Vector, Object) - Method in class HierarchicalDocumentReader

Traverses the entry-fork starting with this target (which is assumed to point at a component and an entry)
The guards and assignments present in the connections are collected textually (Vector of strings), without any assumption on the order.

NOTE:The result of this process possibly has to be adjusted to the current instantiation (i.e., names have to be mapped) The information for this can be extraced from the context, which is a list (stack?) of renamings.

complete() - Method in class FlatDocumentWriter

Main Method

completed - Variable in class FlatDocumentWriter

Keeping track, whether the full-translation is already done

componentCount - Static variable in class Flatten

Counter to make introduced locations for components unique

componentElement - Variable in class TextualInstantiation

The (hierarchical old) component, where this object instanted

ComponentMapper - class ComponentMapper.

Service Class

ComponentMapper() - Constructor for class ComponentMapper

Default Constructor

computeGlobalJoins() - Method in class InstantiationTree

Compute the global joins starting at this component or at a component below.

conjunctTextualAssignmentToTransition(Element, String) - Method in class FlatDocumentWriter

Adds some assignment text to a transition, i.e.

conjunctTextualGuardToTransition(Element, String) - Method in class FlatDocumentWriter

Adds some guard text to a transition, i.e.

constructFlatDoc(HierarchicalDocumentReader) - Static method in class Flatten

Main Method

content - Variable in class InstantiationTree

copyChannelDeclaration(String, String) - Method in class FlatDocumentWriter

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.

cr - Static variable in class Flatten

Registration of hand-shake communication for Phase III processing

createAssignment() - Method in class FlatDocumentWriter

Creates an assignment Element.

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

kind="assignment"

actual choice depends on FlatDocumentWriter.useLabelConstruct.

createAssignmentInheritingCoordinates(Element) - Method in class FlatDocumentWriter

Create and append an assignment Element to a transition.
Return this Element

createDeclaration(String) - Method in class FlatDocumentWriter

Create a new declaration element
If the argument is empty, the element will be empty

createElement(String) - Method in class FlatDocumentWriter

Create an element particular to the flat hierarchical document

createGuard() - Method in class FlatDocumentWriter

Creates a guard Element.

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

kind="guard"

actual choice depends on FlatDocumentWriter.useLabelConstruct.

createGuardInheritingCoordinates(Element) - Method in class FlatDocumentWriter

Create and append an guard Element to a transition.
Return this Element

createHurryDummy() - Method in class FlatDocumentWriter

Create a dummy automaton trying constantly to synchronize on an urgent channel

createInvariant() - Method in class FlatDocumentWriter

Creates a invariant Element.

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

kind="invariant"

!LABEL!, see FlatDocumentWriter.useLabelForInvariants.

createJoinsForGlobalExits(TextualInstantiation, Element) - Method in class HierarchicalDocumentReader

Create the Joins for stopping global elements (direct children of root);

createKickTemplate(Vector) - Method in class FlatDocumentWriter

Create the kickoff-templates, that starts the global process.

createNameElement(String) - Method in class DocumentWriter

Returns a Element that is a name tag with specified content

createNameElement(String) - Method in class FlatDocumentWriter

Returns a Element that is a name tag with specified content

createParameter(Vector) - Method in class FlatDocumentWriter

Create a new parameter element
The argument is a Vector of Strings -

createSource(String) - Method in class FlatDocumentWriter

Creates a (flat document) source Element and sets the attribute ref.

The attriubte exitref remains unset.

createSynchronisation() - Method in class FlatDocumentWriter

Creates a synchronisation Element.

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

kind="synchronisation"

actual choice depends on FlatDocumentWriter.useLabelConstruct.

createSynchronisationInheritingCoordinates(Element) - Method in class FlatDocumentWriter

Create and append an synchronisation Element to a transition.
Return this Element

createTarget(Element) - Method in class FlatDocumentWriter

Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.

createTarget(String) - Method in class FlatDocumentWriter

Creates a (flat document) target Element and sets the attribute ref.

The attriubte exitref remains unset.

createTemplate() - Method in class FlatDocumentWriter

Returns a (fresh) template node and insert it in the list of known templates.

createTransition(String, String) - Method in class FlatDocumentWriter

Returns a basic transition, given source and target id

createTransitionChildInheritingCoordinates(Element, String) - Method in class FlatDocumentWriter

Create and append a child Element to a transition.
Return this Element

createTransitionInTemplate(Element) - Method in class FlatDocumentWriter

Returns a (fresh) template node and insert it in the list of known templates.

currentTemplatePrefix - Static variable in class Flatten

Prefix that makes the currently translated Template unique

D

data - Variable in class MutableNodeListImpl

debug - Static variable in class ComponentMapper

Spam out debuggin information, if debug is true

debug - Variable in class DocumentWriter

Spam out debuggin information, if debug is true

debug - Static variable in class Flatten

Spam out debuggin information, if debug is true

debug - Static variable in class GlobalJoin

For Spamming out information

debug - Static variable in class HierarchicalDocumentReader

Spam out debuggin information, if debug is true

debug - Static variable in class LocationMapper

Spam out debuggin information, if debug is true

debug - Static variable in class SimpleLayouter

debug - Static variable in class SkewedGridLayouter

debug - Static variable in class TextualInstantiation

Spam out debuggin information, if debug is true

declaration - Variable in class FlatDocumentWriter

declarationText - Static variable in class FlatDocumentWriter

Text inserted in the (flat) declaration label.

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

doc - Variable in class DocumentWriter

XML document where the written version is constructed

docToString() - Method in class HierarchicalDocumentReader

Return the original document as string

DocumentReader - class DocumentReader.

Accessor Class

DocumentReader(Document) - Constructor for class DocumentReader

Constructor with hand-over of document

DocumentWriter - class DocumentWriter.

Constructor Class

DocumentWriter() - Constructor for class DocumentWriter

Default Constructor: Creates the (global) document

E

element - Variable in class TinstElementPair

The element (as defined in the template).

elementCount - Static variable in class Flatten

Counter to make hashing of elements unique

ElementElementPair - class ElementElementPair.

Wrapper Class for Pair of Elements

ElementElementPair(Element, Element) - Constructor for class ElementElementPair

The only constructor.

enterTextualInstantiation(Element, TextualInstantiation, TextualInstantiation) - Method in class ComponentMapper

Create an entry in
Component * TextualInstantiation ---> TextualInstantiation

The first TextualInstantiation is the declaringContext, the result TextualInstantiation is the (sub-)declared one.

enumChildren() - Method in class InstantiationTree

Return enumeration of the children

enumTinstsOutsideTinst(TextualInstantiation) - Method in class ChannelRegistry

Enumerate textual Instantiations (including root) outside a specific one, i.e., above and incomparable to it.

enumTinstTransitionsWithSyncOutsideTinst(String, TextualInstantiation) - Method in class ChannelRegistry

The transitions OUTSIDE a tinst (those have to be cloned in phase III) Return enumeration of TinstElementPairs

enumTransitionsWithSyncOusideTinst(String, TextualInstantiation) - Method in class ChannelRegistry

Returns an enumeration of all (flat) transtions, that carry the specified sync and reside outside the specific tinst.
(possibly the empty enumeration).

Only works properly, if all transitions were registered with ChannelRegistry.registerSync(java.lang.String, org.w3c.dom.Element, TextualInstantiation).

exitSignal - Variable in class TextualInstantiation

The signal that is issued, if the component becomes idle.
This is NOT specific to any particular exit, but only to the TextualInstantiation itself.

exitSignalCounter - Static variable in class TextualInstantiation

Auxillary Variable, to make exit signals unique.

F

factor - Static variable in class Flatten

Factor for indenting

fakeIDCounter - Static variable in class HierarchicalDocumentReader

AUX counter to create unique fake IDs

fakeIDName - Static variable in class HierarchicalDocumentReader

Name of Component IDs that are not present in the original document

used in HierarchicalDocumentReader.wrapAroundInstHashTable.

father - Variable in class TextualInstantiation

Pointer to the direct father.

fdw - Static variable in class Flatten

The way to create the flat document

fdw - Variable in class LocationMapper

Relevant writer (necessary to create object)

fdw - Variable in class SimpleLayouter

fdw - Variable in class SkewedGridLayouter

findNodeWithContent(TextualInstantiation) - Method in class InstantiationTree

Returns the node of the tree that contains the specific TextualInstantiation.

Returns null, if it is not found.

finishGrowth() - Method in class GlobalJoin

Grow loop

first - Variable in class ElementElementPair

First of pair

flatDoc - Static variable in class Flatten

The document that the Flatten.fdw is writing

FlatDocumentWriter - class FlatDocumentWriter.

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

FlatDocumentWriter() - Constructor for class FlatDocumentWriter

Default Constructor

Flatten - class Flatten.

Flattening Huppaal Definitions

Flatten() - Constructor for class Flatten

freshLocationName() - Static method in class DocumentWriter

Return a new, unique location name

freshSynchronisationName() - Static method in class DocumentWriter

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

freshTemplateName() - Static method in class DocumentWriter

Return a new, unique template name

G

generateEndTemplateSemaphores() - Method in class FlatDocumentWriter

Insert a comment line at the end of every template.

(To be called after completion).

geoCount - Variable in class DocumentWriter

Parameter for default layout computatation

geoCount - Variable in class SimpleLayouter

Parameter for default layout computatation

geoCount - Variable in class SkewedGridLayouter

Parameter for default layout computatation

geoXOffset - Variable in class DocumentWriter

geoXOffset - Variable in class SimpleLayouter

geoXOffset - Variable in class SkewedGridLayouter

geoYOffset - Variable in class DocumentWriter

geoYOffset - Variable in class SimpleLayouter

geoYOffset - Variable in class SkewedGridLayouter

getActiveSubcomponentID(TextualInstantiation) - Static method in class Flatten

Takes the instantiation of the component as an argument and returns the (flat) location-ID, that corresponds to the situation, that this component is active, i.e.

getAllAliveGlobalInits() - Method in class HierarchicalDocumentReader

Return the list of global inits, that refer to a root element that is part of the system.

getAllChildrenThatAreAssignments(Element) - Method in class HierarchicalDocumentReader

Retrieve all child nodes that are assignments.

getAllChildrenThatAreGuards(Element) - Method in class HierarchicalDocumentReader

Retrieve all child nodes that are guards.

getAllChildrenThatAreSynchronisation(Element) - Method in class HierarchicalDocumentReader

Retrieve all child nodes that are synchronisations.

getAllChildrenWithLabel(Element, String) - Static method in class DocumentReader

Return all child nodes that have a specific label

getAllExitsOfComponent(Element) - Method in class HierarchicalDocumentReader

Returns a Vector of exit Elements, that correspond to the exits of the template this component instantiates.

getAllExitsOfTemplate(Element) - Static method in class HierarchicalDocumentReader

Returns a Vector of exit Elements, that correspond to the exits of this template.

getAllLocationsAndComponents(Element) - Static method in class HierarchicalDocumentReader

Return a vector with all locations and components.

getAllTemplates() - Method in class HierarchicalDocumentReader

Return the (complete) list of defined hierarchical templates

getAllTransitionsLeadingToLocation(Element) - Method in class FlatDocumentWriter

Returns a Vector, where all the (immediate) transitions to a specific location are stored.

Should be called only after all transitions are created!

getAllTransitionsStartingAtLocation(Element) - Method in class FlatDocumentWriter

Returns a Vector, where all the (immediate) transitions from a specific location are stored.

Should be called only after all transitions are created!

getCdataOfElement(Element) - Static method in class DocumentReader

If the Element is a tag containing CDATA, then this data is returned.

getConnectionOfEntry(Element) - Method in class HierarchicalDocumentReader

Returns the (one) connection an entry points to

getConnectionsToExitOrExitpoint(Element) - Method in class HierarchicalDocumentReader

Returns s Vector of Elements, containing all the pointing-to connections.

getDeclarationText() - Method in class HierarchicalDocumentReader

Retrieve the texutal declaration data from element tag, if present

getDirectChildNodes() - Method in class HierarchicalDocumentReader

All direct Children of root

getDirectChildNodesWithTag(String) - Method in class HierarchicalDocumentReader

Some direct children of root

getDoc() - Method in class FlatDocumentWriter

Return the (completed) XMLDocument

getElementByID(String) - Method in class DocumentReader

Return the Element-Node in the original document that is augmented with the specific id
Throw excpetion, if it does not exist.

getElementID(Element) - Static method in class DocumentReader

Read the id of a given element
Throw exception, if it does not exist

getElementName(Element) - Static method in class DocumentReader

Read the contens of name child of a given element
Throw exception, if it does not exist

getEntryATargetPointsTo(Element) - Method in class HierarchicalDocumentReader

Returns the (one) <entry&rt; element that a target points to

getFirstChildThatIsElement(Element, String) - Static method in class Flatten

Return the first child element that is of the given kind.
Throws an Exception, if no such child exists.

getFirstChildWithLabel(Element, String) - Static method in class DocumentReader

Get first child that has the designated label.
Throw exception, if no such child exists

getFirstChildWithLabelIfExists(Element, String) - Static method in class DocumentReader

Get first child that has the designated label.
Returns null, if no such child exists

getForkElementOfEntry(Element) - Method in class HierarchicalDocumentReader

Map <entry> or <entrypoint> to the (single) corresponding fork Element.
Throws exception, if used wrongly or in wrong context.

getFreshObjectName(String) - Static method in class TextualInstantiation

uniqueName, due to containment of non-user string "--"

getGlobalJoin(Element, TextualInstantiation) - Static method in class GlobalJoin

Constructor specifying the root transition (in the hierarchical version)

Throws Exception, if HierarchicalDocumentReader.addGuardsAndAssignmentsOfConnectionInContext fails.

If the second argument is Flatten.rootInstDummy, then this gobal join is global exit of a component.

getInstantiationText() - Method in class HierarchicalDocumentReader

Retrieve the texutal instantiation data from element tag, if present

getLength() - Method in class MutableNodeListImpl

getNamesOfAliveSystemParts() - Method in class HierarchicalDocumentReader

Browse the system definition to get the name of instantiations that are declared to be part of the top-level parallel composition.

getNodeOfTemplate(String) - Static method in class Flatten

Return the node with specified template name

getSignal(String, Element) - Static method in class Flatten

The signal this entry/exit corresponds to (without !/?)
If the component in question is not a enty/exit, an exception is thrown.

getSystemText() - Method in class HierarchicalDocumentReader

Retrieve the texutal system data from element tag, if present

getTargetElementOfEntry(Element) - Method in class HierarchicalDocumentReader

Map <entry> or <entrypoint> to the (single) corresponding target Element.
Throws exception, if used wrongly or in wrong context.

getTargetsOfFork(Element) - Method in class HierarchicalDocumentReader

getTemplateWithName(String) - Method in class HierarchicalDocumentReader

Returns the Element in the original (hierarchical) document, that has the specified name.
Throws Exception, if not found.

getTextualAssignmentOfTransitionIfPresent(Element) - Method in class HierarchicalDocumentReader

Returns the text of a assignment, if present and not the empty string, otherwise, returns null.

Throws Exception, if not called on transition or connection.

getTextualGuardOfTransitionIfPresent(Element) - Method in class HierarchicalDocumentReader

Returns the text of a guard, if present and not the empty string, otherwise, returns null.

Throws Exception, if not called on transition or connection.

getTheChildAssignmentIfExists(Element) - Static method in class HierarchicalDocumentReader

Retrieve (if existent) the child that is assignment.

Return null, if it does not exist.

Throws exception, if more than two such children exist.

getTheChildGuardIfExists(Element) - Static method in class HierarchicalDocumentReader

Retrieve (if existent) the child that is guard.

Return null, if it does not exist.

Throws exception, if more than two such children exist.

getTheChildInvariantIfExists(Element) - Static method in class HierarchicalDocumentReader

Retrieve (if existent) the child that is invariant.

Return null, if it does not exist.

Throws exception, if more than two such children exist.

getTheChildSynchronisationIfExists(Element) - Static method in class HierarchicalDocumentReader

Retrieve (if existent) the child that is synchronisation.

Return null, if it does not exist.

Throws exception, if more than two such children exist.

getTheChildThatIsAssignmentIfExists(Element) - Static method in class FlatDocumentWriter

Return the child label Element, that is an assignment.

getTheChildThatIsGuardIfExists(Element) - Static method in class FlatDocumentWriter

Return the child label Element, that is an guard.

getTheChildThatIsInvariantIfExists(Element) - Static method in class FlatDocumentWriter

Return the child label Element, that is an invariant.

getTheChildThatIsSynchronisationIfExists(Element) - Static method in class FlatDocumentWriter

Return the child label Element, that is an synchronisation.

getTheChildWithLabel(Element, String) - Static method in class DocumentReader

Get the child that has the designated label.
Throw exception, if none or more than one such child exists.

getTheChildWithLabelIfExists(Element, String) - Static method in class DocumentReader

Get the child that has the designated label.
Throw exception, if more than one such child exists.

getTopmostComponent() - Method in class GlobalJoin

Returns the (hierarchical) component that is left here, as seen from the rootTransitions.

getTopmostExit() - Method in class GlobalJoin

Returns the (only) exit that the global join is allowed to be specific to, before GlobalJoin.finishGrowth() is called.

Thrwos exception, if it is not exactly one.

getXCoordinate(Element) - Method in class DocumentReader

Read x coordinate (as long).
Return "0L" if not present

getYCoordinate(Element) - Method in class DocumentReader

Read y coordinate (as long).
Return "0L" if not present

globalGeoXOffset - Variable in class DocumentWriter

x-Distance from upper left corner

globalGeoXOffset - Variable in class SimpleLayouter

x-Distance from upper left corner

globalGeoXOffset - Variable in class SkewedGridLayouter

x-Distance from upper left corner

globalGeoYOffset - Variable in class DocumentWriter

y-Distance from upper left corner

globalGeoYOffset - Variable in class SimpleLayouter

y-Distance from upper left corner

globalGeoYOffset - Variable in class SkewedGridLayouter

y-Distance from upper left corner

globalInstantiationTree - Static variable in class Flatten

The tree the system is mapped to

GlobalJoin - class GlobalJoin.

Global Join

GlobalJoin() - Constructor for class GlobalJoin

Internal constructor, used for cloning (and of course not setting the static fields again).

Needed also, when GlobalJoin.getGlobalJoin(org.w3c.dom.Element, TextualInstantiation) did not yield an existing join.

grow(TextualInstantiation, Element) - Method in class GlobalJoin

Main method telling the global join to continue to grow, starting with one particular <exit> or <exitpoint> the search for possibly different growth stops, when the listOfExitPoints contains only exits of OR templates/components if a grow is completed, the join is defined completely the last thing that is set is the GlobalJoin.triggerVariable if at some point in the growing, the join has several options to continue, it splits itself according to these options, adds all of the new ones to the Vector GlobalJoin.allGlobalJoins and calls grow() on them

growAll() - Static method in class GlobalJoin

Finish growing all global joins.

That typicaly increases their number.

growObligations - Variable in class GlobalJoin

Contains all the unfinished intermediates nodes, i.e.

guard - Static variable in class Flatten

guardXOffset - Static variable in class SimpleLayouter

guardXOffset - Static variable in class SkewedGridLayouter

guardXShift - Static variable in class SimpleLayouter

guardXShift - Static variable in class SkewedGridLayouter

guardYOffset - Static variable in class SimpleLayouter

guardYOffset - Static variable in class SkewedGridLayouter

guardYShift - Static variable in class SimpleLayouter

guardYShift - Static variable in class SkewedGridLayouter

H

hasDefaultExit(Element) - Static method in class HierarchicalDocumentReader

Checks whether this template has a default exit.

hashElementsToIDs - Static variable in class Flatten

Hashtable storing the IDs the tranlation of elements corresponds to ?t?

hashHierarchicalComponentsToHashtable - Variable in class ComponentMapper

Maps (basic) hierarchical components to another hashtable, that TextualInstantiation to TextualInstantiation, namely those that correspond to the instantiation of the component in this context.

hashHierarchicalLocationsToHashtable - Variable in class LocationMapper

Maps (basic) hierarchical locations to another hashtable, that maps textual instantiations to Elements, namely the Element this particular instantion of a location was translated to.

hashIDConcatenationsToFlatLocations - Variable in class LocationMapper

Maps concatentations of separators to another hashtable, that maps TextualInstantiations to (flat) locations.
Used to map entries of hierarchical components.

hashIDsToNewLocationElements - Static variable in class FlatDocumentWriter

Store all newly generated (flat) locations.
Requires the use of the methods FlatDocumentWriter.inventLocation(java.lang.String) and FlatDocumentWriter.changeLocationID(org.w3c.dom.Element, java.lang.String) in order to work properly.

hashInstComponentToTInst - Static variable in class Flatten

Hashtable mapping instantiation/componentID to the TextualInstantiation it corresponds to.

hashOriginalIDsToElements - Variable in class DocumentReader

Store once for every translation

hashTemplateNamesToElements - Static variable in class Flatten

Hashtable mapping (original, hierarchical) template names to the corresponding Element nodes, see Flatten.memorizeTemplate(org.w3c.dom.Element)

hashTextualInstantitionsToActiveLocation - Variable in class LocationMapper

Maps textual instantions to their active locations.

In Vanilla-1, there is only one unique active location per AND Component.

hashTextualInstantitionsToIdleLocation - Variable in class LocationMapper

Maps textual instantions to their idle locations.

In Vanilla-1, there is only one unique active location per Component.

hdr - Static variable in class Flatten

The way to access the hierarchical document

hdr - Static variable in class GlobalJoin

The hierarchical document reader

hdr - Variable in class LocationMapper

Relevant reader (necessary to follow ID references)

HierarchicalDocumentReader - class HierarchicalDocumentReader.

Wrapper Class

HierarchicalDocumentReader(Document) - Constructor for class HierarchicalDocumentReader

Default Constructor

huppaalDTD - Static variable in class HierarchicalDocumentReader

Version of the hierarchical Huppaal grammar

I

idNameCount - Static variable in class DocumentWriter

Counter to make introduced ID names unique

inheritedInvariant - Variable in class TextualInstantiation

Contains (texutally conjunct) the invariants inherited by ancestors; they are assumed to be parameter-corrected allready.
Is initialized on call of TextualInstantiation.setup(java.lang.String, java.util.Vector, TextualInstantiation, org.w3c.dom.Element, org.w3c.dom.Element, org.w3c.dom.Element).

ASSUMPTION: ALL ANCHESTORS ARE SETUP BEFORE THEIR DESCENDANDTS.

init(ComponentMapper, HierarchicalDocumentReader) - Static method in class GlobalJoin

Required static setups

instantiation - Variable in class FlatDocumentWriter

instantiation - Static variable in class Flatten

instantiationsToBeTranslated - Static variable in class Flatten

Main stack that contains the instantiations of templates to be processed

instantiationText - Static variable in class FlatDocumentWriter

Text describing the Instantiations of templates used for the system.

InstantiationTree - class InstantiationTree.

This Datat Type implements a tree structure, where every Node correspons to a TextualInstantiation.

InstantiationTree(TextualInstantiation) - Constructor for class InstantiationTree

Default Constructor

inventExitSignal() - Method in class TextualInstantiation

Set the exit signal.
(Unfortunately, this cannot be dependent on the NAME of the textual instantiation, for it has to be present, before the setup is called).

inventFreshID() - Static method in class DocumentWriter

Return a unique ID string

inventLocation() - Method in class FlatDocumentWriter

Create a new unique location without caring about the name (Exception is never really thrown)

inventLocation(String) - Method in class FlatDocumentWriter

Create a new unique location with a specified name

inventLocationInTemplate(Element) - Method in class FlatDocumentWriter

Invent a new location and append it to the specified (flat) template.

inventLocationInTemplate(String, Element) - Method in class FlatDocumentWriter

Invent a new named location and append it to the specified (flat) template.

inventNewGoegraphicalLocations - Static variable in class FlatDocumentWriter

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 FlatDocumentWriter.inventLocation(java.lang.String) for creation of new locations.

inventNewTriggerVariable() - Static method in class GlobalJoin

Make a new Variable name

isANDComponent - Variable in class TextualInstantiation

Set to true, if the exit point of this instantiaion are connected to a join
Note that an arbitrary amount of global joins can be related to this particular instantiation.

isANDComponent(Element) - Method in class HierarchicalDocumentReader

Returns true, if the component is isantiation of an AND template.

Trows Exception, if called on a non-component

isANDTemplate(Element) - Method in class HierarchicalDocumentReader

Returns true, if the template is an AND element.

Trows Exception, if called on a non-template

isAssignment(Element) - Static method in class FlatDocumentWriter

Test, whether this is an assignment Element.

Depends on FlatDocumentWriter.useLabelConstruct.

isAssignmentElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether this is an assignment Element.

Depends on HierarchicalDocumentReader.useLabelConstruct.

isComponent(Element) - Static method in class HierarchicalDocumentReader

Test whether this element is a component.

Throws Exception, if the element is not a location or component.

isDefaultExitOrExitpoint(Element) - Static method in class HierarchicalDocumentReader

Returns true, if the element is a default exit or an exitpoint.
Throws exception on type error.

isGuard(Element) - Static method in class FlatDocumentWriter

Test, whether this is an guard Element.

Depends on FlatDocumentWriter.useLabelConstruct.

isGuardElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether this is an guard Element.

Depends on HierarchicalDocumentReader.useLabelConstruct.

isHistoryComponent(Element) - Method in class HierarchicalDocumentReader

Returns true, if the component is a history element.

Trows Exception, if called on a non-component

isHistoryEntry(Element) - Static method in class HierarchicalDocumentReader

Returns true, if the entry is a history element.

Trows Exception, if called on a non-entry

isHistoryTemplate(Element) - Method in class HierarchicalDocumentReader

Returns true, if the template is a history element.

Trows Exception, if called on a non-template

isInvariant(Element) - Static method in class FlatDocumentWriter

Test, whether this is an invariant Element.

Depends on FlatDocumentWriter.useLabelForInvariants.

isInvariantElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether this is an invariant Element.

Depends on HierarchicalDocumentReader.useLabelConstruct.

isNailElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether a node is an Element and a nail

isSourceElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether a node is an Element and a source

isSynchronisation(Element) - Static method in class FlatDocumentWriter

Test, whether this is an synchronisation Element.

Depends on FlatDocumentWriter.useLabelConstruct.

isSynchronisationElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether this is an synchronisation Element.

Depends on HierarchicalDocumentReader.useLabelConstruct.

isTargetElement(Node) - Static method in class HierarchicalDocumentReader

Test, whether a node is an Element and a target

item(int) - Method in class MutableNodeListImpl

iTree - Static variable in class GlobalJoin

The (global) tree of instantiation, these joins are relative to.
This is not patrticular to one global join.
Not copied, when cloned.

K

kickOffDoneID - Variable in class FlatDocumentWriter

Id of kickoff location, where every direct child of the root is activated.

Needed for global exits.

kickOffTemplate - Variable in class FlatDocumentWriter

Store kickoff template Element, once crated...

L

layouter - Variable in class FlatDocumentWriter

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

Layouter - interface Layouter.

Interface for Layout modules

layoutTemplate(Element) - Method in interface Layouter

layoutTemplate(Element) - Method in class SimpleLayouter

layoutTemplate(Element) - Method in class SkewedGridLayouter

lm - Static variable in class Flatten

An entity that translates basic locations and keeps track of them

location - Static variable in class Flatten

LocationMapper - class LocationMapper.

Service Class

LocationMapper(HierarchicalDocumentReader, FlatDocumentWriter) - Constructor for class LocationMapper

Default Constructor

locationNameCount - Static variable in class DocumentWriter

Counter to make introduced location names unique

locLabelXShift - Static variable in class SkewedGridLayouter

locLabelYShift - Static variable in class SkewedGridLayouter

locNameXOffset - Static variable in class DocumentWriter

locNameXOffset - Static variable in class SimpleLayouter

locNameXOffset - Static variable in class SkewedGridLayouter

locNameXShift - Static variable in class SkewedGridLayouter

locNameYOffset - Static variable in class DocumentWriter

locNameYOffset - Static variable in class SimpleLayouter

locNameYOffset - Static variable in class SkewedGridLayouter

locNameYShift - Static variable in class SkewedGridLayouter

M

main(String[]) - Static method in class Flatten

Default Constructor: missing (only static)

makeIDSafe(String) - Static method in class DocumentWriter

Transform the ID (Attribute value) to a safe version, i.e.

makeLocationCommitted(Element) - Method in class FlatDocumentWriter

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 FlatDocumentWriter.uppaalDTD)

makeLocationInitial(Element) - Method in class FlatDocumentWriter

NOTE: Only works, if location has been inserted in a template element alread!

makeNameSafe(String) - Static method in class DocumentWriter

Transform the name (cdata content of a Element) to a safe version, i.e.

makeSignalSafe(String) - Static method in class DocumentWriter

Transform the signal (i.e.

mapAssignmentText(String) - Static method in class Flatten

Maps a assignment text of a hierarchical to a flat location.
Used in translation of locations &l; components.

mapComponentToActiveID(Element) - Static method in class Flatten

mapElementToID(Element) - Static method in class Flatten

Get/invent the ID an component maps to

USES Flatten.elementCount

mapEntryToID(Element) - Static method in class Flatten

Compute the ID of the translation of an entry.
A transition in the flat version goes to this ID.

mapExitToID(Element) - Static method in class Flatten

Compute the ID of the translation of an exit.
A transition in the flat version goes to this ID.

mapGuardText(String) - Static method in class Flatten

Maps a guard text of a hierarchical to a flat location.
Used in translation of locations &l; components.

mapHierachicalLocationToFlatOne(Element, TextualInstantiation) - Method in class LocationMapper

Computes the mapping

{Locations, Components} * TextualInstantiation -> Location


Throws an exception, if there is no entry.

mapID(TextualInstantiation, String) - Static method in class Flatten

Maps an ID in a way, such that the output is deterministic the outcome is different for different inputs the outcome is different from flat locations Used in translation of locations &l; components.

mapInvariantText(String) - Static method in class Flatten

Maps an (textual) invariant to a flat location.
Used in translation of locations and components.

mapNail(Element) - Static method in class Flatten

Maps a nail of a hierarchical to a flat location.
Used in translation of locations &l; components.

mapName(String) - Static method in class Flatten

Maps an name in a way, such that the output is deterministic the outcome is different for different inputs the outcome is different from flat locations Used in translation of locations &l; components.

mapSourceToID(String, Element) - Static method in class Flatten

CHECK THAT THIS IS USED CONSISTENTLY WITH INSTANTIATIONS OF ENTRIES/EXITS

mapSynchronisationText(String) - Static method in class Flatten

Maps a synchronisation text of a hierarchical to a flat location.
Used in translation of locations &l; components.

mapTargetIDEntryrefToFlatLocation(String, String, TextualInstantiation) - Method in class LocationMapper

Map ID of Element a connection points to and (possibly) the ID of the entry to a coresponding flat location.
(If it does not exist yet, invent a new (flat) location for it).

If the target point to a basic location, it behaves like

mapTargetToFlatLocation(Element, TextualInstantiation) - Method in class LocationMapper

Map a (hierarchical) target to the flat location it points to.
(If it does not exist yet, invent a new (flat) location for it).

If the target point to a basic location, it behaves like

mapTargetToID(String, Element) - Static method in class Flatten

CHECK THAT THIS IS USED CONSISTENTLY WITH INSTANTIATIONS OF ENTRIES/EXITS

mapTextualInstantiationToActiveLocation(TextualInstantiation) - Method in class LocationMapper

for instantiations of AND templates

mapTextualInstantiationToIdleLocation(TextualInstantiation) - Method in class LocationMapper

for instantiations of XOR/AND templates

mapTinstToHashtable - Variable in class ChannelRegistry

Maps Textual instantiations to hashtables, that contain the syncs occuring in this particular tinst as keys and Vectors of transitions as elements

matchingSync(String) - Static method in class ChannelRegistry

Return matching sync (handshake)
Throw Exception, if the input is not a sync.

max(int, int) - Static method in class ChannelRegistry

MAXimum of two integers.

max(int, int) - Static method in class DocumentReader

the larger of two integers

max(long, long) - Static method in class DocumentReader

the larger of two longs

max3(int, int, int) - Static method in class DocumentReader

the larger of three integers

max4(int, int, int, int) - Static method in class DocumentReader

the larger of four integers

max5(int, int, int, int, int) - Static method in class DocumentReader

the larger of five integers

memorizeIDsOfOriginalDocument() - Method in class DocumentReader

Enter IDs in the hashtable DocumentReader.hashOriginalIDsToElements

Throws exception, if document is not set properly

memorizeInstantionAndComponentIDToTextualInstantiation(String, String, TextualInstantiation) - Static method in class Flatten

Remember the mapping from instantiation + componentID to the TextualInstantiaion this component corresponds to.

Necessary for computing the target/source-ID of non-elementary transitions

memorizeTemplate(Element) - Static method in class Flatten

Remember the connection between (original, hierarchical) templates and names, accesible then in Flatten.hashTemplateNamesToElements

Throws exception, if two templates have the same name

migrateOrdinaryLocation(Element, TextualInstantiation) - Method in class LocationMapper

Take an ordinary location and return a flattened one.

Does NOT migrate all the children (this is job of Flatten, in particular of the methos transformLocationToFlat) and the ID is up to a change later.

However, it records a mapping
{Location, Component} * TextualInstantiation -> Location

that is needed in the translations of global joins.

migrateTransitionChildren(Element, TextualInstantiation, Element) - Static method in class Flatten

Browse the children of the original transition, transform them and add them to the new transition (in the specific instantiation)

min(int, int) - Static method in class DocumentReader

the lesser of two integers

MutableNodeListImpl - class MutableNodeListImpl.

Implements a list of nodes, that Sun could as well have declared as a Vector but is not.

MutableNodeListImpl() - Constructor for class MutableNodeListImpl

Default Constructor

N

name - Static variable in class Flatten

NAME_SEPARATOR_CHAR - Static variable in class DocumentWriter

Separator that can be used in <name> elements

newLocName - Static variable in class SkewedGridLayouter

Name for (formerly) anonymous locations

newLocNameCount - Static variable in class SkewedGridLayouter

Counter for (formerly) anonymous locations

newPostfix() - Static method in class ChannelRegistry

New (uniquifying) postfix to keep track of channel copies

notACommentedLine(String) - Method in class FlatDocumentWriter

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.

O

objectCounter - Static variable in class TextualInstantiation

Counter to provide unique object names

objectName - Variable in class TextualInstantiation

The name of the incarnated object

occursIn(String, TextualInstantiation) - Method in class ChannelRegistry

Check Hashtable for entry

occursInOrBelow(String, TextualInstantiation) - Method in class ChannelRegistry

Checks, whether there exist an entry for sync in the textual instantiation or in any descendand of it

oddSq(long) - Method in class SkewedGridLayouter

-1 if odd, 1 if even

offsetFactor - Static variable in class InstantiationTree

Space indentations when displaying children

oldRoot - Variable in class HierarchicalDocumentReader

original, hierarchical document-root

origDoc - Variable in class DocumentReader

Document it wraps around

originalInstantiationName - Variable in class TextualInstantiation

Object name in the original hierarchical version
Only relevant for global elements

out - Static variable in class Flatten

Output stream writer

P

parameters - Variable in class TextualInstantiation

List of parameters

possibleConflicts - Variable in class ChannelRegistry

Stack of synchronisations that might cause conflicts.
Use method ChannelRegistry.addConflict(java.lang.String, org.w3c.dom.Element, TextualInstantiation) to access it.

processGlobalJoin(GlobalJoin) - Static method in class Flatten

Processing Global Joins

R

recallInstantionAndComponentIDToTextualInstantiation(String, String) - Static method in class Flatten

Counterpart to Flatten.memorizeInstantionAndComponentIDToTextualInstantiation(java.lang.String, java.lang.String, TextualInstantiation).
Maps back to the TextualInstantiation

recomputeAllTemplateLayouts() - Method in class FlatDocumentWriter

Browse through all templates (the ones already in the documnent),
and call the Layouter method on them

registerSync(String, Element, TextualInstantiation) - Method in class ChannelRegistry

Regiser a sync occuring on a specific transition in a specific texual instantiation

(I.e., create appropriate hashtable entries)

resetDefaultLayout() - Method in class DocumentWriter

Start coordinate-counting anew

retrieveTextualInstantiation(Element, TextualInstantiation) - Method in class ComponentMapper

Get the TextualInstantiation according to the mapping

Component * TextualInstantiation ---> TextualInstantiation

The first TextualInstantiation is the declaringContext, the result TextualInstantiation is the (sub-)declared one.

If the TextualInstantiation is not entered yet, it is created with the empty constructor.

root - Variable in class FlatDocumentWriter

Root of DocumentWriter.doc

rootInstDummy - Static variable in class Flatten

Textual instantiation corresponding to the root.

rootOfInstTree - Variable in class ChannelRegistry

(completed) tree of textual instantiations
Needed to compute father/child replation

rootTinst - Variable in class GlobalJoin

The TextualInstantiation, where the rootTransition is instantiated in.

rootTransitions - Variable in class GlobalJoin

A list of transitions, that is taken, after the join has been transformed.
(i.e.

S

SAFE_SEPARATOR_CHAR - Static variable in class DocumentWriter

Separator that can be used everywhere

sanityChecks - Static variable in class DocumentReader

Setting this true, slows down but is good for debugging.

sanityChecks - Static variable in class DocumentWriter

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

sanityChecks - Static variable in class Flatten

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

sanityChecks - Static variable in class GlobalJoin

Setting this true, slows down but is good for debugging.

sanityChecks - Static variable in class LocationMapper

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

sanityChecks - Static variable in class SimpleLayouter

sanityChecks - Static variable in class SkewedGridLayouter

second - Variable in class ElementElementPair

Second of pair

setActivator(String) - Method in class TextualInstantiation

Set the field TextualInstantiation.activator

setup(String, Vector, TextualInstantiation, Element, Element, Element) - Method in class TextualInstantiation

Is assumed to be called exactly once.

showWithOffset(int) - Method in class InstantiationTree

Return a string representing the (sub-)tree, with InstantiationTree.offsetFactor*offset spaces before the name

SimpleLayouter - class SimpleLayouter.

SimpleLayouter(FlatDocumentWriter) - Constructor for class SimpleLayouter

Default Constructor
Needs the flat document writer to access elements by ID (fast)

SkewedGridLayouter - class SkewedGridLayouter.

SkewedGridLayouter(FlatDocumentWriter) - Constructor for class SkewedGridLayouter

Default Constructor
Needs the flat document writer to access elements by ID (fast)

slackInstantiations - Static variable in class FlatDocumentWriter

A vector of Strings that are to be added to the (global) instantiation

source - Static variable in class Flatten

spaces - Static variable in class InstantiationTree

splitCommaSeperatedString(String) - Static method in class HierarchicalDocumentReader

Given a string containing a comma-speparated list, split it into a vector of Strings (without the commata).
Trims the strings (cuts away whitespaces).

stopGrowingThisOne() - Method in class GlobalJoin

Remove from {link #allGlobalJoins} and terminate the growth obligations.

sync - Variable in class SyncTransTinstTriple

synchronisation - Static variable in class Flatten

synchronisationNameCount - Static variable in class DocumentWriter

Counter to make introduced channel names unique

synchronisationXOffset - Static variable in class SimpleLayouter

synchronisationXOffset - Static variable in class SkewedGridLayouter

synchronisationXShift - Static variable in class SimpleLayouter

synchronisationXShift - Static variable in class SkewedGridLayouter

synchronisationYOffset - Static variable in class SimpleLayouter

synchronisationYOffset - Static variable in class SkewedGridLayouter

synchronisationYShift - Static variable in class SimpleLayouter

synchronisationYShift - Static variable in class SkewedGridLayouter

SyncTransTinstTriple - class SyncTransTinstTriple.

SyncTransTinstTriple(String, Element, TextualInstantiation) - Constructor for class SyncTransTinstTriple

Default Constructor

system - Variable in class FlatDocumentWriter

system - Static variable in class Flatten

systemComponents - Variable in class FlatDocumentWriter

Store all (instantiated) component of the system by the name String

systemText - Variable in class FlatDocumentWriter

Text declaring the flat system.
Accumulates all the timed automata executed in parallel.

T

target - Static variable in class Flatten

template - Static variable in class Flatten

templateElement - Variable in class TextualInstantiation

The (hierarchical old) Element node this object instantiates

templateNameCount - Static variable in class DocumentWriter

Counter to make introduced template names unique

templates - Variable in class FlatDocumentWriter

Templates that are to be instantiated at some point

testGeoCordinates(long) - Method in class DocumentWriter

TextualInstantiation - class TextualInstantiation.

Stores information about textual instantiations.

TextualInstantiation() - Constructor for class TextualInstantiation

Empty Constructor; use TextualInstantiation.setup(java.lang.String, java.util.Vector, TextualInstantiation, org.w3c.dom.Element, org.w3c.dom.Element, org.w3c.dom.Element) to fill with meaning.

TextualInstantiation(String, Vector, TextualInstantiation, Element, Element, Element) - Constructor for class TextualInstantiation

Default Constructor objectPrefix gives a hint, in how to name the object such that the origin is derivable The vector gives the list of parameters fatherPrefix is the textual prefix of the father instantiation
it is used for unique naming templateElement is the node in the hierarchical document that is instanciated
(for the kicker, this is null) NOTE:Equivalently, you can call the empty constructor and later call TextualInstantiation.setup(java.lang.String, java.util.Vector, TextualInstantiation, org.w3c.dom.Element, org.w3c.dom.Element, org.w3c.dom.Element) with the same arguments.

textuallyConjunctInvariants(String, String) - Static method in class FlatDocumentWriter

Returns (texualy) a logical and of two invariant texts.
(does not manipulate the texts themselves)

threshold - Variable in class GlobalJoin

Number of locations that are required to take the join.

tinst - Variable in class SyncTransTinstTriple

tinst - Variable in class TinstElementPair

The textual instantiation the element belongs to

TinstElementPair - class TinstElementPair.

Wrapper Class for a pair describing an explicit element.
Usually used for Exits and Locations.

TinstElementPair(TextualInstantiation, Element) - Constructor for class TinstElementPair

Default Constructor

tinstsToExit - Variable in class GlobalJoin

Stack that collects the textual instantiaions, that have to be exited, when the join is taken.
It preserves a partial order in the sense, that the top-most element in the stack is always at the lowest level and a sub-component A of a component B is always higher in the stack than B.

toString() - Method in class GlobalJoin

Exhaustively describes this global join

toString() - Method in class TextualInstantiation

Returns the instantiation text

objectName := templateName(parameters)

toString() - Method in class TinstElementPair

trans - Variable in class SyncTransTinstTriple

transformLocationToFlat(TextualInstantiation, Element) - Static method in class Flatten

Returns a flat location that corresponds to the hierarchical one, but name is altered IDs are mapped Coordinates are copied

transformSimpleNode(Node) - Static method in class Flatten

Transforms the following simple elements to a flat element name invariant urgent committed (does alter names/ids/etc.

transition - Static variable in class Flatten

translateANDTemplateInstantiation(TextualInstantiation) - Static method in class Flatten

Translates a instantiation of a hierarchical AND template to a flat (xor) template instantiation

translateTemplateInstantiation(TextualInstantiation) - Static method in class Flatten

Translates a instantiation of a hierarchical template to a flat one

translateXORTemplateInstantiation(TextualInstantiation) - Static method in class Flatten

Translates a instantiation of a hierarchical AND template to a flat (xor) template instantiation

translationOfTemplateElement - Variable in class TextualInstantiation

Pointer to the (flat) template Element this textual instantiation was translated to.

Used for the global joins, i.e.

traverse(Document, String) - Static method in class Flatten

Traverse and spam...

traverseNode(Node, int) - Static method in class Flatten

triggerVariable - Variable in class GlobalJoin

Name of the counter associated with the global join.
It is also used as a trigger to perform the join completly

triggerVariableCounter - Static variable in class GlobalJoin

To make trigger Variables unique

typeOfSync(String) - Static method in class ChannelRegistry

Return 'type' of sync (handshake), i.e.

U

unambigousIDSeparator - Static variable in class LocationMapper

Separates IDs of element and contiains characters that are disallowed for XML IDs, thus no concatations of different IDs with this separator can give a clash

unambigousNameSeparator - Static variable in class HierarchicalDocumentReader

Separate Strings (names) for hashing

uniquePostfix - Static variable in class ChannelRegistry

Postfix for channel copies NOTE:!!! Should contain some chars that the user cannot use !!!

unregisterSync(String, Element, TextualInstantiation) - Method in class ChannelRegistry

UNRegiser a sync occuring on a specific transition in a specific texual instantiation, i.e., remove from database
(Needed if the synchronization changes)
Throws exception, if there was no registration entry.

uppaalDTD - Static variable in class FlatDocumentWriter

Version of the flat uppaal grammar that is used.

uppaalDTD_URI - Static variable in class FlatDocumentWriter

Used DTD for flat Uppaal documents.
Give the http:// or file:/ location

useLabelConstruct - Static variable in class FlatDocumentWriter

Determines whether translations uses the <label> construct or not.

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

useLabelConstruct - Static variable in class HierarchicalDocumentReader

Determines whether translations uses the <label> construct for assignments, guards and synchronisations.

useLabelForInvariants - Static variable in class FlatDocumentWriter

Determines whether grammar uses the <label> construct also for invariants.

useLabelForInvariants - Static variable in class HierarchicalDocumentReader

Determines whether translations uses the <label> construct also for invariants.

V

VERSION - Static variable in class Flatten

String describing the version of this API

VERSION_DATE - Static variable in class Flatten

Date of last changes

VERSION_NAME - Static variable in class Flatten

Name of this version (should be global for project)

W

wrapAroundInstHashTable - Variable in class HierarchicalDocumentReader

Hashing global element names to dummy component Elements

wrapComponentAroundGlobalInstantiation(String, String) - Method in class HierarchicalDocumentReader

Returns a (dummy) component Element, that points to a global instantiation.
Once constructed, these Elements are stored in a Hashtable, so the result on the same call will be unique.

writeToFile(String) - Method in class FlatDocumentWriter

Output the (current) flat document to a given file.
Old file contents, if any, are destroyed.

X

xSkew - Static variable in class SkewedGridLayouter

Value 0 corresponds to simple grid layout

Y

ySkew - Static variable in class SkewedGridLayouter

Value 0 corresponds to simple grid layout

A B C D E F G H I K L M N O P R S T U V W X Y