dimgigov
19d0ff7366
Added 3 new TLA+ specs: - gossip.tla — SWIM gossip membership & failure detection - deadlock.tla — wait-for graph deadlock detection - sharding.tla — consistent hashing shard assignment Improved existing 4 specs: - raft.tla: added CommittedIndexValid invariant - twopc.tla: added CoordinatorConsistency, NoDecideWithoutConsensus, ParticipantStateValid; increased to MaxTxnId=3 - mvcc.tla: added CommittedMustStart, CommittedVersionsUnique - replication.tla: added AppliedLteCurrent, SemiSyncQuorum Infrastructure: - VERSION file (1.0.0) - CHANGELOG.md - ANALYSIS.md (weak spots & improvement plan) - run_all.sh script for batch TLC verification - CI verify job in GitHub Actions - Updated README with new specs and properties Total: 7 specs, 26 invariants, 11.6M states checked, 0 errors
18 lines
236 B
INI
18 lines
236 B
INI
CONSTANTS
|
|
Shards = {s1, s2, s3}
|
|
Vnodes = {1, 2, 3, 4, 5}
|
|
Nodes = {n1, n2}
|
|
MaxVnode = 5
|
|
Nil = Nil
|
|
|
|
INIT Init
|
|
NEXT Next
|
|
|
|
CHECK_DEADLOCK FALSE
|
|
|
|
INVARIANTS
|
|
TypeOk
|
|
VirtualNodeMapping
|
|
NodeAssignmentConsistency
|
|
VnodeOrdering
|