Skip to content

ccfraft!AdvanceCommitIndex advance to the smalles possible index, whereas raft.h advances to the largest possible one. #1012

ccfraft!AdvanceCommitIndex advance to the smalles possible index, whereas raft.h advances to the largest possible one.

ccfraft!AdvanceCommitIndex advance to the smalles possible index, whereas raft.h advances to the largest possible one. #1012

Workflow file for this run

name: "TLA+ Spec Verification"
on:
push:
paths:
- "tla/**"
pull_request:
paths:
- "tla/**"
workflow_dispatch:
jobs:
model-checking-consistency:
name: Model Checking - Consistency
runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
container:
image: ccfmsrc.azurecr.io/ccf/ci:07-12-2023-virtual-clang15
steps:
- uses: actions/checkout@v3
- 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@v3
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@v3
- 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@v3
- run: python3 ./tla/install_deps.py
- name: consistency/MultiNodeReads.cfg
run: |
cd tla/
./tlc.sh -workers auto -simulate num=5 -depth 50 consistency/MultiNodeReads.tla -dumpTrace json MultiNodeReads.json
- name: Upload traces in TLA and JSON format
uses: actions/upload-artifact@v3
if: ${{ failure() }}
with:
name: tlc
path: |
tla/consistency/*_TTrace_*.tla
tla/*.json