Class 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.

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 Commands:

 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:
      "Process = Template();\n"+
      "system Process;");
Then the model can be saved into an XML file:
 try {"sampledoc.xml");
 } catch (IOException e) {
For further examples, visit Engine on how to compile and interact with simulator and verifier.
See Also:
Template, Location, Edge, Element, Property, Serialized Form
  • Constructor Details

    • Document

      public Document()
      Constructor without a prototype.
    • Document

      public Document​(Element prototype)
      Constructor using the given prototype.
      prototype - - The element prototype
  • Method Details

    • getVersion

      public String getVersion()
      Get the current number of the document
      sb - The version number
    • getQueryList

      public QueryList getQueryList()
      Returns the model of the list of queries defined in this document.
      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!
      - 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!
      - 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.
      - The abstract template
    • getTemplate

      public AbstractTemplate getTemplate​(String name)
      Returns the first template with the given name or null if no such template exists.
      name - - The template name
      - The abstract template
    • getLastTATemplate

      public AbstractTemplate getLastTATemplate()
      Returns the last TA template or null if no such template exists.
      - 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.
      accept in class Node
      visitor - - The visitor
      Exception - the visitor threw an exception.
    • getDocument

      public Document getDocument()
      Description copied from class: Element
      Returns the document of this element.
      getDocument in class Element
      The document object
    • resolveXPath

      public Element resolveXPath​(String path)
      Resolve the path
      path - - The path
      - 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.
      source - - The source abstract template
      target - - The target abstract template
      merging successful
    • save

      public void save​(String path) throws IOException
      Save the data into the file
      path - - The file path to save to
      IOException - file system I/O error.
    • save

      public void save​(File file) throws IOException
      Save the data into the file
      file - - The output file
      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
      getXPathTag in class Node
      local address of this element