<?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_2.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;

broadcast chan        appr[N], stop[N], leave[N];
urgent broadcast 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>
			<label kind="exponentialrate" x="-16" y="96">(1 + id) : N*N</label>
		</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="176">
		</location>
		<location id="id6" x="192" y="360">
			<name x="208" y="344">Stopping</name>
			<committed/>
		</location>
		<location id="id7" x="192" y="264">
			<name x="208" y="264">Occ</name>
		</location>
		<location id="id8" x="192" y="96">
			<name x="208" y="64">Free</name>
			<committed/>
		</location>
		<init ref="id8"/>
		<transition>
			<source ref="id5"/>
			<target ref="id7"/>
			<label kind="select" x="200" y="192">e:id_t</label>
			<label kind="synchronisation" x="200" y="208">appr[e]?</label>
			<label kind="assignment" x="200" y="224">enqueue(e)</label>
		</transition>
		<transition>
			<source ref="id7"/>
			<target ref="id6"/>
			<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="id7"/>
			<target ref="id8"/>
			<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="96"/>
		</transition>
		<transition>
			<source ref="id6"/>
			<target ref="id7"/>
			<label kind="synchronisation" x="224" y="304">stop[tail()]!</label>
			<nail x="216" y="312"/>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id7"/>
			<label kind="guard" x="112" y="176">len &gt; 0</label>
			<label kind="synchronisation" x="112" y="192">go[front()]!</label>
			<nail x="96" y="96"/>
			<nail x="96" y="264"/>
		</transition>
		<transition>
			<source ref="id8"/>
			<target ref="id5"/>
			<label kind="guard" x="200" y="120">len == 0</label>
		</transition>
	</template>
	<system>system Train, Gate;

gantt {
  G: // gate line
     Gate.len&gt;0 -&gt; 2+17*(Gate.len-1)/2; // shade of blue
  T(i:id_t): // train lines
     //Train(i).Safe -&gt; 3, // violet, or omit for white
     Train(i).Appr -&gt; 6, // yellow
     Train(i).Stop -&gt; 1, // green
     Train(i).Start -&gt; 2, // blue
     Train(i).Cross -&gt; 0; // red
   //C(i:int[0,64]): true -&gt; i; // color palette
}</system>
	<queries>
		<query>
			<formula>simulate[&lt;=100]{ Train(0).x, Gate.len }</formula>
			<comment>Plot the change in the clock x and the queue length over time.
Expect two trajectories from one simulation of up to 100 time units.</comment>
		</query>
		<query>
			<formula>simulate[&lt;=100; 10]{ Train(0).x, Gate.len }</formula>
			<comment>Plot the change in the clock x and the queue length over time.
Expect 10+10 trajectories from 10 simulations of up to 100 time units.</comment>
		</query>
		<query>
			<formula>simulate[&lt;=100]{ sum(i:id_t) Train(i).Stop }</formula>
			<comment>Count the trains that are stopped over time.
Expect one trajectory from one simulation.</comment>
		</query>
		<query>
			<formula>E[&lt;=100](max: sum(i:id_t) Train(i).Stop)</formula>
			<comment>Compute an expected maximum value of trains being stopped.
Expect a mean estimate based on two samples
(one statistical degree of freedom, assuming Student's t-distribution).</comment>
		</query>
		<query>
			<formula>E[&lt;=100; 2000](max: sum(i:id_t) Train(i).Stop)</formula>
			<comment>Compute an expected maximum value of trains being stopped.
Expect a mean estimate based on 2000 samples (assuming Student's t-distribution).</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(0).Cross)</formula>
			<comment>Estimate the probability that the train arrives to the crossing before 100 time units.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(1).Cross)</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(2).Cross)</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(3).Cross)</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(4).Cross)</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(5).Cross)</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100; 400](&lt;&gt; Train(5).Cross)</formula>
			<comment>Estimate the probability of the train arriving to the crossing before 100 time units.
Expect more precise estimate (and more refined distribution plots) from 400 simulation runs.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(0).Cross and (forall(i : id_t) i != 0 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(1).Cross and (forall(i : id_t) i != 1 imply Train(i).Stop))
			</formula>
			<comment>
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(2).Cross and (forall(i : id_t) i != 2 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(3).Cross and (forall(i : id_t) i != 3 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(4).Cross and (forall(i : id_t) i != 4 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(5).Cross and (forall(i : id_t) i != 5 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[&lt;=600](&lt;&gt; Train(1).Cross and (forall(i : id_t) i != 1 imply Train(i).Stop)) &gt;=
Pr[&lt;=600](&lt;&gt; Train(5).Cross and (forall(i : id_t) i != 5 imply Train(i).Stop))</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Pr[#&lt;=20]([] 
  forall(i : id_t) 
    forall(j : id_t) 
      Train(i).Cross &amp;&amp; Train(j).Cross imply i == j
) &gt;= 0.98</formula>
			<comment>Check that within 20 discrete transition the probability of no colision 
(no two trains in the crossing) is larger than 98%.</comment>
		</query>
		<query>
			<formula></formula>
			<comment>===== Validation Properties:</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Gate.Occ</formula>
			<comment>Gate can receive (and store in queue) msg's from approaching trains.</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Train(0).Cross</formula>
			<comment>Train 0 can reach crossing.</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Train(1).Cross	</formula>
			<comment>Train 1 can reach crossing.</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Train(0).Cross and Train(1).Stop</formula>
			<comment>Train 0 can be crossing bridge while Train 1 is waiting to cross.</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Train(0).Cross and (forall (i : id_t) i != 0 imply Train(i).Stop)</formula>
			<comment>Train 0 can cross bridge while the other trains are waiting to cross.</comment>
		</query>
		<query>
			<formula></formula>
			<comment>===== Safety Properties:</comment>
		</query>
		<query>
			<formula>A[] forall (i : id_t) forall (j : id_t) Train(i).Cross &amp;&amp; Train(j).Cross imply i == j</formula>
			<comment>There is never more than one train crossing the bridge (at
any time instance).</comment>
		</query>
		<query>
			<formula>A[] Gate.list[N] == 0</formula>
			<comment>There can never be N elements in the queue (thus the array will not overflow).</comment>
		</query>
		<query>
			<formula></formula>
			<comment>===== Liveness Properties:</comment>
		</query>
		<query>
			<formula>Train(0).Appr --&gt; Train(0).Cross</formula>
			<comment>Whenever a train approaches the bridge, it will eventually cross.</comment>
		</query>
		<query>
			<formula>Train(1).Appr --&gt; Train(1).Cross</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Train(2).Appr --&gt; Train(2).Cross</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Train(3).Appr --&gt; Train(3).Cross</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Train(4).Appr --&gt; Train(4).Cross</formula>
			<comment></comment>
		</query>
		<query>
			<formula>Train(5).Appr --&gt; Train(5).Cross</formula>
			<comment></comment>
		</query>
	</queries>
</nta>
