term count

microsoft · Oct 2, 2024 · d85c1f9 · d85c1f9
1 parent cef81be
commit d85c1f9
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 16 deletions.
diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml
@@ -115,8 +115,8 @@ jobs:
           python3 install_deps.py
 
       - run: ./tlc.py mc consensus/MCabs.tla
-      - run: ./tlc.py --trace-name 1C2N mc --max-term-count 2 --max-request-count 2 --raft-configs 1C2N consensus/MCccfraft.tla
-      - run: ./tlc.py --trace-name 1C3N mc --max-term-count 2 --max-request-count 2 --raft-configs 1C3N consensus/MCccfraft.tla
+      - run: ./tlc.py --trace-name 1C2N mc --term-count 2 --max-request-count 2 --raft-configs 1C2N consensus/MCccfraft.tla
+      - run: ./tlc.py --trace-name 1C3N mc --term-count 2 --max-request-count 2 --raft-configs 1C3N consensus/MCccfraft.tla
 
       - name: Upload TLC traces
         uses: actions/upload-artifact@v4

diff --git a/.github/workflows/long-verification.yml b/.github/workflows/long-verification.yml
@@ -34,7 +34,7 @@ jobs:
           sudo apt install -y default-jre
           python3 install_deps.py
 
-      - run: ./tlc.py --trace-name 2C2N mc --max-term-count 2 --max-request-count 0 --raft-configs 2C2N --disable-check-quorum consensus/MCccfraft.tla
+      - run: ./tlc.py --trace-name 2C2N mc --term-count 2 --max-request-count 0 --raft-configs 2C2N --disable-check-quorum consensus/MCccfraft.tla
 
       - name: Upload TLC traces
         uses: actions/upload-artifact@v4
@@ -62,7 +62,7 @@ jobs:
           sudo apt install -y default-jre
           python3 install_deps.py
 
-      - run: ./tlc.py --trace-name 3C2N mc --max-term-count 2 --max-request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla
+      - run: ./tlc.py --trace-name 3C2N mc --term-count 2 --max-request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla
 
       - name: Upload TLC traces
         uses: actions/upload-artifact@v4

diff --git a/doc/architecture/raft_tla.rst b/doc/architecture/raft_tla.rst
@@ -29,7 +29,7 @@ You can also check the consensus specification including reconfiguration as foll
 
 .. code-block:: bash
 
-    $ ./tlc.py --max-term-count 2 --max-request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla
+    $ ./tlc.py --term-count 2 --max-request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla
 
 Using TLC to exhaustively check our models can take any time between minutes (for small configurations) and days (especially for the full consensus model with reconfiguration) on a 128 core VM (specifically, we used an `Azure HBv3 instance <https://docs.microsoft.com/en-us/azure/virtual-machines/hbv3-series>`_.
 

diff --git a/tla/consensus/MCccfraft.tla b/tla/consensus/MCccfraft.tla
@@ -17,11 +17,11 @@ Configurations ==
     ELSE Print("RAFT_CONFIGS is not set, defaulting to 1C2N: <<{NodeOne, NodeTwo}>>.", default)
 ASSUME Configurations \in Seq(SUBSET Servers)
 
-MaxTermCount ==
-    IF "MAX_TERM_COUNT" \in DOMAIN IOEnv
-    THEN atoi(IOEnv.MAX_TERM_COUNT)
-    ELSE Print("MAX_TERM_COUNT is not set, defaulting to 0", 0)
-ASSUME MaxTermCount \in Nat
+TermCount ==
+    IF "TERM_COUNT" \in DOMAIN IOEnv
+    THEN atoi(IOEnv.TERM_COUNT)
+    ELSE Print("TERM_COUNT is not set, defaulting to 0", 0)
+ASSUME TermCount \in Nat
 
 \* Limit on client requests
 MaxRequestCount ==
@@ -55,7 +55,7 @@ MCChangeConfigurationInt(i, newConfiguration) ==
 \* constraint below is too restrictive.
 MCTimeout(i) ==
     \* Limit the term of each server to reduce state space
-    /\ currentTerm[i] < StartTerm + MaxTermCount
+    /\ currentTerm[i] < StartTerm + TermCount
     \* Limit max number of simultaneous candidates
     \* We made several restrictions to the state space of Raft. However since we
     \* made these restrictions, Deadlocks can occur at places that Raft would in
@@ -143,12 +143,12 @@ DebugNotTooManySigsInv ==
 
 \* 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 + ((MaxRequestCount + Len(Configurations)) * 2) + MaxTermCount
+    4 + ((MaxRequestCount + Len(Configurations)) * 2) + TermCount
 
 MappingToAbs == 
   INSTANCE abs WITH
     Servers <- Servers,
-    Terms <- StartTerm..(StartTerm + MaxTermCount),
+    Terms <- StartTerm..(StartTerm + TermCount),
     MaxLogLength <- MaxLogLength,
     cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
 

diff --git a/tla/tlc.py b/tla/tlc.py
@@ -89,10 +89,10 @@ def cli():
     mc = subparsers.add_parser("mc", help="Model checking")
     # Control spec options of MCccfraft
     mc.add_argument(
-        "--max-term-count",
+        "--term-count",
         type=int,
         default=0,
-        help="Maximum number of terms the nodes are allowed to advance through, defaults to 0",
+        help="Number of terms the nodes are allowed to advance through, defaults to 0",
     )
     mc.add_argument(
         "--max-request-count",
@@ -199,7 +199,7 @@ def cli():
 
     if args.cmd == "mc":
         if args.max_term_count is not None:
-            env["MAX_TERM_COUNT"] = str(args.max_term_count)
+            env["TERM_COUNT"] = str(args.max_term_count)
         if args.max_request_count is not None:
             env["MAX_REQUEST_COUNT"] = str(args.max_request_count)
         if args.raft_configs is not None: