<?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>/**
N cowboys stands in a circle with hands on their revolvers, waiting for the clock tower to hit noon.
As the bell rings and they start shooting wildly at eachother.
Who will be the last man standing? How can they collaborate to make any kinds of guarantees?

Black is the environment decided revolver draw time and reloading time.
Dark gray is always part of the coalition and controls listening end of synchronizations.

Note: Since templates cannot be parameterized with a color, we make one template per color.
Hence, the number of cowboys is not defined by N, but by the instantiations in the system declarations.

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;
typedef int[0,N-1] id_t;

const int ENDURANCE = 2; // Hits required to down a cowboy
const int RELOAD_MIN = 6;
const int RELOAD_MAX = 10;
const int DRAW_TIME_MAX = 4; // How fast the cowboys draw their revolver.

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;

clock t_ms;
chan shoot[N];
bool dead[N];
</declaration>
	<template>
		<name x="5" y="5">ShootingRed</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id0" x="111" y="-85">
			<name x="93" y="-144">Reloading</name>
			<label kind="invariant" x="93" y="-127">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id1" x="-144" y="-85">
			<name x="-170" y="-127">Ready</name>
		</location>
		<location id="id2" x="-331" y="-85">
			<name x="-357" y="-127">Init</name>
			<label kind="invariant" x="-390" y="-59">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id2"/>
		<transition id="id3" controllable="false">
			<source ref="id2"/>
			<target ref="id1"/>
		</transition>
		<transition id="id4" controllable="false">
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="guard" x="-93" y="0">x_ms&gt;=RELOAD_MIN</label>
			<nail x="111" y="-9"/>
			<nail x="-144" y="-9"/>
		</transition>
		<transition id="id5" color="#ff0000">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="select" x="-85" y="-204">target : id_t</label>
			<label kind="guard" x="-85" y="-187">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-85" y="-127">shoot[target]!</label>
			<label kind="assignment" x="-86" y="-110">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingOrange</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id6" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id7" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id8" x="-433" y="-34">
			<name x="-459" y="-76">Init</name>
			<label kind="invariant" x="-492" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id8"/>
		<transition id="id9" controllable="false">
			<source ref="id8"/>
			<target ref="id7"/>
		</transition>
		<transition id="id10" controllable="false">
			<source ref="id6"/>
			<target ref="id7"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id11" color="#ffa500">
			<source ref="id7"/>
			<target ref="id6"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingYellow</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id12" x="111" y="-85">
			<name x="93" y="-144">Reloading</name>
			<label kind="invariant" x="93" y="-127">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id13" x="-144" y="-85">
			<name x="-170" y="-127">Ready</name>
		</location>
		<location id="id14" x="-306" y="-85">
			<name x="-332" y="-127">Init</name>
			<label kind="invariant" x="-365" y="-59">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id14"/>
		<transition id="id15" controllable="false">
			<source ref="id14"/>
			<target ref="id13"/>
		</transition>
		<transition id="id16" controllable="false">
			<source ref="id12"/>
			<target ref="id13"/>
			<label kind="guard" x="-93" y="0">x_ms&gt;=RELOAD_MIN</label>
			<nail x="111" y="-9"/>
			<nail x="-144" y="-9"/>
		</transition>
		<transition id="id17" color="#ffff00">
			<source ref="id13"/>
			<target ref="id12"/>
			<label kind="select" x="-85" y="-204">target : id_t</label>
			<label kind="guard" x="-85" y="-187">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-85" y="-127">shoot[target]!</label>
			<label kind="assignment" x="-86" y="-110">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingGreen</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id18" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id19" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id20" x="-399" y="-34">
			<name x="-425" y="-76">Init</name>
			<label kind="invariant" x="-458" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id20"/>
		<transition id="id21" controllable="false">
			<source ref="id20"/>
			<target ref="id19"/>
		</transition>
		<transition id="id22" controllable="false">
			<source ref="id18"/>
			<target ref="id19"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id23" color="#00ff00">
			<source ref="id19"/>
			<target ref="id18"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingCyan</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id24" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id25" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id26" x="-399" y="-34">
			<name x="-425" y="-76">Init</name>
			<label kind="invariant" x="-458" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id26"/>
		<transition id="id27" controllable="false">
			<source ref="id26"/>
			<target ref="id25"/>
		</transition>
		<transition id="id28" controllable="false">
			<source ref="id24"/>
			<target ref="id25"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id29" color="#00ffff">
			<source ref="id25"/>
			<target ref="id24"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingBlue</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id30" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id31" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id32" x="-399" y="-34">
			<name x="-425" y="-76">Init</name>
			<label kind="invariant" x="-458" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id32"/>
		<transition id="id33" controllable="false">
			<source ref="id32"/>
			<target ref="id31"/>
		</transition>
		<transition id="id34" controllable="false">
			<source ref="id30"/>
			<target ref="id31"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id35" color="#0000ff">
			<source ref="id31"/>
			<target ref="id30"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingMagenta</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id36" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id37" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id38" x="-408" y="-34">
			<name x="-434" y="-76">Init</name>
			<label kind="invariant" x="-467" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id38"/>
		<transition id="id39" controllable="false">
			<source ref="id38"/>
			<target ref="id37"/>
		</transition>
		<transition id="id40" controllable="false">
			<source ref="id36"/>
			<target ref="id37"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id41" color="#ff00ff">
			<source ref="id37"/>
			<target ref="id36"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>ShootingPink</name>
		<parameter>const id_t index</parameter>
		<declaration>clock x_ms;
</declaration>
		<location id="id42" x="17" y="-34">
			<name x="-1" y="-93">Reloading</name>
			<label kind="invariant" x="-1" y="-76">x_ms&lt;=RELOAD_MAX</label>
		</location>
		<location id="id43" x="-238" y="-34">
			<name x="-264" y="-76">Ready</name>
		</location>
		<location id="id44" x="-399" y="-34">
			<name x="-425" y="-76">Init</name>
			<label kind="invariant" x="-458" y="-8">x_ms&lt;=DRAW_TIME_MAX</label>
		</location>
		<init ref="id44"/>
		<transition id="id45" controllable="false">
			<source ref="id44"/>
			<target ref="id43"/>
		</transition>
		<transition id="id46" controllable="false">
			<source ref="id42"/>
			<target ref="id43"/>
			<label kind="guard" x="-187" y="51">x_ms&gt;=RELOAD_MIN</label>
			<nail x="17" y="42"/>
			<nail x="-238" y="42"/>
		</transition>
		<transition id="id47" color="#ffc0cb">
			<source ref="id43"/>
			<target ref="id42"/>
			<label kind="select" x="-179" y="-153">target : id_t</label>
			<label kind="guard" x="-179" y="-136">target != index &amp;&amp;
!dead[target] &amp;&amp;
!dead[index]</label>
			<label kind="synchronisation" x="-179" y="-76">shoot[target]!</label>
			<label kind="assignment" x="-180" y="-59">x_ms := 0</label>
		</transition>
	</template>
	<template>
		<name>Health</name>
		<parameter>const id_t index</parameter>
		<declaration>int[0,ENDURANCE] hits_taken := 0;
</declaration>
		<location id="id48" x="42" y="-102">
			<name x="32" y="-136">Alive</name>
		</location>
		<location id="id49" x="-408" y="59">
			<name x="-418" y="25">Dead</name>
		</location>
		<location id="id50" x="-128" y="59">
			<committed/>
		</location>
		<init ref="id48"/>
		<transition id="id51" color="#ffc0cb">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="0">shoot[index]?</label>
			<nail x="25" y="17"/>
			<nail x="-128" y="17"/>
		</transition>
		<transition id="id52" color="#ff00ff">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-17">shoot[index]?</label>
			<nail x="25" y="0"/>
			<nail x="-128" y="0"/>
		</transition>
		<transition id="id53" color="#0000ff">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-34">shoot[index]?</label>
			<nail x="25" y="-17"/>
			<nail x="-128" y="-17"/>
		</transition>
		<transition id="id54" color="#00ffff">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-51">shoot[index]?</label>
			<nail x="25" y="-34"/>
			<nail x="-128" y="-34"/>
		</transition>
		<transition id="id55" color="#00ff00">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-68">shoot[index]?</label>
			<nail x="25" y="-51"/>
			<nail x="-128" y="-51"/>
		</transition>
		<transition id="id56" color="#ffff00">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-85">shoot[index]?</label>
			<nail x="25" y="-68"/>
			<nail x="-128" y="-68"/>
		</transition>
		<transition id="id57" color="#ffa500">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-102">shoot[index]?</label>
			<nail x="25" y="-85"/>
			<nail x="-128" y="-85"/>
		</transition>
		<transition id="id58" color="#ff0000">
			<source ref="id48"/>
			<target ref="id50"/>
			<label kind="synchronisation" x="-110" y="-119">shoot[index]?</label>
			<nail x="-128" y="-102"/>
		</transition>
		<transition id="id59">
			<source ref="id50"/>
			<target ref="id48"/>
			<label kind="guard" x="-93" y="68">hits_taken + 1 &lt; ENDURANCE</label>
			<label kind="assignment" x="-93" y="85">hits_taken++</label>
			<nail x="42" y="59"/>
		</transition>
		<transition id="id60">
			<source ref="id50"/>
			<target ref="id49"/>
			<label kind="guard" x="-382" y="68">hits_taken + 1 == ENDURANCE</label>
			<label kind="assignment" x="-382" y="85">hits_taken++,
dead[index] := true</label>
		</transition>
	</template>
	<system>S0 = ShootingRed(RED); H0 = Health(RED);
S1 = ShootingOrange(ORANGE); H1 = Health(ORANGE);
S2 = ShootingYellow(YELLOW); H2 = Health(YELLOW);
S3 = ShootingGreen(GREEN); H3 = Health(GREEN);
S4 = ShootingCyan(CYAN); H4 = Health(CYAN);
S5 = ShootingBlue(BLUE); H5 = Health(BLUE);
S6 = ShootingMagenta(MAGENTA); H6 = Health(MAGENTA);
S7 = ShootingPink(PINK); H7 = Health(PINK);
system 
    S0, H0
    ,S1, H1
    ,S2, H2
    ,S3, H3
    ,S4, H4
//    ,S5, H5
//    ,S6, H6
//    ,S7, H7
;
</system>
	<queries>
		<query>
			<formula>&lt;&lt;red&gt;&gt; [] !dead[RED]</formula>
			<comment>Can RED guarantee own survival?
EXPECT: False
RESOURCES: &lt;2 s</comment>
		</query>
		<query>
			<formula>[[ ]] [] !dead[RED]</formula>
			<comment>Does a trace exists where RED survives?
EXPECT: True
RESOURCES: &lt;10 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red&gt;&gt; [!dead[RED] U t_ms &gt; 1000]</formula>
			<comment>Can RED guarantee to survive for 4000 ms?
EXPECT: False
RESOURCES: &lt;30 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red&gt;&gt; &lt;&gt; dead[RED]</formula>
			<comment>Can RED guarantee suicide?
EXPECT: False
RESOURCES: &lt;10 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red&gt;&gt; &lt;&gt; dead[YELLOW]</formula>
			<comment>Can RED guarantee killing YELLOW?
EXPECT: False
RESOURCES: &lt;10 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red,orange&gt;&gt; &lt;&gt; dead[YELLOW]</formula>
			<comment>Can RED and ORANGE guarantee killing YELLOW?
EXPECT: False
RESOURCES: &lt;10 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red,orange,yellow&gt;&gt; [] !(dead[RED] &amp;&amp; dead[ORANGE] &amp;&amp; dead[YELLOW])</formula>
			<comment>Can half the cowboys guarantee that any of them survives?
EXPECT: False
RESOURCES: &lt;2 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;black,red,orange,yellow&gt;&gt; [] !(dead[RED] &amp;&amp; dead[ORANGE] &amp;&amp; dead[YELLOW])</formula>
			<comment>Can half the cowboys guarantee that any of them survives - if they are fast?
EXPECT: False
RESOURCES: &lt;30 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;red&gt;&gt; &lt;&gt; (&lt;&lt;orange&gt;&gt; &lt;&gt; H2.hits_taken &gt; 0)</formula>
			<comment>Can RED ensure a state is reached where ORANGE can ensure YELLOW is hit?
EXPECT: False
RESOURCES: &lt;30 s</comment>
		</query>
	</queries>
</nta>
