<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.6//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_6.dtd'>
<nta>
	<declaration>/**
Train Gate
N trains share the same bridge crossing.
If they attempt to cross at the same time they will collide.
A controller can signal trains to stop when they approach the bridge and to start again to proceed with the crossing.

From: "On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions" in CONCUR'25,
by Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiri Srba.
DOI: https://doi.org/10.4230/LIPIcs.CONCUR.2025.5
*/

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

const int RED = 0;
const int ORANGE = 1;
const int YELLOW = 2;
const int GREEN = 3;
const int CYAN = 4;
const int BLUE = 5;
const int MAGENTA = 6;
const int PINK = 7;

broadcast chan appr[N], stop[N], leave[N], go[N];

int[0,N] crossing = 0;

clock time;
clock z; // Formula clock
</declaration>
	<template>
		<name x="40" y="16">TrainRed</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id0" x="96" y="96">
			<name x="48" y="80">Safe</name>
		</location>
		<location id="id1" x="176" y="320" color="#00ff00">
			<name x="192" y="328">Stop</name>
		</location>
		<location id="id2" x="256" y="96" color="#0000ff">
			<name x="272" y="68">Cross</name>
			<label kind="invariant" x="272" y="85">x&lt;=5</label>
		</location>
		<location id="id3" x="96" y="232" color="#ffff00">
			<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" color="#ffa500">
			<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" color="#ff0000">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="guard" x="119" y="136">x&gt;=10</label>
			<label kind="assignment" x="119" y="153">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id6" controllable="false">
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="51" y="263">stop[id]?</label>
		</transition>
		<transition id="id7" color="#ff0000">
			<source ref="id2"/>
			<target ref="id0"/>
			<label kind="guard" x="127" y="17">x&gt;=3</label>
			<label kind="synchronisation" x="127" y="34">leave[id]!</label>
			<label kind="assignment" x="127" y="51">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id8" color="#ff0000">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="25" y="119">appr[id]!</label>
			<label kind="assignment" x="34" y="136">x=0</label>
		</transition>
		<transition id="id9" color="#ff0000">
			<source ref="id4"/>
			<target ref="id2"/>
			<label kind="guard" x="264" y="144">x&gt;=7</label>
			<label kind="assignment" x="264" y="160">x:=0, crossing += 1</label>
		</transition>
		<transition id="id10" controllable="false">
			<source ref="id1"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="221" y="272">go[id]?</label>
			<label kind="assignment" x="221" y="289">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainOrange</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id11" x="-178" y="-127">
			<name x="-226" y="-143">Safe</name>
		</location>
		<location id="id12" x="-98" y="97" color="#00ff00">
			<name x="-82" y="105">Stop</name>
		</location>
		<location id="id13" x="-18" y="-127" color="#0000ff">
			<name x="-2" y="-155">Cross</name>
			<label kind="invariant" x="-2" y="-138">x&lt;=5</label>
		</location>
		<location id="id14" x="-178" y="9" color="#ffff00">
			<name x="-242" y="-7">Appr</name>
			<label kind="invariant" x="-242" y="9">x&lt;=20</label>
		</location>
		<location id="id15" x="-18" y="9" color="#ffa500">
			<name x="-2" y="-7">Start</name>
			<label kind="invariant" x="-2" y="9">x&lt;= 15</label>
		</location>
		<init ref="id11"/>
		<transition id="id16" color="#ffa500">
			<source ref="id14"/>
			<target ref="id13"/>
			<label kind="guard" x="-155" y="-87">x&gt;=10</label>
			<label kind="assignment" x="-155" y="-70">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id17" controllable="false">
			<source ref="id14"/>
			<target ref="id12"/>
			<label kind="synchronisation" x="-223" y="40">stop[id]?</label>
		</transition>
		<transition id="id18" color="#ffa500">
			<source ref="id13"/>
			<target ref="id11"/>
			<label kind="guard" x="-153" y="-204">x&gt;=3</label>
			<label kind="synchronisation" x="-153" y="-187">leave[id]!</label>
			<label kind="assignment" x="-153" y="-170">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id19" color="#ffa500">
			<source ref="id11"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="-249" y="-104">appr[id]!</label>
			<label kind="assignment" x="-240" y="-87">x=0</label>
		</transition>
		<transition id="id20" color="#ffa500">
			<source ref="id15"/>
			<target ref="id13"/>
			<label kind="guard" x="-10" y="-79">x&gt;=7</label>
			<label kind="assignment" x="-10" y="-63">x:=0, crossing += 1</label>
		</transition>
		<transition id="id21" controllable="false">
			<source ref="id12"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="-53" y="49">go[id]?</label>
			<label kind="assignment" x="-53" y="66">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainYellow</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id22" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id23" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id24" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id25" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id26" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id22"/>
		<transition id="id27" color="#ffff00">
			<source ref="id25"/>
			<target ref="id24"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id28" controllable="false">
			<source ref="id25"/>
			<target ref="id23"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id29" color="#ffff00">
			<source ref="id24"/>
			<target ref="id22"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id30" color="#ffff00">
			<source ref="id22"/>
			<target ref="id25"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id31" color="#ffff00">
			<source ref="id26"/>
			<target ref="id24"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id32" controllable="false">
			<source ref="id23"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainGreen</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id33" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id34" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id35" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id36" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id37" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id33"/>
		<transition id="id38" color="#00ff00">
			<source ref="id36"/>
			<target ref="id35"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id39" controllable="false">
			<source ref="id36"/>
			<target ref="id34"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id40" color="#00ff00">
			<source ref="id35"/>
			<target ref="id33"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id41" color="#00ff00">
			<source ref="id33"/>
			<target ref="id36"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id42" color="#00ff00">
			<source ref="id37"/>
			<target ref="id35"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id43" controllable="false">
			<source ref="id34"/>
			<target ref="id37"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainCyan</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id44" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id45" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id46" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id47" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id48" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id44"/>
		<transition id="id49" color="#00ffff">
			<source ref="id47"/>
			<target ref="id46"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id50" controllable="false">
			<source ref="id47"/>
			<target ref="id45"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id51" color="#00ffff">
			<source ref="id46"/>
			<target ref="id44"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id52" color="#00ffff">
			<source ref="id44"/>
			<target ref="id47"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id53" color="#00ffff">
			<source ref="id48"/>
			<target ref="id46"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id54" controllable="false">
			<source ref="id45"/>
			<target ref="id48"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainBlue</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id55" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id56" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id57" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id58" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id59" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id55"/>
		<transition id="id60" color="#0000ff">
			<source ref="id58"/>
			<target ref="id57"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id61" controllable="false">
			<source ref="id58"/>
			<target ref="id56"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id62" color="#0000ff">
			<source ref="id57"/>
			<target ref="id55"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id63" color="#0000ff">
			<source ref="id55"/>
			<target ref="id58"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id64" color="#0000ff">
			<source ref="id59"/>
			<target ref="id57"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id65" controllable="false">
			<source ref="id56"/>
			<target ref="id59"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainMagenta</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id66" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id67" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id68" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id69" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id70" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id66"/>
		<transition id="id71" color="#ff00ff">
			<source ref="id69"/>
			<target ref="id68"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id72" controllable="false">
			<source ref="id69"/>
			<target ref="id67"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id73" color="#ff00ff">
			<source ref="id68"/>
			<target ref="id66"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id74" color="#ff00ff">
			<source ref="id66"/>
			<target ref="id69"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id75" color="#ff00ff">
			<source ref="id70"/>
			<target ref="id68"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id76" controllable="false">
			<source ref="id67"/>
			<target ref="id70"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>TrainPink</name>
		<parameter>const id_t id</parameter>
		<declaration>clock x;
bool crossed = false;</declaration>
		<location id="id77" x="-255" y="-161">
			<name x="-303" y="-177">Safe</name>
		</location>
		<location id="id78" x="-175" y="63" color="#00ff00">
			<name x="-159" y="71">Stop</name>
		</location>
		<location id="id79" x="-95" y="-161" color="#0000ff">
			<name x="-79" y="-189">Cross</name>
			<label kind="invariant" x="-79" y="-172">x&lt;=5</label>
		</location>
		<location id="id80" x="-255" y="-25" color="#ffff00">
			<name x="-319" y="-41">Appr</name>
			<label kind="invariant" x="-319" y="-25">x&lt;=20</label>
		</location>
		<location id="id81" x="-95" y="-25" color="#ffa500">
			<name x="-79" y="-41">Start</name>
			<label kind="invariant" x="-79" y="-25">x&lt;= 15</label>
		</location>
		<init ref="id77"/>
		<transition id="id82" color="#ffc0cb">
			<source ref="id80"/>
			<target ref="id79"/>
			<label kind="guard" x="-232" y="-121">x&gt;=10</label>
			<label kind="assignment" x="-232" y="-104">x:=0,
crossing += 1</label>
		</transition>
		<transition id="id83" controllable="false">
			<source ref="id80"/>
			<target ref="id78"/>
			<label kind="synchronisation" x="-300" y="6">stop[id]?</label>
		</transition>
		<transition id="id84" color="#ffc0cb">
			<source ref="id79"/>
			<target ref="id77"/>
			<label kind="guard" x="-229" y="-238">x&gt;=3</label>
			<label kind="synchronisation" x="-229" y="-221">leave[id]!</label>
			<label kind="assignment" x="-229" y="-204">crossing -= 1,
crossed = true</label>
		</transition>
		<transition id="id85" color="#ffc0cb">
			<source ref="id77"/>
			<target ref="id80"/>
			<label kind="synchronisation" x="-326" y="-138">appr[id]!</label>
			<label kind="assignment" x="-317" y="-121">x=0</label>
		</transition>
		<transition id="id86" color="#ffc0cb">
			<source ref="id81"/>
			<target ref="id79"/>
			<label kind="guard" x="-87" y="-113">x&gt;=7</label>
			<label kind="assignment" x="-87" y="-97">x:=0, crossing += 1</label>
		</transition>
		<transition id="id87" controllable="false">
			<source ref="id78"/>
			<target ref="id81"/>
			<label kind="synchronisation" x="-130" y="15">go[id]?</label>
			<label kind="assignment" x="-130" y="32">x=0</label>
		</transition>
	</template>
	<template>
		<name>BridgeControl</name>
		<declaration>int[0,N] c = 0;
id_t queue[N];

void enqueue(id_t id) {
    queue[c] = id;
    c += 1;
}

void remove(id_t id) {
    int i = 0;
    while (i &lt; c) {
        if (queue[i] == id) {
            int j = i + 1;
            while (j &lt; c) {
                queue[j - 1] = queue[j];
                j += 1;
            }
            c -= 1;
            queue[c] = 0;
            return;
        }
        i += 1;
    }
}</declaration>
		<location id="id88" x="-425" y="-305">
			<name x="-399" y="-314">Idle</name>
		</location>
		<location id="id89" x="-297" y="314">
			<name x="-323" y="339">Response</name>
			<committed/>
		</location>
		<init ref="id88"/>
		<transition id="id90">
			<source ref="id88"/>
			<target ref="id88"/>
			<label kind="select" x="-400" y="-416">e:id_t</label>
			<label kind="synchronisation" x="-400" y="-399">go[e]!</label>
			<nail x="-400" y="-374"/>
			<nail x="-357" y="-374"/>
		</transition>
		<transition id="id91">
			<source ref="id88"/>
			<target ref="id88"/>
			<label kind="select" x="-501" y="-416">e:id_t</label>
			<label kind="synchronisation" x="-501" y="-399">stop[e]!</label>
			<nail x="-502" y="-374"/>
			<nail x="-459" y="-374"/>
		</transition>
		<transition id="id92" color="#ffc0cb">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="187">leave[PINK]?</label>
			<label kind="assignment" x="-204" y="204">remove(PINK)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="221"/>
			<nail x="-102" y="221"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id93" color="#ff00ff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="127">leave[MAGENTA]?</label>
			<label kind="assignment" x="-204" y="144">remove(MAGENTA)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="162"/>
			<nail x="-102" y="162"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id94" color="#0000ff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="68">leave[BLUE]?</label>
			<label kind="assignment" x="-204" y="85">remove(BLUE)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="102"/>
			<nail x="-102" y="102"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id95" color="#00ffff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="8">leave[CYAN]?</label>
			<label kind="assignment" x="-204" y="25">remove(CYAN)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="43"/>
			<nail x="-102" y="43"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id96" color="#00ff00">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="-51">leave[GREEN]?</label>
			<label kind="assignment" x="-204" y="-34">remove(GREEN)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="-16"/>
			<nail x="-102" y="-16"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id97" color="#ffff00">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="-110">leave[YELLOW]?</label>
			<label kind="assignment" x="-204" y="-93">remove(YELLOW)</label>
			<nail x="-213" y="-195"/>
			<nail x="-213" y="-76"/>
			<nail x="-103" y="-76"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id98" color="#ffa500">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="-170">leave[ORANGE]?</label>
			<label kind="assignment" x="-204" y="-153">remove(ORANGE)</label>
			<nail x="-212" y="-195"/>
			<nail x="-212" y="-135"/>
			<nail x="-102" y="-135"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id99" color="#ffc0cb">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="187">appr[PINK]?</label>
			<label kind="assignment" x="-416" y="204">enqueue(PINK)</label>
			<nail x="-425" y="221"/>
			<nail x="-297" y="221"/>
		</transition>
		<transition id="id100" color="#ff00ff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="127">appr[MAGENTA]?</label>
			<label kind="assignment" x="-416" y="144">enqueue(MAGENTA)</label>
			<nail x="-425" y="161"/>
			<nail x="-297" y="161"/>
		</transition>
		<transition id="id101" color="#0000ff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="68">appr[BLUE]?</label>
			<label kind="assignment" x="-416" y="85">enqueue(BLUE)</label>
			<nail x="-425" y="102"/>
			<nail x="-297" y="102"/>
		</transition>
		<transition id="id102" color="#00ffff">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="8">appr[CYAN]?</label>
			<label kind="assignment" x="-416" y="25">enqueue(CYAN)</label>
			<nail x="-425" y="42"/>
			<nail x="-297" y="42"/>
		</transition>
		<transition id="id103" color="#00ff00">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="-51">appr[GREEN]?</label>
			<label kind="assignment" x="-416" y="-34">enqueue(GREEN)</label>
			<nail x="-425" y="-17"/>
			<nail x="-297" y="-17"/>
		</transition>
		<transition id="id104" color="#ffff00">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="-110">appr[YELLOW]?</label>
			<label kind="assignment" x="-416" y="-93">enqueue(YELLOW)</label>
			<nail x="-425" y="-76"/>
			<nail x="-297" y="-76"/>
		</transition>
		<transition id="id105" color="#ffa500">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-416" y="-170">appr[ORANGE]?</label>
			<label kind="assignment" x="-416" y="-153">enqueue(ORANGE)</label>
			<nail x="-425" y="-136"/>
			<nail x="-297" y="-136"/>
		</transition>
		<transition id="id106">
			<source ref="id89"/>
			<target ref="id88"/>
			<nail x="-476" y="297"/>
			<nail x="-476" y="-280"/>
		</transition>
		<transition id="id107">
			<source ref="id89"/>
			<target ref="id88"/>
			<label kind="select" x="-663" y="229">e:id_t</label>
			<label kind="synchronisation" x="-663" y="246">go[e]!</label>
			<nail x="-663" y="314"/>
			<nail x="-663" y="-305"/>
		</transition>
		<transition id="id108">
			<source ref="id89"/>
			<target ref="id88"/>
			<label kind="select" x="-578" y="229">e:id_t</label>
			<label kind="synchronisation" x="-578" y="246">stop[e]!</label>
			<nail x="-578" y="297"/>
			<nail x="-578" y="-280"/>
		</transition>
		<transition id="id109" color="#ff0000">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-204" y="-229">leave[RED]?</label>
			<label kind="assignment" x="-204" y="-212">remove(RED)</label>
			<nail x="-212" y="-195"/>
			<nail x="-102" y="-195"/>
			<nail x="-102" y="314"/>
		</transition>
		<transition id="id110" color="#ff0000">
			<source ref="id88"/>
			<target ref="id89"/>
			<label kind="synchronisation" x="-417" y="-229">appr[RED]?</label>
			<label kind="assignment" x="-416" y="-212">enqueue(RED)</label>
			<nail x="-425" y="-195"/>
			<nail x="-297" y="-195"/>
		</transition>
	</template>
	<system>T_RED = TrainRed(RED);
T_ORANGE = TrainOrange(ORANGE);
T_YELLOW = TrainYellow(YELLOW);
T_GREEN = TrainGreen(GREEN);
T_CYAN = TrainCyan(CYAN);
T_BLUE = TrainBlue(BLUE);
T_MAGENTA = TrainMagenta(MAGENTA);
T_PINK = TrainPink(PINK);

system BridgeControl
    ,T_RED
    ,T_ORANGE
    ,T_YELLOW
    ,T_GREEN
//    ,T_CYAN
//    ,T_BLUE
//    ,T_MAGENTA
//    ,T_PINK
;
</system>
	<queries>
		<query>
			<formula>&lt;&lt;black&gt;&gt; [] crossing &lt;= 1</formula>
			<comment>The bridge controller can ensure no trains are crossing at the same time
EXPECT: True
RESOURCES: &lt;120 s</comment>
		</query>
		<query>
			<formula>[[red,orange,yellow]] [] crossing &lt;= 1</formula>
			<comment>Despite what RED, ORANGE, and YELLOW do, there is only one train crossing at a time.
EXPECT: True
RESOURCES: &lt;20 s</comment>
		</query>
		<query>
			<formula>[[red]] [] !T_RED.Cross</formula>
			<comment>Despite REDs actions there exists a trace where RED never crosses
EXPECT: True
RESOURCES: &lt;20 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;black&gt;&gt; [] (T_RED.crossed || !T_ORANGE.crossed)</formula>
			<comment>Bridge controller can make sure RED crosses before ORANGE
EXPECT: True
RESOURCES: &lt;30 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;black&gt;&gt; [] (T_RED.crossed || !T_ORANGE.crossed) &amp;&amp; (T_ORANGE.crossed || !T_YELLOW.crossed)</formula>
			<comment>Bridge controller can make sure RED crosses before ORANGE and that ORANGE crosses before YELLOW
EXPECT: True
RESOURCES: &lt;60 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (&lt;&lt;black&gt;&gt; &lt;&gt; T_RED.Cross &amp;&amp; T_ORANGE.Cross) || !T_RED.Stop || !T_ORANGE.Stop</formula>
			<comment>Can the bride controller ensure RED and ORANGE collide on crossing if they are both stopped?
EXPECT: False
RESOURCES: &lt;30 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;black&gt;&gt; [] crossing &lt;= 1 &amp;&amp; (!T_RED.Appr || T_RED.x == 0) &amp;&amp; (!T_ORANGE.Appr || T_ORANGE.x == 0) &amp;&amp; (!T_YELLOW.Appr || T_YELLOW.x == 0)</formula>
			<comment>The bridge controller can ensure no trains are crossing at the same time and RED, ORANGE, and YELLOW are always instructed immediately when approaching
EXPECT: True
RESOURCES: &lt;5 min</comment>
		</query>
		<query>
			<formula>&lt;&lt;black&gt;&gt; [] (&lt;&lt;black,red&gt;&gt; &lt;&gt; crossing &gt; 2) || !T_ORANGE.Stop || !T_YELLOW.Stop</formula>
			<comment>The bridge controller can ensure that whenever ORANGE and YELLOW is stopped, the bridge controller and RED can ensure a 3-way collision
EXPECT: True
RESOURCES: &lt;60 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (z @ (&lt;&lt;black&gt;&gt; [z &lt;= 10 U z &gt; 0 &amp;&amp; crossing != 0])) || crossing != 1 || BridgeControl.c &lt;= 1</formula>
			<comment>Whenever a train is crossing while another is not safe, the bridge controller can ensure a new crossing starts with 10 time units after the first ends
EXPECT: False
RESOURCES: &lt;180 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (z @ (&lt;&lt;black&gt;&gt; [z &lt;= 15 U z &gt; 0 &amp;&amp; crossing != 0])) || crossing != 1 || BridgeControl.c &lt;= 1</formula>
			<comment>Whenever a train is crossing while another is not safe, the bridge controller can ensure a new crossing starts with 15 time units after the first ends
EXPECT: True
RESOURCES: &lt;180 s</comment>
		</query>
	</queries>
</nta>
