Gossa V1

constants

CONSTANTS NodeCount
VARIABLES running,
          peer_status
Nodes == 1..NodeCount

converged

Converged ==
    ~\E local, remote \in Nodes :
       /\ running[local] = TRUE 
       /\ \/ /\ peer_status[local][remote] = Dead 
             /\ running[remote] = TRUE
          \/ /\ peer_status[local][remote] = Alive 
             /\ running[remote] = FALSE

detect_dead

CorrectlyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = FALSE
        /\ peer_status[local][remote] = Alive
        /\ peer_status' = [peer_status EXCEPT ![local][remote] = Dead]
        /\ UNCHANGED running

die

Die ==
    \E node \in Nodes :
        /\ running[node] = TRUE
        /\ running' = [running EXCEPT ![node] = FALSE]
        /\ UNCHANGED peer_status

gossa_v1.tla

--------------------------- MODULE gossa_v1 ---------------------------

EXTENDS Naturals

CONSTANTS NodeCount
VARIABLES running,
          peer_status

vars == <<running, peer_status>>

Nodes == 1..NodeCount

\* Node peer states
Alive == 1
Dead == 2
          
Init ==
    /\ running     = [node \in Nodes |-> TRUE]
    /\ peer_status = [node1 \in Nodes |->
                        [node2 \in Nodes |-> Alive]]

\*****************************************************************
\* ACTIONS
\*****************************************************************

MergePeerStateBlindly(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        IF node = local_node
        THEN local_ps[node]
        ELSE remote_ps[node]]

Gossip ==
    \E source, dest \in Nodes :
        LET gossip_sent      == peer_status[source]
            merged_on_dest   == MergePeerStateBlindly(
                                    dest, 
                                    peer_status[dest],
                                    gossip_sent)
            gossip_replied   == merged_on_dest
            merged_on_source == MergePeerStateBlindly(
                                    source,
                                    peer_status[source],
                                    gossip_replied)
        IN
            /\ running[source] = TRUE
            /\ running[dest] = TRUE
            /\ gossip_sent # peer_status[dest]
            /\ peer_status' = [peer_status EXCEPT 
                                    ![dest]   = merged_on_dest,
                                    ![source] = merged_on_source]
            /\ UNCHANGED running

Die ==
    \E node \in Nodes :
        /\ running[node] = TRUE
        /\ running' = [running EXCEPT ![node] = FALSE]
        /\ UNCHANGED peer_status
        
Start ==
    \E node \in Nodes :
        /\ running[node] = FALSE
        /\ running' = [running EXCEPT ![node] = TRUE]
        /\ UNCHANGED peer_status

CorrectlyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = FALSE
        /\ peer_status[local][remote] = Alive
        /\ peer_status' = [peer_status EXCEPT ![local][remote] = Dead]
        /\ UNCHANGED running
        
FalselyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = TRUE
        /\ peer_status[local][remote] = Alive
        /\ peer_status' = [peer_status EXCEPT ![local][remote] = Dead]
        /\ UNCHANGED running        

Next ==
    \/ Gossip
    \/ Die
    \/ CorrectlyDetectDeadNode
    \/ FalselyDetectDeadNode
    \/ Start

\* SAFETY PROPERTIES ------------        
TypeOK ==
    /\ running \in [Nodes -> BOOLEAN]
    /\ peer_status \in [Nodes ->
                           [Nodes -> {Alive, Dead}]]

\* LIVENESS PROPERTIES ------------        
Converged ==
    ~\E local, remote \in Nodes :
       /\ running[local] = TRUE 
       /\ \/ /\ peer_status[local][remote] = Dead 
             /\ running[remote] = TRUE
          \/ /\ peer_status[local][remote] = Alive 
             /\ running[remote] = FALSE
    
EventuallyConverges ==
    ~Converged ~> Converged
    
Liveness ==
    WF_vars(\/ Gossip
            \/ CorrectlyDetectDeadNode)

\* Temporal formula    
Spec == Init /\ [][Next]_vars
LivenessSpec == Init /\ [][Next]_vars /\ Liveness    

=============================================================================

gossip

Gossip ==
    \E source, dest \in Nodes :
        LET gossip_sent      == peer_status[source]
            merged_on_dest   == MergePeerStateBlindly(
                                    dest, 
                                    peer_status[dest],
                                    gossip_sent)
            gossip_replied   == merged_on_dest
            merged_on_source == MergePeerStateBlindly(
                                    source,
                                    peer_status[source],
                                    gossip_replied)
        IN
            /\ running[source] = TRUE
            /\ running[dest] = TRUE
            /\ gossip_sent /= peer_status[dest]
            /\ peer_status' = [peer_status EXCEPT 
                                    ![dest]   = merged_on_dest,
                                    ![source] = merged_on_source]
            /\ UNCHANGED running

init

\* Node peer states
Alive == 1
Dead == 2
          
Init ==
    /\ running     = [node \in Nodes |-> TRUE]
    /\ peer_status = [node1 \in Nodes |->
                        [node2 \in Nodes |-> Alive]]

liveness

Liveness ==
    WF_vars(\/ Gossip
            \/ CorrectlyDetectDeadNode)
            

merge_blindly

MergePeerStateBlindly(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        IF node = local_node
        THEN local_ps[node]
        ELSE remote_ps[node]]

next

Next ==
    \/ Gossip
    \/ Die
    \/ Start
    \/ CorrectlyDetectDeadNode
    \/ FalselyDetectDeadNode

start

Start ==
    \E node \in Nodes :
        /\ running[node] = FALSE
        /\ running' = [running EXCEPT ![node] = TRUE]
        /\ UNCHANGED peer_status

type_ok

TypeOK ==
    /\ running \in [Nodes -> BOOLEAN]
    /\ peer_status \in [Nodes ->
                           [Nodes -> {Alive, Dead}]]