4. TLAplus建模实战：用TLA+建模一个简单的计数器系统
好，咱们今天来点真格的。
前面聊了那么多理论，什么TLA+和RTLA的区别，什么形式化验证的价值。但说实话，光说不练假把式。这一章，我就带你亲手用TLA+建模一个最简单的系统——计数器。
你别小看计数器。我当年刚接触TLA+时，就是从这个例子入门的。它麻雀虽小，五脏俱全。你把它吃透了，后面那些分布式共识算法、缓存一致性协议，理解起来就顺了。
4.1 我们要建模什么？
一个计数器，说白了就是一个整数变量，支持两个操作：自增和读取。
听起来简单吧？但你要用形式化语言把它描述清楚，就没那么简单了。你得定义：
- 计数器的初始值是什么？
- 自增操作怎么改变状态？
- 读取操作返回什么？
- 系统允许哪些行为序列？
嗯，这里要注意：TLA+建模的不是“程序怎么运行”，而是“系统允许哪些行为”。这是思维上的一个坎，迈过去就好了。
核心思想：TLA+描述的是系统所有可能的行为轨迹，而不是某一条具体的执行路径。
4.2 第一个TLA+规范：从零开始
好，我们直接上代码。这是计数器最基础的TLA+规范：
---- MODULE Counter ----
EXTENDS Naturals
VARIABLE counter
Init == counter = 0
Increment == counter' = counter + 1
Read == TRUE
Next == Increment \/ Read
Spec == Init /\ [][Next]_counter
====我来一行行拆解给你看。
EXTENDS Naturals：引入自然数模块。TLA+本身没有内置整数，你得显式引入。我刚开始写的时候老忘这行，结果报错半天找不到原因。
VARIABLE counter：声明一个变量叫counter。注意，TLA+里变量是全局的，没有局部变量这个概念。这是和编程语言很大的不同。
Init == counter = 0：定义初始状态。counter等于0。这里的==是“定义为”的意思，不是赋值。
Increment == counter' = counter + 1：自增操作。注意那个counter'，带撇号表示“下一个状态的值”。整句话的意思是：下一个状态中，counter的值等于当前状态的值加1。
Read == TRUE：读取操作。它不改变任何变量，所以条件就是TRUE——永远可以执行。
Next == Increment \/ Read：下一步要么自增，要么读取。这是系统的所有可能动作。
Spec == Init /\ [][Next]_counter：完整的规范。初始状态满足Init，并且每一步要么执行Next，要么保持counter不变（这是[]和下标_counter的含义）。
个人经验：我见过很多新手把Next写成Increment /\ Read，用AND代替OR。结果系统永远只能同时做两件事，这显然不对。记住：\/是“或”，/\是“与”。
4.3 运行模型检查：让TLC帮你找bug
规范写完了，怎么验证它是对的？用TLC模型检查器。
你需要在规范里加一行配置：
====
\* 下面是模型检查的配置
INVARIANT counter >= 0
====这个不变量是说：counter永远不能小于0。你想想看，如果系统里有人执行了counter' = counter - 1，那这个检查就会报错。
我当年第一次跑TLC时，看到那个绿色的“No error found”，心里那个爽啊。但别高兴太早——TLC只能检查有限状态。如果你的计数器没有上限，理论上状态是无限的。你需要设置一个边界，比如：
CONSTANT MaxCounter = 100
然后修改Increment：
Increment == counter < MaxCounter /\ counter' = counter + 1
这样TLC就能在有限空间里检查了。
避坑指南：我曾经犯过一个错误——忘了加边界条件，结果TLC跑了两个小时还没跑完。后来才发现状态空间爆炸了。记住：模型检查不是万能的，你得给它一个合理的边界。
4.4 增加复杂度：多线程计数器
单线程的计数器太简单了。咱们来点挑战——两个线程同时操作同一个计数器。
在TLA+里，多线程就是多个动作的交替执行：
---- MODULE ConcurrentCounter ----
EXTENDS Naturals
VARIABLE counter, thread1_done, thread2_done
Init == counter = 0 /\ thread1_done = FALSE /\ thread2_done = FALSE
Thread1Increment == ~thread1_done /\ counter' = counter + 1 /\ thread1_done' = TRUE /\ UNCHANGED thread2_done
Thread2Increment == ~thread2_done /\ counter' = counter + 1 /\ thread2_done' = TRUE /\ UNCHANGED thread1_done
Next == Thread1Increment \/ Thread2Increment
Spec == Init /\ [][Next]_<>
==== 这里我引入了两个布尔变量，标记每个线程是否已经执行过。每个线程只能自增一次。
你猜最终counter的值是多少？
如果两个线程都执行了，counter应该是2。但如果TLC检查时发现counter可能等于1，那就说明有线程没执行——规范有问题。
关键点：并发系统的核心问题是“交错”。TLA+天然支持所有可能的交错序列，这正是它的威力所在。
4.5 用SVG画一张流程图
说了这么多，咱们用一张图把计数器的建模流程串起来：
4.6 验证结果怎么看？
TLC跑完之后，会给你一个报告。我总结一下常见的几种结果：
| 结果 | 含义 | 怎么办？ |
|---|---|---|
| No error found | 在检查的边界内，所有不变量都成立 | 恭喜！但别忘了扩大边界再测一次 |
| Invariant violation | 某个不变量被违反了 | 查看TLC给出的反例轨迹，找到哪一步出了问题 |
| Deadlock detected | 系统卡住了，没有下一步可执行 | 检查Next公式，是不是漏了某个动作？ |
| State space exhausted | 状态太多，TLC跑不完 | 缩小边界，或者用对称性减少状态 |
我的习惯：每次修改规范后，先跑一个小边界（比如MaxCounter=5），快速验证逻辑对不对。确认无误后再放大边界。这样能节省大量时间。
4.7 小结：你学到了什么？
这一章，我们亲手建了一个计数器模型。你学会了：
- 怎么声明变量、定义初始状态
- 怎么用
counter'描述状态变化 - 怎么用
Next组合多个动作 - 怎么用TLC做模型检查
- 怎么处理多线程并发
说实话，计数器虽然简单，但它包含了TLA+建模的所有核心要素。你把这个吃透了，后面那些复杂的系统——分布式锁、Raft共识算法、两阶段提交——本质上都是在这个基础上做加法。
嗯，下一章咱们会聊一个更实际的例子。但在此之前，我建议你亲手把这段代码敲一遍，跑一跑TLC。纸上得来终觉浅，绝知此事要躬行。
公众号:蓝海资料掘金营，微信deep3321