Standard declarations E e INT BOOL STRING block DATA colset DATA = string; NO 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 success var success : 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 Transmit (success,pack) = if success then 1`pack else empty; fun Transmit (success,pack) = if success then 1`pack 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 success 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 success then 1`n else empty n data k k n if k=n then k+1 else 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 success then 1`(n,d) else empty (n,d) AddData (data,d,n,k) n (n,d) (n,d) UpdSeq(n,k) n if success then 1`n else empty n n data k UpdSeq(n,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) Transmit (success, (n,d)) (n,d) AddData (data,d,n,k) n (n,d) (n,d) UpdSeq(n,k) n Transmit (success,n) n data UpdSeq(n,k) k n k <same as model> true true false false false true true false false true false false true false true false false true true false false false false false false false false true false true false false true true false false false true false