Leader election ring btw

A module containing the axioms of total order

module total_order_properties(t) = {
    property [transitivity] X:t < Y & Y < Z -> X < Z
    property [antisymmetry] ~(X:t < Y & Y < X)
    property [totality] X:t < Y | X = Y | Y < X
}

ADT describing a totally ordered datatype

isolate id = {
    type this
    specification {
        instantiate total_order_properties(this)
    }

    implementation {
        interpret this -> bv[64]
    }
}

ADT describing a ring topology.

Nodes are totally ordered and provide a get_next action that gets the next element of the ring in round-robin order.

isolate node = {
    type this
    action get_next(x:this) returns (y:this)
    function pid(X:node) : id          # map each node to an id

    axiom [injectivity] pid(X) = pid(Y) -> X = Y

    specification {

        relation btw(X:this,Y:this,Z:this)

        property btw(W, Y, Z) & btw(W, X, Y) -> btw(X, Y, Z)
        property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, X, Y)
        property btw(W, X, Z) & btw(X, Y, Z) -> btw(W, Y, Z)
        property btw(W, Y, Z) & btw(W, X, Y) -> btw(W, X, Z)
        property W = X | btw(W, X, W)
        property ~btw(X, X, Y)
        property ~btw(X, Y, Y)
        property btw(X,Y,Z) |  Y = Z |  btw(X,Z,Y)
        property btw(X,Y,Z) |  Y = X |  btw(Y,X,Z)

        after get_next {
            assert ~btw(x,Z,y)
        }
    }

    implementation {
        definition btw(X,Y,Z) = (X < Y & Y < Z) | (X < Y & Z <= X) | (Y < Z & Z <= X)
        interpret this -> bv[8]
        implement get_next {
            y := x + 1;
        }
    }
}

The transport-layer service specification

isolate trans = {

    action send(src:node, dst:node, v:id)
    action recv(dst:node, v:id)

    specification {
        relation sent(V:id, N:node) # The identity V is sent at node N

        after init {
            sent(V, N) := false;
        }

    before send {
        sent(v,dst) := true
    }

    before recv {
        require sent(v,dst)
    }
    }
}

The high-level service specification

isolate app = {

    action tick(me:node)                 # called when a timer expires
    action elect(me:node)                 # called when v is elected leader

    specification {
    before elect {
        ensure me.pid >= node.pid(X)    # only the max pid can be elected
    }
    }

    implementation {
        implement tick(me:node) {
        call trans.send(me,me.get_next,me.pid);
        }

        implement trans.recv(me:node,v:id) {
            if v = me.pid {  # Found a leader
                call elect(me);
            }
        else if v > me.pid  { # pass message to next node
            call trans.send(me,me.get_next,v);
            }
        }
    }

    private {

invariant ~(node.pid(P) < node.pid(N) & trans.sent(node.pid(P),P)) invariant ~(node.pid(Q) < node.pid(P) & node.pid(P) < node.pid(N) & trans.sent(node.pid(P),Q) & node.btw(Q,P,N))

    }

} with node, id, trans

import app.elect
export app.tick
import trans.send
export trans.recv