leaderelection.spec 205 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
    Inext(a,b) -> msg += (a,b)
loop {
	forall a
		msg(a,a) -> leader += (a)
	forall a,b,c
		(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
}

Target

msg(a1, a2)

Causality