2. 准备工具

1. 装 Java 11 或更新的版本。 我在盒子上用的是 Temurin 21。pstack 自己固定用 Java 25，两者跑这些小例子结果一样。
2. 下载 tla2tools.jar。 从 https://github.com/tlaplus/tlaplus/releases 下载。我用的是 v1.7.4，TLC 自报版本 “TLC2 Version 2.19”。
3. 每个例子两份文件。 X.tla 是规格，X.cfg 是配置：告诉 TLC 从哪个公式开始、检查哪些规则。
4. 运行。 java -cp tla2tools.jar tlc2.TLC -config X.cfg X.tla。配套压缩包（tla.zip）里的 run-all.sh 会把下面所有例子按顺序跑一遍。

输出的开头几行是版本、内存和一条“建议用 -XX:+UseParallelGC”的提示，可以忽略。下面只贴关键行。连续快速跑好几次时，TLC 可能报“目录已存在”，这时加 -metadir /tmp/某个新目录 就好，我跑的时候加了 -workers 1 -metadir ...。