Add DistributedReplicatedLog example.

The property `IsSync` in `DistributedReplicatedLog.tla` does not hold; the node
with the longest log may forever append a value before the other nodes can catch
up.  TLC finds the following (valid) counterexample (for three nodes):

```tla
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
cLogs = (n1 :> <<>> @@ n2 :> <<>> @@ n3 :> <<>>)

State 2: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog>
cLogs = (n1 :> <<>> @@ n2 :> <<v>> @@ n3 :> <<>>)

State 3: <Extend(n2) line 35, col 5 to line 38, col 49 of module DistributedReplicatedLog>
cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<>>)

State 4: <Copy(n3) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog>
cLogs = (n1 :> <<>> @@ n2 :> <<v, v>> @@ n3 :> <<v>>)

Back to state 2: <Copy(n1) line 26, col 9 to line 32, col 96 of module DistributedReplicatedLog>
```

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

specifications/FiniteMonotonic/DistributedReplicatedLog.tla

@@ -0,0 +1,74 @@
+This spec was inspired by https://github.com/microsoft/CCF/blob/main/tla/consensus/abs.tla.
+
+This spec has a machine-closed fairness constraint, which differs from the the CRDT and
+ReplicatedLog examples.  However, this spec assumes that a server can consistently read the
+state of all other servers, which is clearly not a realistic assumption for a real
+distributed system.  A real system would rely on some messaging protocol to determine the
+lag between servers (compare Raft).
+
+---- MODULE DistributedReplicatedLog ----
+EXTENDS Sequences, SequencesExt, Integers, FiniteSets, FiniteSetsExt
+
+CONSTANT Lag, Servers, Values
+ASSUME Lag \in Nat /\ IsFiniteSet(Servers)
+
+VARIABLE cLogs
+vars == <<cLogs>>
+
+TypeOK ==
+    /\ cLogs \in [Servers -> Seq(Values)]
+    
+Init ==
+    /\ cLogs \in [Servers -> {<< >>}]
+
+Copy(i) ==
+    \E j \in Servers: 
+        /\ Len(cLogs[j]) > Len(cLogs[i])
+        /\ \* Sync some prefix up to prefix = suffix of the unsynced suffix.
+           LET L == (Len(cLogs[j]) - Len(cLogs[i]))
+           \* Force to proportionally to the lag L copy more.
+           \* Lag: 1 -> 0..L, 2 -> 1..L, 3 -> 2..L 
+           IN  \E l \in L-1 .. L:
+                    cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]
+
+Extend(i) ==
+    /\ \A j \in Servers:
+            Len(cLogs[j]) \leq Len(cLogs[i])
+    /\ \E s \in BoundedSeq(Values, Lag - Max({Len(cLogs[i]) - Len(cLogs[j]) : j \in Servers})):
+            cLogs' = [cLogs EXCEPT ![i] = @ \o s]
+
+Next ==
+    \E i \in Servers: 
+        \/ Copy(i) 
+        \/ Extend(i)
+
+Spec ==
+    /\ Init
+    /\ [][Next]_vars
+    /\ \A s \in Servers: WF_vars(Extend(s)) /\ WF_vars(Copy(s))
+
+----
+\* Invariants
+
+Abs(n) ==
+    IF n < 0 THEN -n ELSE n
+
+BoundedLag ==
+    \A i, j \in Servers: Abs(Len(cLogs[i]) - Len(cLogs[j])) <= Lag
+
+THEOREM Spec => []BoundedLag
+
+----
+\* Liveness
+
+AllExtending ==
+    \A s \in Servers: []<><<IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+THEOREM Spec => AllExtending
+
+InSync ==
+    \* TLC correctly verifies that InSync is not a property of the system because
+    \* followers are permitted to copy only a prefix of the missing suffix.
+    \A i, j \in Servers : []<>(cLogs[i] = cLogs[j])
+
+====

specifications/FiniteMonotonic/MCDistributedReplicatedLog.cfg

@@ -0,0 +1,21 @@
+SPECIFICATION
+    Spec
+
+CONSTANTS
+    Servers = {n1, n2, n3}
+    Values = {v}
+    Lag = 3
+
+INVARIANTS
+    TypeOK
+    BoundedLag
+
+PROPERTIES
+    AllExtending
+    InSync
+
+VIEW 
+    DropCommonPrefix
+
+CHECK_DEADLOCK 
+    TRUE

specifications/FiniteMonotonic/MCDistributedReplicatedLog.tla

@@ -0,0 +1,23 @@
+---- MODULE MCDistributedReplicatedLog ----
+EXTENDS DistributedReplicatedLog, FiniteSetsExt
+
+ASSUME
+    \* LongestCommonPrefix in View for a single server would always shorten the
+    \* log to <<>>, reducing the state-space to a single state.
+    Cardinality(Servers) > 1
+
+----
+
+\* Combining the following conditions makes the state space finite:
+\* 1) The divergence of any two logs is bounded (See Extend action)
+\*
+\* 2) Terms is a *finite* set.
+ASSUME IsFiniteSet(Values)
+\*
+\* 3) The longest common prefix of all logs is discarded.
+DropCommonPrefix ==
+    LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs)))
+        Drop(seq, idx) == SubSeq(seq, idx + 1, Len(seq))
+    IN [ s \in Servers |-> Drop(cLogs[s], commonPrefixBound) ]
+
+====

specifications/FiniteMonotonic/README.md

@@ -4,4 +4,5 @@ Neither this approach nor the older approach have a proof of soundness and compl
 
 Specs & models include:
 - `CRDT.tla`: the spec of a basic grow-only counter CRDT
-- `ReplicatedLog.tla`: the "spec of a basic append-only replicated log
+- `ReplicatedLog.tla`: the spec of a basic append-only replicated log
+- `DistributedReplicatedLog.tla`: a spec of a distributed replicated log that demonstrates how the technique can be used to find violations of a liveness property (`Insync`).