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