Leader election ring bug

A module for axiomatizing a total order

module total_order(r) = {
    axiom r(X,X)                        # Reflexivity
    axiom r(X, Y) & r(Y, Z) -> r(X, Z)  # Transitivity
    axiom r(X, Y) & r(Y, X) -> X = Y    # Anti-symmetry
    axiom r(X, Y) | r(Y, X)             # Totality
}

Module describing a ring topology.

The module includes a ring_head and ring_tail elements, and a ring total order relation.

The module also includes get_next and get_prev actions.

In this module, the ring topology is arbitrary and fixed.

module ring_topology(carrier) = {
    individual head:carrier  # ring head
    individual tail:carrier  # ring tail
    relation le(X:carrier,Y:carrier)  # total order describing ring topology

Axioms that ensure that le is a total order, with head the minimal element and tail the maximal element.

    instantiate total_order(le)  # total order
    axiom le(head, X)            # head is minimal
    axiom le(X, tail)            # tail is maximal

    action get_next(x:carrier) returns (y:carrier) = {
       assume (x = tail & y = head) | (le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)))
    }

    action get_prev(y:carrier) returns (x:carrier) = {
       assume (x = tail & y = head) | (le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)))
    }

}

Types, relations and functions describing state of the network

type node
type id

A ring topology of nodes

instantiate ring : ring_topology(node)

A total order on ids

relation le(X:id, Y:id)
instantiate total_order(le)

A function relating a node to its id

individual idn(X:node) : id

BUG - the fact that idn is injective is commented out: axiom idn(X)=idn(Y) -> X=Y # the idn function is injective

A relation that keeps track of nodes that think they are the leader

relation leader(N:node)
init ~leader(N)

A relation for pending messages, a message is just an id

relation pending(V:id, N:node) # The identity V is pending at node N
init ~pending(V, N)

Protocol description

Two action: send and receive

action send = {
    local n1:node, n2:node {

send my own id to the next node

        n2 := ring.get_next(n1);
        pending(idn(n1), n2) := true
    }
}

action receive = {
    local n1:node, n2:node, m:id {

receive a message from the right neighbor

        assume pending(m, n1);
        pending(m, n1) := *; # abstract the number of pending messages
        if m = idn(n1) {  # Found a leader
            leader(n1) := true
        } else {
            if le(idn(n1), m) { # pass message to next node
                n2 := ring.get_next(n1);
                pending(m, n2) := true
            } # otherwise drop the message...
        }
    }
}

export send
export receive

The safety property:

conjecture leader(X) & leader(Y) -> X = Y  # at most one leader