<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.5//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_5.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="-8" y="93">(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 id="id5">
			<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 id="id6">
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="guard" x="85" y="272">x&lt;=10</label>
			<label kind="synchronisation" x="76" y="289">stop[id]?</label>
		</transition>
		<transition id="id7">
			<source ref="id2"/>
			<target ref="id0"/>
			<label kind="guard" x="144" y="60">x&gt;=3</label>
			<label kind="synchronisation" x="144" y="76">leave[id]!</label>
		</transition>
		<transition id="id8">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="17" y="127">appr[id]!</label>
			<label kind="assignment" x="17" y="143">x=0</label>
		</transition>
		<transition id="id9">
			<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 id="id10">
			<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="id11" x="195" y="178">
		</location>
		<location id="id12" x="195" y="357">
			<name x="211" y="341">Stopping</name>
			<committed/>
		</location>
		<location id="id13" x="195" y="263">
			<name x="211" y="263">Occ</name>
		</location>
		<location id="id14" x="195" y="93">
			<name x="204" y="68">Free</name>
			<committed/>
		</location>
		<init ref="id14"/>
		<transition id="id15">
			<source ref="id11"/>
			<target ref="id13"/>
			<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 id="id16">
			<source ref="id13"/>
			<target ref="id12"/>
			<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 id="id17">
			<source ref="id13"/>
			<target ref="id14"/>
			<label kind="select" x="297" y="151">e : id_t</label>
			<label kind="guard" x="297" y="167">e == front()</label>
			<label kind="synchronisation" x="297" y="183">leave[e]?</label>
			<label kind="assignment" x="297" y="199">dequeue()</label>
			<nail x="289" y="263"/>
			<nail x="289" y="93"/>
		</transition>
		<transition id="id18">
			<source ref="id12"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="224" y="304">stop[tail()]!</label>
			<nail x="216" y="312"/>
		</transition>
		<transition id="id19">
			<source ref="id14"/>
			<target ref="id13"/>
			<label kind="guard" x="85" y="187">len &gt; 0</label>
			<label kind="synchronisation" x="85" y="204">go[front()]!</label>
			<nail x="76" y="93"/>
			<nail x="76" y="263"/>
		</transition>
		<transition id="id20">
			<source ref="id14"/>
			<target ref="id11"/>
			<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, Train(1).x, Train(2).x, Train(3).x, Train(4).x, Train(5).x }</formula>
			<comment>Trajectories of the clock values.
Right-click the query to inspect the plot.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { Gate.len }</formula>
			<comment>Trajectory of the queue length in the Gate controller.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { 
  Train(0).Safe+Train(0).Appr*2+Train(0).Stop*3+Train(0).Start*4+Train(0).Cross*5
}</formula>
			<comment>Trajectory of Train(0) location.
(right-click on the plot and disable Legend in the Show popup menu)</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { 
  Train(0).location+6*5, Train(1).location+6*4, Train(2).location+6*3,
  Train(3).location+6*2, Train(4).location+6*1, Train(5).location
}</formula>
			<comment>Trajectory of train locations.
Expect a plot similar to a Gantt chart where locations are encoded as number values.</comment>
		</query>
		<query>
			<formula>E[&lt;=100; 2000](max: sum(i:id_t) Train(i).Stop)</formula>
			<comment>The expected maximum number of stopped/waiting Trains.
The query estimates (1-α) confidence interval of ε width assuming t-distribution.
Expect ~4.55 trains on average. 
Note that the maximum length increases with longer traces.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(0).Cross)</formula>
			<comment>Probability of Train(0) arriving into crossing.
The query estimate (1-α) confidence interval of ε width.
Expect ~58.6%</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(1).Cross)</formula>
			<comment>Probability of Train(1) arriving into crossing.
Expect ~84.5%</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(2).Cross)</formula>
			<comment>Probability of Train(2) arriving into crossing.
Expect ~93.6%</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(3).Cross)</formula>
			<comment>Probability of Train(3) arriving into crossing.
Expect ~97.5%</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(4).Cross)</formula>
			<comment>Probability of Train(4) arriving into crossing.
Expect ~98.7%</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100](&lt;&gt; Train(5).Cross)</formula>
			<comment>Probability of Train(5) arriving into crossing.
Expect 99.5%</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>Probability of other trains waiting/being stopped while Train(0) is in the crossing.
Expect ~39%</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>What is the probability of other trains waiting/being stopped/preempted when Train(1) is in the crossing.
Expect ~45.3%</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>What is the probability of other trains waiting/being stopped/preempted when Train(2) is in the crossing.
Expect ~46.8%</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>What is the probability of other trains waiting/being stopped/preempted when Train(3) is in the crossing.
Expect ~46.3%</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>What is the probability of other trains waiting/being stopped/preempted when Train(4) is in the crossing.
Expect ~46.6%</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>What is the probability of other trains waiting/being stopped/preempted when Train(5) is in the crossing.
Expect ~46.2%</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>Compare probabilities of Train(1) stopping other trains and Train(5) stopping other trains.
The query uses u0 and u1 ratios as stopping criteria.
Expect the probability of Train(0) being smaller until 150, then larger until 580.
</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=1000]([] forall (i : id_t) forall (j : id_t) Train(i).Cross &amp;&amp; Train(j).Cross imply i == j) &gt;= 0.98</formula>
			<comment>Is the probability of safe system run (without collisions) larger than 98%?
Expect that the probability is larger than 98%+δ, where +δ is specified in the statistical parameters.</comment>
		</query>
		<query>
			<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/>
			<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/>
			<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/>
		</query>
		<query>
			<formula>Train(2).Appr --&gt; Train(2).Cross</formula>
			<comment/>
		</query>
		<query>
			<formula>Train(3).Appr --&gt; Train(3).Cross</formula>
			<comment/>
		</query>
		<query>
			<formula>Train(4).Appr --&gt; Train(4).Cross</formula>
			<comment/>
		</query>
		<query>
			<formula>Train(5).Appr --&gt; Train(5).Cross</formula>
			<comment/>
		</query>
	</queries>
</nta>
