//
// This file implements Stenning's protocol which considers faulty channels.
// A process sends another process messages over a faulty channel. The other
// process acknowledges the received message by sending back the message tag
// which is a unique integer for each message.
//
// References: Nancy Lynch; Distributed Algorithms, Morgan Kaufman Publishers
// =========================================================================

package Communication.Stenning;

macro bits = 4;

module Stenning(
    event ?duplicateSDCH,	// duplicate message in Sender Channel
	  ?looseSDCH,		// loose message in Sender Channel
	  ?duplicateRCCH,	// duplicate message in Receiver Channel
	  ?looseRCCH,		// loose message in Receiver Channel
	  !delivered,		// holds if a message has been correctly acknowledged
	  send_messageSD,	// holds if Sender sends a message to Sender Channel
   int 	  out_tagSD,		// tag of message sent by Sender to Sender Channel
   event  !send_messageSDCH,	// holds if Sender Channel sends a message to Receiver
   int	  !out_tagSDCH,		// tag of message sent by Sender Channel to Receiver
	  min_tagSDCH,		// minimal tag stored in Sender Channel
	  max_tagSDCH, 	// maximal tag stored in Sender Channel
   event  send_messageRC,	// holds if Receiver sends a message to Receiver Channel
   int	  out_tagRC,		// tag of message sent by Receiver to Receiver Channel
   event  send_messageRCCH,	// holds if Receiver Channel sends a message to Sender
   int    !out_tagRCCH,	// tag of message sent by Receiver Channel to Sender
	  min_tagRCCH, // minimal tag stored in Receiver Channel
	  max_tagRCCH) // maximal tag stored in Receiver Channel
{
  event receive_messageRCCH;
  int in_tagRCCH;
  
      SD   : Sender
		(receive_messageRCCH,in_tagRCCH,
		send_messageSD,out_tagSD,delivered);
   || SDCH : Channel
		(send_messageSD,out_tagSD,duplicateSDCH,looseSDCH,
		min_tagSDCH,max_tagSDCH,send_messageSDCH,out_tagSDCH);
   || RC   : Receiver
		(receive_messageRCCH,in_tagRCCH,
		send_messageSD,out_tagSD);
   || RCCH : Channel
		(send_messageRC,out_tagRC,duplicateRCCH,looseRCCH,
		min_tagRCCH,max_tagRCCH,send_messageRCCH,out_tagRCCH);
}satisfies {
  works : assert A G (A F delivered);
}