tlaplus.yml

name: "Verification"

on:
  schedule:
    - cron: "0 0 * * 0"
  pull_request:
    paths:
      - "tla/**"
      - "src/consensus/**"
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

permissions:
  actions: read
  contents: read
  security-events: write

jobs:
  model-checking-consistency:
    name: Model Checking - Consistency
    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
    container:
      image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024

    steps:
      - uses: actions/checkout@v4
      - run: |
          sudo apt update
          sudo apt install -y default-jre
          python3 ./tla/install_deps.py

      - name: consistency/MCSingleNode.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto consistency/MCSingleNode.tla -dumpTrace json MCSingleNode.json

      - name: consistency/MCSingleNodeReads.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto consistency/MCSingleNodeReads.tla -dumpTrace json MCSingleNodeReads.json

      - name: consistency/MCMultiNode.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto consistency/MCMultiNode.tla -dumpTrace json MCMultiNode.json

      - name: consistency/MCMultiNodeReads.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto consistency/MCMultiNodeReads.tla -dumpTrace json MCMultiNodeReads.json

      - name: consistency/MCMultiNodeReadsAlt.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto consistency/MCMultiNodeReadsAlt.tla -dumpTrace json MCMultiNodeReadsAlt.json

      - 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/consistency/*_TTrace_*.tla
            tla/*.json

  counterexamples-consistency:
    name: Counterexamples - Consistency
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v4
      - run: python3 ./tla/install_deps.py

      - name: consistency/MCSingleNodeCommitReachability.cfg
        run: |
          cd tla/
          ./tlc_debug.sh -workers auto -config consistency/MCSingleNodeCommitReachability.cfg consistency/MCSingleNodeReads.tla

      - name: consistency/MCMultiNodeCommitReachability.cfg
        run: |
          cd tla/
          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeCommitReachability.cfg consistency/MCMultiNodeReads.tla

      - name: consistency/MCMultiNodeInvalidReachability.cfg
        run: |
          cd tla/
          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeInvalidReachability.cfg consistency/MCMultiNodeReads.tla

      - name: consistency/MCMultiNodeReadsNotLinearizable.cfg
        run: |
          cd tla/
          ./tlc_debug.sh -workers auto -config consistency/MCMultiNodeReadsNotLinearizable.cfg consistency/MCMultiNodeReads.tla

  simulation-consistency:
    name: Simulation - Consistency
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v4
      - run: python3 ./tla/install_deps.py

      - name: consistency/MultiNodeReads.cfg
        run: |
          cd tla/
          ./tlc.sh -workers auto -simulate num=500 -depth 50 consistency/MultiNodeReads.tla -dumpTrace json MultiNodeReads.json

      - name: Upload traces in TLA and JSON format
        uses: actions/upload-artifact@v4
        if: ${{ failure() }}
        with:
          name: tlc
          path: |
            tla/consistency/*_TTrace_*.tla
            tla/*.json

  model-checking-consensus:
    name: Model Checking - Consensus
    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
    container:
      image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024

    steps:
      - uses: actions/checkout@v4
      - run: |
          sudo apt update
          sudo apt install -y default-jre
          python3 ./tla/install_deps.py

      - name: MCabs.cfg
        run: |
          set -x
          cd tla/
          ./tlc.sh -workers auto consensus/MCabs.tla -dumpTrace tla MCabs.trace.tla -dumpTrace json MCabs.json

      - name: MCccfraft.cfg
        run: |
          set -x
          cd tla/
          ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json

      - name: MCccfraftAtomicReconfig.cfg
        run: |
          set -x
          cd tla/
          ./tlc.sh -workers auto -config consensus/MCccfraftAtomicReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftAtomicReconfig.trace.tla -dumpTrace json MCccfraftAtomicReconfig.json

      - 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

  model-checking-with-reconfig-consensus:
    name: Model Checking With Reconfig - Consensus
    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
    container:
      image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024

    steps:
      - uses: actions/checkout@v4
      - run: |
          sudo apt update
          sudo apt install -y default-jre
          python3 ./tla/install_deps.py

      - name: MCccfraftWithReconfig.cfg
        run: |
          set -x
          cd tla/
          ./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json

      - 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: |
          set -x
          cd tla/
          ./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
        env:
          SIM_TIMEOUT: 3000

      - name: Upload artifacts.
        uses: actions/upload-artifact@v4
        if: ${{ failure() }}
        with:
          name: tlc
          path: |
            tla/*

  trace-validation-consensus:
    name: Trace Validation - Consensus
    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
    container:
      image: ghcr.io/microsoft/ccf/ci/default:build-25-07-2024

    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
        shell: bash

      - name: "Build"
        run: |
          git config --global --add safe.directory /__w/CCF/CCF
          mkdir build
          cd build
          cmake -L -GNinja .. -DCMAKE_BUILD_TYPE=Debug -DLVI_MITIGATIONS=OFF -DVERBOSE_LOGGING=ON -DCOMPILE_TARGET=virtual -DCCF_RAFT_TRACING=ON
          ninja raft_driver
        shell: bash

      - name: "Test"
        run: |
          set -x
          cd build
          rm -rf /github/home/.cache
          mkdir -p /github/home/.cache
          ./tests.sh -VV --timeout --no-compress-output -T Test -L raft_scenario
        shell: bash

      - name: Run trace validation
        run: |
          set -x
          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)
        shell: bash

      - name: Upload artifacts.
        uses: actions/upload-artifact@v4
        if: always()
        with:
          name: tlc
          path: |
            tla/traces/*