From 4e80174991ee2181797a4f69af4d58ccc8978918 Mon Sep 17 00:00:00 2001
From: Max Tropets <maxtropets@microsoft.com>
Date: Tue, 16 Jul 2024 14:42:17 +0000
Subject: [PATCH] WIP

---
 .github/workflows/consensus-tla.yml           | 138 ++++++++++++++++++
 .../{tlaplus.yml => consistency-tla.yml}      |   2 +-
 2 files changed, 139 insertions(+), 1 deletion(-)
 create mode 100644 .github/workflows/consensus-tla.yml
 rename .github/workflows/{tlaplus.yml => consistency-tla.yml} (98%)

diff --git a/.github/workflows/consensus-tla.yml b/.github/workflows/consensus-tla.yml
new file mode 100644
index 000000000000..cb6df2d068fd
--- /dev/null
+++ b/.github/workflows/consensus-tla.yml
@@ -0,0 +1,138 @@
+name: "TLA+ Spec Verification - Consensus"
+
+on:
+  schedule:
+    - cron: "0 0 * * 0"
+  pull_request:
+    # TODO update to tla change only / weekly
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  actions: read
+  contents: read
+  security-events: write
+
+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:2024-06-26-virtual-clang15
+
+    steps:
+      - uses: actions/checkout@v4
+      - 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/
+          JVM_OPTIONS=-Dtlc2.TLCGlobals.coverage=1 ./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/
+          JVM_OPTIONS=-Dtlc2.TLCGlobals.coverage=1 ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
+
+      - name: Coverage
+        run: |
+          cd tla/
+          python3 -mvenv env
+          source env/bin/activate
+          pip install -r requirements.txt
+          ls -tr MCccfraftAtomicReconfig_coverage.json | xargs cat | python3 actions.py MCccfraftAtomicReconfig.html
+          rm MCccfraftAtomicReconfig_coverage.json
+          ls -tr MCccfraftWithReconfig_coverage.json | xargs cat | python3 actions.py MCccfraftWithReconfig.html
+          rm MCccfraftWithReconfig_coverage.json
+          deactivate
+          rm -rf env
+
+      - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
+        uses: actions/upload-artifact@v4
+        if: ${{ failure() }}
+        with:
+          name: tlc
+          path: |
+            tla/consensus/*_TTrace_*.tla
+            tla/*.json
+
+  simulation-consensus:
+    name: Simulation - Consensus
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - run: |
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
+
+      - name: Simulation
+        run: |
+          cd tla/
+
+          ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
+        env:
+          SIM_TIMEOUT: 6000  # TODO parametrise outside?..
+
+      # TODO upload artifacts?..
+
+  trace-validation:
+    name: Trace Validation - Consensus
+    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
+    container:
+      image: ccfmsrc.azurecr.io/ccf/ci:2024-06-26-virtual-clang15
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - run: |
+          sudo apt update
+          sudo apt install -y default-jre parallel
+          python3 ./tla/install_deps.py
+
+      # TODO reuse build+test?..
+
+      - name: "Build"
+        run: |
+          git config --global --add safe.directory /__w/CCF/CCF
+          mkdir build
+          cd build
+          cmake -GNinja -DCOMPILE_TARGET=virtual ..
+          ninja
+        shell: bash
+
+      - name: "Test ${{ matrix.platform.name }}"
+        run: |
+          cd build
+          rm -rf /github/home/.cache
+          mkdir -p /github/home/.cache
+          export ASAN_SYMBOLIZER_PATH=$(realpath /usr/bin/llvm-symbolizer-15)
+          # Unit tests
+          ./tests.sh --output-on-failure -L unit -j$(nproc --all)
+          # All other acceptably fast tests, mostly end-to-end
+          ./tests.sh --timeout 360 --output-on-failure -LE "benchmark|perf|protocolstest|vegeta|suite|unit"
+          # Partitions tests
+          ./tests.sh --timeout 240 --output-on-failure -L partitions -C partitions
+        shell: bash
+
+      - name: Run trace validation
+        run: |
+          cd tla/
+          mkdir -p traces/consensus
+          mv ../build/consensus traces/
+          parallel 'JVM_OPTIONS=-Dtlc2.tool.queue.IStateQueue=StateDeque JSON={} ./tlc.sh -dump dot,constrained,colorize,actionlabels {}.dot -dumpTrace tla {}.trace.tla -dumpTrace json {}.trace.json consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
+
+        # TODO upload artifacts?..
diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/consistency-tla.yml
similarity index 98%
rename from .github/workflows/tlaplus.yml
rename to .github/workflows/consistency-tla.yml
index de42cf1dd728..02b63738a3b1 100644
--- a/.github/workflows/tlaplus.yml
+++ b/.github/workflows/consistency-tla.yml
@@ -1,4 +1,4 @@
-name: "TLA+ Spec Verification"
+name: "TLA+ Spec Verification - Consistency"
 
 on:
   schedule: