Merge branch 'master' of https://github.com/hengxin/tlaplus-lamport-p…

…rojects

tlaplus-projects/Zhifu-Wang/Wang-crdt-tla/StateCounter.tla

@@ -0,0 +1,144 @@
+---------------------------- MODULE StateCounter ----------------------------
+
+(**********************************************************************)
+(* TLA+ module for State-based Counter.                               *)
+(* See its implementation in paper Burckhardt@POPL'2014.              *)
+(* We check that the State-based Counter satisfies the                *)
+(* strong eventual convergence property (SEC)                         *)
+(**********************************************************************)
+
+EXTENDS Naturals, Sequences, Bags, TLC
+
+CONSTANTS 
+    (**********************************************************************)
+    (* Protocol variables.                                                *)
+    (**********************************************************************)
+    Replica,        \* the set of replicas
+    (**********************************************************************)
+    (* Auxiliary variables for model checking.                            *)
+    (**********************************************************************)
+    Max             \* Max[r]: the maximum number of the Inc() event replica r \in Replica can issue; 
+                    \* for finite-state model checking
+
+VARIABLES 
+    (**********************************************************************)
+    (* Protocol variables.                                                *)
+    (**********************************************************************)
+    vc,             \* vc[r][r]: the current value of the counter vector at replica r \in Replica
+    incoming,       \* incoming[r]: incoming messages at replica r \in Replica
+    (**********************************************************************)
+    (* Auxiliary variables for model checking.                            *)
+    (**********************************************************************)
+    inc,            \* inc[r]: the number of Inc() events issued by the replica r \in Replica
+    sendAllowed     \* sendAllowed[r]: is the replica r \in Replica allowed to send a message
+
+(**********************************************************************)
+(* The type correctness predicate.                                    *)
+(**********************************************************************)
+TypeOK == /\ vc \in [Replica -> [Replica -> Nat]]
+          /\ inc \in [Replica -> Nat]
+          /\ sendAllowed \in [Replica -> {0,1}]
+          \* /\ incoming \in [Replica -> SubBag(SetToBag(Nat))] \* message ordering is not important; using bag (i.e., multiset)
+
+-----------------------------------------------------------------------------
+(**********************************************************************)
+(* The initial state predicate.                                       *)
+(**********************************************************************)
+
+Init == /\ vc = [r \in Replica |-> [s \in Replica |-> 0]]
+        /\ incoming = [r \in Replica |-> EmptyBag]
+        /\ inc = [r \in Replica |-> 0]
+        /\ sendAllowed = [r \in Replica |-> 0]
+
+-----------------------------------------------------------------------------
+(**********************************************************************)
+(* Replica r \in Replica issues an Read() event.                      *)
+(**********************************************************************)
+
+(**********************************************************************)
+(* Replica r \in Replica issues an Inc() event.                       *)
+(**********************************************************************)
+Inc(r) == /\ inc[r] < Max[r]                   
+          \* each replica r \in Replica can issue at most Max[r] Inc() events.
+          /\ vc' = [vc EXCEPT ![r][r] = @ + 1] \* current counter + 1
+          /\ inc' = [inc EXCEPT ![r] = @ + 1]
+          /\ sendAllowed' = [sendAllowed EXCEPT ![r] = 1]
+          /\ UNCHANGED <<incoming>>
+
+(**********************************************************************)
+(* Broadcast a message m to all replicas except the sender s.         *)
+(**********************************************************************)
+Broadcast(s, m) == [r \in Replica |-> 
+                        IF s = r 
+                        THEN incoming[s] 
+                        ELSE incoming[r] (+) SetToBag({m})]
+
+(**********************************************************************)
+(* Replica r issues a Send() event, sending an update message.        *)
+(**********************************************************************)
+Send(r) == /\ sendAllowed[r] = 1
+           /\ incoming' = Broadcast(r, vc[r])  \* broadcast vc[r] to other replicas
+           /\ sendAllowed' = [sendAllowed EXCEPT ![r] = 0]
+           /\ UNCHANGED <<vc, inc>>
+
+(**********************************************************************)
+(* Replica r issues a Receive() event, receiving an update message.   *)
+(**********************************************************************)
+SetMax(r, s) == IF r > s THEN r ELSE s
+
+Receive(r) == /\ incoming[r] # EmptyBag \* there are accumulated increments from other replicas
+              /\ \E m \in BagToSet(incoming[r]): \* message reordering can be tolerant
+                    (/\ \A s \in Replica: vc' = [vc EXCEPT ![r][s] = SetMax(@, m[s])]
+                     /\ incoming' = [incoming EXCEPT ![r] = @ (-) SetToBag({m})])  \* each message is delivered exactly once
+              /\ sendAllowed' = [sendAllowed EXCEPT ![r] = 1]
+              /\ UNCHANGED <<inc>>
+-----------------------------------------------------------------------------
+(**********************************************************************)
+(* The Next-state relation.                                           *)
+(**********************************************************************)
+Next == /\ \E r \in Replica: Inc(r) \/ Send(r) \/ Receive(r)
+
+(**********************************************************************)
+(* The specification.                                                 *)
+(**********************************************************************)
+vars == <<vc, incoming, inc, sendAllowed>>
+Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
+
+-----------------------------------------------------------------------------
+
+(**********************************************************************)
+(* The correctness of counter:                                        *)
+(* Eventual Convergence (EC), Quiescent Consistency (QC),             *)
+(* and Strong Eventual Convergence (SEC).                             *)
+(**********************************************************************)
+
+-----------------------------------------------------------------------------
+(**********************************************************************)
+(* Eventual Consistency (EC)                                          *)
+(* If clients stop issuing Incs,                                      *)
+(* then the counters at all replicas will be eventually the same.     *)
+(**********************************************************************)
+Convergence == /\ \A r, s \in Replica: vc[r] = vc[s]
+               /\ \E r, s \in Replica: vc[r][s] # 0 \* excluding the initial state
+EC == <>Convergence
+
+(**********************************************************************)
+(* Quiescent Consistency (QC)                                         *)
+(* If the system is at quiescent,                                     *)
+(* then the counters at all replicas must be the same.                *)
+(**********************************************************************)
+
+AccBroadcast == \A r \in Replica: sendAllowed[r] = 0 \* all r \in Replica are not allowed to send
+MessageDelivery == \A r \in Replica: incoming[r] = EmptyBag \* all messages have been delivered
+QConvergence == \A r, s \in Replica: vc[r] = vc[s] \* no counter[r] # 0
+
+QC == [](AccBroadcast /\ MessageDelivery => QConvergence)
+
+(**********************************************************************)
+(* Strong Eventual Consistency (SEC)                                  *)
+(**********************************************************************)
+
+=============================================================================
+\* Modification History
+\* Last modified Sat Aug 11 11:49:53 CST 2018 by zfwang
+\* Created Fri Aug 03 09:57:12 CST 2018 by zfwang

tlaplus-seminar/11-20180608-OpCounter-Wei/Counter.tla

@@ -127,7 +127,7 @@ QConvergence == \A r, s \in Replica: counter[r] = counter[s] \* no counter[r] #
 QC == []((AccBroadcast /\ MessageDelivery) => QConvergence)
 
 (**********************************************************************)
-(* Strong Eventual Consistency (SEC)                                         *)
+(* Strong Eventual Consistency (SEC)                                  *)
 (**********************************************************************)
 =============================================================================
 \* Modification History

tlaplus-seminar/13-20180713-RefinementMapping-Ji/MinMax1.tla

@@ -0,0 +1,103 @@
+------------------------------- MODULE MinMax1 ------------------------------
+(***************************************************************************)
+(* This module and modules MinMax2 and MinMax2H are used as examples in    *)
+(* Sections 1 and 2 of the paper "Auxiliary Variables in TLA+".            *)
+(*                                                                         *)
+(* This module specifies a tiny system in which a user presents a server   *)
+(* with a sequence of integer inputs, and the server responds to each      *)
+(* input value i with with one of the following outputs: Hi if i is the    *)
+(* largest number input so far, Lo if it's the smallest number input so    *)
+(* far, Both if it's both, and None if it's neither.                       *)
+(*                                                                         *)
+(* The module is part of an example illustrating the use of a history      *)
+(* variable.  The example includes this module, module MinMax2, and module *)
+(* MinMax2H which adds a history variable to the specification of MinMax2  *)
+(* and shows that the resulting specification implements implements the    *)
+(* specification of the current module under a suitable refinement         *)
+(* mapping.                                                                *)
+(***************************************************************************)
+EXTENDS Integers
+
+(***************************************************************************)
+(* We define setMax(S) and setMin(S) to be largest and smallest value in a *)
+(* nonempty finite set S of integers.                                      *)
+(***************************************************************************)
+setMax(S) == CHOOSE t \in S : \A s \in S : t >= s
+setMin(S) == CHOOSE t \in S : \A s \in S : t =< s
+
+(***************************************************************************)
+(* The possible values that can be returned by the system are declared to  *)
+(* be constants, which we assume are not integers.                         *)
+(***************************************************************************)
+CONSTANTS Lo, Hi, Both, None
+ASSUME {Lo, Hi, Both, None} \cap Int = { }
+
+(***************************************************************************)
+(* The the value of the variable x is the value input by the user or the   *)
+(* value output by the system, the variable `turn' indicating which.  The  *)
+(* variable y holds the set of all values input thus far.  We consider x   *)
+(* and `turn' to be externally visible and y to be internal.               *)
+(***************************************************************************)
+VARIABLES x, turn, y
+vars == <<x, turn, y>>
+
+(***************************************************************************)
+(* The initial predicate Init:                                             *)
+(***************************************************************************)
+Init ==  /\ x = None
+         /\ turn = "input" 
+         /\ y = {}
+
+(***************************************************************************)
+(* The user's input action:                                                *)
+(***************************************************************************)
+InputNum ==  /\ turn = "input"
+             /\ turn' = "output"
+             /\ x' \in Int
+             /\ y' = y
+
+(***************************************************************************)
+(* The systems response action:                                            *)
+(***************************************************************************)
+Respond == /\ turn = "output"
+           /\ turn' = "input"
+           /\ y' = y \cup {x}
+           /\ x' = IF x = setMax(y') THEN IF x = setMin(y') THEN Both ELSE Hi  
+                                     ELSE IF x = setMin(y') THEN Lo   ELSE None
+
+(***************************************************************************)
+(* The next-state action:                                                  *)
+(***************************************************************************)  
+Next == InputNum \/ Respond
+
+(***************************************************************************)
+(* The specification, which is a safety property (it asserts no liveness   *)
+(* condition).                                                             *)
+(***************************************************************************)
+Spec == Init /\ [][Next]_vars
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Below, we check that specification Spec implements specification Spec   *)
+(* of module MinMax2 under a suitable refinement mapping.  The following   *)
+(* definitions of Infinity and MinusInfinity are copied from module        *)
+(* MinMax2.                                                                *)
+(***************************************************************************)
+Infinity      == CHOOSE n : n \notin Int
+MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})
+
+M == INSTANCE MinMax2 
+        WITH min <- IF y = {} THEN Infinity      ELSE setMin(y),
+             max <- IF y = {} THEN MinusInfinity ELSE setMax(y)
+
+(***************************************************************************)
+(* The following theorem asserts that Spec implements the specification    *)
+(* Spec of module MinMax2 under the refinement mapping defined by the      *)
+(* INSTANCE statement.  The theorem can be checked with TLC using a model  *)
+(* having M!Spec as the temporal property to be checked.                   *)
+(***************************************************************************)
+THEOREM Spec => M!Spec
+=============================================================================
+\* Modification History
+\* Last modified Thu Jul 12 17:03:29 CST 2018 by xhdn
+\* Last modified Fri Oct 21 23:48:10 PDT 2016 by lamport
+\* Created Fri Aug 26 14:28:26 PDT 2016 by lamport

tlaplus-seminar/13-20180713-RefinementMapping-Ji/MinMax2.tla

@@ -0,0 +1,57 @@
+------------------------------ MODULE MinMax2 -------------------------------
+(***************************************************************************)
+(* This module specifies a system with the same interaction between a user *)
+(* and a server as the one in module MinMax1, but instead of remembering   *)
+(* the entire set of inputs, it uses two variables min and max to keep the *)
+(* largest and smallest values input thus far.  Initially min equals       *)
+(* Infinity and max equals MinusInfinity, where Infinity and MinusInfinity *)
+(* are two values that are considered greater than and less than any       *)
+(* integer, respectively.                                                  *)
+(***************************************************************************)
+EXTENDS Integers, Sequences
+
+CONSTANTS Lo, Hi, Both, None
+\*ASSUME {Lo, Hi, Both, None} \cap Int = { }
+
+Infinity      == CHOOSE n : n \notin Int
+MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})
+
+(***************************************************************************)
+(* The operators IsLeq and IsGeq extend =< and >=, respectively, to have   *)
+(* the correct meaning when Infinity or MinusInfinity is one of the        *)
+(* arguments.                                                              *)
+(***************************************************************************)
+IsLeq(i, j) == (j = Infinity) \/ (i =< j)
+IsGeq(i, j) == (j = MinusInfinity) \/ (i >= j) 
+
+(***************************************************************************)
+(* The rest of the specification is straightforward.                       *)
+(***************************************************************************)
+VARIABLES x, turn, min, max
+vars == <<x, turn, min, max>>
+
+Init ==  /\ x = None
+         /\ turn = "input" 
+         /\ min = Infinity 
+         /\ max = MinusInfinity
+
+InputNum ==  /\ turn = "input"
+             /\ turn' = "output"
+             /\ x' \in Int
+             /\ UNCHANGED <<min, max>>
+
+Respond  ==  /\ turn = "output"
+             /\ turn' = "input"
+             /\ min' = IF IsLeq(x, min) THEN x ELSE min 
+             /\ max' = IF IsGeq(x, max) THEN x ELSE max
+             /\ x' = IF x = max' THEN IF x = min' THEN Both ELSE Hi  
+                                 ELSE IF x = min' THEN Lo   ELSE None
+
+Next == InputNum \/ Respond
+
+Spec == Init /\ [][Next]_vars
+=============================================================================
+\* Modification History
+\* Last modified Thu Jul 12 16:35:43 CST 2018 by xhdn
+\* Last modified Fri Oct 21 23:57:32 PDT 2016 by lamport
+\* Created Fri Aug 26 14:32:23 PDT 2016 by lamport