Testing

include tcp

type data

module replica = {
    individual value : data
    after init {
    value := 0;
    }
    action upd(inp : data) returns (out : data) = {
    out := value;
    value := value + inp;
    }
}

module reference = {
    ghost type txid
    instance rep : replica

    action create(inp : data) returns (tx : txid)
    action commit(tx : txid)
    action eval(tx : txid) returns (res : data)

    individual next : txid
    function txs(X:txid) : data
    function txres(X:txid) : data
    relation committed(X:txid)

    after init {
    next := 0;
    committed(X) := false;
    }

    implement create {
    tx := next;
    txs(tx) := inp;
    next := next + 1;
    }

    implement commit {
    assert 0 <= tx & tx < next;
    assert ~committed(tx);
    txres(tx) := rep.upd(txs(tx));
    committed(tx) := true;
    }
    delegate commit

    implement eval {
    assert committed(tx);
    res := txres(tx);
    }
    delegate eval

    interpret txid -> int
}

instance ref : reference

type msg = struct {
    val : data,
    tx : ref.txid
}

module client(req_chan,rsp_chan) = {

action request_upd(val : data) = {
call req_chan.sender.send(val);
}

action response_upd(val : data)

implement rsp_chan.receiver.recv(val : data) {
call response_upd(val : data)
}

}

module client(out_chan) = {

    action request_upd(val : data) returns (tx : ref.txid)

    implement request_upd {
    local m : msg {
        m.val := val;
        m.tx := tx;
        call out_chan.send(m);
    }
    }
}

module head_node(req_chan1, req_chan2, out_chan) = {
    instance rep : replica

    action upd(inp : msg) = {
    call ref.commit(inp.tx);           # this is ghost!
    var res := rep.upd(inp.val);  # ignore the result
    call out_chan.send(inp);
    }

    implement req_chan1.recv(inp : msg) {
    call upd(inp);
    }
    implement req_chan2.recv(inp : msg) {
    call upd(inp);
    }
}

module tail_node(inp_chan, out_chan) = {
    instance rep : replica

    action upd(inp : msg) = {
    local out : msg {
        out.val := rep.upd(inp.val);
        out.tx := inp.tx;
        call out_chan.send(out);
    }
    }

    implement inp_chan.recv(inp : msg) {
    call upd(inp);
    }
}


instance clrq1 : tcp_channel("localhost:44090",msg)
instance clrq2 : tcp_channel("localhost:44091",msg)
instance headtail : tcp_channel("localhost:44092",msg)
instance sysout : tcp_channel("localhost:44093",msg)

instance cl1 : client(clrq1.sndr)
instance cl2 : client(clrq2.sndr)
instance head : head_node(clrq1.rcvr,clrq2.rcvr,headtail.sndr)
instance tail : tail_node(headtail.rcvr,sysout.sndr)


object inspec = {
    before cl1.request_upd(inp : data) returns (tx:ref.txid) {
    tx := ref.create(inp);
    }
    before cl2.request_upd(inp : data) returns (tx:ref.txid) {
    tx := ref.create(inp);
    }
}

object outspec = {
    before sysout.sndr.send(m : msg) {
    assert m.val = ref.eval(m.tx);
    }
}

object htspec = {
    instance queue : unbounded_queue(ref.txid)

    after ref.commit(tx:ref.txid) {
    call queue.push(tx);
    }

    before headtail.sndr.send(m : msg) {
    assert m.val = ref.txs(m.tx);
    assert m.tx = queue.pop;
    }
}

export cl1.request_upd
export cl2.request_upd
import sysout.rcvr.recv

isolate iso_head = head with cl1,cl2,clrq1,clrq2,ref,inspec,htspec
trusted isolate iso_tail = tail with headtail,ref,htspec,outspec

interpret data -> bv[16]