Move refinement mapping from TLC-specific module into ccfraft.

Depends on TLA+ PR tlaplus/tlaplus#1014

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

tla/consensus/MCccfraft.cfg

@@ -50,6 +50,8 @@ CONSTANTS
     NodeTwo = n2
     NodeThree = n3
 
+    RefinementToAbsProp <- MCRefinementToAbsProp
+
 SYMMETRY Symmetry
 VIEW View
 

tla/consensus/MCccfraft.tla

@@ -128,18 +128,9 @@ DebugNotTooManySigsInv ==
 
 ----
 \* Refinement
-
-\* The inital log is up to 4 entries long + one log entry per request/reconfiguration + one signature per request/reconfiguration or new view (no consecutive sigs except across views)
 MaxLogLength == 
     4 + ((RequestLimit + Len(Configurations)) * 2) + MaxTermLimit
 
-MappingToAbs == 
-  INSTANCE abs WITH
-    Servers <- Servers,
-    Terms <- StartTerm..MaxTermLimit,
-    MaxLogLength <- MaxLogLength,
-    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
-
-RefinementToAbsProp == MappingToAbs!AbsSpec
+MCRefinementToAbsProp == MappingToAbs(StartTerm..MaxTermLimit, MaxLogLength)!AbsSpec
 
 ===================================

tla/consensus/ccfraft.tla

@@ -1671,4 +1671,20 @@ DebugCommittedEntriesTermsInv ==
             k <= commitIndex[i]
             => log[i][k].term >= log[j][k].term
 
+
+------------------------------------------------------------------------------
+\* Refinement of the more high-level specification abs.tla that abstracts the
+\* asynchronous network and the message passing between nodes.  Instead, any
+\* node may atomically observe the state of any other node.
+
+MappingToAbs(T, MLL) == 
+  INSTANCE abs WITH
+    Servers <- Servers,
+    Terms <- T,
+    MaxLogLength <- MLL,
+    cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
+
+RefinementToAbsProp == \EE T, M : MappingToAbs(T, M)!AbsSpec
+THEOREM Spec => RefinementToAbsProp
+
 ===============================================================================