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.

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