--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>\r
+<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>\r
+<nta>\r
+ <declaration>// Place global declarations here.
+
+const int N = 13;
+typedef int[0,N-1] id_c;
+
+chan up[N], down[N], left[N], right[N];</declaration>\r
+ <template>\r
+ <name x="5" y="5">VertCar</name>\r
+ <parameter>int[2,3] length, const id_c id, int[0,5] x, const int[0,4] y</parameter>\r
+ <declaration>// Place local declarations here.</declaration>\r
+ <location id="id0" x="-212" y="-76">\r
+ </location>\r
+ <init ref="id0"/>\r
+ <transition>\r
+ <source ref="id0"/>\r
+ <target ref="id0"/>\r
+ <label kind="guard" x="-288" y="-68">x>0</label>\r
+ <label kind="synchronisation" x="-288" y="-51">down[id]!</label>\r
+ <label kind="assignment" x="-288" y="-34">x:=x-1</label>\r
+ <nail x="-306" y="8"/>\r
+ <nail x="-136" y="0"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id0"/>\r
+ <target ref="id0"/>\r
+ <label kind="guard" x="-306" y="-204">x+length < 6</label>\r
+ <label kind="synchronisation" x="-314" y="-153">up[id]!</label>\r
+ <label kind="assignment" x="-306" y="-178">x:=x+1</label>\r
+ <nail x="-323" y="-102"/>\r
+ <nail x="-195" y="-178"/>\r
+ <nail x="-110" y="-102"/>\r
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>HorzCar</name>\r
+ <parameter>int[2,3] length, const id_c id, const int[0,4] x, int[0,5] y</parameter>\r
+ <location id="id1" x="-102" y="-34">\r
+ </location>\r
+ <init ref="id1"/>\r
+ <transition>\r
+ <source ref="id1"/>\r
+ <target ref="id1"/>\r
+ <label kind="guard" x="-135" y="8">y>0</label>\r
+ <label kind="synchronisation" x="-135" y="25">left[id]!</label>\r
+ <label kind="assignment" x="-135" y="42">y:=y-1</label>\r
+ <nail x="-153" y="42"/>\r
+ <nail x="-34" y="42"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id1"/>\r
+ <target ref="id1"/>\r
+ <label kind="guard" x="-160" y="-102">y+length < 6</label>\r
+ <label kind="synchronisation" x="-160" y="-85">right[id]!</label>\r
+ <label kind="assignment" x="-160" y="-68">y:=y+1</label>\r
+ <nail x="-178" y="-102"/>\r
+ <nail x="-34" y="-102"/>\r
+ </transition>\r
+ </template>\r
+ <system>// Place template instantiations here.
+H1 = HorzCar(2, 0, 0, 5);
+H2 = HorzCar(2, 1, 2, 5);
+V3 = VertCar(2, 2, 4, 4);
+V4 = VertCar(2, 3, 2, 3);
+V5 = VertCar(3, 4, 5, 2);
+V6 = VertCar(2, 5, 1, 3);
+H7 = HorzCar(2, 6, 3, 4);
+H8 = HorzCar(2, 7, 3, 2);
+V9 = VertCar(3, 8, 0, 0);
+HA = HorzCar(2, 9, 1, 0);
+VB = VertCar(2, 10, 3, 0);
+HC = HorzCar(2, 11, 4, 1);
+HD = HorzCar(2, 12, 4, 0);
+// List one or more processes to be composed into a system.
+system H1, H2, V3, V4, V5, V6, H7, H8, V9, HA, VB, HC, HD;
+ </system>\r
+ <queries>\r
+ </queries>\r
+</nta>\r