Trivnet

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 {
    implement intf.send {
    call intf.recv(x)
    }
}

import intf.recv
export intf.send