dimgigov
cd46edcb67
CI / test (push) Has been cancelled
CI / verify (push) Has been cancelled
Clients CI / build-server (push) Has been cancelled
Clients CI / test-python (push) Has been cancelled
Clients CI / test-javascript (push) Has been cancelled
Clients CI / test-nim (push) Has been cancelled
Clients CI / test-rust (push) Has been cancelled
Storage fixes: - Fix bloom filter hash2 OverflowDefect (uint64 instead of int Hash) - Fix MemTable.put size calculation on overwrite (was leaking size) - Fix fuzz_test duplicate-key issues in LSM delete and SSTable tests Test fixes: - Fix stress_test.nim: replace deprecated threadpool with std/threads - Fix fuzz_test.nim: add missing imports (tables, algorithm, sets) - Fix fuzz_test.nim: var sst for close() compatibility - Remove unused imports from test_all.nim and bench_all.nim Docker / CI fixes: - Fix Dockerfile.source: invalid nimlang/nim:2.2.10-alpine tag → 2.2.10 + ubuntu:24.04 runtime - Fix Dockerfile.source healthcheck (--spider → -qO- for 200 OK) - Fix Dockerfile run comment ports (9470/9471 → 9912/9913) - Fix scripts/docker-run.sh healthcheck port (9470 → 9912) - Add ARG BUILD_DATE/VCS_REF to Dockerfile for docker-build.sh - Update all version strings 1.1.4 → 1.1.6 across nimble/docker/source/docs
41 lines
1.5 KiB
Bash
Executable File
41 lines
1.5 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# BaraDB Formal Verification Suite — Run All TLC Model Checks
|
|
set -euo pipefail
|
|
|
|
SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
|
|
JAR="$SCRIPT_DIR/tla2tools.jar"
|
|
|
|
if [ ! -f "$JAR" ]; then
|
|
echo "ERROR: tla2tools.jar not found at $JAR"
|
|
echo "Download from https://github.com/tlaplus/tlaplus/releases"
|
|
exit 1
|
|
fi
|
|
|
|
run_tlc() {
|
|
local spec="$1"
|
|
local cfg="$2"
|
|
echo "=============================================="
|
|
echo " TLC: $spec (cfg: $cfg)"
|
|
echo "=============================================="
|
|
java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -workers auto -config "$cfg" "$spec" 2>&1 | tail -5
|
|
echo ""
|
|
}
|
|
|
|
echo "=============================================="
|
|
echo " BaraDB Formal Verification Suite v1.1.6"
|
|
echo " Running TLC model checker on all specs"
|
|
echo "=============================================="
|
|
echo ""
|
|
|
|
run_tlc "$SCRIPT_DIR/raft.tla" "$SCRIPT_DIR/models/raft.cfg"
|
|
run_tlc "$SCRIPT_DIR/twopc.tla" "$SCRIPT_DIR/models/twopc.cfg"
|
|
run_tlc "$SCRIPT_DIR/mvcc.tla" "$SCRIPT_DIR/models/mvcc.cfg"
|
|
run_tlc "$SCRIPT_DIR/replication.tla" "$SCRIPT_DIR/models/replication.cfg"
|
|
run_tlc "$SCRIPT_DIR/gossip.tla" "$SCRIPT_DIR/models/gossip.cfg"
|
|
run_tlc "$SCRIPT_DIR/deadlock.tla" "$SCRIPT_DIR/models/deadlock.cfg"
|
|
run_tlc "$SCRIPT_DIR/sharding.tla" "$SCRIPT_DIR/models/sharding.cfg"
|
|
run_tlc "$SCRIPT_DIR/backup.tla" "$SCRIPT_DIR/models/backup.cfg"
|
|
run_tlc "$SCRIPT_DIR/recovery.tla" "$SCRIPT_DIR/models/recovery.cfg"
|
|
|
|
echo "All verification runs completed."
|