Iteration on TLC wrapper script #5

Workflow file for this run

.github/workflows/ci-verification.yml at 39f2fcd

	name: "Continuous 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
	- name: Install TLC dependencies
	run: \|
	sudo apt update
	sudo apt install -y default-jre
	python3 ./tla/install_deps.py

	- name: consistency/MCSingleNode.cfg
	run: \|
	cd tla/
	./tlc.py consistency/MCSingleNode.tla

	- name: consistency/MCSingleNodeReads.cfg
	run: \|
	cd tla/
	./tlc.py consistency/MCSingleNodeReads.tla

	- name: consistency/MCMultiNode.cfg
	run: \|
	cd tla/
	./tlc.py consistency/MCMultiNode.tla

	- name: consistency/MCMultiNodeReads.cfg
	run: \|
	cd tla/
	./tlc.py consistency/MCMultiNodeReads.tla

	- name: consistency/MCMultiNodeReadsAlt.cfg
	run: \|
	cd tla/
	./tlc.py consistency/MCMultiNodeReadsAlt.tla

	- 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-model-checking-consistency
	path: \|
	tla/consistency/_TTrace_.tla
	tla/*.json

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

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

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

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

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

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

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

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

	- name: consistency/MultiNodeReads.cfg
	run: \|
	cd tla/
	./tlc.py --simulate num=500 --depth 50 consistency/MultiNodeReads.tla

	- name: Upload traces in TLA and JSON format
	uses: actions/upload-artifact@v4
	if: ${{ failure() }}
	with:
	name: tlc-simulation-consistency
	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
	- name: Install TLC dependencies
	run: \|
	sudo apt update
	sudo apt install -y default-jre
	python3 ./tla/install_deps.py

	- name: MCabs.cfg
	run: \|
	set -x
	cd tla/
	./tlc.py consensus/MCabs.tla

	- name: MCccfraft - Configurations=1C2N
	run: \|
	set -x
	cd tla/
	Configurations=1C2N MaxTermLimit=2 RequestLimit=3 ./tlc.py --trace-name MCccfraft1C2NT2R3 consensus/MCccfraft.tla

	- name: MCccfraft - Configurations=1C3N
	run: \|
	set -x
	cd tla/
	Configurations=1C3N MaxTermLimit=2 RequestLimit=3 ./tlc.py --trace-name MCccfraft1C3N2T3R consensus/MCccfraft.tla

	- 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-model-checking-consensus
	path: \|
	tla/consensus/_TTrace_.tla
	tla/*.json

	simulation-consensus:
	name: Simulation - Consensus
	runs-on: ubuntu-latest

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

	- name: Simulation
	run: \|
	set -x
	cd tla/
	./tlc.py --simulate num=100 consensus/SIMccfraft.tla

	- name: Upload artifacts.
	uses: actions/upload-artifact@v4
	if: ${{ failure() }}
	with:
	name: tlc-simulation-consensus
	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
	- name: Install TLC dependencies
	run: \|
	sudo apt update
	sudo apt install -y default-jre parallel
	python3 ./tla/install_deps.py

	- 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 './tlc.py --workers 1 --dfs --driver-trace {} --dot --trace-name {} consensus/Traceccfraft.tla' ::: $(ls traces/consensus/*.ndjson)
	shell: bash

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Iteration on TLC wrapper script #5

Workflow file

Iteration on TLC wrapper script #5

Jobs

Run details

Workflow file for this run