Move simulation to ADO too, and shorten the length of its run to not delay PRs

.azure-pipelines-templates/matrix.yml

@@ -157,6 +157,15 @@ jobs:
           depends_on:
             - configure
 
+  - ${{ if eq(parameters.perf_tests, 'run') }}:
+      - template: simulation.yml
+        parameters:
+          target: Virtual
+          env: ${{ parameters.env.Virtual }}
+          installExtendedTestingTools: false
+          depends_on:
+            - configure
+
   - ${{ if eq(parameters.perf_tests, 'run') }}:
       - template: cimetrics.yml
         parameters:
@@ -171,6 +180,7 @@ jobs:
             - Virtual_Perf_MultiThreaded
             - SGX_Perf_MultiThreaded
             - Model_Checking
+            - Simulation
 
   # Release
   - ${{ if eq(parameters.perf_or_release, 'release') }}:

.azure-pipelines-templates/simulation.yml

@@ -0,0 +1,38 @@
+jobs:
+  - job: Simulation
+    displayName: Simulation
+    variables:
+      Codeql.SkipTaskAutoInjection: true
+      skipComponentGovernanceDetection: true
+
+    ${{ insert }}: ${{ parameters.env }}
+
+    steps:
+      - checkout: self
+        clean: true
+        fetchDepth: 1
+
+      - script: |
+          set -ex
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
+        displayName: Setup
+
+      - script: ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
+        workingDirectory: tla
+        displayName: Simulation
+
+      - script: |
+          set -ex
+          ./cimetrics_env.sh python upload_tlc_stats.py sim ../tla/SIMccfraft_stats.json
+        env:
+          METRICS_MONGO_CONNECTION: $(METRICS_MONGO_CONNECTION)
+        workingDirectory: tests
+        displayName: Uploading TLC stats to cimetrics
+
+      - task: PublishPipelineArtifact@1
+        inputs:
+          artifactName: "Simulation Traces"
+          targetPath: tla
+        condition: or(failed(), canceled())

.github/workflows/tlaplus.yml

@@ -10,30 +10,6 @@ on:
   workflow_dispatch:
 
 jobs:
-  simulation-consensus:
-    name: Simulation - Consensus
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v3
-      - run: python3 ./tla/install_deps.py
-
-      - name: SIMccfraft.tla
-        run: |
-          cd tla/
-          ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
-
-      - name: Upload traces in TLA and JSON format
-        uses: actions/upload-artifact@v3
-        if: ${{ failure() }}
-        with:
-          name: tlc
-          path: |
-            tla/consensus/*_TTrace_*.tla
-            tla/consensus/*_TTrace_*.bin
-            tla/*.trace.tla
-            tla/*.json
-
   model-checking-consistency:
     name: Model Checking - Consistency
     runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]

tests/upload_tlc_stats.py

@@ -13,12 +13,19 @@ def run(test_label, filename):
             data = json.load(f)
             duration_sec = data["duration"]
             dstates = data["distinct"]
-            print(
-                f"Uploading metrics for {test_label} - duration: {duration_sec}, distinct states: {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)
+            traces = data.get("traces", 0)
+            levelmean = data.get("levelmean", 0)
+            print(f"Uploading metrics for {test_label}: {data}")
+            if dstates == -1:
+                # Simulation
+                with cimetrics.upload.metrics(complete=False) as metrics:
+                    metrics.put(f"tlc_{test_label}_traces", traces)
+                    metrics.put(f"tlc_{test_label}_levelmean", levelmean)
+            else:
+                # Model checking
+                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:
         print(f"Could not find file {filename}: skipping metrics upload")

tla/consensus/MCccfraftWithReconfig.cfg

@@ -50,7 +50,7 @@ VIEW View
 CHECK_DEADLOCK 
     FALSE
 
-POSTCONDITION 
+POSTCONDITION
     WriteStatsFile
 
 PROPERTIES

tla/consensus/SIMccfraft.cfg

@@ -33,6 +33,8 @@ CONSTANTS
     NodeFour = n4
     NodeFive = n5
 
+    StatsFilename = "SIMccfraft_stats.json"
+
 CONSTRAINT
     StopAfter
 
@@ -48,6 +50,9 @@ PROPERTIES
     PendingBecomesFollowerProp
     NeverCommitEntryPrevTermsProp
 
+POSTCONDITION
+    WriteStatsFile
+
 INVARIANTS
     LogInv
     MoreThanOneLeaderInv

tla/consensus/SIMccfraft.tla

@@ -1,5 +1,5 @@
 ---------- MODULE SIMccfraft ----------
-EXTENDS ccfraft, TLC, Integers
+EXTENDS ccfraft, TLC, Integers, StatsFile, IOUtils
 
 CONSTANTS
     NodeOne, NodeTwo, NodeThree, NodeFour, NodeFive
@@ -44,8 +44,9 @@ SIMSpec ==
 \* The state constraint  StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounteres an error first.
 StopAfter ==
-    (* The smoke test has a time budget of 50 minutes. *)
-    TLCSet("exit", TLCGet("duration") > 3000)
+    LET timeout == IF "SIM_TIMEOUT" \in DOMAIN IOEnv THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
+    (* The smoke test has a time budget of 20 minutes. *)
+    IN TLCSet("exit", TLCGet("duration") > timeout)
 
 =============================================================================