removing StartTerm

microsoft · Sep 2, 2024 · 6af5820 · 6af5820
1 parent 4f7f5a9
commit 6af5820
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 6 deletions.
diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
@@ -7,7 +7,6 @@ CONSTANTS
     Servers <- MCServers
     Terms <- MCTerms
     MaxLogLength <- MCMaxLogLength
-    StartTerm <- MCStartTerm
 
 INVARIANTS
     NoConflicts

diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
@@ -7,6 +7,5 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
 MCServers == {NodeOne, NodeTwo, NodeThree}
 MCTerms == 2..4
 MCMaxLogLength == 7
-MCStartTerm == 2
 
 ====
diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -136,9 +136,8 @@ MaxLogLength ==
 MappingToAbs == 
   INSTANCE abs WITH
     Servers <- Servers,
-    Terms <- 1..MaxTermLimit,
+    Terms <- StartTerm..MaxTermLimit,
     MaxLogLength <- MaxLogLength,
-    StartTerm <- StartTerm,
     CLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 
 RefinementToAbsProp == MappingToAbs!AbsSpec

diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
@@ -2,9 +2,9 @@
 \* Abstract specification for a distributed consensus algorithm.
 \* Assumes that any node can atomically inspect the state of all other nodes. 
 
-EXTENDS Sequences, SequencesExt, Naturals, FiniteSets
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt
 
-CONSTANT Servers, Terms, MaxLogLength, StartTerm
+CONSTANT Servers, Terms, MaxLogLength
 
 \* Commit logs from each node
 \* Each log is append-only and the logs will never diverge.
@@ -14,6 +14,8 @@ TypeOK ==
     /\ CLogs \in [Servers -> 
         UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
 
+StartTerm == Min(Terms)
+
 InitialLogs == {
     <<>>,
     <<StartTerm, StartTerm>>,