title: Trying to understand clocks and timeouts in UPPAAL
body: <p>I need to model a system as a timed automaton with UPPAAL and I'm really puzzled with the way UPPAAL manages clocks and guards according to elapsed time: it looks like UPPAAL just ignores clock guards!
  I suppose my problem is that I'm approaching modelling from a very "physical" approach, and so I'm facing this kind of problems.</p>
  
  <p>So here comes a trivial automaton. When run on UPPAAL simulation, I would  expect that it loops forever between initial and A locations, never going to B. But this is not the case: it alternates randomly between A and B (at least using the latest UPPAAL snapshot; I cannot try the release, as there's no Linux 64 version).</p>
  
  <p>So what I'm missing? How really UPPAAL treats clock guards?</p>
  
  <p>What I was trying to do when I first encountered this issue is to model a timeout, so the automaton takes a different edge if the guard of the nominal behavior is not meet before 30 seconds.</p>
  
  <p>Thank you a lot</p>
  
  <pre><code>&lt;?xml version="1.0" encoding="utf-8"?&gt;
  &lt;!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'&gt;
  &lt;nta&gt;
      &lt;declaration&gt;// Place global declarations here.
  
  clock t;&lt;/declaration&gt;
      &lt;template&gt;
          &lt;name x="5" y="5"&gt;Template&lt;/name&gt;
          &lt;declaration&gt;// Place local declarations here.
  &lt;/declaration&gt;
          &lt;location id="id0" x="153" y="8"&gt;
              &lt;name x="170" y="0"&gt;B&lt;/name&gt;
          &lt;/location&gt;
          &lt;location id="id1" x="0" y="119"&gt;
              &lt;name x="-8" y="136"&gt;A&lt;/name&gt;
          &lt;/location&gt;
          &lt;location id="id2" x="0" y="0"&gt;
          &lt;/location&gt;
          &lt;init ref="id2"/&gt;
          &lt;transition&gt;
              &lt;source ref="id0"/&gt;
              &lt;target ref="id2"/&gt;
              &lt;label kind="assignment" x="60" y="-55"&gt;t:=0&lt;/label&gt;
              &lt;nail x="153" y="-8"/&gt;
              &lt;nail x="42" y="-102"/&gt;
          &lt;/transition&gt;
          &lt;transition&gt;
              &lt;source ref="id1"/&gt;
              &lt;target ref="id2"/&gt;
              &lt;label kind="assignment" x="-135" y="55"&gt;t:=0&lt;/label&gt;
              &lt;nail x="-153" y="-8"/&gt;
          &lt;/transition&gt;
          &lt;transition&gt;
              &lt;source ref="id2"/&gt;
              &lt;target ref="id0"/&gt;
              &lt;label kind="guard" x="93" y="-17"&gt;t &amp;gt; 30&lt;/label&gt;
          &lt;/transition&gt;
          &lt;transition&gt;
              &lt;source ref="id2"/&gt;
              &lt;target ref="id1"/&gt;
              &lt;label kind="guard" x="0" y="25"&gt;t&amp;lt;30&lt;/label&gt;
          &lt;/transition&gt;
      &lt;/template&gt;
      &lt;system&gt;// Place template instantiations here.
  
  // List one or more processes to be composed into a system.
  system Template;
      &lt;/system&gt;
      &lt;queries&gt;
          &lt;query&gt;
              &lt;formula&gt;sup: t
              &lt;/formula&gt;
              &lt;comment&gt;
              &lt;/comment&gt;
          &lt;/query&gt;
      &lt;/queries&gt;
  &lt;/nta&gt;
  </code></pre>