/* sliding window protocol */

{
 wSize(2).     // window size
 nMAX(3).      // the maximum n for controlling retransmission etc.
 idMAX(3).     // the max id for checking the correctness of transmitted data
 error(false). // error detection flag
 
 sender{ n(0), nextId(0), sucId(0), c(0). }. // sender of data
 ss=rr.                                      // channel for data
 rs=sr.                                      // channel for ACK
 receiver{ n(0), expId(0). }.                // receiver of data
 
 // sender sends data:  sender -> [data]
 sd@@ sender{ n(N), nextId(ID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=SC
   :- C<W, C_=C+1, DN=(N+C) mod NMAX, ID_=(ID+1) mod IDMAX, int(SucID)
   |  sender{ n(N), nextId(ID_),sucId(SucID), c(C_)}, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=[data(DN,ID)|SC].
 
 // receiver receives expected data and sends ACK:  [data] -> receiver -> [ack]
 rs@@ receiver{ n(N), expId(EID) }, nMAX(NMAX), idMAX(IDMAX), SC=[data(DN,ID)|rr], rs=RC
   :- N=:=DN, EID=:=ID, N_=(N+1) mod NMAX, EID_=(EID+1) mod IDMAX
    | receiver{ n(N_),expId(EID_)}, nMAX(NMAX), idMAX(IDMAX), SC=rr, rs=[ack(DN)|RC].
 
 // receiver receives data and discards it, detecting data loss:
 // [data] -> receiver
 ru@@ receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr]
   :- N=\=DN, int(ID), int(EID), ground(SC)
    | receiver{ n(N), expId(EID) }, SC=rr.
 
 // receiver receives incorrect data:  [data] -> receiver -> error
 re@@ error(false), receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr], rs=RC, sender{ $p[] }
   :- N=:=DN, EID=\=ID, ground(SC), ground(RC)
    | error(true).
 
 // sender receives an expected ACK:  [ack] -> slide
 s@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), RC=[ack(ACK)|sr]
  :- N=:=ACK, C>0, N_=(N+1) mod NMAX, SucID_=(SucID+1) mod IDMAX, C_=C-1, int(NextID)
   | sender{ n(N_),nextId(NextID), sucId(SucID_),c(C_)}, nMAX(NMAX), idMAX(IDMAX), RC=sr.
 
 // sender receives an ACK and detects data or ACK loss:  [ack] -> reset
 r@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, RC=[ack(ACK)|sr]
  :- N=\=ACK, int(NextID), int(SucID), int(C)
   | sender{ n(N), nextId(SucID),  sucId(SucID), c(0) }, RC=sr.
 
 // sender detects timeout:  [timeout] -> reset
 t@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, timeout
  :- int(N), int(NextID), int(SucID), int(C)
   | sender{ n(N), nextId(SucID),  sucId(SucID), c(0) }.
 
 // channel loses data or ACK:  [data] -> [], [ack] -> []
 ld@@ X=[data(DN,ID)|Y] :- int(DN),int(ID) | X=Y.
 la@@ X=[ack(ACK)|Y] :- int(ACK) | X=Y .
}.

// timeout:  [] -> [timeout]
o@@ { error(false), $p, @p }/ :- { timeout, error(false), $p, @p }.