gossa_v2.tla

gossa_v2.tla

--------------------------- MODULE gossa_v2 ---------------------------
(*
To hit the liveness property of stuttering while still not
converged, comment out the actions Die and CorrectlyDetectDeadNode
in the Next state formula.
*)


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
\*****************************************************************

Highest(status1, status2) ==
    IF status1 > status2
    THEN status1 ELSE status2
    
MergePeerState(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        IF node = local_node
        THEN local_ps[node]
        ELSE Highest(local_ps[node], remote_ps[node])]

Gossip ==
    \E source, dest \in Nodes :
        LET gossip_sent      == peer_status[source]
            merged_on_dest   == MergePeerState(
                                    dest, 
                                    peer_status[dest],
                                    gossip_sent)
            gossip_replied   == merged_on_dest
            merged_on_source == MergePeerState(
                                    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    

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

merge

Alive == 1
Dead == 2

Highest(status1, status2) ==
    IF status1 > status2
    THEN status1 ELSE status2
    
MergePeerState(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        IF node = local_node
        THEN local_ps[node]
        ELSE Highest(local_ps[node], remote_ps[node])]

next_cycle_fixed

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