A TLA+ Model of Plumtree (http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=4365705) showing it is not tolerant to a network which can drop messages

ClusterMetaSimple.tla

------------------------- MODULE ClusterMetaSimple -------------------------
EXTENDS Integers, Sequences, TLC

(***************************************************************************
Global States
 ***************************************************************************)
\* Set of nodes in the cluster
CONSTANT Nodes

\* The node that will be the only sender
CONSTANT Root

\* Broadasts to be performed
CONSTANT Broadcasts

\* Broadcasts performed
VARIABLE performedBroadcasts

\* Types of Messages in the System
CONSTANT BroadcastMessageType, PruneMessageType,
         IHaveMessageType, GraftMessageType

\* Set of in-flight messages (messages sent by a node but not yet received)
\* TODO: this doesn't allow for duplicating messages (like Raft proof) since
\*       it is a set
VARIABLE messages

(***************************************************************************
 per-node state
 ***************************************************************************)
\* Initial Eagers & Lazys for each node
CONSTANT InitEagers, InitLazys

\* Sets of Eager and Lazy peers
VARIABLE eagerPeers, lazyPeers

\* Received Broadcasts
VARIABLE received

(***************************************************************************
Message Builders
 ***************************************************************************)
BroadcastMessage(s,d,id,round) == [type   |-> BroadcastMessageType,
                                   source |-> s,
                                   dest   |-> d,
                                   bid    |-> id,
                                   round  |-> round]
                                   
PruneMessage(broadcast)== [type   |-> PruneMessageType,
                           \* responding to broadcast so switch sender/dest
                           source |-> broadcast.dest,
                           dest   |-> broadcast.source]
                           
\* An IHave looks the same as a Broadcast in this model because BroadcastMessage
\* does not include a payload. However, they are semantically different
IHaveMessage(s,d,id,round) == [type   |-> IHaveMessageType,
                               source |-> s,
                               dest   |-> d,
                               bid    |-> id,
                               round  |-> round]
                             
GraftMessage(ihave) == [type   |-> GraftMessageType,
                        \* responding to ihave so switch sender/dest
                        source |-> ihave.dest,
                        dest   |-> ihave.source,
                        bid    |-> ihave.bid,
                        round  |-> ihave.round]

(***************************************************************************
Helpers
 ***************************************************************************)
OutstandingBroadcasts == Broadcasts \ performedBroadcasts

SendAll(m) == messages' = UNION {messages,m}
WithSent(m) == UNION {messages, m}

Discard(m) == messages' = messages \ {m}
WithRemoved(m) == messages \ m
    
\* Builder for eager and lazy messages (broadcasts and ihaves)
PeerMessages(bid, receivedfrom, sender, round, peers, MessageBuilder(_, _, _, _)) ==
    LET dests == { d \in peers[sender] : ~(d = receivedfrom) }
    IN { MessageBuilder(sender, d, bid, round) : d \in dests }
    
Received(bid, node) == received' = [received EXCEPT ![node] = UNION {@, {bid}}]

AddEager(node, eager) == /\ eagerPeers' = [eagerPeers EXCEPT ![node]=UNION {@, {eager}}]
                         /\ lazyPeers'  = [lazyPeers  EXCEPT ![node]= @ \ {eager}]
                         
AddLazy(node, lazy) == /\ lazyPeers'  = [lazyPeers  EXCEPT ![node] = UNION {@, {lazy}}]
                       /\ eagerPeers' = [eagerPeers EXCEPT ![node] = @ \ {lazy}]

(***************************************************************************
Message Handlers
 ***************************************************************************)
HandleBroadcastMessage(m) == \/ /\ m.bid \notin received[m.dest]
                                /\ Received(m.bid, m.dest)
                                \* use m.dest because we are sending this from the node
                                \* that received the message
                                /\ messages' = 
                                    UNION { messages, 
                                            PeerMessages(m.bid, m.source, m.dest, m.round+1, eagerPeers, BroadcastMessage),
                                            PeerMessages(m.bid, m.source, m.dest, m.round+1, lazyPeers, IHaveMessage)
                                           } \ {m}
                                \* add source to destinations eager set
                                /\ AddEager(m.dest, m.source)
                             \/ /\ m.bid \in received[m.dest]
                                \* add source to destinations lazy set and prune
                                /\ AddLazy(m.dest, m.source)
                                /\ messages' = UNION { messages, {PruneMessage(m)} } \ {m}
                                /\ UNCHANGED <<received>>
                                
HandleIHaveMessage(m) == \/ /\ m.bid \notin received[m.dest]
                            \* send graft message for broadcast we haven't received
                            \* TODO: don't send graft message immediately, put ihave in missing set, use timer
                            /\ messages' = UNION { messages \ {m}, { GraftMessage(m) } }
                            \* add source to destinations eager set
                            /\ AddEager(m.dest, m.source)
                         \/ /\ m.bid \in received[m.dest]
                            /\ messages' = messages \ {m}
                            /\ UNCHANGED <<eagerPeers, lazyPeers>>
                         /\ UNCHANGED <<received>>

HandlePruneMessage(m) == /\ messages' = messages \ {m}
                         \* move source of message to dest's lazy set
                         /\ AddLazy(m.dest, m.source)
                         /\ UNCHANGED <<received>>
                         
HandleGraftMessage(m) == /\ AddEager(m.dest, m.source)
                         \* send broadcast back to grafter
                         /\ messages' = UNION { messages \ {m},
                                                 { BroadcastMessage(m.dest,m.source,m.bid,m.round) } }
                         /\ UNCHANGED received
                                                 
(***************************************************************************
Initial State
 ***************************************************************************)
InitNodeState == /\ eagerPeers = [i \in Nodes |-> InitEagers[i]]
                 /\ lazyPeers = [i \in Nodes |-> InitLazys[i]]
                 /\ received = [i \in Nodes |-> {}]
                 
Init == /\ performedBroadcasts = {}
        /\ messages = {}
        /\ InitNodeState

(***************************************************************************
Transitions
 ***************************************************************************)
DropMessage == /\ \E m \in messages : messages' = messages \ {m}
               /\ UNCHANGED <<received, eagerPeers, lazyPeers, performedBroadcasts>>
 
\* Begin a broadcast from the root of the tree
Broadcast(bid) == /\ performedBroadcasts' = UNION {performedBroadcasts, {bid}}
                  /\ Received(bid, Root)
                  /\ messages' = UNION {messages, 
                                        PeerMessages(bid, Root, Root, 0, eagerPeers, BroadcastMessage),
                                        PeerMessages(bid, Root, Root, 0, lazyPeers, IHaveMessage)}
                  /\ UNCHANGED <<eagerPeers, lazyPeers>>

\* Receive a message
Receive == \E m \in messages : 
                \/ m.type = BroadcastMessageType /\ HandleBroadcastMessage(m)
                \/ m.type = PruneMessageType /\ HandlePruneMessage(m)
                \/ m.type = IHaveMessageType /\ HandleIHaveMessage(m)
                \/ m.type = GraftMessageType /\ HandleGraftMessage(m)
                /\ UNCHANGED <<performedBroadcasts>>

Next == \/ \E m \in OutstandingBroadcasts : Broadcast(m)
        \/ Receive
        \/ DropMessage

(***************************************************************************
Invariants
 ***************************************************************************)
\* TODO: "type invariants"

ValidPeers == \A n \in Nodes : /\ \A e \in eagerPeers[n] : e \notin lazyPeers[n]
                               /\ n \notin eagerPeers[n]
                               /\ n \notin lazyPeers[n]

\* When there are no more messages in the network and no more broadcasts
\* the system should be consistent                              
EventuallyConsistent == messages = {} /\ performedBroadcasts = Broadcasts => 
                            \A b \in Broadcasts : \A n \in Nodes : b \in received[n]
=============================================================================
\* Modification History
\* Last modified Mon Jul 08 22:17:01 PDT 2013 by jordan
\* Created Sun Jul 07 18:06:19 PDT 2013 by jordan