Ping application

include ping_byte_stream

action app_send_event(src:ip.endpoint, dst:ip.endpoint, data : stream_data, pos : stream_pos, close : bool)

function ping_data : stream_data
function ping_packet_end : stream_pos
function ping_pos : stream_pos
function ping_packet_finished : bool

after init {
    ping_pos := 0;
    ping_packet_finished := false;
}

after app_send_event {
    var send_end := pos + data.end;
    require ~(send_end > ping_packet_end & ping_packet_finished);  # [4]
    var end := ping_data.end;
    if end < send_end {
        end := send_end
    };
    ping_data := ping_data.resize(end,0);  # [1]
    var idx := data.begin;
    while idx < data.end {
        var val := ping_data.value(pos + idx);

TODO: using zero as a "null" value is not correct here. We need a data structure to capture the known intervals!

        require val ~= 0 ->  data.value(idx) = val;  # [2]
        ping_data := ping_data.set(pos+idx,data.value(idx));
        idx := idx.next
    };
    ping_packet_end := end;  # [1]
    if close {
        ping_packet_finished := true;  # [3]
    }
}