leaderelection_unsafe.spec

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)) -> msg += (a,c)
}

Target

msg(a1, a2)

Causality