--- /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.
+clock x, y, z;
+
+chan approach, in, out, ex, lower, raise, down, up;</declaration>\r
+ <template>\r
+ <name x="5" y="5">Train</name>\r
+ <declaration>// Place local declarations here.</declaration>\r
+ <location id="id0" x="-119" y="17">\r
+ <name x="-187" y="-17">safe</name>\r
+ <label kind="invariant" x="-187" y="17">x<=5</label>\r
+ </location>\r
+ <location id="id1" x="8" y="17">\r
+ <name x="-2" y="-17">unsafe</name>\r
+ <label kind="invariant" x="-2" y="34">x<=5</label>\r
+ </location>\r
+ <location id="id2" x="0" y="-110">\r
+ <name x="-10" y="-144">aproaching</name>\r
+ <label kind="invariant" x="25" y="-136">x<=5</label>\r
+ </location>\r
+ <location id="id3" x="-127" y="-102">\r
+ <name x="-137" y="-136">initial</name>\r
+ </location>\r
+ <init ref="id3"/>\r
+ <transition>\r
+ <source ref="id0"/>\r
+ <target ref="id3"/>\r
+ <label kind="synchronisation" x="-119" y="-59">ex!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id1"/>\r
+ <target ref="id0"/>\r
+ <label kind="synchronisation" x="-101" y="0">out!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id2"/>\r
+ <target ref="id1"/>\r
+ <label kind="guard" x="4" y="-80">x>2</label>\r
+ <label kind="synchronisation" x="4" y="-63">in!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id3"/>\r
+ <target ref="id2"/>\r
+ <label kind="synchronisation" x="-102" y="-127">approach!</label>\r
+ <label kind="assignment" x="-93" y="-102">x:=0</label>\r
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>Stupid</name>\r
+ <location id="id4" x="0" y="0">\r
+ </location>\r
+ <init ref="id4"/>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id4"/>\r
+ <label kind="synchronisation" x="-119" y="-59">in?</label>\r
+ <nail x="-68" y="-85"/>\r
+ <nail x="-85" y="-8"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id4"/>\r
+ <label kind="synchronisation" x="93" y="-17">out?</label>\r
+ <nail x="93" y="-59"/>\r
+ <nail x="85" y="42"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id4"/>\r
+ <label kind="synchronisation" x="-67" y="4">down?</label>\r
+ <nail x="-85" y="42"/>\r
+ <nail x="25" y="68"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id4"/>\r
+ <target ref="id4"/>\r
+ <label kind="synchronisation" x="1" y="-85">up?</label>\r
+ <nail x="-17" y="-68"/>\r
+ <nail x="68" y="-68"/>\r
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>Gate</name>\r
+ <location id="id5" x="-204" y="-25">\r
+ <name x="-246" y="0">raising</name>\r
+ <label kind="invariant" x="-274" y="-33">y<=2</label>\r
+ </location>\r
+ <location id="id6" x="-42" y="-25">\r
+ <name x="-34" y="8">lowered</name>\r
+ </location>\r
+ <location id="id7" x="-42" y="-161">\r
+ <name x="-52" y="-195">lowering</name>\r
+ <label kind="invariant" x="-25" y="-161">y<=1</label>\r
+ </location>\r
+ <location id="id8" x="-204" y="-161">\r
+ <name x="-214" y="-195">raised</name>\r
+ </location>\r
+ <init ref="id8"/>\r
+ <transition>\r
+ <source ref="id5"/>\r
+ <target ref="id8"/>\r
+ <label kind="guard" x="-191" y="-127">y>=1</label>\r
+ <label kind="synchronisation" x="-178" y="-110">up!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id6"/>\r
+ <target ref="id5"/>\r
+ <label kind="synchronisation" x="-160" y="-42">raise?</label>\r
+ <label kind="assignment" x="-160" y="-25">y:=0</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id7"/>\r
+ <target ref="id6"/>\r
+ <label kind="synchronisation" x="-42" y="-110">down!</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id8"/>\r
+ <target ref="id7"/>\r
+ <label kind="synchronisation" x="-160" y="-178">lower?</label>\r
+ <label kind="assignment" x="-160" y="-161">y:=0</label>\r
+ </transition>\r
+ </template>\r
+ <template>\r
+ <name>Controller</name>\r
+ <location id="id9" x="187" y="-68">\r
+ <name x="177" y="-102">trainComing</name>\r
+ <label kind="invariant" x="229" y="-76">z<=1</label>\r
+ </location>\r
+ <location id="id10" x="-153" y="-76">\r
+ <name x="-229" y="-51">trainLeaving</name>\r
+ <label kind="invariant" x="-221" y="-85">z <= 1</label>\r
+ </location>\r
+ <location id="id11" x="-8" y="-76">\r
+ </location>\r
+ <init ref="id11"/>\r
+ <transition>\r
+ <source ref="id10"/>\r
+ <target ref="id11"/>\r
+ <label kind="synchronisation" x="-143" y="-178">raise!</label>\r
+ <nail x="-161" y="-161"/>\r
+ <nail x="-17" y="-161"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id11"/>\r
+ <target ref="id10"/>\r
+ <label kind="synchronisation" x="-135" y="-93">ex?</label>\r
+ <label kind="assignment" x="-135" y="-76">z:=0</label>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id9"/>\r
+ <target ref="id11"/>\r
+ <label kind="guard" x="10" y="-22">z==1</label>\r
+ <label kind="synchronisation" x="10" y="-5">lower!</label>\r
+ <nail x="187" y="17"/>\r
+ <nail x="-8" y="8"/>\r
+ </transition>\r
+ <transition>\r
+ <source ref="id11"/>\r
+ <target ref="id9"/>\r
+ <label kind="synchronisation" x="10" y="-89">approach?</label>\r
+ <label kind="assignment" x="10" y="-72">z:=0</label>\r
+ </transition>\r
+ </template>\r
+ <system>// Place template instantiations here.
+T = Train();
+G = Gate();
+C = Controller();
+Gezeik = Stupid();
+// List one or more processes to be composed into a system.
+system T, G, C, Gezeik;
+ </system>\r
+ <queries>\r
+ </queries>\r
+</nta>\r
repositories / mc1516the.git / commitdiff