Merge branch 'main' of github.com:microsoft/CCF into reelection_take2

eddyashton · Jan 23, 2024 · a5d9d0b · a5d9d0b
2 parents 5d4321c + aeddbfb
commit a5d9d0b
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 8 deletions.
diff --git a/.azure-pipelines-templates/daily-matrix.yml b/.azure-pipelines-templates/daily-matrix.yml
@@ -132,3 +132,12 @@ jobs:
       ctest_filter: '-LE "benchmark|perf|rotation"'
       depends_on: configure
       installExtendedTestingTools: true
+
+  - template: simulation.yml
+    parameters:
+      target: Virtual
+      timeout: 3000
+      env: ${{ parameters.env.Virtual }}
+      installExtendedTestingTools: false
+      depends_on:
+        - configure
diff --git a/.azure-pipelines-templates/matrix.yml b/.azure-pipelines-templates/matrix.yml
@@ -163,6 +163,7 @@ jobs:
           target: Virtual
           env: ${{ parameters.env.Virtual }}
           installExtendedTestingTools: false
+          metrics: true
           depends_on:
             - configure
 

diff --git a/.azure-pipelines-templates/simulation.yml b/.azure-pipelines-templates/simulation.yml
@@ -20,16 +20,19 @@ jobs:
         displayName: Setup
 
       - script: ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
+        env:
+          SIM_TIMEOUT: ${{ parameters.timeout }}
         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
+      - ${{ if eq(parameters.metrics, true) }}:
+          - 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:

diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
@@ -36,7 +36,7 @@ SIMTimeout(i) ==
 \* The state constraint  StopAfter  stops TLC after the alloted
 \* time budget is up, unless TLC encounteres an error first.
 StopAfter ==
-    LET timeout == IF "SIM_TIMEOUT" \in DOMAIN IOEnv THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
+    LET timeout == IF ("SIM_TIMEOUT" \in DOMAIN IOEnv) /\ IOEnv.SIM_TIMEOUT # "" THEN atoi(IOEnv.SIM_TIMEOUT) ELSE 1200
     (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)