A communication protocol with alternating confirmation code.

In this problem, there are four parties to consider: the message sender, the message receiver, the message channel and the confirmation code channel. The sender transmits the message body through the message channel together with a control code 0. When the receiver receives a message with the control code 0, it sends the 0 through the confirmation code channel. When the sender receives this confirmation, it sends the next packet with the control code 1. If the receiver receives it, it confirms by sending a 1 through the confirmation code channel. By alternating the control code, both receiver and sender can guard against message duplication and message loss, i.e., they ignore messages that have unexpected control code. NOTE: if the sender doesnt get the expected confirmation, it continues re-sending the message until the confirmation arrives. If the receiver doesnt get a message with the expected control code, it continuously resends the previous confirmation.

Requirements: Fairness is necessary. This is because, although we want to model the fact that the channel can lose messages, we want to assume that if we send a message often enough, eventually it will arrive.

TO DO: Write a NuSMV program, possibly to include multiple modules, to verify the above protocol based on the scenarios described.