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])
}

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