Class Flatten

java.lang.Object
  |
  +--org.xml.sax.helpers.DefaultHandler
        |
        +--Flatten

All Implemented Interfaces:

org.xml.sax.ContentHandler, org.xml.sax.DTDHandler, org.xml.sax.EntityResolver, org.xml.sax.ErrorHandler

public class Flatten

extends org.xml.sax.helpers.DefaultHandler

Flattening Huppaal Definitions

This is a prototype for flattening a hierarchical timed automata definition (according to DOM HierarchicalDocumentReader.huppaalDTD)
The optained description has the same behaviour (modulo some construction slack) as the hierarchical one.

For a detailled description see hu.tex

Jargon

• slack: overhead introduced by the translation
• create: do what you are told
• invent: create and add some unique value
• copy: mirror without changes
• transform: mirror with changes
• migrate: mirror with changes and append to some argument
• map: transformation of Strings

To be sorted out

• translation of TCTL formulas?
• relationship between original and newly introduced names
• modularity of templates (currently: one new flat template per instantiation of a hierarchical one)
• translation of traces back and forth

Known Problems

• all variables are global (the translations of global joins works like this at the moment
• name clashes are not detected
• order of assignments in global joins might be strange
• geometrical Layout has to be fixed

Version:

Vanilla-1 Mon Apr 9 14:28:09 2001

Author:

M. Oliver Möller

See Also:

GlobalJoin

Field Summary

(package private) static org.w3c.dom.Element	assignment
(package private) static int	attIndent Additional Indentation for attributes
(package private) static java.lang.String	blanks
private static ComponentMapper	cm An entity that translates pairs (hierarchial component, textual instantiation) to the textual instantiation of this compenent.
(package private) static java.util.Vector	collectedInstantiations
(package private) static long	componentCount Counter to make introduced locations for components unique
private static ChannelRegistry	cr Registration of hand-shake communication for Phase III processing
(package private) static java.lang.String	currentTemplatePrefix Prefix that makes the currently translated Template unique
(package private) static boolean	debug Spam out debuggin information, if debug is true
(package private) static long	elementCount Counter to make hashing of elements unique
(package private) static int	factor Factor for indenting
private static FlatDocumentWriter	fdw The way to create the flat document
private static org.apache.crimson.tree.XmlDocument	flatDoc The document that the fdw is writing
(package private) static InstantiationTree	globalInstantiationTree The tree the system is mapped to
(package private) static org.w3c.dom.Element	guard
private static java.util.Hashtable	hashElementsToIDs Hashtable storing the IDs the tranlation of elements corresponds to ?t?
private static java.util.Hashtable	hashInstComponentToTInst Hashtable mapping instantiation/componentID to the TextualInstantiation it corresponds to.
private static java.util.Hashtable	hashTemplateNamesToElements Hashtable mapping (original, hierarchical) template names to the corresponding Element nodes, see memorizeTemplate(org.w3c.dom.Element)
(package private) static HierarchicalDocumentReader	hdr The way to access the hierarchical document
(package private) static org.w3c.dom.Element	instantiation
(package private) static java.util.Stack	instantiationsToBeTranslated Main stack that contains the instantiations of templates to be processed
private static LocationMapper	lm An entity that translates basic locations and keeps track of them
(package private) static org.w3c.dom.Element	location
(package private) static org.w3c.dom.Element	name
private static java.io.Writer	out Output stream writer
protected static TextualInstantiation	rootInstDummy Textual instantiation corresponding to the root.
(package private) static boolean	sanityChecks Do (possibly time-consuming) sanity checks, if true
(package private) static org.w3c.dom.Element	source
(package private) static org.w3c.dom.Element	synchronisation
(package private) static org.w3c.dom.Element	system
(package private) static org.w3c.dom.Element	target
(package private) static org.w3c.dom.Element	template
(package private) static org.w3c.dom.Element	transition
static java.lang.String	VERSION String describing the version of this API
static java.lang.String	VERSION_DATE Date of last changes
static java.lang.String	VERSION_NAME Name of this version (should be global for project)

Constructor Summary

Flatten()

Method Summary

private static org.w3c.dom.Element	addRegisteredReceiveSynchronisationToTransition(java.lang.String syncText, org.w3c.dom.Element transition, TextualInstantiation tinst) Add RECEIVE synchronization and provide registration in {@see ChannelRegistry} Returns the synchronisation Element (only necessary for original (hierarchical) synchronizations) ??? necessary ???
private static org.w3c.dom.Element	addRegisteredSendSynchronisationToTransition(java.lang.String syncText, org.w3c.dom.Element transition, TextualInstantiation tinst) Add SEND synchronization and provide registration in {@see ChannelRegistry} Returns the synchronisation Element (only necessary for original (hierarchical) synchronizations) ??? necessary ???
private static org.w3c.dom.Element	addRegisteredSynchronisationToTransition(java.lang.String syncText, org.w3c.dom.Element transition, TextualInstantiation tinst) Add synchronization and provide registration in {@see ChannelRegistry} Returns the synchronisation Element (only necessary for original (hierarchical) synchronizations)
static org.apache.crimson.tree.XmlDocument	constructFlatDoc(HierarchicalDocumentReader reader) Main Method
private static java.lang.String	getActiveSubcomponentID(TextualInstantiation cpt) 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.
private static org.w3c.dom.Element	getFirstChildThatIsElement(org.w3c.dom.Element el, java.lang.String tagName) Return the first child element that is of the given kind. Throws an Exception, if no such child exists.
static org.w3c.dom.Element	getNodeOfTemplate(java.lang.String s) Return the node with specified template name
private static java.lang.String	getSignal(java.lang.String instantiationName, org.w3c.dom.Element entryOrExit) The signal this entry/exit corresponds to (without !/?) If the component in question is not a enty/exit, an exception is thrown.
static void	main(java.lang.String[] argv) Default Constructor: missing (only static)
static java.lang.String	mapAssignmentText(java.lang.String text) Maps a assignment text of a hierarchical to a flat location. Used in translation of locations &l; components.
static java.lang.String	mapComponentToActiveID(org.w3c.dom.Element compt)
private static java.lang.String	mapElementToID(org.w3c.dom.Element el) Get/invent the ID an component maps to USES elementCount
static java.lang.String	mapEntryToID(org.w3c.dom.Element entry) Compute the ID of the translation of an entry. A transition in the flat version goes to this ID.
static java.lang.String	mapExitToID(org.w3c.dom.Element exit) Compute the ID of the translation of an exit. A transition in the flat version goes to this ID.
static java.lang.String	mapGuardText(java.lang.String text) Maps a guard text of a hierarchical to a flat location. Used in translation of locations &l; components.
private static java.lang.String	mapID(TextualInstantiation tinst, java.lang.String ID) 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.
static java.lang.String	mapInvariantText(java.lang.String inv) Maps an (textual) invariant to a flat location. Used in translation of locations and components.
static org.w3c.dom.Element	mapNail(org.w3c.dom.Element nail) Maps a nail of a hierarchical to a flat location. Used in translation of locations &l; components.
private static java.lang.String	mapName(java.lang.String name) 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.
static java.lang.String	mapSourceToID(java.lang.String instantiationName, org.w3c.dom.Element source) CHECK THAT THIS IS USED CONSISTENTLY WITH INSTANTIATIONS OF ENTRIES/EXITS
static java.lang.String	mapSynchronisationText(java.lang.String syncText) Maps a synchronisation text of a hierarchical to a flat location. Used in translation of locations &l; components.
static java.lang.String	mapTargetToID(java.lang.String instantiationName, org.w3c.dom.Element target) CHECK THAT THIS IS USED CONSISTENTLY WITH INSTANTIATIONS OF ENTRIES/EXITS
static void	memorizeInstantionAndComponentIDToTextualInstantiation(java.lang.String instantiationName, java.lang.String componentID, TextualInstantiation tinst) Remember the mapping from instantiation + componentID to the TextualInstantiaion this component corresponds to. Necessary for computing the target/source-ID of non-elementary transitions
static void	memorizeTemplate(org.w3c.dom.Element template) Remember the connection between (original, hierarchical) templates and names, accesible then in hashTemplateNamesToElements Throws exception, if two templates have the same name
private static void	migrateTransitionChildren(org.w3c.dom.Element origTransition, TextualInstantiation tinst, org.w3c.dom.Element newTransition) Browse the children of the original transition, transform them and add them to the new transition (in the specific instantiation)
private static void	processGlobalJoin(GlobalJoin gj) Processing Global Joins
static TextualInstantiation	recallInstantionAndComponentIDToTextualInstantiation(java.lang.String instantiationName, java.lang.String componentID) Counterpart to memorizeInstantionAndComponentIDToTextualInstantiation(java.lang.String, java.lang.String, TextualInstantiation). Maps back to the TextualInstantiation
private static org.w3c.dom.Element	transformLocationToFlat(TextualInstantiation tinst, org.w3c.dom.Element loc) Returns a flat location that corresponds to the hierarchical one, but name is altered IDs are mapped Coordinates are copied
private static org.w3c.dom.Element	transformSimpleNode(org.w3c.dom.Node node) Transforms the following simple elements to a flat element name invariant urgent committed (does alter names/ids/etc.
private static java.lang.String	translateANDTemplateInstantiation(TextualInstantiation tinst) Translates a instantiation of a hierarchical AND template to a flat (xor) template instantiation
private static java.lang.String	translateTemplateInstantiation(TextualInstantiation tinst) Translates a instantiation of a hierarchical template to a flat one
private static java.lang.String	translateXORTemplateInstantiation(TextualInstantiation tinst) Translates a instantiation of a hierarchical AND template to a flat (xor) template instantiation
private static void	traverse(org.w3c.dom.Document doc, java.lang.String root) Traverse and spam...
private static void	traverseNode(org.w3c.dom.Node n, int o)

Methods inherited from class org.xml.sax.helpers.DefaultHandler

characters, endDocument, endElement, endPrefixMapping, error, fatalError, ignorableWhitespace, notationDecl, processingInstruction, resolveEntity, setDocumentLocator, skippedEntity, startDocument, startElement, startPrefixMapping, unparsedEntityDecl, warning

Methods inherited from class java.lang.Object

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

Field Detail

VERSION_NAME

public static final java.lang.String VERSION_NAME

Name of this version (should be global for project)

VERSION_DATE

public static final java.lang.String VERSION_DATE

Date of last changes

VERSION

public static final java.lang.String VERSION

String describing the version of this API

factor

static int factor

Factor for indenting

attIndent

static int attIndent

Additional Indentation for attributes

blanks

static java.lang.String blanks

hdr

static HierarchicalDocumentReader hdr

The way to access the hierarchical document

fdw

private static FlatDocumentWriter fdw

The way to create the flat document

lm

private static LocationMapper lm

An entity that translates basic locations and keeps track of them

cm

private static ComponentMapper cm

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

cr

private static ChannelRegistry cr

Registration of hand-shake communication for Phase III processing

flatDoc

private static org.apache.crimson.tree.XmlDocument flatDoc

The document that the fdw is writing

rootInstDummy

protected static TextualInstantiation rootInstDummy

Textual instantiation corresponding to the root.

globalInstantiationTree

static InstantiationTree globalInstantiationTree

The tree the system is mapped to

instantiation

static org.w3c.dom.Element instantiation

system

static org.w3c.dom.Element system

template

static org.w3c.dom.Element template

location

static org.w3c.dom.Element location

name

static org.w3c.dom.Element name

transition

static org.w3c.dom.Element transition

source

static org.w3c.dom.Element source

target

static org.w3c.dom.Element target

guard

static org.w3c.dom.Element guard

synchronisation

static org.w3c.dom.Element synchronisation

assignment

static org.w3c.dom.Element assignment

collectedInstantiations

static java.util.Vector collectedInstantiations

currentTemplatePrefix

static java.lang.String currentTemplatePrefix

Prefix that makes the currently translated Template unique

instantiationsToBeTranslated

static java.util.Stack instantiationsToBeTranslated

Main stack that contains the instantiations of templates to be processed

In Vanilla-1, every template is instantiated exactly once

componentCount

static long componentCount

Counter to make introduced locations for components unique

elementCount

static long elementCount

Counter to make hashing of elements unique

hashTemplateNamesToElements

private static java.util.Hashtable hashTemplateNamesToElements

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

hashElementsToIDs

private static java.util.Hashtable hashElementsToIDs

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

hashInstComponentToTInst

private static java.util.Hashtable hashInstComponentToTInst

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

out

private static java.io.Writer out

Output stream writer

debug

static boolean debug

Spam out debuggin information, if debug is true

sanityChecks

static boolean sanityChecks

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

Constructor Detail

Flatten

public Flatten()

Method Detail

main

public static void main(java.lang.String[] argv)

Default Constructor: missing (only static)

constructFlatDoc

public static org.apache.crimson.tree.XmlDocument constructFlatDoc(HierarchicalDocumentReader reader)
                                                            throws java.lang.Exception

Main Method

Create an nta document that is a translation of the original one
Uses auxillary global fields, like hdr or flatDoc. Constructs the globalInstantiationTree, which is used to compute the global joins.

getNodeOfTemplate

public static org.w3c.dom.Element getNodeOfTemplate(java.lang.String s)
                                             throws java.lang.Exception

Return the node with specified template name

getFirstChildThatIsElement

private static org.w3c.dom.Element getFirstChildThatIsElement(org.w3c.dom.Element el,
                                                              java.lang.String tagName)
                                                       throws java.lang.Exception

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

translateTemplateInstantiation

private static java.lang.String translateTemplateInstantiation(TextualInstantiation tinst)
                                                        throws java.lang.Exception

Translates a instantiation of a hierarchical template to a flat one

Assumes:

• Every component will be translated (somewhere else)
• The activator of a component is "_activate_" + ID
• the activator has been declared as a channel

Add the template to fdw via the method FlatDocumentWriter.addTemplate(org.w3c.dom.Element). Returns the textual name of the generated instantiation.

Creates a flat template from a hierarchical one

• the result will have no name
• the result has always an parameter element, possibly it is empty
• there is an additional initial location ("_idle")
• !!! entry points
• !!! exit points
• components are translated into ordinary locations
• transitions to components are augmented with the appropriate ?-synchronisation
• transitions from components are augmented with the appropriate ?-synchronisation

Constructs the globalInstantiationTree as it goes along

USES GLOBAL FIELD currentTemplatePrefix

translateXORTemplateInstantiation

private static java.lang.String translateXORTemplateInstantiation(TextualInstantiation tinst)
                                                           throws java.lang.Exception

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

(called from translateTemplateInstantiation)

translateANDTemplateInstantiation

private static java.lang.String translateANDTemplateInstantiation(TextualInstantiation tinst)
                                                           throws java.lang.Exception

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

(called from translateTemplateInstantiation)

processGlobalJoin

private static void processGlobalJoin(GlobalJoin gj)
                               throws java.lang.Exception

Processing Global Joins

For every global join, do

• push the guard of the outgoing transition inside
• declare sync channels
  if required, make the synchronization channels urgent
• for the locations associated with this global join:
  • to ingoing transitions, add increment to counterVariable
  • to outgoing transitions (that are not modelling the join), add decrement to counterVariable
  • to join-transition, add reset of counterVariable

Structure of the translation

The translation is basically a chain of committed locations, that synchronizes by sending exit signals to the corresponding sub-components. This is done in the translation of the sub-component, where the root transition of the global join starts
The first transition contains

• all the guards (in particular the one that states, whether it can be taken)
• all the assignment
• the synchronisation of the root transition (if any)

NOTE: Uses {@see ChannelRegistry} to enter possible Phase III conflicts

migrateTransitionChildren

private static void migrateTransitionChildren(org.w3c.dom.Element origTransition,
                                              TextualInstantiation tinst,
                                              org.w3c.dom.Element newTransition)
                                       throws java.lang.Exception

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

mapID

private static java.lang.String mapID(TextualInstantiation tinst,
                                      java.lang.String ID)

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.

mapName

private static java.lang.String mapName(java.lang.String name)

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.

mapInvariantText

public static java.lang.String mapInvariantText(java.lang.String inv)

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

!!! Might be necessary to translate the variable names !!!

mapSynchronisationText

public static java.lang.String mapSynchronisationText(java.lang.String syncText)
                                               throws java.lang.Exception

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

!!! Might be necessary to translate the variable names !!!

mapAssignmentText

public static java.lang.String mapAssignmentText(java.lang.String text)
                                          throws java.lang.Exception

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

!!! Might be necessary to translate the variable names !!!

mapGuardText

public static java.lang.String mapGuardText(java.lang.String text)
                                     throws java.lang.Exception

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

!!! Might be necessary to translate the variable names !!!

mapNail

public static org.w3c.dom.Element mapNail(org.w3c.dom.Element nail)
                                   throws java.lang.Exception

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

mapSourceToID

public static java.lang.String mapSourceToID(java.lang.String instantiationName,
                                             org.w3c.dom.Element source)
                                      throws java.lang.Exception

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

mapTargetToID

public static java.lang.String mapTargetToID(java.lang.String instantiationName,
                                             org.w3c.dom.Element target)
                                      throws java.lang.Exception

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

mapEntryToID

public static java.lang.String mapEntryToID(org.w3c.dom.Element entry)
                                     throws java.lang.Exception

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

mapExitToID

public static java.lang.String mapExitToID(org.w3c.dom.Element exit)
                                    throws java.lang.Exception

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

mapComponentToActiveID

public static java.lang.String mapComponentToActiveID(org.w3c.dom.Element compt)
                                               throws java.lang.Exception

mapElementToID

private static java.lang.String mapElementToID(org.w3c.dom.Element el)
                                        throws java.lang.Exception

Get/invent the ID an component maps to

USES elementCount

getSignal

private static java.lang.String getSignal(java.lang.String instantiationName,
                                          org.w3c.dom.Element entryOrExit)
                                   throws java.lang.Exception

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

transformLocationToFlat

private static org.w3c.dom.Element transformLocationToFlat(TextualInstantiation tinst,
                                                           org.w3c.dom.Element loc)
                                                    throws java.lang.Exception

Returns a flat location that corresponds to the hierarchical one, but

• name is altered
• IDs are mapped
• Coordinates are copied

Takes care of

• invariants
• committed location propagation
• synchronisation

transformSimpleNode

private static org.w3c.dom.Element transformSimpleNode(org.w3c.dom.Node node)
                                                throws java.lang.Exception

Transforms the following simple elements to a flat element

• name
• invariant
• urgent
• committed

(does alter names/ids/etc. in the canonical way)

Will swallow (i.e. return null on the following:

• parameter (since if it occurs in components, THOSE are translated to locations

Returns null, if the node is not an Element.
Throws exception if the way to deal with it is unknown.

addRegisteredSynchronisationToTransition

private static org.w3c.dom.Element addRegisteredSynchronisationToTransition(java.lang.String syncText,
                                                                            org.w3c.dom.Element transition,
                                                                            TextualInstantiation tinst)
                                                                     throws java.lang.Exception

Add synchronization and provide registration in {@see ChannelRegistry}

Returns the synchronisation Element

(only necessary for original (hierarchical) synchronizations)

addRegisteredSendSynchronisationToTransition

private static org.w3c.dom.Element addRegisteredSendSynchronisationToTransition(java.lang.String syncText,
                                                                                org.w3c.dom.Element transition,
                                                                                TextualInstantiation tinst)
                                                                         throws java.lang.Exception

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

Returns the synchronisation Element

(only necessary for original (hierarchical) synchronizations)

??? necessary ???

addRegisteredReceiveSynchronisationToTransition

private static org.w3c.dom.Element addRegisteredReceiveSynchronisationToTransition(java.lang.String syncText,
                                                                                   org.w3c.dom.Element transition,
                                                                                   TextualInstantiation tinst)
                                                                            throws java.lang.Exception

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

Returns the synchronisation Element

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

getActiveSubcomponentID

private static java.lang.String getActiveSubcomponentID(TextualInstantiation cpt)
                                                 throws java.lang.Exception

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. the locations lives in the translation of the instantiation of the father component of this one.

It is unique, since this version introduces new templates for everything.

memorizeTemplate

public static void memorizeTemplate(org.w3c.dom.Element template)
                             throws java.lang.Exception

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

Throws exception, if two templates have the same name

memorizeInstantionAndComponentIDToTextualInstantiation

public static void memorizeInstantionAndComponentIDToTextualInstantiation(java.lang.String instantiationName,
                                                                          java.lang.String componentID,
                                                                          TextualInstantiation tinst)

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

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

recallInstantionAndComponentIDToTextualInstantiation

public static TextualInstantiation recallInstantionAndComponentIDToTextualInstantiation(java.lang.String instantiationName,
                                                                                        java.lang.String componentID)

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

traverseNode

private static void traverseNode(org.w3c.dom.Node n,
                                 int o)

traverse

private static void traverse(org.w3c.dom.Document doc,
                             java.lang.String root)
                      throws java.lang.Exception

Traverse and spam...