We has formally verified the Perlman Spanning Tree Algorithm. For more information about Perlman you can refer to this paper:
Perlman R., “An Algorithm for Distributed Computation of a Spanning Tree in an Extended LAN”, Ninth ACM Data Communications Symposium, v. 20, n. 7, pp. 44-52, 1985.
- Closed world model pack.
- Compositional model (Designated Bridge) pack.
- Compositional model (Best Port) pack.
- The specification of the model [zip]