<?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>/**
Phase King consensus algorithm.
Time is divided into phases consisting of two rounds and each phase has a king process determined by id.
In the first round, everyone broadcasts their value to everyone.
In the second round, the phase king broadcasts the value that it received from &gt;=2/3 of nodes or its own value if none such value.
Other nodes then updates their value, choosing the value they received from &gt;=2/3 of nodes or the kings value if none such value.

It has been proved that consensus is maintained as long as &lt;=1/3 of nodes are malicious.

In this implementation, (malicious) nodes may deviate from the protocol by not sending certain messages.
(Note: Allowing malicious nodes to send arbitrary values makes it possible for nice nodes to do so too.
Since there is no hidden information, this results in unmeaningful tests.
And no, it is not possible to make maliciousness a parameter based on coalition.
We would have to hardcode malicousness.)

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 = 5;
const int V = 3;
const int MAX_VAL = V - 1;
typedef int[0,N-1] id_t;
typedef int[0,MAX_VAL] val_t;
typedef int[-1,MAX_VAL] opt_val_t;

const int ROUND_DUR = 100;
const int PHASE_DUR = 2 * ROUND_DUR;
const int PHASES = N;
const int ROUNDS = 2 * PHASES;

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 z;

broadcast chan phase_end;
broadcast chan round_end;
broadcast chan transmit[N][MAX_VAL + 1];

bool first_round = true;
int phase = 0;

bool initialized[N];
val_t initial[N];
val_t estimate[N];

bool all_initialized() {
    return forall (i : id_t) initialized[i];
}

bool consensus2(id_t p1, id_t p2) {
    return estimate[p1] == estimate[p2];
}

bool consensus3(id_t p1, id_t p2, id_t p3) {
    return estimate[p1] == estimate[p2] &amp;&amp; estimate[p2] == estimate[p3];
}

bool consensus4(id_t p1, id_t p2, id_t p3, id_t p4) {
    return estimate[p1] == estimate[p2] &amp;&amp; estimate[p2] == estimate[p3] &amp;&amp; estimate[p3] == estimate[p4];
}

bool consensus5(id_t p1, id_t p2, id_t p3, id_t p4, id_t p5) {
    return estimate[p1] == estimate[p2] &amp;&amp; estimate[p2] == estimate[p3] &amp;&amp; estimate[p3] == estimate[p4] &amp;&amp; estimate[p4] == estimate[p5];
}

bool consensus6(id_t p1, id_t p2, id_t p3, id_t p4, id_t p5, id_t p6) {
    return estimate[p1] == estimate[p2] &amp;&amp; estimate[p2] == estimate[p3] &amp;&amp; estimate[p3] == estimate[p4] &amp;&amp; estimate[p4] == estimate[p5] &amp;&amp; estimate[p5] == estimate[p6];
}

bool consensus7(id_t p1, id_t p2, id_t p3, id_t p4, id_t p5, id_t p6, id_t p7) {
    return estimate[p1] == estimate[p2] &amp;&amp; estimate[p2] == estimate[p3] &amp;&amp; estimate[p3] == estimate[p4] &amp;&amp; estimate[p4] == estimate[p5] &amp;&amp; estimate[p5] == estimate[p6] &amp;&amp; estimate[p6] == estimate[p7];
}</declaration>
	<template>
		<name x="5" y="5">ProcessRed</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id0" x="-1351" y="-246">
		</location>
		<location id="id1" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id2" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id3" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id1"/>
		<transition id="id4" controllable="false">
			<source ref="id3"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id5" controllable="false">
			<source ref="id2"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id6" controllable="false">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id7" color="#ff0000">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id8" controllable="false">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id9" color="#ff0000">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id10" color="#ff0000">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id11" color="#ff0000">
			<source ref="id0"/>
			<target ref="id2"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id12" controllable="false">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessOrange</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id13" x="-1351" y="-246">
		</location>
		<location id="id14" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id15" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id16" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id14"/>
		<transition id="id17" controllable="false">
			<source ref="id16"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id18" controllable="false">
			<source ref="id15"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id19" controllable="false">
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id20" color="#ffa500">
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id21" controllable="false">
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id22" color="#ffa500">
			<source ref="id13"/>
			<target ref="id16"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id23" color="#ffa500">
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id24" color="#ffa500">
			<source ref="id13"/>
			<target ref="id15"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id25" controllable="false">
			<source ref="id14"/>
			<target ref="id13"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessYellow</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id26" x="-1351" y="-246">
		</location>
		<location id="id27" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id28" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id29" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id27"/>
		<transition id="id30" controllable="false">
			<source ref="id29"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id31" controllable="false">
			<source ref="id28"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id32" controllable="false">
			<source ref="id26"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id33" color="#ffff00">
			<source ref="id26"/>
			<target ref="id26"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id34" controllable="false">
			<source ref="id26"/>
			<target ref="id26"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id35" color="#ffff00">
			<source ref="id26"/>
			<target ref="id29"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id36" color="#ffff00">
			<source ref="id26"/>
			<target ref="id26"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id37" color="#ffff00">
			<source ref="id26"/>
			<target ref="id28"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id38" controllable="false">
			<source ref="id27"/>
			<target ref="id26"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessGreen</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id39" x="-1351" y="-246">
		</location>
		<location id="id40" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id41" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id42" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id40"/>
		<transition id="id43" controllable="false">
			<source ref="id42"/>
			<target ref="id39"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id44" controllable="false">
			<source ref="id41"/>
			<target ref="id39"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id45" controllable="false">
			<source ref="id39"/>
			<target ref="id39"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id46" color="#00ff00">
			<source ref="id39"/>
			<target ref="id39"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id47" controllable="false">
			<source ref="id39"/>
			<target ref="id39"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id48" color="#00ff00">
			<source ref="id39"/>
			<target ref="id42"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id49" color="#00ff00">
			<source ref="id39"/>
			<target ref="id39"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id50" color="#00ff00">
			<source ref="id39"/>
			<target ref="id41"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id51" controllable="false">
			<source ref="id40"/>
			<target ref="id39"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessCyan</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id52" x="-1351" y="-246">
		</location>
		<location id="id53" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id54" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id55" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id53"/>
		<transition id="id56" controllable="false">
			<source ref="id55"/>
			<target ref="id52"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id57" controllable="false">
			<source ref="id54"/>
			<target ref="id52"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id58" controllable="false">
			<source ref="id52"/>
			<target ref="id52"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id59" color="#00ffff">
			<source ref="id52"/>
			<target ref="id52"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id60" controllable="false">
			<source ref="id52"/>
			<target ref="id52"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id61" color="#00ffff">
			<source ref="id52"/>
			<target ref="id55"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id62" color="#00ffff">
			<source ref="id52"/>
			<target ref="id52"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id63" color="#00ffff">
			<source ref="id52"/>
			<target ref="id54"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id64" controllable="false">
			<source ref="id53"/>
			<target ref="id52"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessBlue</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id65" x="-1351" y="-246">
		</location>
		<location id="id66" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id67" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id68" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id66"/>
		<transition id="id69" controllable="false">
			<source ref="id68"/>
			<target ref="id65"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id70" controllable="false">
			<source ref="id67"/>
			<target ref="id65"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id71" controllable="false">
			<source ref="id65"/>
			<target ref="id65"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id72" color="#0000ff">
			<source ref="id65"/>
			<target ref="id65"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id73" controllable="false">
			<source ref="id65"/>
			<target ref="id65"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id74" color="#0000ff">
			<source ref="id65"/>
			<target ref="id68"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id75" color="#0000ff">
			<source ref="id65"/>
			<target ref="id65"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id76" color="#0000ff">
			<source ref="id65"/>
			<target ref="id67"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id77" controllable="false">
			<source ref="id66"/>
			<target ref="id65"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessMagenta</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id78" x="-1351" y="-246">
		</location>
		<location id="id79" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id80" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id81" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id79"/>
		<transition id="id82" controllable="false">
			<source ref="id81"/>
			<target ref="id78"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id83" controllable="false">
			<source ref="id80"/>
			<target ref="id78"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id84" controllable="false">
			<source ref="id78"/>
			<target ref="id78"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id85" color="#ff00ff">
			<source ref="id78"/>
			<target ref="id78"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id86" controllable="false">
			<source ref="id78"/>
			<target ref="id78"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id87" color="#ff00ff">
			<source ref="id78"/>
			<target ref="id81"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id88" color="#ff00ff">
			<source ref="id78"/>
			<target ref="id78"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id89" color="#ff00ff">
			<source ref="id78"/>
			<target ref="id80"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id90" controllable="false">
			<source ref="id79"/>
			<target ref="id78"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>ProcessPink</name>
		<parameter>const int index</parameter>
		<declaration>
opt_val_t msgs[N];
bool msg_sent = false;

void clear_msgs() {
    for (i : id_t) {
        msgs[i] = i == index ? estimate[index] : -1;
    }
}

val_t majority() {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }
    return maj;
}

void update_estimate(int tiebreaker) {
    int mult[MAX_VAL+1];
    val_t maj = 0;
    int[0,N] maj_mult = 0;
    for (i : id_t) {
        if (msgs[i] != -1) {
            mult[msgs[i] ] += 1;
        }
    }
    for (v : val_t) {
        if (mult[v] &gt; maj_mult) {
            maj = v;
            maj_mult = mult[v];
        }
    }

    // More than 2/3 of votes?
    if (3 * maj_mult &gt;= 2 * N) {
        estimate[index] = maj;
    } else {
        estimate[index] = tiebreaker;
    }
}</declaration>
		<location id="id91" x="-1351" y="-246">
		</location>
		<location id="id92" x="-1547" y="-246">
			<committed/>
		</location>
		<location id="id93" x="-1096" y="-391">
			<label kind="comments" x="-1402" y="-518">All broadcasts happen on a committed location.
It is the only way to avoid some receiver
preventing it from happening.</label>
			<committed/>
		</location>
		<location id="id94" x="-1096" y="-187">
			<committed/>
		</location>
		<init ref="id92"/>
		<transition id="id95" controllable="false">
			<source ref="id94"/>
			<target ref="id91"/>
			<label kind="synchronisation" x="-1207" y="-170">transmit[index][majority()]!</label>
			<nail x="-1317" y="-187"/>
		</transition>
		<transition id="id96" controllable="false">
			<source ref="id93"/>
			<target ref="id91"/>
			<label kind="synchronisation" x="-1215" y="-374">transmit[index][estimate[index] ]!</label>
			<nail x="-1309" y="-391"/>
		</transition>
		<transition id="id97" controllable="false">
			<source ref="id91"/>
			<target ref="id91"/>
			<label kind="synchronisation" x="-1657" y="-16">round_end?</label>
			<label kind="assignment" x="-1657" y="1">msg_sent = false</label>
			<nail x="-1632" y="-25"/>
			<nail x="-1555" y="-25"/>
		</transition>
		<transition id="id98" color="#ffc0cb">
			<source ref="id91"/>
			<target ref="id91"/>
			<label kind="select" x="-1071" y="-119">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-102">!first_round</label>
			<label kind="synchronisation" x="-1071" y="-85">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-68">update_estimate(v)</label>
			<nail x="-1317" y="-111"/>
			<nail x="-1079" y="-111"/>
			<nail x="-1079" y="-51"/>
			<nail x="-1317" y="-51"/>
		</transition>
		<transition id="id99" controllable="false">
			<source ref="id91"/>
			<target ref="id91"/>
			<label kind="synchronisation" x="-1470" y="-16">phase_end?</label>
			<label kind="assignment" x="-1470" y="1">update_estimate(estimate[index]),
clear_msgs()</label>
			<nail x="-1461" y="-25"/>
			<nail x="-1402" y="-25"/>
		</transition>
		<transition id="id100" color="#ffc0cb">
			<source ref="id91"/>
			<target ref="id94"/>
			<label kind="guard" x="-1071" y="-221">!first_round &amp;&amp; phase == index &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-204">msg_sent = true</label>
			<nail x="-1318" y="-220"/>
			<nail x="-1096" y="-221"/>
		</transition>
		<transition id="id101" color="#ffc0cb">
			<source ref="id91"/>
			<target ref="id91"/>
			<label kind="select" x="-1072" y="-331">i : id_t, v : val_t</label>
			<label kind="guard" x="-1071" y="-314">first_round &amp;&amp; msgs[i] == -1</label>
			<label kind="synchronisation" x="-1071" y="-297">transmit[i][v]?</label>
			<label kind="assignment" x="-1071" y="-280">msgs[i] = v</label>
			<nail x="-1317" y="-322"/>
			<nail x="-1079" y="-322"/>
			<nail x="-1079" y="-263"/>
			<nail x="-1317" y="-263"/>
		</transition>
		<transition id="id102" color="#ffc0cb">
			<source ref="id91"/>
			<target ref="id93"/>
			<label kind="guard" x="-1071" y="-425">first_round &amp;&amp; !msg_sent</label>
			<label kind="assignment" x="-1071" y="-408">msg_sent = true</label>
			<nail x="-1317" y="-416"/>
			<nail x="-1096" y="-416"/>
		</transition>
		<transition id="id103" controllable="false">
			<source ref="id92"/>
			<target ref="id91"/>
			<label kind="select" x="-1530" y="-331">v : val_t</label>
			<label kind="assignment" x="-1530" y="-314">initialized[index] = true,
initial[index] = v,
estimate[index] = v,
clear_msgs()</label>
		</transition>
	</template>
	<template>
		<name>RoundCounter</name>
		<declaration>clock x;
</declaration>
		<location id="id104" x="-289" y="59">
			<label kind="invariant" x="-340" y="84">x&lt;=ROUND_DUR</label>
		</location>
		<location id="id105" x="-17" y="59">
			<committed/>
		</location>
		<location id="id106" x="-289" y="-42">
			<name x="-391" y="-33">PhaseBegin</name>
			<committed/>
		</location>
		<location id="id107" x="-518" y="-42">
			<committed/>
		</location>
		<init ref="id107"/>
		<transition id="id108" controllable="false">
			<source ref="id107"/>
			<target ref="id106"/>
			<label kind="guard" x="-484" y="-67">all_initialized()</label>
		</transition>
		<transition id="id109" controllable="false">
			<source ref="id106"/>
			<target ref="id104"/>
		</transition>
		<transition id="id110" controllable="false">
			<source ref="id105"/>
			<target ref="id106"/>
			<label kind="guard" x="-399" y="-229">!first_round</label>
			<label kind="synchronisation" x="-399" y="-212">phase_end!</label>
			<label kind="assignment" x="-399" y="-195">first_round = true,
phase = (phase + 1) % PHASES</label>
			<nail x="-289" y="-144"/>
		</transition>
		<transition id="id111" controllable="false">
			<source ref="id105"/>
			<target ref="id104"/>
			<label kind="guard" x="-68" y="-187">first_round</label>
			<label kind="assignment" x="-68" y="-170">first_round = false</label>
			<nail x="-17" y="-136"/>
		</transition>
		<transition id="id112" controllable="false">
			<source ref="id104"/>
			<target ref="id105"/>
			<label kind="guard" x="-170" y="68">x==ROUND_DUR</label>
			<label kind="synchronisation" x="-170" y="85">round_end!</label>
			<label kind="assignment" x="-271" y="59">x:=0</label>
		</transition>
	</template>
	<system>R0 = ProcessRed(0);
R1 = ProcessOrange(1);
R2 = ProcessYellow(2);
R3 = ProcessGreen(3);
R4 = ProcessCyan(4);
R5 = ProcessBlue(5);
R6 = ProcessMagenta(6);
R7 = ProcessPink(7);

system RoundCounter
    ,R0
    ,R1
    ,R2
    ,R3
    ,R4
//    ,R5
//    ,R6
//    ,R7
;
</system>
	<queries>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (&lt;&lt;red&gt;&gt; [] estimate[RED] == 0) || estimate[RED] != 0 || !RoundCounter.PhaseBegin</formula>
			<comment>Red can guarantee that its estimate value stay 0 forever
EXPECT: False
RESOURCES: &lt;5 s</comment>
		</query>
		<query>
			<formula>[[ ]] &lt;&gt; !RoundCounter.PhaseBegin &amp;&amp; consensus3(RED,ORANGE,YELLOW)</formula>
			<comment>There exists a trace where RED, ORANGE, and YELLOW reaches consensus
EXPECT: True
RESOURCES: &lt;1 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; &lt;&gt; RoundCounter.PhaseBegin &amp;&amp; consensus3(RED,ORANGE,YELLOW)</formula>
			<comment>RED, ORANGE, and YELLOW eventually reach consensus in all traces
EXPECT: False
RESOURCES: &lt;120 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (&lt;&lt;red,orange,yellow&gt;&gt; [] consensus3(RED,ORANGE,YELLOW) || !RoundCounter.PhaseBegin) || !consensus3(RED,ORANGE,YELLOW) || !RoundCounter.PhaseBegin</formula>
			<comment>If RED, ORAGE, and YELLOW have consensus, then they can stay in consensus (validity)
EXPECT: True
RESOURCES: &lt;10 min</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (z @ (&lt;&lt;red,orange&gt;&gt; [] consensus3(RED,ORANGE,YELLOW) || z &gt; PHASE_DUR || !RoundCounter.PhaseBegin)) || !consensus3(RED,ORANGE,YELLOW) || !RoundCounter.PhaseBegin</formula>
			<comment>Can RED, ORANGE, and YELLOW lose consensus within one phase if YELLOW stops cooperating
EXPECT: True
RESOURCES: &lt;5 min</comment>
		</query>
		<query>
			<formula>[[ ]] &lt;&gt; !RoundCounter.PhaseBegin &amp;&amp; consensus4(RED,ORANGE,YELLOW,GREEN)</formula>
			<comment>There exists a trace where RED, ORANGE, YELLOW, and GREEN reaches consensus
EXPECT: True
RESOURCES: &lt;1 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; &lt;&gt; RoundCounter.PhaseBegin &amp;&amp; consensus4(RED,ORANGE,YELLOW,GREEN)</formula>
			<comment>RED, ORANGE, YELLOW, and GREEN eventually reach consensus in all traces
EXPECT: False
RESOURCES: &lt;120 s</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (&lt;&lt;red,orange,yellow,green&gt;&gt; [] consensus4(RED,ORANGE,YELLOW,GREEN) || !RoundCounter.PhaseBegin) || !consensus4(RED,ORANGE,YELLOW,GREEN) || !RoundCounter.PhaseBegin</formula>
			<comment>If RED, ORANGE, YELLOW, and GREEN have consensus, then they can stay in consensus (validity)
EXPECT: True
RESOURCES: &lt;5 min</comment>
		</query>
		<query>
			<formula>&lt;&lt;&gt;&gt; [] (z @ (&lt;&lt;red,orange,yellow&gt;&gt; [] consensus4(RED,ORANGE,YELLOW,GREEN) || z &gt; PHASE_DUR || !RoundCounter.PhaseBegin)) || !consensus4(RED,ORANGE,YELLOW,GREEN) || !RoundCounter.PhaseBegin</formula>
			<comment>Can RED, ORANGE, YELLOW, and GREEN lose consensus within one phase if GREEN stops cooperating
EXPECT: False
RESOURCES: &lt;5 min</comment>
		</query>
	</queries>
</nta>
