From aeddbfb99d42a60fe26658fa12e1001c8d88c6f7 Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Mon, 22 Jan 2024 18:15:20 +0000
Subject: [PATCH] Run simulation longer in Daily (#5946)

---
 .azure-pipelines-templates/daily-matrix.yml |  9 +++++++++
 .azure-pipelines-templates/matrix.yml       |  1 +
 .azure-pipelines-templates/simulation.yml   | 17 ++++++++++-------
 tla/consensus/SIMccfraft.tla                |  2 +-
 4 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/.azure-pipelines-templates/daily-matrix.yml b/.azure-pipelines-templates/daily-matrix.yml
index 865ad39d0b24..0a516b541106 100644
--- 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
index cd99ac1a0943..d0e76bdd84fc 100644
--- 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
index b2131a872449..01ff9efc12c5 100644
--- 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
index d3608f579b7b..175f970adba9 100644
--- 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)