Adding TLC stats to cimetrics

.azure-pipelines-templates/model_checking.yml

@@ -23,13 +23,24 @@ jobs:
         workingDirectory: tla
         displayName: MCccfraft.cfg
 
-      - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json
-        workingDirectory: tla
-        displayName: MCccfraftAtomicReconfig.cfg
+      # - script: ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json
+      #   workingDirectory: tla
+      #   displayName: MCccfraftAtomicReconfig.cfg
 
-      - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
-        workingDirectory: tla
-        displayName: MCccfraftWithReconfig.cfg
+      # - script: ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
+      #   workingDirectory: tla
+      #   displayName: MCccfraftWithReconfig.cfg
+
+      - script: |
+          set -ex
+          python3.8 -m venv env
+          source env/bin/activate
+          python -m pip install -r requirements.txt
+          python3 upload_tlc_stats.py 3node_fixed ../tla/MCccfraft.json
+        env:
+          METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION)
+        workingDirectory: tests
+        displayName: Uploading TLC stats to cimetrics
 
       - task: PublishPipelineArtifact@1
         inputs:

metrics.yml

@@ -10,4 +10,5 @@ monitoring_span: 150
 groups:
   "SGX": ".*_sgx_.*"
   "Virtual": ".*_virtual_.*"
+  "TLC": "tlc_.*"
   "Others": ".*"

tests/upload_tlc_stats.py

@@ -0,0 +1,46 @@
+# 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(test_label, 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 for {} - duration: {}, distinct states: {}",
+                test_label,
+                duration_sec,
+                dstates,
+            )
+            with cimetrics.upload.metrics(complete=False) as metrics:
+                metrics.put(f"tlc_{test_label}_duration_s", duration_sec)
+                metrics.put(f"tlc_{test_label}_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(
+        "test_label",
+        help="test name to upload metrics under",
+    )
+
+    parser.add_argument(
+        "filename",
+        help="TLC stats JSON file to upload",
+    )
+
+    args = parser.parse_args()
+    run(args.test_label, args.filename)

tla/.gitignore

@@ -12,4 +12,5 @@ tools/
 *.dot
 *TTrace*.tla
 *TTrace*.bin
-**/states.dump*
+*_stats.json
+**/states.dump*

tla/StatsFile.tla

@@ -0,0 +1,14 @@
+---- MODULE StatsFile----
+EXTENDS TLC, Json, Sequences
+
+\* Filename to write TLC stats to
+CONSTANT StatsFilename
+ASSUME StatsFilename \in STRING
+
+\* 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/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, StatsFile
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree
@@ -21,6 +21,7 @@ ASSUME MaxCommitsNotified \in Nat
 CONSTANT RequestLimit
 ASSUME RequestLimit \in Nat
 
+
 ToServers ==
     UNION Range(Configurations)
 
@@ -137,4 +138,6 @@ AllReconfigurationsCommitted ==
 DebugAllReconfigurationsReachableInv ==
     ~AllReconfigurationsCommitted
 
+
+
 ===================================

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

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