Examp1 l2s

This is the example of Fig 1 in the paper, using the DL2S technique. Note, the proof can be done in EPR, but the invariant is a bit hard to understand.

include order

instance time : unbounded_sequence

A signal with zero parameters

module signal = {
    action raise

    specification {
        relation now
        after init { now := false; }
        before raise {
            now := true;
            now := false;
        }
        invariant ~now
    }
}

A signal with one parameter

module signal1(data) = {
    action raise(val:data)

    specification {
        relation now
        var value : data
        after init { now := false; }
        before raise {
            value := val;
            now := true;
            now := false;
        }
        invariant ~now
    }
}

An unbounded queue module, with liveness property. Notice this module is an isolate and depends on the theory of the index type 'nat'.

module isolate unbounded_queue with time = {

This action sends a message. Since the queue is unbounded, this action always succeeds.

    action send(x:time)

This action receives a message. It returns a success code 'ok' and a value 'x' if 'ok' is true. If the queue is empty, 'ok is false.

    action recv

    specification {
        var pending(X:time) : bool

        after init {
            pending(X) := false;
        }

        instance sending : signal1(time)
        instance trying : signal
        instance receiving : signal1(time)

        before send {
            require pending(T) -> T < x;
            pending(x) := true;
            sending.raise(x);   # ghost action to signal a send
        }

        before recv {
            trying.raise;      # ghost action signalling polling of queue
            if some (y:time) pending(y) minimizing y {
                pending(y) := false;
                receiving.raise(y);
            }
        }

This is the liveness property of the queue. It says that if messages X is eventually sent and if the queue is polled infinitely often, then message X is eventually received.

        temporal property [lpq]
        (globally eventually trying.now)
        ->
        forall X. globally (sending.now & sending.value = X) ->
                           (eventually receiving.now & receiving.value = X)
        proof {
            tactic skolemize;
            tactic l2s with {
                invariant [inv1] pending(X) -> l2s_d(X)
                invariant [inv2] (l2s_frozen | l2s_saved) & (pending(X) | ($was. pending(X))) & X <= _X -> l2s_a(X)
                invariant [inv3] ($happened. trying.now) -> exists X. X <= _X & ($was. pending(X)) & ~pending(X)
                invariant [inv4] (~l2s_waiting |
                                  ~($l2s_w. ~((sending.now & sending.value = _X) ->
                                              (eventually receiving.now & receiving.value = _X)))) ->
                                    (pending(_X) & globally ~(receiving.now & receiving.value = _X))
                invariant [inv5] (l2s_waiting & ($l2s_w. ~((sending.now & sending.value = _X) ->
                                              (eventually receiving.now & receiving.value = _X)))) ->
                ~(globally (sending.now & sending.value = _X) ->
                (eventually receiving.now & receiving.value = _X))
                invariant [inv6] ~(l2s_waiting & l2s_frozen) & ~(l2s_waiting & l2s_saved) & ~(l2s_frozen & l2s_saved)
                invariant [inv7] globally eventually trying.now
                invariant [inv8] l2s_saved & X <= _X & pending(X) -> ($was. pending(X))
            }
            showgoals
        }
    }
}

instance q : unbounded_queue

export q.send
export q.recv