spanning.tla

------------------------------ MODULE spanning ------------------------------
EXTENDS Integers
CONSTANTS Proc, NoPrnt, root, nbrs
ASSUME NoPrnt \notin Proc /\ nbrs \subseteq Proc \times Proc
VARIABLES prnt, rpt, msg
vars == <<prnt, rpt, msg>> 
             
Init == /\ prnt = [i \in Proc |-> NoPrnt]
        /\ rpt = [i \in Proc |-> FALSE]
        /\ msg = {}

CanSend(i, j) ==  (<<i, j>> \in nbrs) /\ (i = root \/ prnt[i] # NoPrnt)

Update(i, j) == /\ prnt' = [prnt EXCEPT ![i] = j]
                /\ UNCHANGED <<rpt, msg>>
    
Send(i) == \E k \in Proc: /\ CanSend(i, k) /\ (<<i, k>> \notin msg)
                          /\ msg' = msg \cup {<<i, k>>}
                          /\ UNCHANGED <<prnt, rpt>>
                                                                                    
Parent(i) == /\ prnt[i] # NoPrnt /\ ~rpt[i]
             /\ rpt' = [rpt EXCEPT ![i] = TRUE] 
             /\ UNCHANGED <<msg, prnt>>
             
Next == \E i, j \in Proc: IF i # root /\ prnt[i] = NoPrnt /\ <<j, i>> \in msg
                          THEN Update(i, j)
                          ELSE \/ Send(i) \/ Parent(i) 
                               \/ UNCHANGED <<prnt, msg, rpt>>                   
                                                        
Spec == /\ Init /\ [][Next]_vars 
        /\ WF_vars(\E i, j \in Proc: IF i # root /\ prnt[i] = NoPrnt /\ <<j, i>> \in msg
                                     THEN Update(i, j)
                                     ELSE \/ Send(i) \/ Parent(i) 
                                          \/ UNCHANGED <<prnt, msg, rpt>>)
                                           
TypeOK == /\ \A i \in Proc : prnt[i] = NoPrnt \/ <<i, prnt[i]>> \in nbrs             
          /\ rpt \in [Proc -> BOOLEAN]  
          /\ msg \subseteq Proc \times Proc
  
Termination == <>(\A i \in Proc : i = root \/ (prnt[i] # NoPrnt /\ <<i, prnt[i]>> \in nbrs)) 

OneParent == [][\A i \in Proc : prnt[i] # NoPrnt => prnt[i] = prnt'[i]]_vars

SntMsg == \A i \in Proc: (i # root /\ prnt[i] = NoPrnt => \A j \in Proc: <<i ,j>> \notin msg)

=============================================================================
\* Modification History
\* Last modified Mon Jul 09 13:30:26 CEST 2018 by tthai