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. 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.