Alternating Bit Protocol - Core to Spin , by - Avi Magid

Protocol description :

 A protocol for managing the retransmission of lost messages.
 Consider a sender and a receiver , and assume that the channel from
sender to receiver is initialized so that there are no messages in
transit. the alternating bit protocol works as follows:

1. Each data message sent by Sender contains a protocol bit , 0 or 1.
2. When Sender sends a message , it send it repeatedly (with its
   corresponding bit) until receiving an acknowledgment (ACK) from
   Receiver that contains the same protocol bit as the message being
   sent. 
3. When Receiver receives a message , it sends an ACK to Sender and
   includes the protocol bit of the message received. The first time
   the message is received , the protocol delivers the message for
   processing. Subsequent messages with the same bit are simply
   acknowledged.
4. When Sender receives ACK containing the same bit as the mesage it
   is currently transmitting , it stops transmitting that message ,
   flips the protocol bit , and repeats the protocol for the next
   message. 

The Core program (file - abp1):

Contains 3  modules - SENDER and RECEIVER represents the sender and
the receiver respectively and SYSTEM module that instantinates the
Sender and Receiver modules.
The Sender and the Receiver modules are asynchronous so that messages
and acknowledgements can be transfered in a asynchronous way , but 
non of the messages will be lost because of the protocol.

Remarks about the Spin translated program (file - spin_program):

1. All the global variables in the Core program remained global in the Spin
   program.
2. in version2 directory there is another version of
   alternating bit protocol (file - abp2).
   In this version  the variables message_exists and ack_exists are  common to
   two module  instantinations , but not global , by using the same actual parameters
   for the SENDER and RECEIVER instantinations.
   In the Spin translated program -    the two common variables - message_exists
   and ack_exists became global variables - global_message_exists_0
   and global_ack_exists_0 .