OpCounter.tla

----------------------------- MODULE OpCounter -----------------------------
EXTENDS Counter, FiniteSets
CONSTANTS Read(_), InitMsg
-----------------------------------------------------------------------------
VARIABLES 
    counter,    \* counter[r]: current value at r \in Replica
    buf,        \* buf[r]: buffer of increments at 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,     \* uset[r]: the set of updates delivered by replica r \in Replica
    uincoming,  \* uincoming[r]: incoming channel for broadcasting/delivering updates at r \in Replica
    buset       \* buset[r]: the buffer of local updates made by r \in Replica since the last broadcast 

nVars == <<incoming, lmsg>>
cVars == <<doset, delset, uincoming, buset>> 
vars == <<counter, buf, seq, nVars, cVars>>   
-----------------------------------------------------------------------------
Msg == [aid : Aid, buf : Nat]
Network == INSTANCE ReliableNetwork \* WITH incoming <- incoming, lmsg <- lmsg                                               

ReadOpCounter(r) == counter[r]   \* read the state of r\in Replica                                                     
Correctness == INSTANCE OpCorrectness \* WITH doset <- doset, delset <- delset, uincoming <- uincoming, buset <- buset                                        
-----------------------------------------------------------------------------
TypeOK == 
    /\ counter \in [Replica -> Nat]
    /\ buf \in [Replica -> Nat]
    /\ IntTypeOK
    /\ Correctness!CTypeOK
-----------------------------------------------------------------------------
Init ==   
    /\ counter = [r \in Replica |-> 0] 
    /\ buf = [r \in Replica |-> 0] 
    /\ IntInit
    /\ Network!RNInit
    /\ Correctness!OpCInit    
-----------------------------------------------------------------------------
Inc(r) ==  \* r\in Replica adds d \in Data
    /\ counter' = [counter EXCEPT ![r] = @ + 1]
    /\ buf' = [buf EXCEPT ![r] = @ + 1]
    /\ IntDo(r)
    /\ Correctness!OpCDo(r)
    /\ UNCHANGED <<nVars>>     
    
Do(r) == Inc(r)\* We ignore ReadOpCounter(r) since it does not modify states.     
-----------------------------------------------------------------------------                                    
Send(r) ==  \* r\in Replica sends a message 
    /\ buf[r] # 0
    /\ buf' = [buf EXCEPT ![r] = 0]
    /\ Network!RNBroadcast(r, [aid |-> [r |-> r, seq |-> seq[r]], buf |-> buf[r]])
    /\ IntSend(r)
    /\ Correctness!OpCSend(r)
    /\ UNCHANGED <<counter>>  
              
Deliver(r) ==  \* r\in Replica delivers a message (lmsg'[r]) 
    /\IntDeliver(r)
    /\Network!RNDeliver(r)
    /\Correctness!OpCDeliver(r, lmsg'[r].aid)
    /\counter' = [counter EXCEPT ![r] = @ + lmsg'[r].buf]
    /\UNCHANGED <<buf>>    
-----------------------------------------------------------------------------
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 20:36:33 CST 2019 by xhdn
\* Last modified Sat Jul 27 16:05:16 CST 2019 by jywellin
\* Created Thu Jul 25 16:38:30 CST 2019 by jywellin