Package com.uppaal.model.core2
Class Document
- java.lang.Object
-
- com.uppaal.model.core2.Element
-
- com.uppaal.model.core2.Node
-
- com.uppaal.model.core2.Document
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class Document extends Node
Model for a network of timed automata as defined in UPPAAL. The document object is the root of a tree containing templates, locations and edges.This class supports the command pattern: It can execute classes implementing the Command interface. It also supports unlimited undo/redo. When using the command interface, each change will increment a version counter. Notice that the version counter is not incremented if the document tree is modified directly.
Before any xml files are read, we need to set Uppaal XML resolver to support various schema versions:
com.uppaal.model.io2.XMLReader.setXMLResolver(new com.uppaal.model.io2.UXMLResolver());
Then UPPAAL timed automata model document can be loaded from a file or Internet by using a PrototypeDocument.load() method:
Document doc = new PrototypeDocument().load(url);
The following code demonstrates how to create a document from scratch with default properties (colors and so on) without using editor
Command
s:PrototypeDocument prototype = new PrototypeDocument(); Document doc = new Document(prototype); doc.setProperty("declarations", "clock x;"); // shared global clock x
Then a template can be created and manipulated as follows:Template t = doc.createTemplate(); // new TA template with defaults doc.insert(t, null).setProperty("name", "Template"); // insert and set the name t.setProperty("declarations", "clock y;"); // create local clock y
The timed automata elements can be created like-wise:Location l0 = t.createLocation(); // create a location t.insert(l0, null).setProperty("name", "L0"); // insert and name it l0.setProperty("x", 0); // set the graphical position x l0.setProperty("y", 0); // set the graphical position y l0.setFlag("urgent", true); // make the location urgent Location l1 = t.createLocation(); t.insert(l1, l0).setProperty("name", "L1"); l1.setProperty("x", 200); l1.setProperty("y", 0); Edge e = t.createEdge(); // create an edge t.insert(e, l1); // insert it after location l1 (can be null) e.setSource(l0); // set the origin e.setTarget(l1); // set the destination e.setProperty("assignment", "x = 0, y = 0"); // add some assignments
Finally a system declaration should be added:doc.setProperty("system", "Process = Template();\n"+ "system Process;");
Then the model can be saved into an XML file:try { doc.save("sampledoc.xml"); } catch (IOException e) { e.printStackTrace(System.err); }
For further examples, visit Engine on how to compile and interact with simulator and verifier.
-
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description void
accept(Visitor visitor)
Accept a visitor.LscTemplate
createLscTemplate()
Creates a new stand-alone LSC template using a LSC prototype from the document.Template
createTemplate()
Creates a new stand-alone TA template using a template prototype from the document.Document
getDocument()
Returns the document of this element.AbstractTemplate
getLastTATemplate()
Returns the last TA template or null if no such template exists.QueryList
getQueryList()
Returns the model of the list of queries defined in this document.AbstractTemplate
getTemplate(String name)
Returns the first template with the given name or null if no such template exists.AbstractTemplate
getTemplates()
Returns the first template of the document.String
getVersion()
Get the current number of the documentString
getXPathTag()
Computes the local tag of the XPath address.static boolean
merge(AbstractTemplate source, AbstractTemplate target)
Merges the source template into target (useful for pasting from clipboard).Element
resolveXPath(String path)
Resolve the pathvoid
save(File file)
Save the data into the filevoid
save(String path)
Save the data into the file-
Methods inherited from class com.uppaal.model.core2.Node
clone, getFirst, getLast, getNext, getPrevious, insert, move, remove, setPrototype
-
Methods inherited from class com.uppaal.model.core2.Element
acceptSafe, addListener, getColor, getCommandManager, getLocalProperty, getParent, getProperties, getProperty, getPropertyValue, getPrototype, getPrototypeFromParent, getTemplate, getX, getXMLLabelKinds, getXPath, getY, hasFlag, importInto, isPropertyLocal, removeListener, setCommandManager, setProperties, setProperty, setPropertyFromPath
-
-
-
-
Constructor Detail
-
Document
public Document()
Constructor without a prototype.
-
Document
public Document(Element prototype)
Constructor using the given prototype.- Parameters:
prototype
- - The element prototype
-
-
Method Detail
-
getVersion
public String getVersion()
Get the current number of the document- Returns:
- sb - The version number
-
getQueryList
public QueryList getQueryList()
Returns the model of the list of queries defined in this document.- Returns:
- queries - The queries
-
createTemplate
public Template createTemplate()
Creates a new stand-alone TA template using a template prototype from the document. The new template is not added to the document tree!- Returns:
- - The template
-
createLscTemplate
public LscTemplate createLscTemplate()
Creates a new stand-alone LSC template using a LSC prototype from the document. The new template is not added to the document tree!- Returns:
- - the lsc template
-
getTemplates
public AbstractTemplate getTemplates()
Returns the first template of the document. This is the same as calling getFirst() and type casting the result to a Template.- Returns:
- - The abstract template
-
getTemplate
public AbstractTemplate getTemplate(String name)
Returns the first template with the given name or null if no such template exists.- Parameters:
name
- - The template name- Returns:
- - The abstract template
-
getLastTATemplate
public AbstractTemplate getLastTATemplate()
Returns the last TA template or null if no such template exists.- Returns:
- - The abstract template
-
accept
public void accept(Visitor visitor) throws Exception
Description copied from class:Element
Accept a visitor. This method is specialized in every subclass. Part of the visitor pattern.
-
getDocument
public Document getDocument()
Description copied from class:Element
Returns the document of this element.- Overrides:
getDocument
in classElement
- Returns:
- The document object
-
resolveXPath
public Element resolveXPath(String path)
Resolve the path- Parameters:
path
- - The path- Returns:
- - The element object
-
merge
public static boolean merge(AbstractTemplate source, AbstractTemplate target)
Merges the source template into target (useful for pasting from clipboard). The source template gets emptied without a notice. The new elements are placed to the right of existing elements.- Parameters:
source
- - The source abstract templatetarget
- - The target abstract template- Returns:
- merging successful
-
save
public void save(String path) throws IOException
Save the data into the file- Parameters:
path
- - The file path to save to- Throws:
IOException
- file system I/O error.
-
save
public void save(File file) throws IOException
Save the data into the file- Parameters:
file
- - The output file- Throws:
IOException
- file system I/O error.
-
getXPathTag
public String getXPathTag()
Description copied from class:Element
Computes the local tag of the XPath address. Needs to be overwritten by concrete instances- Overrides:
getXPathTag
in classNode
- Returns:
- local address of this element
-
-