=======================================
Algorithm: Retransmit Forever

Implements: StubbornLink / StubbornPointToPointLinks (sl).
Uses: FairLossLink (fll).

upon event < sl, Init > do
	sent := ∅;
	starttimer(Δ);

upon event < Timeout > do
	forall (q, m) ∈ sent do
		trigger < fll, Send | q, m >;
	starttimer(Δ);

upon event < sl, Send | q, m > do
	trigger < fll, Send | q, m >;
	sent := sent ∪ {(q, m)};

upon event < fll, Deliver | p, m > do
	trigger < sl, Deliver | p, m >;

=======================================
Algorithm: Eliminate Duplicates

Implements: PerfectPointToPointLinks, instance pl.
Uses: StubbornPointToPointLinks, instance sl.

upon event < pl, Init > do
	delivered := ∅;

upon event < pl, Send | q, m > do
	trigger < sl, Send | q, m >;

upon event < sl, Deliver | p, m > do
	if m ∉ delivered then
		delivered := delivered ∪ {m};
		trigger < pl, Deliver | p, m >;

=======================================
Algorithm: Exclude on Timeout

Implements: PerfectFailureDetector, instance P.
Uses: PerfectPointToPointLinks, instance pl.

Note: This implement supposes ∆ is known.

upon event < P, Init > do
	alive := Π;
	detected := ∅;
	starttimer(2∆);

upon event < Timeout > do
	forall p ∈ Π do
		if (p ∉ alive) ∧ (p ∉ detected) then
			detected := detected ∪ {p};
			trigger < P, Crash | p >;
		trigger < pl, Send | p, [HEARTBEAT_REQUEST] >;
	alive := ∅;
	starttimer(2∆);

upon event < pl, Deliver | q, [HEARTBEAT_REQUEST] > do
	trigger < pl, Send | q, [HEARTBEAT_REPLY] >;

upon event < pl, Deliver | p, [HEARTBEAT_REPLY] > do
	alive := alive ∪ {p};

=======================================
Implements: EventuallyPerfectFailureDetector, instance ◇P.
Uses: PerfectPointToPointLinks, instance pl.

upon event < ◇P, Init > do
	alive := Π;
	suspected := ∅;
	delay := 2∆';
	starttimer(delay);

upon event < Timeout > do
	if alive ∩ suspected ≠ ∅ then
		delay := delay + 2∆';
	forall p ∈ Π do
		if (p ∉ alive) ∧ (p ∉ suspected) then
			suspected := suspected ∪ {p};
			trigger < ◇P, Suspect | p >;
		else if (p ∈ alive) ∧ (p ∈ suspected) then
			suspected := suspected \ {p};
			trigger < ◇P, Restore | p >;
		trigger < pl, Send | p, [HEARTBEAT_REQUEST] >;
	alive := ∅;
	starttimer(delay);

upon event < pl, Deliver | q, [HEARTBEAT_REQUEST] > do
	trigger < pl, Send | q, [HEARTBEAT_REPLY] >;

upon event < pl, Deliver | p, [HEARTBEAT_REPLY] > do
	alive := alive ∪ {p};

=======================================
Algorithm:  Monarchical Leader Election

Implements: LeaderElection, instance le.
Uses: PerfectFailureDetector, instance P.

upon event < le, Init > do
	suspected := ∅;
	leader := ⊥;

upon event < P , Crash | p > do
	suspected := suspected ∪ {p};

upon leader ≠ maxrank(Π \ suspected) do
	leader := maxrank(Π \ suspected);
	trigger <le, Leader | leader >;

=======================================
Algorithm: Monarchical Eventual Leader Detection

Implements: EventualLeaderDetector, instance Ω.
Uses: EventuallyPerfectFailureDetector, instance ◇P.

upon event < Ω, Init > do
	suspected := ∅;
	leader := ⊥;

upon event < ◇P, Suspect | p > do
	suspected := suspected ∪ {p};

upon event < ◇P, Restore | p > do
	suspected := suspected \ {p};

upon leader ≠ maxrank(Π \ suspected) do
	leader := maxrank(Π \ suspected);
	trigger < Ω, Trust | leader >;

=======================================
Algorithm: Basic broadcast

Implements: BestEffortBroadcast, instance beb.
Uses: PerfectPointToPointLinks, instance pl.

upon event < beb, Broadcast | m > do
	forall q ∈ Π do
		trigger < pl, Send | q, m >;

upon event < pl, Deliver | p, m > do
	trigger < beb, Deliver | p, m >;

=======================================
Algorithm: Lazy Reliable Broadcast

Implements: ReliableBroadcast, instance rb.
Uses: BestEffortBroadcast, instance beb; PerfectFailureDetector, instance P.
upon event < rb, Init > do
	correct := Π;
	delivered := ∅;
	forall p ∈ Π do from[p] := ∅;

upon event < rb, Broadcast | m > do
	trigger < beb, Broadcast | [DATA, self, m] >;

upon event < beb, Deliver | p, [DATA, s, m] > do
	if m ∉ delivered then
		delivered := delivered ∪ {m};
		trigger < rb, Deliver | s, m >;
		from[p] := from[p] ∪ {s, m};
		if p ∉ correct then
			trigger < beb, Broadcast | [DATA, s, m] >;

upon event < P, Crash | p > do
	correct := correct \ {p};
	forall {s, m} ∈ from[p] do
		trigger < beb, Broadcast | [DATA, s, m] >;

=======================================
Algorithm: Eager Reliable Broadcast

Implements: ReliableBroadcast, instance rb.
Uses: BestEffortBroadcast, instance beb.

upon event < rb, Init > do
	delivered := ∅;

upon event < rb, Broadcast | m > do
	trigger < beb, Broadcast | [DATA, self, m] >;

upon event < beb, Deliver | p, [DATA, s, m] > do
	if m ∉ delivered then
		delivered := delivered ∪ {m};
		trigger < rb, Deliver | s, m >;
		trigger < beb, Broadcast | [DATA, s, m] >;

=======================================
Algorithm: All-Ack Uniform Reliable Broadcast

Implements: UniformReliableBroadcast, instance urb.
Uses: BestEffortBroadcast, instance beb; PerfectFailureDetector, instance P.

upon event < urb, Init > do
	delivered := ∅;
	pending := ∅;
	correct := Π;
	forall m do ack[m] := ∅;

upon event < urb, Broadcast | m > do
	pending := pending ∪ {(self, m)};
	trigger < beb, Broadcast | [DATA, self, m] >;

upon event < beb, Deliver | p, [DATA, s, m] > do
	ack[m] := ack[m] ∪ {p};
	if (s, m) ∉ pending then
		pending := pending ∪ {(s, m)};
		trigger < beb, Broadcast | [DATA, s, m] >;

upon event < P, Crash | p > do
	correct := correct \ {p};

function candeliver(m) returns Boolean is
	return (correct ⊆ ack[m]);

upon exists (s, m) ∈ pending such that candeliver(m) ∧ m ∉ delivered do
	delivered := delivered ∪ {m};
	trigger < urb, Deliver | s, m >;

=======================================
Algorithm: Majority-Ack Uniform Reliable Broadcast

Implements: UniformReliableBroadcast, instance urb.
Uses: BestEffortBroadcast, instance beb.

upon event < urb, Init > do
	delivered := ∅;
	pending := ∅;
	forall m do ack[m] := ∅;

upon event < urb, Broadcast | m > do
	pending := pending ∪ {(self, m)};
	trigger < beb, Broadcast | [DATA, self, m] >;

upon event < beb, Deliver | p, [DATA, s, m] > do
	ack[m] := ack[m] ∪ {p};
	if (s, m) ∉ pending then
		pending := pending ∪ {(s, m)};
		trigger < beb, Broadcast | [DATA, s, m] >;

function candeliver(m) returns Boolean is
	return #(ack[m]) > N/2;

upon exists (s, m) ∈ pending such that candeliver(m) ∧ m ∉ delivered do
	delivered := delivered ∪ {m};
	trigger < urb, Deliver | s, m >;

=======================================
Algorithm: Hierarchical Consensus / Consensus algorithm I

Implements: Consensus, instance c.
Uses: BestEffortBroadcast, instance beb; PerfectFailureDetector, instance P.

upon event < c, Init > do
	detectedranks := ∅;
	round := 1;
	proposal := ⊥;
	proposer := 0;
	delivered := [FALSE]N;
	broadcast := FALSE;

upon event < P, Crash | p > do
	detectedranks := detectedranks ∪ {rank(p)};

upon event < c, Propose | v > such that proposal = ⊥ do
	proposal := v;

upon round = rank(self) ∧ proposal ≠ ⊥ ∧ broadcast = FALSE do
    broadcast := TRUE;
    trigger < beb, Broadcast | [DECIDED, proposal] >;
    trigger < c, Decide | proposal >;

upon round ∈ detectedranks ∨ delivered[round] = TRUE do
	round := round + 1;

upon event < beb, Deliver | p, [DECIDED, v] > do
    r := rank(p);
    if r < rank(self) ∧ r > proposer then
		proposal := v;
		proposer := r;
    delivered[r] := TRUE;

=======================================
Algorithm: Uniform Consensus algorithm II

Implements: UniformConsensus, instance uc.
Uses: BestEffortBroadcast, instance beb; PerfectFailureDetector, instance P.

upon event < uc, Init > do
	correct := Π;
	round := 1;
	proposal := ⊥;
	proposer := 0;
	delivered := [FALSE]N;
	broadcast := FALSE;

upon event < P, Crash | p > do
	detectedranks := detectedranks ∪ {rank(p)};

upon event < uc, Propose | v > such that proposal = ⊥ do
	proposal := v;

upon round = rank(self) ∧ proposal ≠ ⊥ ∧ broadcast = FALSE do
    broadcast := TRUE;
    trigger < beb, Broadcast | [PROPOSAL, proposal] >;

upon event < beb, Deliver | p, [PROPOSAL, v] > do
	r := rank(p);
    if r < rank(self) ∧ r > proposer then
		proposal := v;
		proposer := r;
    delivered[r] := TRUE;

upon round ∈ detectedranks ∨ delivered[round] = TRUE do
	if round = 𝑁 then
		trigger < c, Decide | proposal >;
	else
		round := round + 1;

=======================================
Algorithm: Consensus-Based Total-Order Broadcast

Implements: TotalOrderBroadcast, instance tob.
Uses: ReliableBroadcast, instance rb; Consensus (multiple instances).

upon event < tob, Init > do
	unordered := ∅;
	delivered := ∅;
	round := 1;
	wait := FALSE;

upon event < tob, Broadcast | m > do
	trigger < rb, Broadcast | m >;

upon event < rb, Deliver | p, m > do
	if m ∉ delivered then
		unordered := unordered ∪ {(p, m)};

upon unordered ≠ ∅ ∧ wait = FALSE do
	wait := TRUE;
	Initialize a new instance c.round of consensus;
	trigger < c.round, Propose | unordered >;

upon event < c.r, Decide | decided > such that r = round do
	forall (s, m) ∈ sort(decided) do
		trigger < tob, Deliver | s, m >;
	delivered := delivered ∪ decided;
	unordered := unordered \ decided;
	round := round + 1;
	wait := FALSE;

=======================================
Algorithm: Consensus algorithm III

Implements: UniformConsensus, instance uc.
Uses: BestEffortBroadcast, instance beb; EventuallyPerfectFailureDetector, instance ◇P; PerfectPointToPointLinks, instance pl.

upon event < uc, Init > do
	suspected := Ø; nacked := Ø;
	round := 1;
	proposed := false;
	proposal := ⊥;
	estimate := nil;
	estround := 0;
	states := [nil,0]N;
	acks := 0;

upon event < ◇P, Suspect | p> do
     suspected := suspected ∪ {p};

upon event < ◇P, Restore | p> do
     suspected := suspected \ {p};

upon event < uc, Propose | v > such that proposal = ⊥ do
	proposal := v;

upon rank(self) = round and proposed = false and proposal ≠ ⊥ do
	proposed :=true;
	states:=[nil,0]N;
	acks := 0;
	trigger < beb, Broadcast | [READ, round] >;

upon event < beb, Deliver | p, [READ, round] > and rank(p) = round do
	trigger < pl, Send | p, [GATHER, round, estimate, estround] >;

upon event < pl, Deliver | p, [GATHER, round, est, estrnd] > do
	states[p] := [est, estrnd];

upon #states ≥ majority do
	if  states[p] ≠ [nil,0] then
		select states[p]=[est, estrnd] with highest estrnd
		proposal := est;
	states := [nil, 0]N;
	trigger < beb, Broadcast | [IMPOSE, round, proposal] >;

upon event < beb, Deliver | p, [IMPOSE, round, v] > and rank(p) = round do
	estimate := v;
	estround := round;
	trigger < pl, Send | p, [ACK, round] >;

upon event < pl, Deliver | p, [ACK, round] > do
	acks := acks + 1;
	if acks ≥ majority then
		trigger < beb, Broadcast | [DECIDE, proposal] >;

upon event < beb, Deliver | p, [DECIDE, v] > do 
	 trigger < uc, Decide | v >;

upon rank(p) = round and p ∈ suspected do
	trigger < rb, Broadcast | [NACK, round] >;
	
upon event < rb, Deliver | p, [NACK, rnd] >
	nacked := nacked ∪ {rnd};

upon round ∈ nacked do
	proposed := false;
	round := round + 1;

=======================================
Algorithm: Consensus-Based Group Membership

Implements: GroupMembership, instance gm.
Uses: UniformConsensus (multiple instances); PerfectFailureDetector, instance P.

upon event < gm, Init > do
(id, M) := (0, Π);
correct := Π;
wait := FALSE;
trigger < gm, View | (id, M ) >;

upon event < P, Crash | p > do
	correct := correct \ {p};

upon correct ⊊ M ∧ wait = FALSE do
id := id + 1;
wait := TRUE;
Initialize a new instance uc.id;
trigger < uc.id, Propose | correct >;

upon event < uc.i, Decide | M' > such that i = id do
M := M';
wait := FALSE;
trigger < gm, View | (id, M) >;