leaderelection_nonext.spec 261 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Workflow

forall a,b
    ∀d. (d = a ∨ d = b ∨ Ibtw(a,b,d)) -> msg += (a,b)
loop {
	forall a
		msg(a,a) -> leader += (a)
	forall a,b,c
		(∀d. (d = b ∨ d = c ∨ Ibtw(b,c,d)) ∧ msg(a, b) ∧ Ile(b,a)) -> msg += (a,c)
}

Target

msg(a1, a2)

Causality