From 4b5dbee519efc9849523a06ac7ee515f11f5e643 Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Thu, 2 Nov 2023 15:08:26 +0000
Subject: [PATCH 1/3] Move model checking to main CI pipeline

---
 .azure-pipelines-templates/matrix.yml         | 10 ++++++++++
 .azure-pipelines-templates/model_checking.yml | 20 +++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 .azure-pipelines-templates/model_checking.yml

diff --git a/.azure-pipelines-templates/matrix.yml b/.azure-pipelines-templates/matrix.yml
index 9bfdc1de98ce..47a804ac6e64 100644
--- a/.azure-pipelines-templates/matrix.yml
+++ b/.azure-pipelines-templates/matrix.yml
@@ -148,6 +148,15 @@ jobs:
           depends_on: configure
           installExtendedTestingTools: false
 
+  - ${{ if eq(parameters.perf_tests, 'run') }}:
+      - template: model_checking.yml
+        parameters:
+          target: Virtual
+          env: ${{ parameters.env.Virtual }}
+          installExtendedTestingTools: false
+          depends_on:
+            - configure
+
   - ${{ if eq(parameters.perf_tests, 'run') }}:
       - template: cimetrics.yml
         parameters:
@@ -161,6 +170,7 @@ jobs:
             - Virtual_Perf
             - Virtual_Perf_MultiThreaded
             - SGX_Perf_MultiThreaded
+            - Model_Checking
 
   # Release
   - ${{ if eq(parameters.perf_or_release, 'release') }}:
diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml
new file mode 100644
index 000000000000..263c73f0b4b0
--- /dev/null
+++ b/.azure-pipelines-templates/model_checking.yml
@@ -0,0 +1,20 @@
+jobs:
+  - job: Model_Checking
+    displayName: "Model Checking"
+
+    ${{ 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 consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
+        workingDirectory: tla

From 874e8cd58ad77f01fe217d4d3ccc40aee8f0e46b Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Thu, 2 Nov 2023 15:42:39 +0000
Subject: [PATCH 2/3] Other steps and publishing

---
 .azure-pipelines-templates/model_checking.yml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/.azure-pipelines-templates/model_checking.yml b/.azure-pipelines-templates/model_checking.yml
index 263c73f0b4b0..b8e70d712be1 100644
--- a/.azure-pipelines-templates/model_checking.yml
+++ b/.azure-pipelines-templates/model_checking.yml
@@ -1,6 +1,9 @@
 jobs:
   - job: Model_Checking
     displayName: "Model Checking"
+    variables:
+      Codeql.SkipTaskAutoInjection: true
+      skipComponentGovernanceDetection: true
 
     ${{ insert }}: ${{ parameters.env }}
 
@@ -18,3 +21,18 @@ jobs:
 
       - script: ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
         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/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
+        workingDirectory: tla
+        displayName: MCccfraftWithReconfig.cfg
+
+      - task: PublishPipelineArtifact@1
+        inputs:
+          artifactName: "Model Checking Traces"
+          targetPath: tla
+        condition: or(failed(), canceled())

From 5811abf5b959a64325e803aaa01380df512056b8 Mon Sep 17 00:00:00 2001
From: Amaury Chamayou <amchamay@microsoft.com>
Date: Thu, 2 Nov 2023 19:18:41 +0000
Subject: [PATCH 3/3] Remove model checking from GHA

---
 .github/workflows/tlaplus.yml | 39 -----------------------------------
 1 file changed, 39 deletions(-)

diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml
index aa81023a858e..54bd429162dd 100644
--- a/.github/workflows/tlaplus.yml
+++ b/.github/workflows/tlaplus.yml
@@ -10,45 +10,6 @@ on:
   workflow_dispatch:
 
 jobs:
-  model-checking-consensus:
-    name: Model Checking - Consensus
-    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
-    container:
-      image: ccfmsrc.azurecr.io/ccf/ci:26-10-2023-virtual-clang15
-
-    steps:
-      - uses: actions/checkout@v3
-      - run: |
-          sudo apt update
-          sudo apt install -y default-jre
-          python3 ./tla/install_deps.py
-
-      - name: MCccfraft.cfg
-        run: |
-          cd tla/
-          ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
-
-      - name: MCccfraftAtomicReconfig.cfg
-        run: |
-          cd tla/
-          ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json
-
-      - name: MCccfraftWithReconfig.cfg
-        run: |
-          cd tla/
-          ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.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
-
   simulation-consensus:
     name: Simulation - Consensus
     runs-on: ubuntu-latest