<?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>/*
 * For more details about this example, see 
 * "Automatic Verification of Real-Time Communicating Systems by Constraint Solving", 
 * by Wang Yi, Paul Pettersson and Mats Daniels. In Proceedings of the 7th International
 * Conference on Formal Description Techniques, pages 223-238, North-Holland. 1994.
 */

const int N = 6;         // # trains
typedef int[0,N-1] id_t;

chan        appr[N], stop[N], leave[N];
urgent chan go[N];
</declaration><template><name x="40" y="16">Train</name><parameter>const id_t id</parameter><declaration>clock x;</declaration><location id="id0" x="96" y="96"><name x="48" y="80">Safe</name></location><location id="id1" x="176" y="320"><name x="192" y="328">Stop</name></location><location id="id2" x="256" y="96"><name x="272" y="80">Cross</name><label kind="invariant" x="272" y="96">x&lt;=5</label></location><location id="id3" x="96" y="232"><name x="32" y="216">Appr</name><label kind="invariant" x="32" y="232">x&lt;=20</label></location><location id="id4" x="256" y="232"><name x="272" y="216">Start</name><label kind="invariant" x="272" y="232">x&lt;= 15</label></location><init ref="id0"/><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="184" y="160">x&gt;=10</label><label kind="assignment" x="184" y="176">x=0</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="guard" x="88" y="280">x&lt;=10</label><label kind="synchronisation" x="88" y="296">stop[id]?</label></transition><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="184" y="56">x&gt;=3</label><label kind="synchronisation" x="184" y="72">leave[id]!</label></transition><transition><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="32" y="128">appr[id]!</label><label kind="assignment" x="32" y="144">x=0</label></transition><transition><source ref="id4"/><target ref="id2"/><label kind="guard" x="264" y="160">x&gt;=7</label><label kind="assignment" x="264" y="176">x=0</label></transition><transition><source ref="id1"/><target ref="id4"/><label kind="synchronisation" x="224" y="280">go[id]?</label><label kind="assignment" x="224" y="296">x=0</label></transition></template><template><name x="40" y="16">Gate</name><declaration>id_t list[N+1];
int[0,N] len;

// Put an element at the end of the queue
void enqueue(id_t element)
{
        list[len++] = element;
}

// Remove the front element of the queue
void dequeue()
{
        int i = 0;
        len -= 1;
        while (i &lt; len)
        {
                list[i] = list[i + 1];
                i++;
        }
        list[i] = 0;
}

// Returns the front element of the queue
id_t front()
{
   return list[0];
}

// Returns the last element of the queue
id_t tail()
{
   return list[len - 1];
}</declaration><location id="id5" x="192" y="360"><committed/></location><location id="id6" x="192" y="264"><name x="208" y="264">Occ</name></location><location id="id7" x="192" y="128"><name x="208" y="96">Free</name></location><init ref="id7"/><transition><source ref="id6"/><target ref="id5"/><label kind="select" x="104" y="288">e : id_t</label><label kind="synchronisation" x="104" y="304">appr[e]?</label><label kind="assignment" x="104" y="320">enqueue(e)</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="select" x="296" y="152">e : id_t</label><label kind="guard" x="296" y="168">e == front()</label><label kind="synchronisation" x="296" y="184">leave[e]?</label><label kind="assignment" x="296" y="200">dequeue()</label><nail x="288" y="264"/><nail x="288" y="128"/></transition><transition><source ref="id5"/><target ref="id6"/><label kind="synchronisation" x="224" y="304">stop[tail()]!</label><nail x="216" y="312"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="guard" x="104" y="168">len &gt; 0</label><label kind="synchronisation" x="104" y="184">go[front()]!</label><nail x="96" y="128"/><nail x="96" y="264"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="select" x="200" y="152">e : id_t</label><label kind="guard" x="200" y="168">len == 0</label><label kind="synchronisation" x="200" y="184">appr[e]?</label><label kind="assignment" x="200" y="200">enqueue(e)</label></transition></template><system>system Train, Gate;
</system></nta>