Protocol managing retransmissions
when message is lost then retransmission by the sender
sending order is consistent with receiving order
For sender A and receiver B the alternating bit protocol is as follows
Tempura code:
load "tam". /∗ tam provides an api for defining channels and provides the synchronous receive and send commands: chan(C) : defines a channel C wrc(C,X) : send the value of X over channel C rdc(C,V) : receive the value V over channel C ready(C) : there is data in channel C ∗/
/∗ run ∗/ define abp() = { exists D, Ack : { /∗ D : channel used to send and receive data Ack: channel used to send and receive acknowledgements ∗/ /∗ main body of the system, declare 2 channels and let the sender and receiver communicate via those channels ∗/ len(20) and chan(D) and chan(Ack) and sender(D,Ack) and receiver(D,Ack) } }.
/∗ the sender ∗/ define sender(D,Ack) = { exists Sendbuff, Data, RAck : { /∗ Sendbuff: variable containing data to be sent, Data : variable used in the generation of data RAck : variable used to store the received Ack ∗/ define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ /∗ function indicating whether Sendbuff contains data or not ∗/ define new_data() = { Sendbuff ~= no_data } and /∗ generate data and put it in Sendbuff ∗/ define produce() = { format("A is producing %t\n", Data) and Data := Data + 1 and Sendbuff:= Data } and
/∗ send data in Sendbuff via channel D ∗/ define sendD() = { format("A is sending via D %t\n", Sendbuff) and wrc(D,Sendbuff) } and /∗ receive Ack and put it in RAck ∗/ define recAck() = { rdc(Ack,RAck) and format("A is receiving via Ack %t\n",RAck) and Sendbuff := no_data } and /∗ initial state: Sendbuff contains no data and Data is zero ∗/ Sendbuff = no_data and Data = 0 and /∗ show in each state the value of Sendbuff ∗/ always format("A, Sendbuff=%d\n",Sendbuff) and
/∗ main body of the sender ∗/ chopstar{ skip and if new_data() then { sendD() and recAck() and stable(Data) } else { produce() } } } }.
/∗ the receiver ∗/ define receiver(D,Ack) = { exists RData : { /∗ RData: used to store the received data from channel D ∗/ /∗ receive data from channel D and store it in RData ∗/ define recD() = { rdc(D,RData) and format("B is receiving via D %t\n",RData) and format("B is consuming %t\n", RData) } and /∗ send 1 via channel Ack ∗/ define sendAck() = { wrc(Ack, 1) and format("B is sending via Ack %t\n",1) } and
/∗ main body of the receiver ∗/ chopstar{ skip and if ready(D) then { recD() and sendAck() } } } }.
Tempura code:
load "tam". /∗ tam provides an api for defining channels and provides the synchronous receive and send commands: chan(C) : defines a channel C wrc(C,X) : send the value of X over channel C rdc(C,V) : receive the value V over channel C ready(C) : there is data in channel C ∗/
/∗ run ∗/ define abp() = { exists D, Ack : { /∗ D : lossy channel used to send and receive data Ack: channel used to send and receive acknowledgements ∗/ /∗ main body of the system, declare 2 channels and let the sender and receiver communicate via those channels ∗/ len(20) and chan(D) and chan(Ack) and sender(D,Ack) and receiver(D,Ack) } }.
/∗ the sender ∗/ define sender(D,Ack) = { exists Sendbuff, Data, RAck : { /∗ Sendbuff: variable containing data to be sent, Data : variable used in the generation of data RAck : variable used to store the received Ack ∗/ define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ define faulty_s_data = -1 and /∗ indicates faulty sent data ∗/ /∗ function indicating whether Sendbuff contains data or not ∗/ define new_data() = { Sendbuff ~= no_data } and /∗ generate data and put it in Sendbuff ∗/ define produce() = { format("A is producing %t\n", Data) and Data := Data + 1 and Sendbuff:= Data } and
/∗ send data in Sendbuff via lossy channel D ∗/ define sendD() = { format("A is sending via D %t\n", Sendbuff) and if Random mod 2 = 1 then { wrc(D,Sendbuff) } else { wrc(D,faulty_s_data) } } and /∗ receive Ack and put it in RAck if RAck is zero then Sendbuff needs to be sent again ∗/ define recAck() = { rdc(Ack,RAck) and format("A is receiving via Ack %t\n",RAck) and if RAck ~= 0 then { Sendbuff := no_data and format("A, Ack is ok \n") } else { Sendbuff := Sendbuff and format("A, Ack is not ok, resending \n") } } and
/∗ initial state: Sendbuff contains no data and Data is zero ∗/ Sendbuff = no_data and Data = 0 and /∗ show in each state the value of Sendbuff ∗/ always format("A, Sendbuff=%d\n",Sendbuff) and /∗ main body of the sender ∗/ chopstar{ skip and if new_data() then { sendD() and recAck() and stable(Data) } else { produce() } } } }.
/∗ the receiver ∗/ define receiver(D,Ack) = { exists RData : { /∗ RData: variable used to store the received data from channel D ∗/ define faulty_r_data = -1 and /∗ indicates faulty received data ∗/ /∗ receive data from lossy channel D and store it in RData if data is not faulty send 1 via channel Ack if data is faulty send 0 via channel Ack ∗/ define recDsendAck() = { rdc(D,RData) and format("B is receiving via D %t \n", RData) and if RData ~= faulty_r_data then { format("B is consuming %t \n", RData) and format("B is sending via Ack %t \n",1) and wrc(Ack, 1) } else { format("B, Data over D is lost \n") and format("B is sending via Ack %t\n",0) and wrc(Ack, 0) } } and
/∗ main body of the receiver ∗/ chopstar{ skip and if ready(D) then { recDsendAck() } } } }.
Tempura code:
load "tam". /∗ tam provides an api for defining channels and provides the synchronous receive and send commands: chan(C) : defines a channel C wrc(C,X) : send the value of X over channel C rdc(C,V) : receive the value V over channel C ready(C) : there is data in channel C ∗/
/∗ run ∗/ define abp() = { exists D, Ack : { /∗ D : lossy channel used to send and receive data Ack: lossy channel used to send and receive acknowledgements ∗/ /∗ main body of the system, declare 2 channels and let the sender and receiver communicate via those channels ∗/ len(20) and chan(D) and chan(Ack) and sender(D,Ack) and receiver(D,Ack) } }. define flip(X) = { if X=1 then 0 else 1 }.
/∗ the sender ∗/ define sender(D,Ack) = { exists Sendbuff, Data, RAck, Cs : { /∗ Sendbuff: variable containing data to be sent, Data : variable used in the generation of data RAck : variable used to store the received Ack Cs : variable containing the current protocol bit ∗/ define no_data = -2 and /∗ indicates no data in Sendbuff ∗/ define faulty_s_data = [-1,-1] and /∗ indicates faulty sent data ∗/ define faulty_r_ack = -1 and /∗ indicates faulty received ack ∗/ /∗ function indicating whether Sendbuff contains data or not ∗/ define new_data() = { Sendbuff ~= no_data } and /∗ generate data and put it in Sendbuff update the protocol bit in Cs ∗/ define produce() = { format("A is producing %t\n", Data) and Cs := flip(Cs) and Data := Data + 1 and Sendbuff:= Data } and
/∗ send data in Sendbuff via lossy channel D ∗/ define sendD() = { format("A is sending via D %t\n", [Sendbuff,Cs]) and if Random mod 2 = 1 then { wrc(D,[Sendbuff,Cs]) } else { wrc(D,faulty_s_data) } } and
/∗ receive Ack and put it in RAck if RAck is not faulty and is equal to protocol bit Cs then Sendbuff is updated if RAck is not faulty and is not equal to protocol bit Cs then Sendbuff needs to be sent again if RAck is faulty then Sendbuff needs to be sent again ∗/ define recAck() = { rdc(Ack,RAck) and format("A is receiving via Ack %t\n",RAck) and if RAck ~= faulty_r_ack then { if Cs = RAck then { Sendbuff := no_data and format("A, Ack is ok \n") } else { Sendbuff:=Sendbuff and format("A, Ack is not ok, resending\n") } } else { Sendbuff:=Sendbuff and format("A, Ack is lost, resending \n") } } and
/∗ initial state: Sendbuff contains no data and Data is zero protocol bit Cs is zero ∗/ Sendbuff = no_data and Data = 0 and Cs = 0 and /∗ show in each state the value of Sendbuff and protocol bit Cs∗/ always format("A, Sendbuff=%d, Cs=%d\n",Sendbuff,Cs) and /∗ main body of the sender ∗/ chopstar{ skip and if new_data() then { sendD() and recAck() and stable(Data) and stable(Cs) } else { produce() } } } }.
/∗ the receiver ∗/ define receiver(D,Ack) = { exists RData, Cr : { /∗ RData: variable used to store the received data from channel D Cr : variable containing the current protocol bit ∗/ define faulty_r_data = -1 and /∗ indicates faulty received data ∗/ define faulty_s_ack = -1 and /∗ indicates faulty sent ack ∗/ /∗ send over lossy channel Ack the value X ∗/ define lossy_ack_send(X) = { if Random mod 2 = 1 then { wrc(Ack, X) } else { wrc(Ack,faulty_s_ack) } } and
/∗ receive data from lossy channel D and store it in RData if received data is not faulty and is equal to protocol bit Cr then send via Ack protocol bit Cr and update Cr if received data is not faulty and is not equal to protocol bit Cr then send via Ack the complement of protocol bit Cr if received data is faulty then send via Ack the complement of protocol bit Cr ∗/ define recDsendAck() = { rdc(D,RData) and format("B is receiving via D %t\n",RData) and /∗ !!! provide the missing bit here ∗/ } and
/∗ initialise protocol bit Cr to 1 ∗/ Cr = 1 and /∗ show in each state the value of protocol bit Cr ∗/ always format("B, Cr=%d \n",Cr) and /∗ main body of the receiver ∗/ chopstar{ skip and if ready(D) then { recDsendAck() } else { stable(Cr) } } } }.