Update CheckQuorum condition from quorum in any config to quorum in every active config #3643
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: "Long Verification" | |
| on: | |
| pull_request: | |
| types: | |
| - labeled | |
| - synchronize | |
| - opened | |
| - reopened | |
| schedule: | |
| - cron: "0 0 * * 0" | |
| workflow_dispatch: | |
| permissions: read-all | |
| jobs: | |
| model-checking-with-atomic-reconfig-consensus: | |
| name: Model Checking With Atomic Reconfig - Consensus | |
| if: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }} | |
| runs-on: | |
| [ | |
| self-hosted, | |
| 1ES.Pool=gha-vmss-d16av5-ci, | |
| "JobId=long_mc_atomic_reconfig-${{ github.run_id }}-${{ github.run_number }}-${{ github.run_attempt }}", | |
| ] | |
| container: | |
| image: mcr.microsoft.com/azurelinux/base/core:3.0 | |
| options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE | |
| steps: | |
| - name: "Checkout dependencies" | |
| shell: bash | |
| run: | | |
| gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY | |
| tdnf -y update | |
| tdnf -y install ca-certificates git | |
| - uses: actions/checkout@v5 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py --skip-apt-packages | |
| - run: cd tla && ./tlc.py --trace-name 2C2N mc --term-count 2 --request-count 0 --raft-configs 2C2N --disable-check-quorum consensus/MCccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-with-atomic-reconfig-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| model-checking-with-reconfig-consensus: | |
| name: Model Checking With Reconfig - Consensus | |
| if: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }} | |
| runs-on: | |
| [ | |
| self-hosted, | |
| 1ES.Pool=gha-vmss-d16av5-ci, | |
| "JobId=long_mc_reconfig-${{ github.run_id }}-${{ github.run_number }}-${{ github.run_attempt }}", | |
| ] | |
| container: | |
| image: mcr.microsoft.com/azurelinux/base/core:3.0 | |
| options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE | |
| steps: | |
| - name: "Checkout dependencies" | |
| shell: bash | |
| run: | | |
| gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY | |
| tdnf -y update | |
| tdnf -y install ca-certificates git | |
| - uses: actions/checkout@v5 | |
| - name: Install TLC dependencies | |
| run: | | |
| tdnf install -y jre wget | |
| python3 tla/install_deps.py --skip-apt-packages | |
| - run: cd tla && ./tlc.py --trace-name 3C2N mc --term-count 2 --request-count 0 --raft-configs 3C2N --disable-check-quorum consensus/MCccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-model-checking-with-reconfig-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json | |
| simulation-consensus: | |
| name: Simulation - Consensus | |
| if: ${{ contains(github.event.pull_request.labels.*.name, 'run-long-verification') || github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }} | |
| runs-on: ubuntu-latest | |
| defaults: | |
| run: | |
| working-directory: tla | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - run: | | |
| sudo apt update | |
| sudo apt install -y default-jre | |
| python3 install_deps.py | |
| - run: ./tlc.py sim --max-seconds 3000 --depth 500 consensus/SIMccfraft.tla | |
| - name: Upload TLC traces | |
| uses: actions/upload-artifact@v4 | |
| if: ${{ failure() }} | |
| with: | |
| name: tlc-simulation-consensus | |
| path: | | |
| tla/consensus/*_TTrace_*.tla | |
| tla/*.json |