Fewer StartTerm instances (#5840)

microsoft · Nov 17, 2023 · 0f59a5d · 0f59a5d
1 parent a648fc3
commit 0f59a5d
Show file tree

Hide file tree

Showing 6 changed files with 1 addition and 11 deletions.
diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
@@ -4,8 +4,6 @@ CONSTANTS
     Configurations <- 1Configuration
     Servers <- ToServers
 
-    StartTerm = 2
-
     MaxTermLimit = 2
     MaxCommitsNotified = 0
     RequestLimit = 3

diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -4,8 +4,6 @@ CONSTANTS
     Configurations <- 2Configurations
     Servers <- ToServers
 
-    StartTerm = 2
-
     MaxTermLimit = 5
     MaxCommitsNotified = 2
     RequestLimit = 3

diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -4,8 +4,6 @@ CONSTANTS
     Configurations <- 3Configurations
     Servers <- ToServers
 
-    StartTerm = 2
-
     MaxTermLimit = 4
     MaxCommitsNotified = 2
     RequestLimit = 2

diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
@@ -3,8 +3,6 @@ SPECIFICATION SIMSpec
 CONSTANTS
     Servers <- Servers_mc
 
-    StartTerm = 2
-
     Nil = Nil
 
     Follower = Follower

diff --git a/tla/consensus/Traceccfraft.cfg b/tla/consensus/Traceccfraft.cfg
@@ -45,8 +45,6 @@ CONSTANTS
 
     InitReconfigurationVars <- TraceInitReconfigurationVars
 
-    StartTerm = 2
-
     Nil = Nil
 
     Follower = Follower

diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
@@ -83,7 +83,7 @@ CONSTANTS Servers
 ASSUME Servers /= {} /\ IsFiniteSet(Servers)
 
 \* Initial term used by the Start node in the network
-CONSTANT StartTerm
+StartTerm == 2
 
 Nil ==
   (*************************************************************************)