uppaal/1b.xml

   1 <?xml version="1.0" encoding="utf-8"?>
   2 <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
   3 <nta>
   4         <declaration>// Place global declarations here.
   5 clock x, y;
   6 chan a, b, c, d;</declaration>
   7         <template>
   8                 <name x="5" y="5">Template</name>
   9                 <declaration>// Place local declarations here.</declaration>
  10                 <location id="id0" x="102" y="0">
  11                         <name x="92" y="-34">s3</name>
  12                 </location>
  13                 <location id="id1" x="0" y="0">
  14                         <name x="-10" y="-34">s2</name>
  15                         <label kind="invariant" x="-10" y="17">x &lt; 1</label>
  16                 </location>
  17                 <location id="id2" x="-119" y="0">
  18                         <name x="-129" y="-34">s1</name>
  19                         <label kind="invariant" x="-129" y="17">x &lt; 1</label>
  20                 </location>
  21                 <location id="id3" x="-246" y="0">
  22                         <name x="-256" y="-34">s0</name>
  23                 </location>
  24                 <init ref="id3"/>
  25                 <transition>
  26                         <source ref="id0"/>
  27                         <target ref="id0"/>
  28                         <label kind="synchronisation" x="127" y="-17">c</label>
  29                         <nail x="127" y="34"/>
  30                         <nail x="127" y="-34"/>
  31                 </transition>
  32                 <transition>
  33                         <source ref="id0"/>
  34                         <target ref="id3"/>
  35                         <label kind="guard" x="-160" y="-93">y &gt; 2</label>
  36                         <label kind="synchronisation" x="-160" y="-76">d</label>
  37                         <nail x="59" y="-59"/>
  38                         <nail x="-178" y="-59"/>
  39                 </transition>
  40                 <transition>
  41                         <source ref="id1"/>
  42                         <target ref="id0"/>
  43                         <label kind="synchronisation" x="18" y="-17">c</label>
  44                 </transition>
  45                 <transition>
  46                         <source ref="id2"/>
  47                         <target ref="id1"/>
  48                         <label kind="synchronisation" x="-101" y="-17">b</label>
  49                         <label kind="assignment" x="-101" y="0">y:=0</label>
  50                 </transition>
  51                 <transition>
  52                         <source ref="id3"/>
  53                         <target ref="id2"/>
  54                         <label kind="synchronisation" x="-228" y="-17">a</label>
  55                         <label kind="assignment" x="-228" y="0">x:=0</label>
  56                 </transition>
  57         </template>
  58         <system>// Place template instantiations here.
  59 Process = Template();
  60 // List one or more processes to be composed into a system.
  61 system Process;
  62     </system>
  63         <queries>
  64         </queries>
  65 </nta>