Minimize number of TLC configuration files. (#6511)

Signed-off-by: Markus Alexander Kuppe <[email protected]>

.github/workflows/tlaplus.yml

@@ -135,23 +135,23 @@ jobs:
           cd tla/
           ./tlc.sh -workers auto consensus/MCabs.tla -dumpTrace tla MCabs.trace.tla -dumpTrace json MCabs.json
 
-      - name: MCccfraft.cfg
+      - name: MCccfraft - Configurations=1C2N
         run: |
           set -x
           cd tla/
-          ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
+          Configurations=1C2N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C2NT2R3.trace.tla -dumpTrace json MCccfraft1C2NT2R3.json
 
-      - name: MCccfraft2Nodes.cfg
+      - name: MCccfraft - Configurations=1C3N
         run: |
           set -x
           cd tla/
-          ./tlc.sh -workers auto -config consensus/MCccfraft2Nodes.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraft2Nodes.trace.tla -dumpTrace json MCccfraft2Nodes.json
+          Configurations=1C3N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C3N2T3R.trace.tla -dumpTrace json MCccfraft1C3N2T3R.json
 
-      - name: MCccfraftAtomicReconfig.cfg
+      - name: MCccfraft - Configurations=2C2N (atomic reconf) MaxTermLimit=4 RequestLimit=3 NoCheckQuorum
         run: |
           set -x
           cd tla/
-          ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json
+          Configurations=2C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft2C2N4T1R.trace.tla -dumpTrace json MCccfraft2C2N4T1R.json
 
       - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
         uses: actions/upload-artifact@v4
@@ -175,11 +175,11 @@ jobs:
           sudo apt install -y default-jre
           python3 ./tla/install_deps.py
 
-      - name: MCccfraftWithReconfig.cfg
+      - name: MCccfraft - Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum
         run: |
           set -x
           cd tla/
-          ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
+          Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft3C2N4T1R.trace.tla -dumpTrace json MCccfraft3C2N4T1R.json
 
       - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
         uses: actions/upload-artifact@v4

doc/architecture/raft_tla.rst

@@ -29,7 +29,7 @@ You can also check the consensus specification including reconfiguration as foll
 
 .. code-block:: bash
 
-    $ ./tlc.sh consensus/MCccfraft.tla -config consensus/MCccfraftWithReconfig.cfg
+    $ Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh 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>`_.
 

tla/StatsFile.tla

@@ -2,11 +2,17 @@
 EXTENDS TLC, Json, Sequences, Naturals, IOUtils
 
 \* Filename to write TLC stats to
-CONSTANT StatsFilename
+StatsFilename ==
+    IF "StatsFileName" \in DOMAIN IOEnv
+    THEN IOEnv.StatsFileName 
+    ELSE Print("Found no env var StatsFileName.  Falling back to MCccfraft_stats.json.", "MCccfraft_stats.json")
 ASSUME StatsFilename \in STRING
 
 \* Filename to write TLC coverage to
-CONSTANT CoverageFilename
+CoverageFilename ==
+    IF "CoverageFilename" \in DOMAIN IOEnv
+    THEN IOEnv.CoverageFilename 
+    ELSE Print("Found no env var CoverageFilename.  Falling back to MCccfraft_coverage.json.", "MCccfraft_coverage.json")
 ASSUME CoverageFilename \in STRING
 
 \* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format

tla/consensus/MCccfraft.cfg

@@ -1,20 +1,14 @@
 SPECIFICATION mc_spec
 
 CONSTANTS
-    Configurations <- 1Configuration3Nodes
     Servers <- ToServers
-
-    MaxTermLimit = 2
-    RequestLimit = 3
-
-    StatsFilename = "MCccfraft_stats.json"
-    CoverageFilename = "MCccfraft_coverage.json"
 
     Timeout <- MCTimeout
     Send <- MCSend
     ClientRequest <- MCClientRequest
     SignCommittableMessages <- MCSignCommittableMessages
     ChangeConfigurationInt <- MCChangeConfigurationInt
+    CheckQuorum <- MCCheckQuorum
 
     Nil = Nil
 
@@ -59,6 +53,9 @@ CHECK_DEADLOCK
 POSTCONDITION 
     WriteStatsFile
 
+_PERIODIC
+    SerializeCoverage
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp
@@ -68,7 +65,8 @@ PROPERTIES
     MembershipStateTransitionsProp
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
-    RefinementToAbsProp
+    \* Will be checked after https://github.com/microsoft/CCF/pull/6509
+    \* RefinementToAbsProp
 
 INVARIANTS
     LogInv

tla/consensus/MCccfraft.tla

@@ -1,32 +1,43 @@
 ---------- MODULE MCccfraft ----------
-EXTENDS ccfraft, StatsFile, MCAliases
+EXTENDS ccfraft, StatsFile, MCAliases, TLC, IOUtils
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree
 
-\* No reconfiguration
-1Configuration2Nodes == <<{NodeOne, NodeTwo}>>
-1Configuration3Nodes == <<{NodeOne, NodeTwo, NodeThree}>>
-\* Atomic reconfiguration from NodeOne to NodeTwo
-2Configurations == <<{NodeOne}, {NodeTwo}>>
-\* Incremental reconfiguration from NodeOne to NodeOne and NodeTwo, and then to NodeTwo
-3Configurations == <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>>
-
-CONSTANT Configurations
+Configurations ==
+    LET default == <<{NodeOne, NodeTwo}>> IN
+    IF "Configurations" \in DOMAIN IOEnv THEN
+          \* Don't parse and process the string Configurations but keep it simple and just check for known values.
+          CASE IOEnv.Configurations = "1C1N" -> <<{NodeOne}>>
+            [] IOEnv.Configurations = "1C2N" -> default
+            [] IOEnv.Configurations = "1C3N" -> <<{NodeOne, NodeTwo, NodeThree}>>
+            [] IOEnv.Configurations = "2C2N" -> <<{NodeOne}, {NodeTwo}>>
+            [] IOEnv.Configurations = "3C2N" -> <<{NodeOne}, {NodeOne, NodeTwo}, {NodeTwo}>>
+            [] OTHER -> Print("Unknown value for env var Configurations.  Falling back to <<{NodeOne, NodeTwo}>>.", default)
+    ELSE Print("Found no env var Configurations.  Falling back to <<{NodeOne, NodeTwo}>>.", default)
 ASSUME Configurations \in Seq(SUBSET Servers)
 
-CONSTANT MaxTermLimit
+MaxTermLimit ==
+    IF "MaxTermLimit" \in DOMAIN IOEnv
+    THEN atoi(IOEnv.MaxTermLimit)
+    ELSE Print("Found no env var MaxTermLimit.  Falling back to 2 terms.", 2)
 ASSUME MaxTermLimit \in Nat
 
 \* Limit on client requests
-CONSTANT RequestLimit
+RequestLimit ==
+    IF "RequestLimit" \in DOMAIN IOEnv
+    THEN atoi(IOEnv.RequestLimit)
+    ELSE Print("Found no env var RequestLimit.  Falling back to 3 requests.", 3)
 ASSUME RequestLimit \in Nat
 
 ToServers ==
     UNION Range(Configurations)
 
 CCF == INSTANCE ccfraft
 
+MCCheckQuorum(i) ==
+    IF "NoCheckQuorum" \in DOMAIN IOEnv THEN FALSE ELSE CCF!CheckQuorum(i)
+
 \* This file controls the constants as seen below.
 \* In addition to basic settings of how many nodes are to be model checked,
 \* the model allows to place additional limitations on the state space of the program.