第2章 TLAplus基础

2. TLA⁺基础：语言简介、规范结构与模块扩展

好，咱们进入正题。TLA⁺这门语言，说实话第一眼看上去有点怪——数学符号、逻辑表达式，跟咱们平时写的Java、Go完全不是一回事。但别被它吓到，说白了它就是个描述系统行为的数学语言。

我个人习惯把TLA⁺比作「系统的X光机」。代码只能看到实现细节，而TLA⁺能让你看到系统的本质行为。嗯，咱们先看看它长什么样。

2.1 TLA⁺语言简介

TLA⁺的全称是Temporal Logic of Actions，中文叫「动作时序逻辑」。名字听着唬人，核心就两样东西：状态和动作。

状态：系统在某个时刻的快照。比如变量x=3, y=true
动作：从一个状态到另一个状态的转换。比如x' = x + 1

我在项目中遇到过不少同事，上来就想用TLA⁺写复杂的并发算法。结果连状态和动作都没分清楚，写出来的规范根本跑不通。所以咱们先打好基础。

TLA⁺的语法其实很简洁。核心运算符就那么几个：

∧  逻辑与
∨  逻辑或
¬  逻辑非
⇒  蕴含
⇔  等价
'  下一个状态（prime）
[] 总是（always）
◇ 最终（eventually）

你想想看，就靠这些符号，就能描述任何分布式系统的行为。是不是有点意思？

我的小技巧：刚开始写TLA⁺时，别急着写复杂逻辑。先画状态机，把状态和动作列出来，再翻译成TLA⁺。这样不容易出错。

2.2 TLA⁺规范结构

一个完整的TLA⁺规范，通常包含这几个部分。我习惯按这个顺序组织：

模块声明：用---- MODULE 名字 ----开头
扩展语句：引入需要的标准库
常量与变量：定义系统的参数和状态变量
类型定义：用TypeOK定义不变量
初始状态：用Init定义系统起点
动作定义：用Next定义所有可能的转换
规范：用Spec == Init ∧ □[Next]_vars组合起来
属性：用THEOREM或PROPERTY声明要验证的性质

来看个最简单的例子——一个计数器：

---- MODULE Counter ----
EXTENDS Naturals

VARIABLE x

Init == x = 0

Increment == x' = x + 1

Decrement == x' = x - 1

Next == Increment ∨ Decrement

Spec == Init ∧ □[Next]_x

TypeOK == x ∈ Nat

THEOREM Spec ⇒ □TypeOK
====

这段代码描述了一个计数器，可以加一或减一。注意看Spec那行——□[Next]_x的意思是「每一步要么执行Next里的动作，要么x保持不变」。这个叫步进逻辑，是TLA⁺的精髓。

关键理解：TLA⁺的规范不是程序，而是约束。它不告诉你「怎么做」，只告诉你「什么行为是允许的」。这跟编程语言的思维方式完全不同。

2.3 模块与扩展

写复杂系统时，把所有代码塞一个文件里肯定不行。TLA⁺提供了模块化机制，跟Java的package、Python的module类似。

常用的标准模块有这些：

模块名	用途	我常用的函数
Naturals	自然数	+, -, *, ÷, ≤, ≥
Integers	整数	..（区间）, Abs
Sequences	序列（类似数组）	Len, Append, Head, Tail
FiniteSets	有限集合	Cardinality, Union, Intersection
TLC	模型检查配置	模型检查参数设置

扩展模块用EXTENDS关键字：

EXTENDS Naturals, Sequences, TLC

如果你要复用自己写的规范，用INSTANCE：

---- MODULE MyProtocol ----
EXTENDS Naturals

VARIABLE msg

Init == msg = 0
Send == msg' = msg + 1

====

---- MODURE Main ----
EXTENDS Naturals
MyProtocolInstance == INSTANCE MyProtocol

VARIABLE state
Init == state = "idle"
Next == state' = "running"

====

我曾经犯过一个低级错误——在多个模块里定义了同名的变量，结果模型检查时死活跑不通。后来才发现是命名冲突。所以我的建议是：模块命名要有前缀，避免冲突。

避坑指南：我曾经在扩展模块时用了EXTENDS而不是INSTANCE，导致所有变量都变成了全局的。记住：EXTENDS是「复制粘贴」，INSTANCE是「实例化」。前者会污染命名空间，后者更安全。

2.4 知识体系总览

为了让你更直观地理解TLA⁺的规范结构，我画了张图：

这张图展示了一个TLA⁺规范的标准骨架。从上到下依次是：模块声明、扩展、常量变量、类型不变量、初始状态、动作、规范组合、属性验证。每个部分都有明确的职责。

嗯，到这里TLA⁺的基础就讲完了。说白了就是三件事：描述状态、描述动作、组合成规范。模块化帮你组织代码，扩展让你复用已有的东西。下一章咱们会深入TLA⁺的时序逻辑，看看怎么描述「系统最终会怎样」这类性质。

一句话总结：TLA⁺规范 = 状态 + 动作 + 时序约束。模块化是组织手段，扩展是复用机制。掌握这三样，你就能开始写自己的第一个规范了。

公众号:蓝海资料掘金营，微信deep3321

📚 课程目录

2. TLA⁺基础：语言简介、规范结构与模块扩展

2.1 TLA⁺语言简介

2.2 TLA⁺规范结构

2.3 模块与扩展

2.4 知识体系总览