a2f7b7b2e9
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 2s
- check-dist.sh: Prevents DIST DESYNC by verifying all dist/*.js files
are newer than their src/*.ts sources. Fails build if stale.
- Makefile: Standard build targets (build/check-dist/test/recompile/clean)
- src/index.ts: Integrated dist freshness check before compilation
- src/parser.ts: Added List<T> type parsing alongside existing Set<T>/Map<K,V>
(e.g., 'log: List<LogEntry>' now parses as { type: 'list', elementType })
- examples/: Restored v0.3 state machine specs (TigerBeetleLedger,
AccountLedger, ToggleSwitch, TwoPhaseCommit)
- DIST DESYNC is a known recurring anti-pattern — this guard prevents it
Tests: 39/41 pass (2 pre-existing E2E WASM failures due to missing wabt)
97 lines
2.7 KiB
Text
97 lines
2.7 KiB
Text
speck TwoPhaseCommit {
|
|
// TLA+ classic: Two-Phase Commit protocol ported to SpeckDL v0.3
|
|
// Demonstrates Map types, Set operations, and complex action bodies
|
|
// Adapted from https://lamport.azurewebsites.net/tla/two-phase.html
|
|
|
|
state {
|
|
// Resource Manager state: RM id → "working" | "prepared" | "committed" | "aborted"
|
|
rmState: Map(String, String)
|
|
|
|
// Transaction Manager state
|
|
tmState: String
|
|
|
|
// Set of RMs that have sent Prepared
|
|
tmPrepared: Set(String)
|
|
|
|
// Messages in transit
|
|
msgs: Set(Message)
|
|
|
|
// Set of all RM ids
|
|
rms: Set(String)
|
|
}
|
|
|
|
init {
|
|
let allRms := {"rm1", "rm2", "rm3"}
|
|
|
|
rms == allRms
|
|
rmState == mapKeys(allRms, "working")
|
|
tmState == "init"
|
|
tmPrepared == emptySet
|
|
msgs == emptySet
|
|
}
|
|
|
|
invariant TPTypeOK {
|
|
rmState.values subsetOf {"working", "prepared", "committed", "aborted"}
|
|
tmState in {"init", "committed", "aborted"}
|
|
tmPrepared subsetOf rms
|
|
}
|
|
|
|
invariant TPConsistency {
|
|
tmState == "committed" implies forall rm in rms: rmState[rm] == "committed"
|
|
tmState == "aborted" implies forall rm in rms: rmState[rm] == "aborted"
|
|
forall rm in rms:
|
|
rmState[rm] == "committed" implies tmState != "aborted"
|
|
forall rm in rms:
|
|
rmState[rm] == "prepared" implies tmState in {"init", "committed"}
|
|
}
|
|
|
|
action RMPrepare(rm: String) {
|
|
require rm in rms
|
|
require rmState[rm] == "working"
|
|
|
|
rmState[rm] := "prepared"
|
|
msgs := msgs union {{ type: "Prepared", rm: rm }}
|
|
emit Prepared { rm: rm }
|
|
}
|
|
|
|
action TMRcvPrepared(rm: String) {
|
|
require tmState == "init"
|
|
require { type: "Prepared", rm: rm } in msgs
|
|
require rm in rms
|
|
|
|
tmPrepared := tmPrepared union {rm}
|
|
}
|
|
|
|
action TMCommit {
|
|
require tmState == "init"
|
|
require tmPrepared == rms
|
|
|
|
tmState := "committed"
|
|
msgs := msgs union {{ type: "Commit" }}
|
|
forall rm in rms:
|
|
rmState[rm] := "committed"
|
|
emit AllCommitted {}
|
|
}
|
|
|
|
action TMAbort {
|
|
require tmState == "init"
|
|
|
|
tmState := "aborted"
|
|
msgs := msgs union {{ type: "Abort" }}
|
|
forall rm in rms:
|
|
if rmState[rm] != "committed":
|
|
rmState[rm] := "aborted"
|
|
emit Aborted {}
|
|
}
|
|
|
|
action RMChooseToAbort(rm: String) {
|
|
require rm in rms
|
|
require rmState[rm] == "working"
|
|
require tmState == "init"
|
|
|
|
rmState[rm] := "aborted"
|
|
emit RMAborted { rm: rm }
|
|
}
|
|
|
|
next: RMPrepare | TMRcvPrepared | TMCommit | TMAbort | RMChooseToAbort
|
|
}
|