// // 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); }