Move model checking to main CI pipeline

.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') }}:

.azure-pipelines-templates/model_checking.yml

@@ -0,0 +1,38 @@
+jobs:
+  - job: Model_Checking
+    displayName: "Model Checking"
+    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 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())

.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