Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何设计系统规约。 这些Specification表明了系统的Safety属性 — 即系统行为被约束在一定范围内，不会做出一些不被允许的行为(something bad does not happen)。 在TLA+中，通常使用公式 \(Spec \triangleq Init \land \Box [Next]_{vars}\) 来描述系统的Safety属性(约束)。 Safety属性说明了系统中什么不能发生，但无法表达系统中某些时间一定会发生的这类属性，而Liveness便可以表达("something good eventully happen")。 Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land L\) 来同时描述其对Safety和Liveness的要求， 公式末尾的 $L$ 便是描述Liveness属性的公式。

一些概念

value

value表示通常意义上的值，如 $1，2，TRUE, FALSE，[name{\mapsto}``zhangsan\!", age{\mapsto}18]$。 TLA+的语义基于ZF集合论， 因此其value只是集合(set)的另一个称呼。

state

state是对一些变量进行赋值(的结果)，如 $[hr=1]$，$[hr=2]$ 等。

state function

state function 是一个以 变量(不包含 primed variable)、常量、操作符构建的表达式。这个表达式给所有state都映射了一个value。可以理解为每个state都可以经过这个function计算，得到一个 value 。

state predicate

结果 value 为 Boolean 类型的 state function。 即state predicate一个作用于state进行真值判断的公式。

behavior

behavior是 state 组成的无穷序列，如 $\sigma \defeq [hr=1] → [hr=2] → [hr=3] → …​$ 。需要注意的是，一个系统可能有多个behavior，比如并发系统可能有多种执行顺序，产生不同的behavior。

step

step是state之间直接变化的步骤。假如 $s_n$, $s_{n+1}$ 分别是两个相邻的 state ，那么 $s_n → s_{n+1}$ 就是表示 从 $s_n$ 直接变化到 $s_{n+1}$的step，无论 state 中有多少个变量，这个变化都是原子的，不会产生其它中间状态。

primed variable

变量发生变化后的值，如 $hr'=hr+1$ 表示 hr 变量经过一个 step 之后，其值等于原先的值加 1 。

action

包含 primed variable 和 unprimed variable 的 formula。 action 作用于 step 进行真值判断，以断定state(的value)是否可以再发生变化。specification(规约)通常由许多action组成。

formula

值为TRUE或FALSE的逻辑表达式（数理逻辑中的「公式」）

这些定义的形式和语义都不一定准确，只是帮助加深理解TLA+。精确定义详见Specifying Systems，尤其是 Chapter 16 有许多描述。

逻辑基础

命题逻辑

命题逻辑语法可以用如下BNF表示：

\[\phi ::= p | (\lnot\phi) | (\phi\land\phi) | (\phi\lor\phi) | (\phi\to\phi)\]

谓词逻辑

PTL: Propositional Temporal Logic ，是LTL的另一种简称，参考:

Temporal Logic 简介

时态公式是行为(behavior)的真值判断式。对于一个行为 $\sigma$ ，以及一个时态公式 $F$ ，如果 $\sigma$ 满足 $F$ ，则可以表示为：

\[\sigma \models F\]

也可称作时态公式 $F$ 对于行为 $\sigma$ 是真的，或称行为 $\sigma$ 满足公式 $F$。

Tip
 为了便于叙述，我们将“时态公式”简称为“公式”。

公式可以通过连接词进行组合，也可使用量词进行修饰。组合公式的含义如下：

  • $\sigma \models (F \land G) \;\defeq \;(\sigma \models F) \land (\sigma \models G)$

  • $\sigma \models (F \lor G) \;\defeq \;(\sigma \models F) \lor (\sigma \models G)$

  • $\sigma \models (F ⇒ G) \;\defeq \;(\sigma \models F) ⇒ (\sigma \models G)$

  • $\sigma \models \lnot F \;\defeq \;\lnot (\sigma \models F)$

  • $\sigma \models (\forall r \in S: F) \;\defeq \;\forall r \in S : (\sigma \models F)$

上面出现的公式 $F$, $G$ 都未加定义，通常由如下三种形式的公式组成:

  • $P$

    state predicate， P是一个「状态谓词」。其语义是: 如果将 $P$ 看作时态公式， 那么 $\sigma$(behavior) 满足 $P$ 当且仅当 $\sigma$ 中的第一个 state 满足 $P$。

  • $\Box P$

    其中 $P$ 是 state predicate 。behavior 满足 $\Box P$ 当且仅当 behavior 中所有 state 满足 $P$

  • $\Box[N]_\color{red}v$

    其中 $N$ 是 action ，$_\color{red}v$ 是 state function 。 behavior 满足该公式 当且仅当 behavior 中每一对相继的states是一个满足 $[N]_v$ 的step。

    注意： $[N]_v$ 中的 $_v$ 可以是 state function ，并不限定于 variables（如 $\seq{hr ,\, val}$)。 state function 可以增加 prime 运算符形成 transition function 。$[N]_v$ 等价于 $ N \lor (v' = v)$ 。详见 Spcifying Systems 16.2.3。

这三种公式中，虽然$P$ 是一个 state predicate，但可以将其看作是一个没有 primed variables 的 action(这种action作用于state得到新的 state' 没有改变，即一个stuttering step)。 这样，我们就可以把时态公式归纳为两种形式： $A$ 和 $\Box A$，其中 $A$ 是一个 action。

语义解释

定义 $\sigma_i$ 是 $\sigma$的第$(i + 1) ^{st}$个state，$\sigma$即是: $\sigma_0\rightarrow\sigma_1\rightarrow\sigma_2\rightarrow\dotsb$。 注意这里的自然语言表述，第一个 state 是 $\sigma_0$ ，$\sigma_0$ 是第一($i+1$)个state。

$\sigma \models A$ 为 true 等价于 $\sigma_0\rightarrow\sigma_1$ 是一个 $A$ step。特殊场景: 如果$A$ 是一个 state predicate ， 只要 $A$ 对于第一个状态($\sigma_0$)判定为 true ，$\sigma_0\rightarrow\sigma_1$就是一个 $A$ step。

$\sigma \models \Box A$ 为 true 等价于 所有的step($\sigma_n\rightarrow\sigma_{n+1}$)都是一个 $A$ step。

定义: $\sigma^{+n} \defeq \sigma_n\rightarrow\sigma_{n+1}\rightarrow\sigma_{n+2}\rightarrow\dotsb$， 因此$\sigma_n\rightarrow\sigma_{n+1}$ 是$\sigma^{+n}$的第一个step。 $\sigma \models \Box A$ 为 true 等价于 对于所有的 $n$， $\sigma^{+n} \models A$为 true ：

$\sigma \models \Box A \equiv \forall n \in Nat : \sigma^{+n} \models A$

一个很自然的泛化就是把action $A$ 换成 formula $F$：

$\sigma \models \Box F \equiv \forall n \in Nat : \sigma^{+n} \models F$

Important
 因此，$\sigma$ 满足 $\Box F$ 等价于 所有$\sigma$ 后缀的 $\sigma^{+n}$ 满足 $F$。

示例:

更多时态公式定义

  • $\eventual F \defeq \neg\Box\neg F$

  • $F \leadsto G \defeq \Box(F \mimply \eventual G)$

  • $\eventual\seq{A}_v \defeq \neg\Box[\neg A]_v$

    公式中A是一个 action ，$_v$ 是一个 state function，这表示最终某些step是一个改变了$_v$且满足$A$的step。

    如果定义 $\seq{A}_v \defeq A \land (v' \neq v)$ ，那么也可以理解 $\eventual\seq{A}_v$ 是 $\eventual$ 和 $\seq{A}_v$ 的结合，即最终有一个$\seq{A}_v$ step会发生。(这种理解不是完全正确的，因为 $\seq{A}_v$并不是一个合法的公式，只是一个简写)。

  • $\Box\eventual F$ 太好理解，不用解释

  • $\eventual\Box F$ 太好理解，不用解释

时态逻辑重言式(恒等式)

  • $\Box F \mimply F$

  • $\neg\Box F \equiv \eventual\neg F$

  • $\Box(F \land G) \equiv (\Box F) \land (\Box G)$

  • $\eventual(F \lor G) \equiv (\eventual F) \lor (\eventual G)$

  • $\Box\eventual(F \lor G) \equiv (\Box\eventual F) \lor (\Box\eventual G)$

  • $\eventual\Box(F \land G) \equiv (\eventual\Box F) \land (\eventual\Box G)$

  • $\Box\eventual(\seq{A}_v \lor \seq{B}_v) \equiv (\Box\eventual\seq{A}_v) \lor (\Box\eventual\seq{B}_v)$

时态逻辑推理规则(类似于MP规则)

  • 概括(泛化?)规则: $F \mimply \Box F$ ，表示 $F$ 为 true 时， $\Box F$为 true 。

  • 蕴含概括规则: $(F \mimply G) \mimply (\Box F \mimply \Box G)$

需要意与重言式与推理规则的区别。例如，上面的’概括规则’要求 $F$ 为 true 时才能推定 $\Box F$，但重言式没有这个要求，因为重言式的语义是永真的。

Liveness定义

liveness属性可以通过时态逻辑进行描述！

TLA+提供两种标准的(常用的)构建Liveness的符号

Weak Fairness

这些公式的等价性可以通过时态逻辑和命题逻辑的重言式进行证明。 如果用 $E$ 表示 $ENABLED\seq{A}_v$，用 $A$表示 $\seq{A}_v$。 则可以将 $WF_v(A)$ 可表示为 $\Box(\Box E\mimply\eventual A))$。

Strong Fairness