安装
brew install --cask tla+-toolbox
案例——判断死锁
------------------------------ MODULE deadlock ------------------------------
EXTENDS Integers
VARIABLES locks, locksA, locksB
Init ==
/\ locks = {}
/\ locksA = {}
/\ locksB = {}
A_REQUIRE_LOCK_1 ==
/\ ~(1 \in locks)
/\ locks' = locks \cup {1}
/\ locksA' = locksA \cup {1}
/\ locksB' = locksB
A_REQUIRE_LOCK_2 ==
/\ 1 \in locksA
/\ ~(2 \in locks)
/\ locks' = locks \cup {2}
/\ locksA' = locksA \cup {2}
/\ locksB' = locksB
B_REQUIRE_LOCK_1 ==
/\ 2 \in locksB
/\ ~(1 \in locks)
/\ locks' = locks \cup {1}
/\ locksB' = locksB \cup {1}
/\ locksA' = locksA
B_REQUIRE_LOCK_2 ==
/\ ~(2 \in locks)
/\ locks' = locks \cup {2}
/\ locksB' = locksB \cup {2}
/\ locksA' = locksA
Next == A_REQUIRE_LOCK_1
\/ A_REQUIRE_LOCK_2
\/ A_REQUIRE_LOCK_1
\/ A_REQUIRE_LOCK_2
Spec == Init /\ [][Next]_<<locks, locksA, locksB>>
=============================================================================
\* Modification History
\* Last modified Wed Aug 06 12:14:05 CST 2025 by lucas
\* Created Wed Aug 06 12:05:08 CST 2025 by lucas
本质上就是用 latex 的语法去写状态机的状态转移表达式，包括状态转移条件，以及下一个状态。注意每个状态都需要在状态转移表达式中声明（即便没有发生变化，如 locksA' = locksA）
成功检测到了死锁：