Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams