Standard declarations E e INT BOOL STRING block DATA STRING colset DATA = STRING; NO INT colset NO = INT; NOxDATA NO DATA colset NOxDATA = product NO * DATA; NO n k var n,k : NO; DATA d data var d, data : DATA; BOOL ok var ok : BOOL; val AllPackets = 1`(1,"COL" )++ 1`(2,"OUR")++ 1`(3,"ED ")++ 1`(4,"PET")++ 1`(5,"RI ")++ 1`(6,"NET"); val AllPackets = 1`(1,"COL" )++ 1`(2,"OUR")++ 1`(3,"ED ")++ 1`(4,"PET")++ 1`(5,"RI ")++ 1`(6,"NET"); fun UpdSeq (n,k) = if n=k then k+1 else k; fun UpdSeq (n,k) = if n=k then k+1 else k; fun AddData (data,d,n,k) = if n=k then data^d else data; fun AddData (data,d,n,k) = if n=k then data^d else data; fun Trans (ok,p) = if ok then 1`p else empty; fun Trans (ok,p) = if ok then 1`p else empty; Packets To Send B Data Received NextSend A D C NextRec Send Packet Transmit Packet Receive Packet Transmit Ack Receive Ack (n,d) if ok then 1`(n,d) else empty (n,d) if n=k then data^d else data n (n,d) (n,d) if n=k then k+1 else k n if ok then 1`n else empty n n data k if n=k then k+1 else k k Packets To Send B Data Received NextSend A D C NextRec Send Packet Transmit Packet Receive Packet Transmit Ack Receive Ack (n,d) if ok then 1`(n,d) else empty (n,d) AddData(data,d,n,k) n (n,d) (n,d) UpdSeq(n,k) n if ok then 1`n else empty n n data k UpdSeq(n,k) k UpdSeq; AddData; Packets To Send B Data Received NextSend A D C NextRec Send Packet Transmit Packet Receive Packet Transmit Ack Receive Ack (n,d) Trans(ok,(n,d)) (n,d) AddData(data,d,n,k) n (n,d) (n,d) UpdSeq(n,k) n Trans(ok,n) n n data k UpdSeq(n,k) k