In this illustration, we see a blue circle labeled "Wait for 0 from below." A blue arrow extends from the top of this circle to the right and into the top of a second circle, labeled "Wait for 1 from below." This arrow has two labels separated by a black line. On top: "rdt_rvc(rcvpkt) && notcorrupt(rcvpkt) && has_seq0(rcvpkt)." On bottom: "extract(rcvpkt,data) deliver_data(data) compute chksum make_pkt(sendpkt,ACK,chksum) udt_send(sndpkt)."

A smaller blue arrow extends from the top of the second circle and travels in a clockwise motion to the right side of the same circle. This circle has two labels. On top: "rdt_rcv(rcvpkt) && (corrupt(rcvpkt)|| has_seq0(rcvpkt)))." On bottom: "compute chksum make_pkt(sndpkt,NAK,chksum) udt_send(sndpkt)."

A blue arrow extends from the bottom of the second circle to the left and into the bottom of the first circle. This arrow has two labels. On top: "rdt_rvc(rcvpkt) && notcorrupt(rcvpkt) && has_seq1(rcvpkt)." On bottom: "extract(rcvpkt,data) deliver_data(data) compute chksum make_pkt(sendpkt,ACK,chksum) udt_send(sndpkt)."

A smaller circle extends from the bottom of the first circle and travels in a clockwise motion to the left side of the same circle. This arrow has two labels. On top: "rdt_rcv(rcvpkt) && (corrupt(rcvpkt)|| has_seq1(rcvpkt)))."

On bottom: "compute chksum make_pkt(sndpkt,NAK,chksum) udt_send(sndpkt)."