/* Alternating Bit Protocol
*  Follows the treatment in 
*  "Communication and Concurrency", Robin Milner 
*  Prentice-Hall International Series in Computer Science
*/

range BIT = 0..1    //definition of transmitted data type

//Transmitter starts in the state ACCEPT[0]
TX             = ACCEPT[0],
ACCEPT[b:BIT]  = (accept -> SEND[b]),
SEND[b:BIT]    = (send[b] -> SENDING[b]),
SENDING[b:BIT] = (txto -> SEND[b] 
		   | ack[b] -> ACCEPT[!b] 
		   | ack[!b] -> SENDING[b]
		  ).

//Receiver starts in the state  REPLY[1]
RX              = REPLY[1],
DELIVER[b:BIT]  = (deliver -> REPLY[b]),
REPLY[b:BIT]    = (reply[b] -> REPLYING[b]),
REPLYING[b:BIT] = (rxto -> REPLY[b]
		    |trans[!b] -> DELIVER[!b]
                    |trans[b] -> REPLYING[b]
                  ).

//Lossy acknowledge channel 
ACK = (reply[b:BIT] -> (loseack ->ACK | ack[b]->ACK)).

//Lossy transmit channel
TRANS = (send[b:BIT] -> (losesend ->TRANS | trans[b]->TRANS)).

//Safety property that the protocol satsifies the spec for a 
//buffer

property BUFF = (accept -> deliver -> BUFF).

/* set of actions to control in animations */
// accept  - application message
// deliver - " at remote end
// rxto    - receiver timeout
// txto    - transmitter timeout
// loseack - ACK channel loses acknowledgment
// losesend- TRANS channel loses send

MENU = ({accept,deliver,rxto,txto,loseack,losesend}-> MENU).

// Check Safety to see system satisfies BUFF
// Run to get intuition of protocol
||AB_Check = (TX || ACK || TRANS || RX ||MENU|| BUFF).

//Minimise this system to see that AB is observationally equivalent to BUFF
//Use window Draw to display minimised LTS
||AB_Min = ( AB_Check ) @{accept,deliver}.