<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.
const int N=5;//trains+1
int[0,N] el;
chan appr,stop,go,leave;
chan empty,notempty,hd,add,rem;
</declaration><template><name x="5" y="5">Train</name><parameter>int[0,N] &e,const int[0,N] id</parameter><declaration>// Place local declarations here.
clock x;</declaration><location id="id0" x="-2632" y="-144"><name x="-2616" y="-144">Stop</name></location><location id="id1" x="-2760" y="-304"><name x="-2808" y="-328">Appr</name><label kind="invariant" x="-2816" y="-312">x<=20</label></location><location id="id2" x="-2536" y="-304"><name x="-2520" y="-328">Start</name><label kind="invariant" x="-2520" y="-312">x<=15</label></location><location id="id3" x="-2536" y="-496"><name x="-2520" y="-528">Cross</name><label kind="invariant" x="-2520" y="-512">x<=5</label></location><location id="id4" x="-2760" y="-496"><name x="-2800" y="-520">Safe</name></location><init ref="id4"/><transition><source ref="id1"/><target ref="id3"/><label kind="guard" x="-2672" y="-376">x>=10</label><label kind="assignment" x="-2616" y="-424">x:=0</label><nail x="-2656" y="-392"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="-2832" y="-256">(x<=10)&&(e==id)</label><label kind="synchronisation" x="-2736" y="-224">stop?</label><label kind="assignment" x="-2696" y="-192">x:=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="-2528" y="-392">x>=7</label><label kind="assignment" x="-2528" y="-440">x:=0</label><nail x="-2536" y="-480"/></transition><transition><source ref="id0"/><target ref="id2"/><label kind="guard" x="-2592" y="-200">e==id</label><label kind="synchronisation" x="-2568" y="-232">go?</label><label kind="assignment" x="-2552" y="-256">x:=0</label></transition><transition><source ref="id4"/><target ref="id1"/><label kind="synchronisation" x="-2800" y="-432">appr!</label><label kind="assignment" x="-2824" y="-400">e:=id,x:=0</label></transition><transition><source ref="id3"/><target ref="id4"/><label kind="guard" x="-2600" y="-520">x>=3</label><label kind="synchronisation" x="-2656" y="-496">leave!</label><label kind="assignment" x="-2720" y="-536">e:=id,
x:=0</label></transition></template><template><name>Gate</name><location id="id5" x="-584" y="-80"><name x="-568" y="-96">add2</name><committed/></location><location id="id6" x="-776" y="-80"><committed/></location><location id="id7" x="-552" y="-320"><committed/></location><location id="id8" x="-680" y="-272"><name x="-664" y="-288">add1</name><committed/></location><location id="id9" x="-680" y="-368"></location><location id="id10" x="-680" y="-176"><name x="-664" y="-176">Occ</name></location><location id="id11" x="-840" y="-176"><name x="-872" y="-168">Send</name><committed/></location><location id="id12" x="-840" y="-464"><committed/></location><location id="id13" x="-680" y="-464"><name x="-696" y="-496">Free</name><committed/></location><init ref="id13"/><transition><source ref="id7"/><target ref="id13"/><label kind="synchronisation" x="-616" y="-488">rem?</label><nail x="-552" y="-464"/></transition><transition><source ref="id10"/><target ref="id7"/><label kind="synchronisation" x="-608" y="-200">leave?</label><nail x="-552" y="-176"/></transition><transition><source ref="id5"/><target ref="id10"/><label kind="synchronisation" x="-624" y="-136">add!</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="synchronisation" x="-688" y="-96">stop!</label></transition><transition><source ref="id10"/><target ref="id6"/><label kind="synchronisation" x="-768" y="-144">appr?</label></transition><transition><source ref="id8"/><target ref="id10"/><label kind="synchronisation" x="-712" y="-240">add!</label><nail x="-680" y="-184"/><nail x="-680" y="-192"/><nail x="-680" y="-200"/></transition><transition><source ref="id9"/><target ref="id8"/><label kind="synchronisation" x="-720" y="-336">appr?</label><nail x="-680" y="-280"/><nail x="-680" y="-312"/></transition><transition><source ref="id13"/><target ref="id9"/><label kind="synchronisation" x="-728" y="-432">empty?</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="synchronisation" x="-792" y="-176">go!</label></transition><transition><source ref="id12"/><target ref="id11"/><label kind="synchronisation" x="-864" y="-344">hd!</label></transition><transition><source ref="id13"/><target ref="id12"/><label kind="synchronisation" x="-800" y="-488">notempty?</label></transition></template><template><name>IntQueue</name><parameter>int[0,N] &e</parameter><declaration>int[0,N] list[N],len,i;
</declaration><location id="id14" x="-14" y="54"><name x="0" y="40">ShiftDown</name><committed/></location><location id="id15" x="-16" y="-112"><name x="-16" y="-144">Start</name></location><init ref="id15"/><transition><source ref="id14"/><target ref="id14"/><label kind="guard" x="-96" y="152">i<len</label><label kind="assignment" x="-32" y="160">list[i]:=list[i+1],i++</label><nail x="-70" y="150"/><nail x="50" y="150"/><nail x="10" y="94"/></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="40" y="-8">len==i</label><label kind="assignment" x="40" y="-40">list[i]:=0,i:=0</label><nail x="32" y="16"/><nail x="32" y="-56"/></transition><transition><source ref="id15"/><target ref="id14"/><label kind="guard" x="-104" y="-32">len>=1</label><label kind="synchronisation" x="-88" y="-56">rem!</label><label kind="assignment" x="-112" y="-16">len--,i:=0</label><nail x="-56" y="-48"/><nail x="-56" y="8"/></transition><transition><source ref="id15"/><target ref="id15"/><label kind="guard" x="-216" y="-64">len==0</label><label kind="synchronisation" x="-216" y="-88">empty!</label><nail x="-160" y="-24"/><nail x="-176" y="-104"/></transition><transition><source ref="id15"/><target ref="id15"/><label kind="guard" x="-192" y="-216">len>0</label><label kind="synchronisation" x="-172" y="-246">notempty!</label><nail x="-184" y="-176"/><nail x="-96" y="-232"/><nail x="-48" y="-168"/></transition><transition><source ref="id15"/><target ref="id15"/><label kind="synchronisation" x="-76" y="-127">hd?</label><label kind="assignment" x="124" y="-112">e:=list[0]</label><nail x="120" y="-40"/><nail x="112" y="-128"/></transition><transition><source ref="id15"/><target ref="id15"/><label kind="synchronisation" x="-32" y="-240">add?</label><label kind="assignment" x="16" y="-224">list[len]:=e,len++</label><nail x="-32" y="-224"/><nail x="112" y="-168"/><nail x="40" y="-136"/></transition></template><system>// Place template instantiations here.
//Process = Template();
Train1:=Train(el,1);
Train2:=Train(el,2);
Train3:=Train(el,3);
Train4:=Train(el,4);
Queue:=IntQueue(el);
// List one or more processes to be composed into a system.
system
Train1,Train2,Train3,Train4,Gate,Queue;
</system></nta>
