A PAR Protocol

Read Section 3.3.3 from the material that was handed out (taken from Andrew S. Tanenbaum, "Computer Networks", 3rd ed.). Make a Promela model of the PAR protocol and use XSpin to check the following correctness properties:

Deadlock freedom.
No packets are lost or duplicated (between the network layers)
If, from some point on, the channel damages or loses all frames, then it is also the case that from some point on the consumer does not make progress anymore.

(Tip: It may be helpful to use the code of the ABP as a starting point).