This case study models a very simple peer-to-peer protocol, loosely based on BitTorrent.

For more information, see: http://www.prismmodelchecker.org/casestudies/peer2peer.php

=====================================================================================