StateAWSet.tla

----------------------------- MODULE StateAWSet -----------------------------
EXTENDS AWSet, FiniteSets
CONSTANTS Read(_), InitMsg
-----------------------------------------------------------------------------
VARIABLES
    aset,      \* aset[r]: the set of active elements maintained by r \in Replica
    tset,      \* tset[r]: the set of tombstone elements maintained by r \in Replica 
    (* variables for network: *) 
    incoming,  \* incoming[r]: incoming channel at replica r \in Replica
    lmsg,      \* lmsg[r]: the last message delivered at r \in Replica to the upper-layer protocol 
    (* variables for correctness: *) 
    doset,      \* doset[r]: the set of updates generated by replica r \in Replica
    delset,     \* delset[r]: the set of updates delivered by replica r \in Replica
    uincoming   \* uincoming[r]: incoming channel for broadcasting/delivering updates at r \in Replica
    
nVars  == <<incoming, lmsg>>
cVars == <<doset, delset, uincoming>> 
vars == <<aset, tset, seq, nVars, cVars>>
-----------------------------------------------------------------------------  
Msg == [aid : Aid, A: SUBSET Element, T : SUBSET Element]  
Network == INSTANCE BasicNetwork  \* WITH incoming <- incoming, lmsg <- lmsg                                   

ReadStateAWSet(r) == {ele.d: ele \in aset[r]}  \* read the state of r\in Replica
Correctness == INSTANCE StateCorrectness  
                \* WITH doset <- doset, delset <- delset, uincoming <- uincoming                                         
-----------------------------------------------------------------------------    
TypeOK ==
    /\aset \in [Replica -> SUBSET Element]
    /\tset \in [Replica -> SUBSET Element]
    /\IntTypeOK
    /\Correctness!CTypeOK
-----------------------------------------------------------------------------
Init == 
    /\ aset = [r \in Replica |-> {}]
    /\ tset = [r \in Replica |-> {}]   
    /\ IntInit  
    /\ Network!BNInit
    /\ Correctness!StateCInit
-----------------------------------------------------------------------------              
Add(d, r) ==  \* r\in Replica adds d \in Data
    /\ aset'= [aset EXCEPT ![r] = @ \union {[aid |-> [r |-> r, seq |-> seq[r]], d |-> d]}]
    /\ IntDo(r)
    /\ Correctness!StateCDo(r)
    /\ UNCHANGED <<tset, nVars>>
    
Remove(d, r) ==  \* r\in Replica removes d \in Data 
    /\ LET E == {ele \in aset[r] : ele.d = d}  \* E may be empty
       IN  /\ aset' = [aset EXCEPT ![r] = @ \ E]
           /\ tset' = [tset EXCEPT ![r] = @ \cup E] 
    /\ IntDo(r)
    /\ Correctness!StateCDo(r) 
    /\ UNCHANGED <<nVars>>
                      
Do(r) ==  \* We ignore ReadStateAWSet(r) since it does not modify states.
    \E a \in Data: Add(a, r) \/ Remove(a, r)         
-----------------------------------------------------------------------------
Send(r) ==  \* r\in Replica sends a message 
    /\ Network!BNBroadcast(r, [aid |-> [r |-> r, seq |-> seq[r]],  
                                 A |-> aset[r], T |-> tset[r]])  
    /\ IntSend(r)
    /\ Correctness!StateCSend(r) 
    /\ UNCHANGED <<aset, tset>>
           
Deliver(r) ==  \* r\in Replica delivers a message (lmsg'[r]) 
    /\ IntDeliver(r)
    /\ Network!BNDeliver(r)
    /\ Correctness!StateCDeliver(r, lmsg'[r].aid)
    /\ tset' = [tset EXCEPT ![r] = @ \cup lmsg'[r].T]
    /\ aset' = [aset EXCEPT ![r] = (@ \cup lmsg'[r].A) \ tset'[r]]           
    /\ UNCHANGED <<>> 
-----------------------------------------------------------------------------
Next == \E r \in Replica: Do(r) \/ Send(r) \/ Deliver(r) 

Fairness == \A r \in Replica: WF_vars(Send(r)) /\ WF_vars(Deliver(r))

Spec == Init /\ [][Next]_vars /\ Fairness
=============================================================================
\* Modification History
\* Last modified Sat Aug 31 16:08:31 CST 2019 by xhdn
\* Created Fri May 24 14:13:38 CST 2019 by xhdn