In this illustration, a black arrow extends horizontally from the left to right and points at a blue circle labeled "Wait." The black arrow is labeled with a capital lambda over: "expectedseqnum=1 sndpkt=make_pkt(0,ACK,checksum)."

A blue arrow extends from the top left of the circle and arcs to the top right of the circle. This arrow has two labels. The top: "rdt_rcv(rcvpkt) && notcorrupt(rcvpkt)? && hasseqnum(rcvpkt,expectedseqnum)." The bottom: "extract(rcvpkt,data)? deliver_data(data) sndpkt=make_pkt(expectedseqnum,ACK,checksum) udt_send(sndpkt)? expectedseqnum++"

A blue arrow also extends from the bottom right of the circle and arcs upward to the top right of the circle. This arrow has two labels. The top: "default."

The bottom: "udt_send(sndpkt)."