request count

microsoft · Oct 2, 2024 · 0fc1238 · 0fc1238
1 parent d85c1f9
commit 0fc1238
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 --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
+      - run: ./tlc.py --trace-name 1C2N mc --term-count 2 --request-count 2 --raft-configs 1C2N consensus/MCccfraft.tla
+      - run: ./tlc.py --trace-name 1C3N mc --term-count 2 --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 --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 --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 --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 --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 --term-count 2 --max-request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla
+    $ ./tlc.py --term-count 2 --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
@@ -24,11 +24,11 @@ TermCount ==
 ASSUME TermCount \in Nat
 
 \* Limit on client requests
-MaxRequestCount ==
-    IF "MAX_REQUEST_COUNT" \in DOMAIN IOEnv
-    THEN atoi(IOEnv.MAX_REQUEST_COUNT)
-    ELSE Print("MAX_REQUEST_COUNT is not set, defaulting to 3", 3)
-ASSUME MaxRequestCount \in Nat
+RequestCount ==
+    IF "REQUEST_COUNT" \in DOMAIN IOEnv
+    THEN atoi(IOEnv.REQUEST_COUNT)
+    ELSE Print("REQUEST_COUNT is not set, defaulting to 3", 3)
+ASSUME RequestCount \in Nat
 
 ToServers ==
     UNION Range(Configurations)
@@ -70,8 +70,8 @@ MCTimeout(i) ==
 
 \* Limit number of requests (new entries) that can be made
 MCClientRequest(i) ==
-    \* Allocation-free variant of Len(SelectSeq(log[i], LAMBDA e: e.contentType = TypeEntry)) <= MaxRequestCount
-    /\ FoldSeq(LAMBDA e, count: IF e.contentType = TypeEntry THEN count + 1 ELSE count, 0, log[i]) <= MaxRequestCount
+    \* Allocation-free variant of Len(SelectSeq(log[i], LAMBDA e: e.contentType = TypeEntry)) <= RequestCount
+    /\ FoldSeq(LAMBDA e, count: IF e.contentType = TypeEntry THEN count + 1 ELSE count, 0, log[i]) <= RequestCount
     /\ CCF!ClientRequest(i)
 
 MCSignCommittableMessages(i) ==
@@ -143,7 +143,7 @@ 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) + TermCount
+    4 + ((RequestCount + Len(Configurations)) * 2) + TermCount
 
 MappingToAbs == 
   INSTANCE abs WITH

diff --git a/tla/tlc.py b/tla/tlc.py
@@ -95,7 +95,7 @@ def cli():
         help="Number of terms the nodes are allowed to advance through, defaults to 0",
     )
     mc.add_argument(
-        "--max-request-count",
+        "--request-count",
         type=int,
         default=3,
         help="Maximum number of requests the nodes are allowed to advance through, defaults to 3",
@@ -200,8 +200,8 @@ def cli():
     if args.cmd == "mc":
         if args.max_term_count is not None:
             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.request_count is not None:
+            env["REQUEST_COUNT"] = str(args.request_count)
         if args.raft_configs is not None:
             env["RAFT_CONFIGS"] = args.raft_configs
         if args.disable_check_quorum is not None: