<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -->
<!-- Revised hierarchical document definition                      -->
<!--                                                               -->
<!-- Synopsis:                                                     -->
<!--  XML, hierarchical Uppaal                                     -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -->
<!-- @TABLE OF CONTENTS:		 [TOCD: 15:22 22 May 2001] -->
<!--								   -->
<!--  [1] Basic structural elements				   -->
<!--  [2] Modified elements here				   -->
<!--  [3] Classical things below				   -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~	   -->
<!-- @FILE:    huppaal-1.1.dtd                                     -->
<!-- @PLACE:   BRICS AArhus; host:harald			   -->
<!-- @FORMAT:  XML Document Type Definition                        -->
<!-- @AUTHOR:  M. Oliver M'o'ller     <omoeller@brics.dk>          -->
<!--           Emmanuel Fleury        <fleury@cs.auc.dk>           -->
<!--           Gerd Behrmann          <behrmann@cs.auc.dk>         -->
<!-- @BEGUN:   Wed Oct 18 14:02:43 2000                            -->
<!-- @VERSION  V1.1   Tue May 22 15:22:32 2001			   -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -->

<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->
<!-- [1] Basic structural elements				       -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->

<!ELEMENT hta (imports?, declaration?, template+, instantiation?, system,
               globalinit*)>
<!-- ?? no sure, whether this is needed -->
<!ELEMENT imports (#PCDATA)>
<!ELEMENT declaration (#PCDATA)>
<!ELEMENT template (name,
                    parameter?,
                    declaration?,
                    location*,
                    superlocation*,
                    transition*
                      )>
<!ATTLIST template type CDATA #IMPLIED> <!-- NN -->
<!-- the type is intended to be "XOR" (default) or "AND"
"XOR" means: 
 * we have locations of kind "basic", "entry", "exit"
 * we have transitions

 Well-formedness conditions: 
 - entry: exactly one outgoing and no ingoing transition
 - exit: no outgoing and arbitrary many ingoing transitions
 - there is at least one entry

"AND" means:
 * there are only  locations of kind "entry", "exit", and "junction"
 * transitions connect locations and superlocations

 Well-formedness conditions: 
 - there are two or more <superlocation> tags
 - a junction is either
   (1) [fork]
       reached by a transition from an location kind "entry"
       has #superlocations outgoing transitions, connecting to entries
           of different superlocations
   (2) [join]
       has #superlocations ingoing transitions from different superlocation
           exits
       has exactly one outgoing transition connecting to an exit
 - every entry, that is connected to in one instantiation of the template,
   has exactly one outgoing transition
 - every exit, that is connected to in one instantiation of the template,
   has exactly one ingoing transition
  -->

<!-- "history" template is not specified explicitly;
     The reason for this is, that having a history is not an isolated
     property, but requires a designated
      <location kind="entry" type="history">
     There can be at most one such entry. -->

<!-- the instantiates attribute refers to the (textual) NAME of the template
     (this makes imports easier)
     The optional labels include invariants, and (possibly) comments.  -->
<!ELEMENT superlocation (name, label*)>
<!ATTLIST superlocation instantiates   CDATA #REQUIRED
                        withparameters CDATA #IMPLIED
                        id             ID    #REQUIRED
                        x              CDATA #IMPLIED
                        y              CDATA #IMPLIED>


<!-- point to an entry in a fundamental superlocation, i.e., an instantiation
     and an entry (ref) of it.
     the attibute CDATA is by default
        "no", other values are
        "all", or
        "specified".
     In the "all" case, every exit is a possible starting point.
     In the "specified" case, the transition elements point to the relevant
     exits and can also carry synchronisations/guards/assignments. 
-->             
<!ELEMENT globalinit (transition)*>
<!ATTLIST globalinit instantiationname CDATA #REQUIRED
                     ref               IDREF #IMPLIED
		     canexit	       CDATA #IMPLIED>


<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->
<!-- [2] Modified elements here					       -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->

<!-- locations are of kind
     "basic":    (default) basic location (XOR templates only)
                 can be of type "urgent" or "committed"
     "entry":    can be of type "default" or "history"
     "exit":     can be of type "default"
     "junction": (AND templates only)
-->
<!ELEMENT location (name, label*)>
<!ATTLIST location id   ID #REQUIRED
                   kind CDATA #IMPLIED
                   type CDATA #IMPLIED
                   x    CDATA #IMPLIED
                   y    CDATA #IMPLIED>

<!-- if source points to a superlocation, then
     exitref: points to an exit or exitpoint
     of the template the superlocation instantiates -->
<!ELEMENT source EMPTY>
<!ATTLIST source ref      IDREF #REQUIRED
                 exitref  IDREF #IMPLIED>

<!-- if target points to a superlocation, then
     entryref: points to an entry or entrypoint
     of the template the superlocation instantiates -->
<!ELEMENT target EMPTY>
<!ATTLIST target ref      IDREF #REQUIRED
                 entryref IDREF #IMPLIED>

<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->
<!-- [3] Classical things below					       -->
<!-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      -->

<!ELEMENT name (#PCDATA)>
<!ATTLIST name x   CDATA #IMPLIED
               y   CDATA #IMPLIED>
<!ELEMENT parameter (#PCDATA)>
<!ATTLIST parameter x   CDATA #IMPLIED
                    y   CDATA #IMPLIED>
<!-- kind values:
     "assignment"
     "guard"
     "synchronisation"
     "invariant"
 -->
<!ELEMENT label (#PCDATA)>
<!ATTLIST label kind CDATA #REQUIRED
                x    CDATA #IMPLIED
                y    CDATA #IMPLIED>
<!ELEMENT nail EMPTY>
<!ATTLIST nail x   CDATA #REQUIRED
               y   CDATA #REQUIRED>
<!ELEMENT instantiation (#PCDATA)>
<!ELEMENT system (#PCDATA)>

<!ELEMENT transition (source, target, label*, nail*)>
<!ATTLIST transition x   CDATA #IMPLIED
                     y   CDATA #IMPLIED>
                                                
<!-- Change history:

0.2: made name of joins optional
     removed init
             instead, introduced element globalinit
     changed "instanciates" to "instantiates"
     made "parameter" in superstates optional
     added optional superstate part "invariant"
     changed exit-definition: no "fromref" anymore, exits will be pointed to
        by transitions (like ordinary locations)
     introduced <entrypoint> and <exitpoint> as notational alternative
     joins include an required pointer to an exit
0.3: allowed more-than-binary branching (AND components/forks/joins)
     added attribute shape to <hta> (can be "BINTREE" to indicate binary
     branching structure)
     added connection element (aka pseudo-transition) and introduced them
0.4: replaced assignment/guard/synchronisation with the label construct
0.5: replaced invariant with label construct
     changed number of connections an entry can have (introduced possibility
      of nondeterminism).
     changed globalinit to contain the name of the instantiation as an
      attribute (necessary, if system should be relaxed to be the parallel
      composition of some instantiations).
0.6: added an optional attribute canexit to the globalinit tag
     added optional connections (possibly with guard and sync) to the
     globalinit tag
1.0: replaces entry, exit, fork, join by element "pseudostate" with
     appropriate "kind" label
     replaced "component" by "superstate"
     removed entrypoint, exitpoint, connection
1.1: renamed "superstate" to "superlocation"
     removed pseudolocation; only locations now with different kind
     introduced kind="junction" to subsume join and fork
     -->
