leaderelection_withB.spec 222 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
Workflow

Christian Müller's avatar
Christian Müller committed
3
forall a,b,i
Christian Müller's avatar
Christian Müller committed
4
    (Inext(a,b) ∧ B(a,b,i)) -> msg += (i,b)
Christian Müller's avatar
Christian Müller committed
5 6 7
loop {
	forall a
		msg(a,a) -> leader += (a)
Christian Müller's avatar
Christian Müller committed
8
	forall a,b,c
Christian Müller's avatar
Christian Müller committed
9 10 11 12 13 14 15 16
		(Inext(b, c) ∧ msg(a, b) ∧ Ile(b, a)) -> msg += (a,c)
}

Target

msg(a1, a2)

Causality