Să se modeleze în PROMELA următorul protocol de comunicație între un transmițător și un receptor:
Canalele de transmisie dintre cele două procese transmit mesajele în ordine, dar pot avea erori. O eroare e modelată prin schimbarea mesajului transmis într-un mesaj special de tipul eroare. Receptorul trimite, după fiecare mesaj primit, un mesaj de tipul ACK dacă recepția a fost corectă sau un mesaj de tipul NAK dacă a primit o eroare. Transmițătorul (re)transmite doar după primirea unei confirmări, și etichetează fiecare mesaj cu un câmp suplimentar ACK dacă a recepționat corect confirmarea precedentă, și NAK dacă a recepționat o eroare. (Eticheta primului mesaj nu contează, nefiind nimic de confirmat). Mesajele nu sunt etichetate în vreun alt fel.
Să se verifice cu Spin dacă protocolul asigură recepția mesajelor fără scăpări sau duplicate. În caz că nu, să se proiecteze un protocol corectat.