As expect, AllSyncing is not a theorem of the spec:

```tla
-> % tlc -note MCabs.tla
TLC2 Version 2.20 of Day Month 20?? (rev: cc65eef)
Running breadth-first search Model-Checking with fp 8 and seed -6640873860738991250 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 28225] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.25 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/MCabs.tla
Parsing file /Users/markus/src/TLA/_specs/MSFT/CCF/tla/consensus/abs.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Relation.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Relation.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-4226323038874662463/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module TLC
Semantic processing of module SequencesExt
Semantic processing of module Relation
Semantic processing of module abs
Semantic processing of module Integers
Semantic processing of module MCabs
Starting... (2024-10-28 10:30:27)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Finished computing initial states: 27 states generated, with 7 of them distinct at 2024-10-28 10:30:27.
Progress(3) at 2024-10-28 10:30:28: 26,895 states generated, 127 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 127 total distinct states at (2024-10-28 10:30:28)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

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

State 2: <Extend(n1) line 44, col 5 to line 46, col 49 of module abs>
cLogs = (n1 :> <<3, 2>> @@ n2 :> <<>> @@ n3 :> <<>>)

State 3: <Copy(n2) line 35, col 9 to line 37, col 92 of module abs>
cLogs = (n1 :> <<3, 2>> @@ n2 :> <<3, 2>> @@ n3 :> <<>>)

Back to state 1: <Copy(n3) line 35, col 9 to line 37, col 92 of module abs>

Finished checking temporal properties in 00s at 2024-10-28 10:30:28
26895 states generated, 127 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
Finished in 00s at (2024-10-28 10:30:28)
```

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

tla/consensus/MCabs.cfg

@@ -17,6 +17,7 @@ INVARIANTS
 PROPERTIES 
     InSync
     Syncing
+    AllSyncing
     AppendOnlyProp
     \* EquivExtendProp
     \* EquivCopyMaxAndExtendProp

tla/consensus/abs.tla

@@ -135,6 +135,10 @@ Syncing ==
 
 THEOREM MachineClosedFairSpec => Syncing
 
+AllSyncing ==
+    []<><<\A s \in Servers: IsStrictPrefix(cLogs[s], cLogs'[s])>>_cLogs
+
+\* NOT A THEOREM:  MachineClosedFairSpec => AllSyncing
 ----
 
 \* abs models ccfraft's logs up to the commitIndex and the extension of the