Finite Monotonic

specifications/FiniteMonotonic/CRDT.tla

@@ -5,6 +5,7 @@ EXTENDS Naturals
 CONSTANT Node
 
 VARIABLE counter
+vars == counter
 
 TypeOK == counter \in [Node -> [Node -> Nat]]
 
@@ -14,7 +15,7 @@ Monotonic == \A n, o \in Node : counter'[n][o] >= counter[n][o]
 
 Monotonicity == [][Monotonic]_counter
 
-Convergence == \A n, o \in Node : counter[n] = counter[o]
+Convergence == []<>(\A n, o \in Node : counter[n] = counter[o])
 
 Init == counter = [n \in Node |-> [o \in Node |-> 0]]
 
@@ -37,5 +38,19 @@ Spec ==
   /\ Init
   /\ [][Next]_counter
 
+THEOREM Spec => []TypeOK
+THEOREM Spec => []Safety
+
+Fairness ==
+    /\ WF_vars(Next)
+    /\ \A n, o \in Node : <>[][Gossip(n,o)]_vars
+
+FairSpec ==
+  /\ Spec
+  /\ Fairness  
+
+THEOREM FairSpec => Convergence
+THEOREM FairSpec => Monotonicity
+
 =============================================================================
 

specifications/FiniteMonotonic/MCCRDT.cfg

@@ -0,0 +1,18 @@
+SPECIFICATION FairSpec
+
+CONSTANTS
+  Node = {n1, n2}
+  Next <- MCNext
+  Fairness <- MCFairness
+  Monotonicity <- MCMonotonicity
+
+INVARIANTS
+    TypeOK
+    Safety
+
+PROPERTIES 
+    Convergence
+    Monotonicity
+
+CONSTRAINTS StateConstraint
+CONSTANTS Increment <- MCIncrement

specifications/FiniteMonotonic/MCCRDT.tla

@@ -0,0 +1,67 @@
+------ MODULE MCCRDT -----
+EXTENDS CRDT, IOUtils, TLC
+
+Divergence == 
+    \* D=0 means there is no divergence. D=1 means Gossip synchronizes the system in a single step. 
+    atoi(IOEnv.D)
+ASSUME Divergence \in Nat
+
+Constraint ==
+    IOEnv.C = ToString(TRUE)
+ASSUME Constraint \in BOOLEAN
+
+GB ==
+    IOEnv.G = ToString(TRUE)
+ASSUME GB \in BOOLEAN
+
+F ==
+    atoi(IOEnv.F)
+ASSUME F \in 0..6
+
+------
+
+GarbageCollect ==
+  LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
+  LET Transpose == SetMin({counter[n][o] : n, o \in Node}) IN
+  counter' = [
+      n \in Node |-> [
+        o \in Node |-> counter[n][o] - Transpose
+      ]
+    ]
+
+------
+
+S == INSTANCE CRDT
+
+MCIncrement(n) ==
+  /\ IF Constraint THEN TRUE ELSE counter[n][n] < Divergence
+  /\ S!Increment(n)
+
+MCNext ==
+  \/ S!Next
+  \/ GB /\ GarbageCollect
+
+MCFairness ==
+    \* Note that TLC doesn't accept the following fairness condition if written with CASE.
+    IF      F = 0 THEN WF_vars(Next) 
+    ELSE IF F = 1 THEN WF_vars(GarbageCollect)
+    ELSE IF F = 2 THEN WF_vars(Next) /\ ~ \E n \in Node : <>[][Increment(n)]_vars
+    ELSE IF F = 3 THEN \A n, o \in Node : WF_vars(Gossip(n,o))
+    ELSE IF F = 4 THEN \A n    \in Node : WF_vars(Increment(n))
+    \* Fairness below are expected to to hold for an Divergence.
+    ELSE IF F = 5 THEN WF_vars(Next) /\ \A n, o \in Node : <>[][Gossip(n,o)]_vars
+    ELSE IF F = 6 THEN Convergence
+    ELSE FALSE
+
+MCMonotonicity == [][
+  \/ S!Monotonic
+  \/ \A a, b, c, d \in Node :
+    (counter'[a][b] - counter[a][b]) = (counter'[c][d] - counter[c][d])
+]_vars
+
+------
+
+StateConstraint == 
+    IF Constraint THEN \A n, o \in Node : counter[n][o] <= Divergence ELSE TRUE
+
+======

specifications/FiniteMonotonic/SCCRDT.tla

@@ -0,0 +1,17 @@
+
+  $ wget https://nightly.tlapl.us/dist/tla2tools.jar
+  $ wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
+  $ java -jar tla2tools.jar -config SCCRDT.tla SCCRDT.tla
+
+----------------------------- MODULE SCCRDT -----------------------------
+EXTENDS TLC, Naturals, Sequences, IOUtils
+
+CmdLine == 
+    <<"java", "-jar", TLCGet("config").install, "-note", "MCCRDT.tla">>
+
+ASSUME \A c \in [ D: 0..3, F: 0..6, G: BOOLEAN, C: BOOLEAN ] : 
+    PrintT(<<"conf", c, IOEnvExec(c, CmdLine).exitValue>>)
+
+=============================================================================
+---- CONFIG SCCRDT ----
+====