Specifying Systems 第二章笔记

本章介绍 TLA+ 如何描述系统。

2.1 动作

TLA+ 通过描述系统的变量在离散时间下的状态转移描述计算机系统。

2.2 一个时钟

本节用时钟为例介绍描述系统。

相邻状态的一次转移叫做步，通过描述步我们可以描述所有合法状态是如何转换的。在一对新旧状态中，通过'表示新状态的变量，例如（/=是不等于符号）

hr' = IF hr /= 12 THEN hr + 1 ELSE 1

这种包含'的公式叫做动作。动作是公式，因此具有布尔值的含义，一些状态转移（步）使得动作的值为真，这类似于运行了一些步。

再加上系统的初始状态公式，我们就可以完整描述系统了。初始状态仅判定一个时刻，即系统初始时刻，而动作判定系统的每次状态转移，我们使用[]formula表示这种每次判定的含义。

现实中的系统在相邻的观察时刻，可能仅有无关变量的改变（例如我们没有描述的变量），动作描述的变量都保持不变。这自然是合法的系统、合法的转移到自身的状态转移，但却使动作判定为假。因此我们使用[][formula]_variable表示允许某些变量保持不变。该语法实际上表示[]formula \/ (variable' = variable)。

目前为止，初始状态公式和状态转移公式组成了系统的规范。

2.3 规范更进一步

规范是时序公式，一些系统使得公式为真，我们可以说这些系统满足规范。那么是否所有满足规范的系统都满足一些性质呢？这需要用到蕴含运算符

specification => some_property

如果上公式为真，我们可以得到“满足规范的系统总是满足这些性质”。我们把上面的公式叫做定理。TLA+ 可以帮助我们判断定理的真假。

2.4 TLA+ 中的规范

---------------------- MODULE HourClock ----------------------
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr /= 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
--------------------------------------------------------------
THEOREM HC => []HCini
==============================================================

上面的 TLA+ 程序是 2.1~2.3 节描述的时钟规范。

第一行：一个 TLA+ 规范由模块组成。

第二行：EXTENDS关键字导入其他模块。Naturals模块包含自然数以及相关运算符。

第三行：VARIABLE关键字定义变量。

第四至六行：==运算符定义公式，其他运算符的含义基本为象形或者英文表达的含义。

第七行：分隔线可以出现在任意位置，分割线的长度需要大于 4。

第八行：THEOREM关键词表示定理。

第九行：表示模块的结束。

2.5 另一个规范

规范可以有多种表示形式，例如将 2.4 中的HCnxt和HC分别替换为

HCnxt2 == hr' = (hr % 12) + 1
HC2 == HCini /\ [][HCnxt2]_hr

可以验证HC与HC2等价。但要注意HCnxt与HCnxt2并不等价，因为hr从 24 到 1 的状态转移仅使后者为真。