Trivnet2

type packet

object intf = {
    action send(x:packet)
    action recv(x:packet)
}

specification {
    relation sent(X:packet)
    after init {
        sent(X) := false
    }

    before intf.send {
    sent(x) := true
    }

    before intf.recv {
    require sent(x)
    }
}

implementation {

    individual full : bool
    individual contents : packet

    after init {
        full := false;
    }

    implement intf.send {
    full := true;
    contents := x
    }

    action async = {
    if full {
        full := false;
        call intf.recv(contents)
    }
    }
}

import intf.recv
export intf.send
export async

interpret packet -> bv[16]