Apache Cassandra 中的 TLA 语言参考从模块结构到 TLC 模型检查实战【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra导读TLATemporal Logic of Actions是 Leslie Lamport 提出的形式化规范语言用于对分布式系统、并发协议与状态机进行精确建模与穷举验证。本篇文章以当前仓库中的 TLA 语言参考 为骨架系统讲解 TLA 的模块结构、类型系统、集合与序列运算、时序逻辑与公平性等核心语法并结合仓库内 tla-plus 技能包 的脚本与模板、以及 Cassandra 在 formalise/accord/execution/tla 目录下真实使用的 Accord 形式化规范AccordExec.tla 等进行源码级佐证。读完本文你将掌握从零编写一个可被 TLC 模型检查器验证的 TLA 规范、编写配套 .cfg 配置文件并正确解读 TLC 输出的完整能力。一、模块结构一切规范的组织单元TLA 规范以模块MODULE为基本单位一个.tla文件对应一个模块。当前仓库的 language.md 给出了最精简的骨架---- MODULE ModuleName ---- EXTENDS Integers, Sequences, FiniteSets, TLC CONSTANTS Const1, Const2 VARIABLES var1, var2 \* Operator definitions \* ... 关键规则模块名必须与文件名去掉.tla后缀完全一致。例如仓库中formalise/accord/execution/tla/AccordExec.tla的模块声明是--------------------------- MODULE AccordExec ---------------------------而 examples/Baseline.tla 通过EXTENDS AccordExec继承该模块——这正体现了 TLA 模块即复用单元的机制EXTENDS把被扩展模块的所有定义带入当前模块与 Java 的继承或 Python 的 import 在语义上类似。模块内部按职责分为几个区段EXTENDS引入标准库模块Integers、Sequences、FiniteSets、TLC、Naturals、Bags 等详见下文“标准模块”一节CONSTANTS声明符号常量它们是不变的具体值通常在.cfg配置文件中绑定VARIABLES声明状态变量是系统状态的全部载体其余部分是运算符operator定义即对上述符号的纯函数式操作。仓库的 templates/basic.tla 给出了一个完整的纯 TLA 状态机模板其结构正是EXTENDS→CONSTANTS→VARIABLES→vars ...→Init→ 动作定义 →Next→Spec→ 性质定义可以作为新规范的标准起点。二、类型与值2.1 原语类型类型示例说明整数0、1、-5需要EXTENDS Integers才能使用算术运算字符串hello只能使用和#比较通常作为不透明标识符布尔值TRUE、FALSE逻辑运算的基础模型值在.cfg中定义未解释常量uninterpreted constant用于表示无法穷举的具体对象模型值model value是 TLA 特有的抽象手段当你并不关心某个对象的内部结构只关心它的身份identity时就在.cfg文件中声明Const m1这样的模型值。TLC 会把它当作一个不可分解的原子符号处理。仓库中 Accord 的 Baseline.cfg 就是典型的模型值用法CmdEntries {c1}、KeyEntries {k1, k2}把命令条目与键条目建模为字符串集合而NumTasks 2直接给出整数常量。2.2 复合类型类型示例关键语义集合Set{1, 2, 3}、{}无序、元素唯一、只能容纳同类型元素序列Sequence/Tuple1, 2, 3、有序、1 起始索引结构体Record[name \|- Alice, age \|- 30]通过s.name或s[name]访问字段函数Function[x \in 1..10 \|- x * x]通过f[3]应用这四类复合值是 TLA 建模的全部“数据结构”。值得注意区分集合与序列{1, 2, 3}没有顺序、没有重复元素1, 2, 3有顺序、允许重复。建模消息队列时必须用序列保持 FIFO 顺序建模“在途消息集合”时常用集合。函数与记录记录本质上是定义域为字符串集合的函数[x \in 1..10 \|- x * x]是定义域为1..10、值域为平方值的函数。AccordExec.tla 的头部注释提到“MODELS the queue as its three regions, with the fifo order derived from fifoAt (Q5) rather than from the array that maintains it”这种把数组抽象为函数键→值映射的建模手法正是 TLA 的常态。三、运算符定义TLA 中没有“函数”关键字一切可复用逻辑都用运算符operator表达且没有副作用纯函数式\* 无参运算符常量 MaxSize 10 \* 带参运算符 Max(a, b) IF a b THEN a ELSE b \* LET 引入局部定义 ThreeMax(a, b, c) LET M(x, y) IF x y THEN x ELSE y IN M(M(a, b), c)LET ... IN ...是唯一的局部绑定机制适合在复杂运算符内部定义辅助逻辑。运算符可以被EXTENDS继承例如Baseline.tla中MCTaskTxns {c1}, {c1}这样的定义就是用来给父模块AccordExec的抽象参数提供具体实例的覆写点。四、布尔逻辑与子弹点记号逻辑TLA 符号数学符号与/\∧或\/∨非~¬蕴含⇒当且仅当⇔子弹点记号bullet-point notation是 TLA 最具辨识度的排版它是对空白敏感的垂直布局一组以/\或\/开头的行隐式组合成一个逻辑表达式/\ A /\ \/ B \/ C /\ D \* 含义A /\ (B \/ C) /\ D缩进决定了结合优先级。这是从 Lamport 原版规范延续下来的写作习惯仓库中 AccordExec.tla 的全部动作与不变量都采用这种风格。阅读时把/\行理解为“AND 列表”把\/行理解为“OR 列表”即可。五、集合运算运算语法备注属于x \in S不属于x \notin S子集S \subseteq T并集S \union T交集S \intersect T差集S \ T基数Cardinality(S)需要FiniteSets幂集SUBSET S笛卡尔积S \X T整数区间a..b全部布尔BOOLEAN即{TRUE, FALSE}映射{f(x) : x \in S}对每个元素应用函数过滤{x \in S : P(x)}筛选满足谓词的元素集合是 TLA 对“状态空间”建模的核心。一个典型的映射用法见仓库 templates/distributed.tla 的初始状态node_state [n \in Nodes |- idle]用函数映射给每个节点赋初始状态AllMsgTypes RequestMsg \union ResponseMsg则用并集组合消息类型集合。六、序列运算EXTENDS Sequences运算语法语义追加Append(s, e)尾部追加元素拼接s1 \o s2两个序列连接头部Head(s)取首元素尾部Tail(s)去掉首元素后的剩余部分长度Len(s)子序列SubSeq(s, from, to)按索引截取索引s[i]注意 1 起始索引配套辅助运算符Range(s) {s[i] : i \in 1..Len(s)}把序列转成元素集合消除顺序与重复。该辅助模式被 distributed.tla 的末尾以及AccordExec一族规范反复使用——例如安全性质中“每个 response 都能在 history 序列中找到对应的 request”就需要先Range(history)再判断。七、函数运算\* 函数定义定义域为 1..10值域为平方 f [x \in 1..10 |- x * x] \* 函数集合所有从 S 到 T 的函数 [S - T] \* EXCEPT 更新函数 f [f EXCEPT ![key] newval] \* 单点更新 f [f EXCEPT ![k1] v1, ![k2] v2] \* 多点更新 f [f EXCEPT ![k] 1] \* 表示旧值函数集合[S - T]是 TLA 表达“复杂不变量”的利器若断言某变量\in [Nodes - StateSet]等于声明“对每个节点其状态都属于 StateSet”。[distributed.tla](https://link.gitcode.com/i/8aa5d81b2ac7f0397ddc5a47507cf081) 的类型不变量node_state \in [Nodes - {idle, waiting, done}] 正是这一写法的范本。EXCEPT是 TLA 唯一的“结构性更新”语法它保证更新后的函数与旧函数仅在指定键上不同引用该键的旧值。AccordExec.tla 对锁与队列区域的建模大量依赖这一机制。八、结构体记录\* 创建 msg [type |- request, from |- A, data |- 42] \* 访问 msg.type \* request msg[type] \* request \* 全部可能记录构成的集合类型声明 MsgType [type: {request, response}, from: Servers, data: Nat] \* EXCEPT 更新记录字段 msg [msg EXCEPT !.data 99]注意[a |- b]与[a: T]的区别前者是单个记录值后者是满足该“模式”的所有记录构成的集合通常用于类型不变量。在 distributed.tla 中RequestMsg [type: {request}, from: Nodes, to: Nodes, data: Nat] ResponseMsg [type: {response}, from: Nodes, to: Nodes, data: Nat] AllMsgTypes RequestMsg \union ResponseMsg消息被建模为记录m.type、m.from用于条件分支这与分布式系统论文中的消息抽象一一对应。Accord 规范的Baseline.cfg中CmdEntries {c1}之类的常量同样服务于这种记录式消息建模。九、量词\* 全称量词 \A x \in S: P(x) \* 存在量词 \E x \in S: P(x) \* 多变量 \A x \in S, y \in T: P(x, y) \* CHOOSE —— 确定性选择 CHOOSE x \in S: P(x)关键规则本参考手册强调的三条红线\A x \in {}: P(x)恒为 TRUE空集上的全称命题平凡成立\E x \in {}: P(x)恒为 FALSE空集上不存在任何元素用搭配\A用/\搭配\E——绝不要用搭配\E。第三条是最常见的建模错误\E x: P(x) Q(x)只要存在一个使P(x)为假的 x 就整体成立几乎总是与直觉相反正确写法是\E x: P(x) /\ Q(x)。invariants.md 的“常见错误”清单第一条再次点名了这一陷阱可见其重要性。CHOOSE是唯一具有“确定性”的选择运算给定同样集合与谓词每次选择结果相同。它适合定义规范内的确定性函数如选取最小元素但要注意 TLC 对 CHOOSE 的求值依赖遍历顺序。十、IF-THEN-ELSE 与 CASEIF cond THEN expr1 ELSE expr2 CASE x 1 - one [] x 2 - two [] OTHER - manyCASE从上到下匹配第一个成立的分支OTHER兜底若没有任何分支匹配且无OTHER结果未定义。IF在 TLA 中是表达式而非语句因此IF ... THEN ... ELSE ...一定有返回值可作为运算符体的一部分。十一、时序运算符Temporal Operators运算符名称含义[]PAlwaysboxP 在每个状态都为真PEventuallydiamondP 在至少一个状态为真[]PEventually alwaysP 最终永久为真收敛[]PInfinitely oftenP 无限次为真反复发生P ~ QLeads-to只要 P 成立Q 最终成立这些运算符构成了 TLA 表达活性liveness与公平性要求的词汇表。语义辨析[]P描述“最终稳定”如分布式系统的收敛convergence、算法终止[]P描述“反复出现”如心跳heartbeat、周期服务P ~ Q描述“请求-响应保证”仓库 invariants.md 给出了r \in pending ~ r \in completed每个请求最终被处理与pc[p] Waiting ~ pc[p] InCS无饥饿等经典模式。Accord 的 Baseline.cfg 中PROPERTY Termination就是一个时序性质声明而matrix.py脚本在--liveness模式下专门校验它见 examples/README.md。十二、动作与带撇变量Primed Variables动作action描述系统状态如何变迁核心记号是带撇变量x——表示 x 在下一个状态的值\* x 是 x 在下一状态的值 Next x x 1 \* UNCHANGED —— 变量保持不变 UNCHANGED x UNCHANGED x, y, z \* Box 动作公式允许停滞stuttering的 A [][A]_v [](A \/ UNCHANGED v) \* Angle 动作公式要求变量真的发生变化的 A A_v A /\ (v # v)UNCHANGED是纯 TLA 建模的纪律所在每个动作必须声明所有变量的去向未提及的变量要么在动作中显式给出新值要么用UNCHANGED声明不变。templates/basic.tla 中每个动作Start/Step/Finish都严格遵循“更新目标变量 UNCHANGED其余变量”的写法值得照抄。SKILL.md 的“Key Principles”第 8 条也明确要求Every action must specify all variables。box 公式[][Next]_vars与 angle 公式Next_vars的区别在于是否允许停滞步stuttering step即所有变量不变但动作未执行——box 允许、angle 不允许。公平性定义正是基于这两个公式构建的。十三、规范结构Spec Structurevars x, y, z Init x 0 /\ y 0 /\ z 0 Next Action1 \/ Action2 \/ Action3 Spec Init /\ [][Next]_vars \* 带公平性 Spec Init /\ [][Next]_vars /\ WF_vars(Next)一个完整的 TLA 规范由三部分构成Init初始状态谓词描述所有合法初始状态Next下一状态关系是若干动作的析取\/表示任意时刻可以执行任意一个使能动作SpecInit /\ [][Next]_vars声明“从某个初始状态出发每个后继状态要么执行 Next 中的动作要么停滞”。vars x, y, z把所有状态变量打包成一个元组供[][Next]_vars引用以判断停滞。FairSpec Spec /\ WF_vars(Next)在规范层面引入公平性保证。仓库 templates/basic.tla 的完整结构Init→Start \/ Step \/ Finish→Spec→TypeInvariant/Safety/Liveness→FairSpec是纯 TLA 规范的标准骨架templates/distributed.tla 则示范了带消息传递的分布式系统规范SendRequest \/ HandleRequest \/ HandleResponse并可显式开启DropMessage模拟丢包网络。十四、公平性FairnessWF_v(A) \* 弱公平若 A 最终持续使能则 A 最终发生 SF_v(A) \* 强公平若 A 反复被使能则 A 最终发生 ENABLED A \* 当前状态是否能使能动作 A弱公平 WF适用于动作一旦使能就持续使能的情形无条件推进强公平 SF适用于动作反复“使能-失能”的情形例如进程等待锁AcquireLock在锁被占用期间反复失能ENABLED A是一个时序运算符判断当前状态是否满足动作 A 的前提。为什么需要公平性因为 TLA 默认假设“一切皆可停滞”everything can crash——不做公平性假设时调度器可以永远不执行某个使能的动作导致活性性质平凡失败。因此凡是要验证活性liveness几乎都必须引入 WF 或 SF。invariants.md 的“Fairness Requirements”一节给出了逐动作公平性的组合模式Spec /\ \A p \in Processes: WF_vars(ReleaseLock(p)) /\ SF_vars(AcquireLock(p))。Accord 的规范在Baseline.cfg中注明“the fairness conjunct in Spec exists for this; matrix.py checks it under --liveness”即公平性合取已内置于Spec供活性验证使用——这是工业级 TLA 实践的标准做法。十五、标准模块Standard Modules模块提供内容Integers、-、*、\div、%、..、Int、NatNaturals与 Integers 相同但只有自然数SequencesAppend、Head、Tail、Len、SubSeq、\o、Seq(S)FiniteSetsCardinality、IsFiniteSetTLCPrint、Assert、:、函数构造器Bags多重集Bag运算Seq(S)生成“S 中元素构成的所有有限序列”的集合是声明“队列变量类型”的标准写法queue \in Seq(MessageType)。注意Naturals与Integers二选一即可——Naturals不含负数能更紧地约束类型不变量invariants.md 建议“越紧越好”。十六、TLC 专用运算符EXTENDS TLC\* 函数构造器键 : 值 f a : 1 b : 2 \* 类似记录的函数 \* Print调试打印 expr求值结果为 val Print(expr, val) \* Assert Assert(cond, msg):与便捷的函数构造语法a : 1 b : 2等价于[a |- 1, b |- 2]适合紧凑定义查找表Print(expr, val)模型检查时打印expr整体表达式的值等于val——这是嵌入规范内部的调试探针Assert(cond, msg)条件为假时 TLC 直接报错可在动作内做“运行时断言”。这些运算符只能在 TLC 环境下求值因此依赖它们的模块必须EXTENDS TLC。在 PlusCal 中对应print x;与assert x 0;语句见 pluscal.md。十七、配置文件.cfgTLC 的检查任务通过.cfg文件声明——规范文件只描述“系统是什么”.cfg描述“这次要检查什么”SPECIFICATION Spec INVARIANT TypeInvariant INVARIANT SafetyInvariant PROPERTY Liveness CONSTANT NumServers 3 NULL NULL CHECK_DEADLOCK FALSE各指令含义SPECIFICATION Spec指定要验证的规范名对应规范中的Spec ...INVARIANT X声明需要检查的不变量安全性质可声明多个TLC 逐个检查每个可达状态PROPERTY P声明时序性质活性检查代价高于不变量CONSTANT为规范中的符号常量绑定具体值支持集合字面量、整数、模型值以及-语法如TaskTxns - MCTaskTxns从被扩展模块中选取定义CHECK_DEADLOCK FALSE关闭死锁检查默认开启进程模型下常用。Accord 的 Baseline.cfg 是工业级配置的范本它一口气声明了 9 个INVARIANTTypeOK、Inv_LockerIsFifo、Inv_LockLeads、Inv_OneProspectiveLocker、Inv_AtMostOneLock、Inv_Isolation、RankOK、NoCycle、NoStuck加 1 个PROPERTY Termination并用-语法把MCTaskTxns等实例定义绑定给抽象常量TaskTxns等。其配套说明examples/README.md特别指出覆盖率探针不能放进 cfg 一起跑因为探针是取反的可达性声明TLC 在第一个被违反的探针处就停机所以要用matrix.py/notify.py驱动逐个检查——这是多性质检查的实战经验。十八、运行 TLC从脚本到命令行仓库 SKILL.md 封装了完整的运行工作流。首次使用需执行bash SKILL_DIR/scripts/setup.sh下载tla2tools.jarv1.8.0并校验 Java 11。随后可用# 推荐解析 模型检查一步完成 bash SKILL_DIR/scripts/check.sh spec.tla --config spec.cfg # 仅语法解析 bash SKILL_DIR/scripts/parse.sh spec.tla # PlusCal 转 TLA纯 TLA 规范可跳过 bash SKILL_DIR/scripts/translate.sh spec.tla -nocfg # 模型检查多核加速 / 关闭死锁检查 bash SKILL_DIR/scripts/tlc.sh spec.tla --config spec.cfg --workers auto bash SKILL_DIR/scripts/tlc.sh spec.tla --no-deadlock等价的原生 Java 调用tla2tools.jar提供全部工具类JARSKILL_DIR/lib/tla2tools.jar java -cp $JAR tla2sany.SANY spec.tla # 解析 java -cp $JAR pcal.trans -nocfg spec.tla # PlusCal 翻译 java -cp $JAR tlc2.TLC -workers auto -config spec.cfg spec.tla # 模型检查 java -cp $JAR tlc2.REPL # 交互式 REPL java -cp $JAR tlc2.TLC -dump dot,actionlabels,colorize states.dot spec.tla # 导出状态图TLC 输出的三种关键结果SKILL.md “Interpreting TLC Output”成功Model checking completed. No error has been found.不变量违反Error: Invariant SafetyInvariant is violated.随后给出从初始状态到违反状态的反例行为序列counter-example逐状态列出变量取值死锁Error: Deadlock reached.意味着所有进程都无法推进——检查await条件与进程完成逻辑活性违反Error: Temporal properties were violated.通常伴随停滞后缀stuttering suffix需要回头检查公平性设置补WF_vars/SF_vars。SKILL.md 给出的建模方法论同样值得固化为工作习惯先写类型不变量 → 用 2~3 个节点的小常量跑 TLC → 逐个追加安全不变量 → 最后加活性性质与公平性 → 逐步增大常量扩大覆盖。其“Key Principles”强调3 个节点能发现大部分 bug10 个节点慢 1000 倍因此状态空间裁剪小常量 CONSTRAINT StateConstraint是 TLC 实践的必修课。十九、仓库实战Cassandra Accord 的 TLA 形式化验证本仓库在 formalise/accord/execution/tla 目录下保存了 Apache Cassandra 5.0 Accord 事务协议的一整套形式化验证资产是本文语法讲解的绝佳落地案例AccordExec.tla建模 Accord 每个 CommandStore 的执行队列AccordCacheEntry、AccordCacheEntryQueue、SafeTask派生的等待关系wait relation并证明三个核心结论模块头部注释明确写出NoStuck不存在一组存活的 task 互相阻塞NoCycle等待关系无环RankOK存在一个字典序秩lexicographic rank见证无环性。AccordAcyclic.lean用 Lean 证明助手从RankOK推导出对任意数量task 与 entry 的无环性——这正是注释中“RankOK is the size-independent certificate”的含义TLC 只负责验证实现是否维持秩假设尺寸无关的结论交给定理证明器二者形成“模型检查 机械证明”的互补闭环。AccordNotify.tla建模 AccordExec 所依赖的通知簿记notification bookkeeping抽象用于“discharge”队列就绪性的抽象假设。examples/Baseline.tla 与 examples/Notify.tla单次运行的实例模块通过EXTENDS AccordExec/EXTENDS AccordNotify继承抽象规范并覆写MCTaskTxns、MCTaskKeys、MCTaskParent等实例定义如MCTaskTxns {c1}, {c1}表示两个 task 都依赖事务 c1。Baseline.cfg配置文件绑定CmdEntries {c1}、KeyEntries {k1, k2}、NumTasks 2等常量声明 9 个不变量与 1 个活性性质并展示TaskTxns - MCTaskTxns的-绑定语法。matrix.py 与 notify.py批量驱动脚本逐个运行覆盖率探针并双向断言解决单次 TLC 运行只能报告第一个违反探针的限制。这组资产完整演示了本节所有语法的工业级用法模型值常量{c1}、{k1, k2}、记录式消息建模、函数与 EXCEPT 更新、集合/序列运算、\A/\E量词、box/angle 动作公式、时序性质PROPERTY Termination与公平性合取以及.cfg驱动的多不变量检查。同时模块头部注释严格区分了PROVES本模型证明的、ASSUMES模型采纳的假设如无故障执行、加载中的 entry 不产生等待边与DELIBERATELY NOT MODELLED刻意未建模的部分如部分失败路径——这展示了形式化建模中“抽象边界必须显式声明”的专业纪律也正是阅读任何 TLA 规范时首先应该查看的部分。结语TLA 语言的表达能力集中在极少数概念上模块、值、运算符、动作、时序性质与公平性。掌握本参考手册的语法后配合仓库提供的 templates/basic.tla、templates/distributed.tla 模板、SKILL.md 的运行脚本以及 Accord 的工业级规范作为范例即可对分布式协议进行穷举模型检查。进阶方向包括PlusCal 高层语言见 pluscal.md、不变量与性质设计模式见 patterns/invariants.md、分布式系统模式见 patterns/distributed-systems.md以及代码到规范的映射与缺陷发现见 patterns/code-to-spec.md。【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考 Apache Cassandra 中的 TLA 语言参考从模块结构到 TLC 模型检查实战【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra导读TLATemporal Logic of Actions是 Leslie Lamport 提出的形式化规范语言用于对分布式系统、并发协议与状态机进行精确建模与穷举验证。本篇文章以当前仓库中的 TLA 语言参考 为骨架系统讲解 TLA 的模块结构、类型系统、集合与序列运算、时序逻辑与公平性等核心语法并结合仓库内 tla-plus 技能包 的脚本与模板、以及 Cassandra 在 formalise/accord/execution/tla 目录下真实使用的 Accord 形式化规范AccordExec.tla 等进行源码级佐证。读完本文你将掌握从零编写一个可被 TLC 模型检查器验证的 TLA 规范、编写配套 .cfg 配置文件并正确解读 TLC 输出的完整能力。一、模块结构一切规范的组织单元TLA 规范以模块MODULE为基本单位一个.tla文件对应一个模块。当前仓库的 language.md 给出了最精简的骨架---- MODULE ModuleName ---- EXTENDS Integers, Sequences, FiniteSets, TLC CONSTANTS Const1, Const2 VARIABLES var1, var2 \* Operator definitions \* ... 关键规则模块名必须与文件名去掉.tla后缀完全一致。例如仓库中formalise/accord/execution/tla/AccordExec.tla的模块声明是--------------------------- MODULE AccordExec ---------------------------而 examples/Baseline.tla 通过EXTENDS AccordExec继承该模块——这正体现了 TLA 模块即复用单元的机制EXTENDS把被扩展模块的所有定义带入当前模块与 Java 的继承或 Python 的 import 在语义上类似。模块内部按职责分为几个区段EXTENDS引入标准库模块Integers、Sequences、FiniteSets、TLC、Naturals、Bags 等详见下文“标准模块”一节CONSTANTS声明符号常量它们是不变的具体值通常在.cfg配置文件中绑定VARIABLES声明状态变量是系统状态的全部载体其余部分是运算符operator定义即对上述符号的纯函数式操作。仓库的 templates/basic.tla 给出了一个完整的纯 TLA 状态机模板其结构正是EXTENDS→CONSTANTS→VARIABLES→vars ...→Init→ 动作定义 →Next→Spec→ 性质定义可以作为新规范的标准起点。二、类型与值2.1 原语类型类型示例说明整数0、1、-5需要EXTENDS Integers才能使用算术运算字符串hello只能使用和#比较通常作为不透明标识符布尔值TRUE、FALSE逻辑运算的基础模型值在.cfg中定义未解释常量uninterpreted constant用于表示无法穷举的具体对象模型值model value是 TLA 特有的抽象手段当你并不关心某个对象的内部结构只关心它的身份identity时就在.cfg文件中声明Const m1这样的模型值。TLC 会把它当作一个不可分解的原子符号处理。仓库中 Accord 的 Baseline.cfg 就是典型的模型值用法CmdEntries {c1}、KeyEntries {k1, k2}把命令条目与键条目建模为字符串集合而NumTasks 2直接给出整数常量。2.2 复合类型类型示例关键语义集合Set{1, 2, 3}、{}无序、元素唯一、只能容纳同类型元素序列Sequence/Tuple1, 2, 3、有序、1 起始索引结构体Record[name \|- Alice, age \|- 30]通过s.name或s[name]访问字段函数Function[x \in 1..10 \|- x * x]通过f[3]应用这四类复合值是 TLA 建模的全部“数据结构”。值得注意区分集合与序列{1, 2, 3}没有顺序、没有重复元素1, 2, 3有顺序、允许重复。建模消息队列时必须用序列保持 FIFO 顺序建模“在途消息集合”时常用集合。函数与记录记录本质上是定义域为字符串集合的函数[x \in 1..10 \|- x * x]是定义域为1..10、值域为平方值的函数。AccordExec.tla 的头部注释提到“MODELS the queue as its three regions, with the fifo order derived from fifoAt (Q5) rather than from the array that maintains it”这种把数组抽象为函数键→值映射的建模手法正是 TLA 的常态。三、运算符定义TLA 中没有“函数”关键字一切可复用逻辑都用运算符operator表达且没有副作用纯函数式\* 无参运算符常量 MaxSize 10 \* 带参运算符 Max(a, b) IF a b THEN a ELSE b \* LET 引入局部定义 ThreeMax(a, b, c) LET M(x, y) IF x y THEN x ELSE y IN M(M(a, b), c)LET ... IN ...是唯一的局部绑定机制适合在复杂运算符内部定义辅助逻辑。运算符可以被EXTENDS继承例如Baseline.tla中MCTaskTxns {c1}, {c1}这样的定义就是用来给父模块AccordExec的抽象参数提供具体实例的覆写点。四、布尔逻辑与子弹点记号逻辑TLA 符号数学符号与/\∧或\/∨非~¬蕴含⇒当且仅当⇔子弹点记号bullet-point notation是 TLA 最具辨识度的排版它是对空白敏感的垂直布局一组以/\或\/开头的行隐式组合成一个逻辑表达式/\ A /\ \/ B \/ C /\ D \* 含义A /\ (B \/ C) /\ D缩进决定了结合优先级。这是从 Lamport 原版规范延续下来的写作习惯仓库中 AccordExec.tla 的全部动作与不变量都采用这种风格。阅读时把/\行理解为“AND 列表”把\/行理解为“OR 列表”即可。五、集合运算运算语法备注属于x \in S不属于x \notin S子集S \subseteq T并集S \union T交集S \intersect T差集S \ T基数Cardinality(S)需要FiniteSets幂集SUBSET S笛卡尔积S \X T整数区间a..b全部布尔BOOLEAN即{TRUE, FALSE}映射{f(x) : x \in S}对每个元素应用函数过滤{x \in S : P(x)}筛选满足谓词的元素集合是 TLA 对“状态空间”建模的核心。一个典型的映射用法见仓库 templates/distributed.tla 的初始状态node_state [n \in Nodes |- idle]用函数映射给每个节点赋初始状态AllMsgTypes RequestMsg \union ResponseMsg则用并集组合消息类型集合。六、序列运算EXTENDS Sequences运算语法语义追加Append(s, e)尾部追加元素拼接s1 \o s2两个序列连接头部Head(s)取首元素尾部Tail(s)去掉首元素后的剩余部分长度Len(s)子序列SubSeq(s, from, to)按索引截取索引s[i]注意 1 起始索引配套辅助运算符Range(s) {s[i] : i \in 1..Len(s)}把序列转成元素集合消除顺序与重复。该辅助模式被 distributed.tla 的末尾以及AccordExec一族规范反复使用——例如安全性质中“每个 response 都能在 history 序列中找到对应的 request”就需要先Range(history)再判断。七、函数运算\* 函数定义定义域为 1..10值域为平方 f [x \in 1..10 |- x * x] \* 函数集合所有从 S 到 T 的函数 [S - T] \* EXCEPT 更新函数 f [f EXCEPT ![key] newval] \* 单点更新 f [f EXCEPT ![k1] v1, ![k2] v2] \* 多点更新 f [f EXCEPT ![k] 1] \* 表示旧值函数集合[S - T]是 TLA 表达“复杂不变量”的利器若断言某变量\in [Nodes - StateSet]等于声明“对每个节点其状态都属于 StateSet”。[distributed.tla](https://link.gitcode.com/i/8aa5d81b2ac7f0397ddc5a47507cf081) 的类型不变量node_state \in [Nodes - {idle, waiting, done}] 正是这一写法的范本。EXCEPT是 TLA 唯一的“结构性更新”语法它保证更新后的函数与旧函数仅在指定键上不同引用该键的旧值。AccordExec.tla 对锁与队列区域的建模大量依赖这一机制。八、结构体记录\* 创建 msg [type |- request, from |- A, data |- 42] \* 访问 msg.type \* request msg[type] \* request \* 全部可能记录构成的集合类型声明 MsgType [type: {request, response}, from: Servers, data: Nat] \* EXCEPT 更新记录字段 msg [msg EXCEPT !.data 99]注意[a |- b]与[a: T]的区别前者是单个记录值后者是满足该“模式”的所有记录构成的集合通常用于类型不变量。在 distributed.tla 中RequestMsg [type: {request}, from: Nodes, to: Nodes, data: Nat] ResponseMsg [type: {response}, from: Nodes, to: Nodes, data: Nat] AllMsgTypes RequestMsg \union ResponseMsg消息被建模为记录m.type、m.from用于条件分支这与分布式系统论文中的消息抽象一一对应。Accord 规范的Baseline.cfg中CmdEntries {c1}之类的常量同样服务于这种记录式消息建模。九、量词\* 全称量词 \A x \in S: P(x) \* 存在量词 \E x \in S: P(x) \* 多变量 \A x \in S, y \in T: P(x, y) \* CHOOSE —— 确定性选择 CHOOSE x \in S: P(x)关键规则本参考手册强调的三条红线\A x \in {}: P(x)恒为 TRUE空集上的全称命题平凡成立\E x \in {}: P(x)恒为 FALSE空集上不存在任何元素用搭配\A用/\搭配\E——绝不要用搭配\E。第三条是最常见的建模错误\E x: P(x) Q(x)只要存在一个使P(x)为假的 x 就整体成立几乎总是与直觉相反正确写法是\E x: P(x) /\ Q(x)。invariants.md 的“常见错误”清单第一条再次点名了这一陷阱可见其重要性。CHOOSE是唯一具有“确定性”的选择运算给定同样集合与谓词每次选择结果相同。它适合定义规范内的确定性函数如选取最小元素但要注意 TLC 对 CHOOSE 的求值依赖遍历顺序。十、IF-THEN-ELSE 与 CASEIF cond THEN expr1 ELSE expr2 CASE x 1 - one [] x 2 - two [] OTHER - manyCASE从上到下匹配第一个成立的分支OTHER兜底若没有任何分支匹配且无OTHER结果未定义。IF在 TLA 中是表达式而非语句因此IF ... THEN ... ELSE ...一定有返回值可作为运算符体的一部分。十一、时序运算符Temporal Operators运算符名称含义[]PAlwaysboxP 在每个状态都为真PEventuallydiamondP 在至少一个状态为真[]PEventually alwaysP 最终永久为真收敛[]PInfinitely oftenP 无限次为真反复发生P ~ QLeads-to只要 P 成立Q 最终成立这些运算符构成了 TLA 表达活性liveness与公平性要求的词汇表。语义辨析[]P描述“最终稳定”如分布式系统的收敛convergence、算法终止[]P描述“反复出现”如心跳heartbeat、周期服务P ~ Q描述“请求-响应保证”仓库 invariants.md 给出了r \in pending ~ r \in completed每个请求最终被处理与pc[p] Waiting ~ pc[p] InCS无饥饿等经典模式。Accord 的 Baseline.cfg 中PROPERTY Termination就是一个时序性质声明而matrix.py脚本在--liveness模式下专门校验它见 examples/README.md。十二、动作与带撇变量Primed Variables动作action描述系统状态如何变迁核心记号是带撇变量x——表示 x 在下一个状态的值\* x 是 x 在下一状态的值 Next x x 1 \* UNCHANGED —— 变量保持不变 UNCHANGED x UNCHANGED x, y, z \* Box 动作公式允许停滞stuttering的 A [][A]_v [](A \/ UNCHANGED v) \* Angle 动作公式要求变量真的发生变化的 A A_v A /\ (v # v)UNCHANGED是纯 TLA 建模的纪律所在每个动作必须声明所有变量的去向未提及的变量要么在动作中显式给出新值要么用UNCHANGED声明不变。templates/basic.tla 中每个动作Start/Step/Finish都严格遵循“更新目标变量 UNCHANGED其余变量”的写法值得照抄。SKILL.md 的“Key Principles”第 8 条也明确要求Every action must specify all variables。box 公式[][Next]_vars与 angle 公式Next_vars的区别在于是否允许停滞步stuttering step即所有变量不变但动作未执行——box 允许、angle 不允许。公平性定义正是基于这两个公式构建的。十三、规范结构Spec Structurevars x, y, z Init x 0 /\ y 0 /\ z 0 Next Action1 \/ Action2 \/ Action3 Spec Init /\ [][Next]_vars \* 带公平性 Spec Init /\ [][Next]_vars /\ WF_vars(Next)一个完整的 TLA 规范由三部分构成Init初始状态谓词描述所有合法初始状态Next下一状态关系是若干动作的析取\/表示任意时刻可以执行任意一个使能动作SpecInit /\ [][Next]_vars声明“从某个初始状态出发每个后继状态要么执行 Next 中的动作要么停滞”。vars x, y, z把所有状态变量打包成一个元组供[][Next]_vars引用以判断停滞。FairSpec Spec /\ WF_vars(Next)在规范层面引入公平性保证。仓库 templates/basic.tla 的完整结构Init→Start \/ Step \/ Finish→Spec→TypeInvariant/Safety/Liveness→FairSpec是纯 TLA 规范的标准骨架templates/distributed.tla 则示范了带消息传递的分布式系统规范SendRequest \/ HandleRequest \/ HandleResponse并可显式开启DropMessage模拟丢包网络。十四、公平性FairnessWF_v(A) \* 弱公平若 A 最终持续使能则 A 最终发生 SF_v(A) \* 强公平若 A 反复被使能则 A 最终发生 ENABLED A \* 当前状态是否能使能动作 A弱公平 WF适用于动作一旦使能就持续使能的情形无条件推进强公平 SF适用于动作反复“使能-失能”的情形例如进程等待锁AcquireLock在锁被占用期间反复失能ENABLED A是一个时序运算符判断当前状态是否满足动作 A 的前提。为什么需要公平性因为 TLA 默认假设“一切皆可停滞”everything can crash——不做公平性假设时调度器可以永远不执行某个使能的动作导致活性性质平凡失败。因此凡是要验证活性liveness几乎都必须引入 WF 或 SF。invariants.md 的“Fairness Requirements”一节给出了逐动作公平性的组合模式Spec /\ \A p \in Processes: WF_vars(ReleaseLock(p)) /\ SF_vars(AcquireLock(p))。Accord 的规范在Baseline.cfg中注明“the fairness conjunct in Spec exists for this; matrix.py checks it under --liveness”即公平性合取已内置于Spec供活性验证使用——这是工业级 TLA 实践的标准做法。十五、标准模块Standard Modules模块提供内容Integers、-、*、\div、%、..、Int、NatNaturals与 Integers 相同但只有自然数SequencesAppend、Head、Tail、Len、SubSeq、\o、Seq(S)FiniteSetsCardinality、IsFiniteSetTLCPrint、Assert、:、函数构造器Bags多重集Bag运算Seq(S)生成“S 中元素构成的所有有限序列”的集合是声明“队列变量类型”的标准写法queue \in Seq(MessageType)。注意Naturals与Integers二选一即可——Naturals不含负数能更紧地约束类型不变量invariants.md 建议“越紧越好”。十六、TLC 专用运算符EXTENDS TLC\* 函数构造器键 : 值 f a : 1 b : 2 \* 类似记录的函数 \* Print调试打印 expr求值结果为 val Print(expr, val) \* Assert Assert(cond, msg):与便捷的函数构造语法a : 1 b : 2等价于[a |- 1, b |- 2]适合紧凑定义查找表Print(expr, val)模型检查时打印expr整体表达式的值等于val——这是嵌入规范内部的调试探针Assert(cond, msg)条件为假时 TLC 直接报错可在动作内做“运行时断言”。这些运算符只能在 TLC 环境下求值因此依赖它们的模块必须EXTENDS TLC。在 PlusCal 中对应print x;与assert x 0;语句见 pluscal.md。十七、配置文件.cfgTLC 的检查任务通过.cfg文件声明——规范文件只描述“系统是什么”.cfg描述“这次要检查什么”SPECIFICATION Spec INVARIANT TypeInvariant INVARIANT SafetyInvariant PROPERTY Liveness CONSTANT NumServers 3 NULL NULL CHECK_DEADLOCK FALSE各指令含义SPECIFICATION Spec指定要验证的规范名对应规范中的Spec ...INVARIANT X声明需要检查的不变量安全性质可声明多个TLC 逐个检查每个可达状态PROPERTY P声明时序性质活性检查代价高于不变量CONSTANT为规范中的符号常量绑定具体值支持集合字面量、整数、模型值以及-语法如TaskTxns - MCTaskTxns从被扩展模块中选取定义CHECK_DEADLOCK FALSE关闭死锁检查默认开启进程模型下常用。Accord 的 Baseline.cfg 是工业级配置的范本它一口气声明了 9 个INVARIANTTypeOK、Inv_LockerIsFifo、Inv_LockLeads、Inv_OneProspectiveLocker、Inv_AtMostOneLock、Inv_Isolation、RankOK、NoCycle、NoStuck加 1 个PROPERTY Termination并用-语法把MCTaskTxns等实例定义绑定给抽象常量TaskTxns等。其配套说明examples/README.md特别指出覆盖率探针不能放进 cfg 一起跑因为探针是取反的可达性声明TLC 在第一个被违反的探针处就停机所以要用matrix.py/notify.py驱动逐个检查——这是多性质检查的实战经验。十八、运行 TLC从脚本到命令行仓库 SKILL.md 封装了完整的运行工作流。首次使用需执行bash SKILL_DIR/scripts/setup.sh下载tla2tools.jarv1.8.0并校验 Java 11。随后可用# 推荐解析 模型检查一步完成 bash SKILL_DIR/scripts/check.sh spec.tla --config spec.cfg # 仅语法解析 bash SKILL_DIR/scripts/parse.sh spec.tla # PlusCal 转 TLA纯 TLA 规范可跳过 bash SKILL_DIR/scripts/translate.sh spec.tla -nocfg # 模型检查多核加速 / 关闭死锁检查 bash SKILL_DIR/scripts/tlc.sh spec.tla --config spec.cfg --workers auto bash SKILL_DIR/scripts/tlc.sh spec.tla --no-deadlock等价的原生 Java 调用tla2tools.jar提供全部工具类JARSKILL_DIR/lib/tla2tools.jar java -cp $JAR tla2sany.SANY spec.tla # 解析 java -cp $JAR pcal.trans -nocfg spec.tla # PlusCal 翻译 java -cp $JAR tlc2.TLC -workers auto -config spec.cfg spec.tla # 模型检查 java -cp $JAR tlc2.REPL # 交互式 REPL java -cp $JAR tlc2.TLC -dump dot,actionlabels,colorize states.dot spec.tla # 导出状态图TLC 输出的三种关键结果SKILL.md “Interpreting TLC Output”成功Model checking completed. No error has been found.不变量违反Error: Invariant SafetyInvariant is violated.随后给出从初始状态到违反状态的反例行为序列counter-example逐状态列出变量取值死锁Error: Deadlock reached.意味着所有进程都无法推进——检查await条件与进程完成逻辑活性违反Error: Temporal properties were violated.通常伴随停滞后缀stuttering suffix需要回头检查公平性设置补WF_vars/SF_vars。SKILL.md 给出的建模方法论同样值得固化为工作习惯先写类型不变量 → 用 2~3 个节点的小常量跑 TLC → 逐个追加安全不变量 → 最后加活性性质与公平性 → 逐步增大常量扩大覆盖。其“Key Principles”强调3 个节点能发现大部分 bug10 个节点慢 1000 倍因此状态空间裁剪小常量 CONSTRAINT StateConstraint是 TLC 实践的必修课。十九、仓库实战Cassandra Accord 的 TLA 形式化验证本仓库在 formalise/accord/execution/tla 目录下保存了 Apache Cassandra 5.0 Accord 事务协议的一整套形式化验证资产是本文语法讲解的绝佳落地案例AccordExec.tla建模 Accord 每个 CommandStore 的执行队列AccordCacheEntry、AccordCacheEntryQueue、SafeTask派生的等待关系wait relation并证明三个核心结论模块头部注释明确写出NoStuck不存在一组存活的 task 互相阻塞NoCycle等待关系无环RankOK存在一个字典序秩lexicographic rank见证无环性。AccordAcyclic.lean用 Lean 证明助手从RankOK推导出对任意数量task 与 entry 的无环性——这正是注释中“RankOK is the size-independent certificate”的含义TLC 只负责验证实现是否维持秩假设尺寸无关的结论交给定理证明器二者形成“模型检查 机械证明”的互补闭环。AccordNotify.tla建模 AccordExec 所依赖的通知簿记notification bookkeeping抽象用于“discharge”队列就绪性的抽象假设。examples/Baseline.tla 与 examples/Notify.tla单次运行的实例模块通过EXTENDS AccordExec/EXTENDS AccordNotify继承抽象规范并覆写MCTaskTxns、MCTaskKeys、MCTaskParent等实例定义如MCTaskTxns {c1}, {c1}表示两个 task 都依赖事务 c1。Baseline.cfg配置文件绑定CmdEntries {c1}、KeyEntries {k1, k2}、NumTasks 2等常量声明 9 个不变量与 1 个活性性质并展示TaskTxns - MCTaskTxns的-绑定语法。matrix.py 与 notify.py批量驱动脚本逐个运行覆盖率探针并双向断言解决单次 TLC 运行只能报告第一个违反探针的限制。这组资产完整演示了本节所有语法的工业级用法模型值常量{c1}、{k1, k2}、记录式消息建模、函数与 EXCEPT 更新、集合/序列运算、\A/\E量词、box/angle 动作公式、时序性质PROPERTY Termination与公平性合取以及.cfg驱动的多不变量检查。同时模块头部注释严格区分了PROVES本模型证明的、ASSUMES模型采纳的假设如无故障执行、加载中的 entry 不产生等待边与DELIBERATELY NOT MODELLED刻意未建模的部分如部分失败路径——这展示了形式化建模中“抽象边界必须显式声明”的专业纪律也正是阅读任何 TLA 规范时首先应该查看的部分。结语TLA 语言的表达能力集中在极少数概念上模块、值、运算符、动作、时序性质与公平性。掌握本参考手册的语法后配合仓库提供的 templates/basic.tla、templates/distributed.tla 模板、SKILL.md 的运行脚本以及 Accord 的工业级规范作为范例即可对分布式协议进行穷举模型检查。进阶方向包括PlusCal 高层语言见 pluscal.md、不变量与性质设计模式见 patterns/invariants.md、分布式系统模式见 patterns/distributed-systems.md以及代码到规范的映射与缺陷发现见 patterns/code-to-spec.md。【免费下载链接】cassandraOpen source transactional distributed database. Linear scalability and proven fault-tolerance on commodity hardware or cloud infrastructure without compromising performance.项目地址: https://gitcode.com/GitHub_Trending/cassa/cassandra创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考