Alternating Bit Protocol - core to smv
		######################################


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:
-----------------

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.


Some remarks about the translation:
-----------------------------------

* _terminate is always 0 because a finite calculation path is not possible, 
  there is always at least one enabled transition.
* in the next statements of num_of_messages and num_of_recv_messages an extra
  condition is added to the case entries where the value given is an expression. 
  this is done in order to maintain the next value of these variables within the 
  bounds of their type range.
* because of the HOLD_PREVIOUS in the core program all the default entries in the 
  next statements of the program's variables keep the current value of these variables.
  we will get to the default entry only if the next transition to be executed
  (the next value of _trans) doesnt change the variable.