Murali Talupur and Mark Tuttle. Going with the flow: Parameterized verification using message flows. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2008.

we used the following murphi models as our examples (grab them all as a single file)

1. The Flash and German cache coherence protocols as modeled by Ching-Tsun Chou and used in the paper C.-T. Chou, P. K. Mannava, and S. Park, A simple method for parameterized verification of cache coherence protocols, FMCAD 2004.
2. The Flash and German protocols abstracted with flows as described in our paper.