Adding TLC stats to cimetrics

.github/workflows/tlaplus.yml

@@ -38,6 +38,12 @@ jobs:
           cd tla/
           ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
 
+      - name: Uploading TLC stats to cimetrics
+        run: |
+          cd tests
+          pip3 install -r requirements.txt 
+          python3 upload_tlc_stats.py ../tla/MCccfraftWithReconfig.json
+
       - name: Upload traces in TLA and JSON format
         uses: actions/upload-artifact@v3
         if: ${{ failure() }}

tests/upload_tlc_stats.py

@@ -0,0 +1,40 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+# Licensed under the Apache 2.0 License.
+
+import json
+import os
+import argparse
+import cimetrics.upload
+
+from loguru import logger as LOG
+
+
+def run(filename):
+    if os.path.exists(filename):
+        with open(filename) as f:
+            data = json.load(f)
+            duration_sec = data["duration"]
+            dstates = data["distinct"]
+            LOG.info(
+                "Uploading metrics - duration: {}, distinct states: {}",
+                duration_sec,
+                dstates,
+            )
+            with cimetrics.upload.metrics(complete=False) as metrics:
+                metrics.put("TLC Duration (s)", duration_sec)
+                metrics.put("TLC Distinct States", dstates)
+
+    else:
+        LOG.warning(f"Could not find file {filename}: skipping metrics upload")
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description="Upload TLC stats to cimetrics.")
+
+    parser.add_argument(
+        "filename",
+        help="TLC stats JSON file to upload",
+    )
+
+    args = parser.parse_args()
+    run(args.filename)

tla/.gitignore

@@ -11,4 +11,5 @@ tools/
 .DS_Store
 *.dot
 *TTrace*.tla
-*TTrace*.bin
+*TTrace*.bin
+*_stats.json

tla/consensus/MCccfraft.cfg

@@ -7,6 +7,8 @@ CONSTANTS
     MaxTermLimit = 1
     MaxCommitsNotified = 0
     RequestLimit = 3
+
+    StatsFilename = "MCccfraft_stats.json"
 
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp

tla/consensus/MCccfraft.tla

@@ -1,5 +1,5 @@
 ---------- MODULE MCccfraft ----------
-EXTENDS ccfraft, TLC
+EXTENDS ccfraft, TLC, Json
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree
@@ -21,6 +21,11 @@ ASSUME MaxCommitsNotified \in Nat
 CONSTANT RequestLimit
 ASSUME RequestLimit \in Nat
 
+\* Filename to write TLC stats to
+CONSTANT StatsFilename
+ASSUME StatsFilename \in STRING
+
+
 ToServers ==
     UNION Range(Configurations)
 
@@ -137,4 +142,10 @@ AllReconfigurationsCommitted ==
 DebugAllReconfigurationsReachableInv ==
     ~AllReconfigurationsCommitted
 
+\* Writes TLC stats (such as number of states and duration) to StatsFilename in ndJson format
+\* Specify WriteStatsFile as a postcondition to write the stats file at the end of model checking
+WriteStatsFile == 
+    /\ PrintT("Writing stats to file: " \o StatsFilename)
+    /\ ndJsonSerialize(StatsFilename, <<TLCGet("stats")>>)
+
 ===================================

tla/consensus/MCccfraftAtomicReconfig.cfg

@@ -7,6 +7,8 @@ CONSTANTS
     MaxTermLimit = 4
     MaxCommitsNotified = 2
     RequestLimit = 3
+
+    StatsFilename = "MCccfraftAtomicReconfig_stats.json"
 
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp

tla/consensus/MCccfraftWithReconfig.cfg

@@ -7,6 +7,8 @@ CONSTANTS
     MaxTermLimit = 3
     MaxCommitsNotified = 2
     RequestLimit = 3
+
+    StatsFilename = "MCccfraftWithReconfig_stats.json"
 
     Timeout <- MCTimeout
     Send <- MCSend
@@ -50,6 +52,9 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
+POSTCONDITION 
+    WriteStatsFile
+
 PROPERTIES
     CommittedLogAppendOnlyProp
     MonotonicTermProp