Trans

include queue
include timeout
include seqnum

module transport(lower,packet,id) = {

    relation sent(D:id,P:packet)

    action send(src:id,dst:id,pkt:packet)
    action recv(dst:id,pkt:packet)

    object spec = {

        after init {
            sent(D,P) := false
        }

        before send {
            assert ~sent(dst,pkt);
            sent(dst,pkt) := true
        }

        before recv {
            assert sent(dst,pkt);
            sent(dst,pkt) := false
        }
    }

    instance seq_num : sequence_numbers

these type describe the format of messages

    type mtype = {msg_t, ack_t}

    object net_msg = {
        type t = struct {
            mty : mtype,
            src : id,
            num : seq_num.t,
            payload : packet
        }
    }

    object impl(me:id) = {

Create one outgoing message queue for each host and a timout for each queue.

        instance mq(D:id) : message_queue(net_msg,seq_num)
        instance timer(D:id) : timeout_sec

Keep track of the latest sequence number sent and received on each channel.

        var send_seq(S:id) : seq_num.t
        var recv_seq(S:id) : seq_num.t

        after init {
            recv_seq(S) := 0;
            send_seq(S) := 0;
        }

Implementations of interface actions

        implement send(dst:id,pkt:packet) {
            var msg : net_msg.t;
            var seq : seq_num.t;
            msg.mty := msg_t;
            msg.src := me;
            msg.num := send_seq(dst);
            msg.payload := pkt;
            send_seq(dst) := send_seq(dst).next;
            call mq(dst).enqueue(msg);
            call lower.send(me,dst,msg)
        }

Receiving a message is the most complicated. First, we send an ack. Then, if the sequence number is correct, we call the application layer action determined by the message type.

        implement lower.recv(msg:net_msg.t) {
            var src:id;
            var seq:seq_num.t;
            seq := msg.num;
            src := msg.src;
            if seq <= recv_seq(src) & msg.mty ~= ack_t  {
                var ack : net_msg.t;
                ack.mty := ack_t;
                ack.src := me;
                ack.num := seq;
                call lower.send(me,src,ack)
            };
            if msg.mty = ack_t {
                call mq(src).delete_all(seq)
            }
            else if seq = recv_seq(src) {
                recv_seq(src) := seq_num.next(recv_seq(src));
                call recv(me,msg.payload)
            }
        }

If an outgoing channel times out and the queue is not empty, we pick an arbitrary message in the queue and retransmit it.

        implement timer.timeout(dst:id) {
            if ~mq(dst).empty {
                call lower.send(me,dst,mq(dst).pick_one)
            }
        }


    }

}