Trans buggy

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.

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

    init recv_seq(S) = 0 & send_seq(S) = 0

Implementations of interface actions

    implement send(dst:id,pkt:packet) {
        local msg : net_msg.t, seq : seq_num.t {
        net_msg.mty(msg) := msg_t;
        net_msg.src(msg) := me;
        net_msg.num(msg) := send_seq(dst);
        net_msg.payload(msg) := pkt;
        send_seq(dst) := seq_num.next(send_seq(dst));
        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) {
        local src:id,seq:seq_num.t {
        seq := net_msg.num(msg);
        src := net_msg.src(msg);
        if seq <= recv_seq(src) & net_msg.mty(msg) ~= ack_t  {
            local ack : net_msg.t {
            net_msg.mty(ack) := ack_t;
            net_msg.src(ack) := me;
            net_msg.num(ack) := seq;
            call lower.send(me,src,ack)
            }
        };
        if net_msg.mty(msg) = 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,net_msg.payload(msg))
        }
        }
    }

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)
        }
    }


    }

}