Write a PROMELA model for the following communication protocol between a sender and a receiver.
The communication channels between the two processes transmit messages in order and without losses, but may be subject to errors. After each message, the receiver sends an ACK if the message was received correctly, and a NAK if there was an error. The sender waits for a reply before transmitting the next message, which is tagged with an ACK if the reply was received correctly, and with NAK if the reply was corrupted. (The tag of the first message does not matter). An error (corrupted message) is modeled by changing its tag to ERR.
Verify with Spin if the protocol ensures message receipt without losses or duplicates. If not, design a corrected protocol.