Leader election

Consider the following partial model of the ring leader election protocol.

open util/ordering[Id]

sig Node {
	id : one Id,
	succ : one Node,
	var inbox : set Id,
	var outbox : set Id
}

sig Id {}

fact ring {
	all i : Id | lone id.i
	all n : Node | Node in n.^succ
}

fun elected : set Node {
	{n : Node | once (n.id in n.inbox)}
}

pred send [n : Node] { ... }

pred compute [n : Node] {
	some i : n.inbox {
		n.inbox' = n.inbox - i
		n.outbox' = n.outbox + (i - n.id.*(~next))
	}
	all m : Node - n | m.inbox' = m.inbox
	all m : Node - n | m.outbox' = m.outbox
}

pred skip {
	inbox' = inbox
	outbox' = outbox
}

fact init {
	no inbox
	outbox = id
}

fact transitions {
	always (skip or some n : Node | send[n] or compute[n])
}

assert safety {
	always lone elected
}
check safety


pred sendEnabled [n : Node] { some n.outbox }
pred computeEnabled [n : Node] { some n.inbox }

pred fairness {
	all n : Node {
		(eventually always sendEnabled[n] implies (always eventually send[n]))
		(eventually always computeEnabled[n] implies (always eventually compute[n]))
	}
}

assert liveness {
	fairness and some Node implies eventually some elected
}
check liveness

1. Finish the model by defining the predicate send.
2. Using the simulator and an empty run command, show that the following scenarios are possible:
   1. Starting with a 3 node ring with ids in increasing order, it is possible to reach a state where one node of them is elected in 5 steps.
   2. Starting with a 2 node ring, it is possible to reach a state where one of them is elected and all the mailboxes are empty.
3. Show how the previous scenarios can be directly generated with a run command.
4. Fix the specification of the safety assertion to ensure that it is not possible for two different processes to be elected at different times.
5. This model can be simplified by removing the Id signature and directly impose the total order over the signature Node. Change the model to reflect this simplification.
6. Use auxiliary functions to visualise which events are occurring at each time.
7. The model can be made more abstract by removing the outbox and by merging the compute and send operations. Change the model to reflect this simplification.