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.

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: 
 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.
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.
      Parameters:
      prototype - - The element prototype

  • Method Details

    • 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.
      Overrides:
      accept in class Node
      Parameters:
      visitor - - The visitor
      Throws:
      Exception - the visitor threw an exception.

    • getDocument

      public Document getDocument()
      Description copied from class: Element
      Returns the document of this element.
      Overrides:
      getDocument in class Element
      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 template
      target - - 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 class Node
      Returns:
      local address of this element