4 Temporal Logic of Action

TLA就是"Temporal Logic of Action"。

我们在刚开始学微积分的时候，觉得最痛苦的概念是什么？无穷和极限，这两者有一定关系。微积分是动态连续系统的无穷和极限，Temporal Logic是动态离散系统的无穷和极限。有一篇论文做了同构映射，把Temporal Logic和一个拓扑空间建立了一个映射，以此来证明Temporal Logic的完备性。这个东西为何就能表示所有行为呢？它必须是完备的？怎么证明呢？一旦建立一个同构映射，你就会发现是完备的。Lamport的大部分工作都在试图简化Temporal Logic，把它变得更容易理解，他才提出了TLA。他觉得在理论上这个思想很好，但不实用，因为太复杂。

4.1 A Digital System - A One-Bit Clock

这是Lamport最喜欢用的例子。

4.1.1 Specifying the One-Bit Clock

这是一个one-bit clock，横坐标是时间，纵坐标是电压，周期性的0、1、0、1 ……。这是物理世界，它有波动，在现实世界不可能实际执行。这其实是一个连续系统，上升沿和下降沿是连续的，只能说很陡但不可能断掉。

我们来看的时候，就把它变成一个动态离散系统，理想化。首先是平的，然后把上升沿和下降沿的动态连续过程去掉，就变成了一个动态离散系统。在这个系统里，时间多少，我们目前不关心，一段可能是1秒或其他值。对于正确性而言，如果不是Real-time系统的话，我们谈S1和S2，不谈S1到S2多长时间。对于并发系统，大部分正确性问题都是步骤之间的交错产生的，而并不是每一步时间长短产生的。但对于有些系统来讲，这个系统如果在1秒内没有Next掉就是错的，这种系统我们称之为Real-time系统。

这个系统能不能用TLA+表达呢？肯定能，而且很简单。

我们先不关心时间，把时间去掉，就变成上面这样，0、1、0、1 ……。用TLA+如何表达呢？

状态是v。Init是v = 0。Next是异或。

状态序列如上图，我们很熟悉了，描述起来也轻而易举。

对这个系统的描述如上所示。state transition有多种方法，这里只是展示了其中一种。

这是一个无穷序列，这个序列会一直走下去，除非它坏了，停止了。停止之后，要么1、要么0，不变了。

4.1.2 Specifying it with One Formula

What Could be More Elegant?

这个写法能不能再优雅些？虽然Lamport不追求优雅，但如果跟实用性之间有冲突的话，他永远让它更实用。如果不破坏实用性，还是要追求优雅的。能否让公式写得更优雅点呢？如果是你，你会怎么想，让它更好一点呢？

Specifying it with one formula.

用一个公式来表达。用一个公式涵盖整个全局的序列。这跟我们在学极限的时候很接近。

TLA的核心就是解决这个问题的。对于一个有无穷序列的系统行为，如何表达系统行为。

4.2 Temporal Formula

4.2.1 Concepts

先讲几个概念。这些概念讲完之后，大家对于前面的CONSTANT就知道什么意思了。

首先它是一个Formula，是个公式。什么叫时态公式呢？一般的Formula，在一阶逻辑里，x = 3，那么x永远等于3。时态公式就是说，对同一个x，在不同的时间可以有不同的值。x在状态S1有一个值，在状态S2有不同的值，在S3有不同的值。它是描述变化的，就像微积分一样。这就是Temporal Formula与Formula的区别。在Formula里，x的值永远是固定的，在Temporal Formula里，时刻不一样，x可以取不同的值。

4.2.1.1 Flexible variables

那些可以在不同时刻取不同值的变量，我们称之为Flexible variables，灵活的变量，也称之为temporal variables，一般用VARIABLE或VARIABLES表达。VARIABLE定义的就是时态变量，时态变量是可以加prime的，prime的意思就是在不同状态下它的值不一样。这就是VARIABLE的精确含义，它在时态逻辑里称之为Flexible variables。

4.2.1.2 Rigid variables

Rigid variables，严格的变量，用CONSTANT来表达，在所有状态下都不能变化。例如：宇宙常数、领域里的常数。

4.2.1.3 Syntactic levels

在Temporal Formula里，语法是分层次的。

• 最小的层次为第0层，即constant表达式，例如：1 + 2、2，在这个表达式里不包含任何temporal variables，只有constant。
• 第1层，state function、state predicate，在第1层里只包含current state，不包含next state，它里面有temporal variables，它是个表达式。如果x是temporal variables，x + 3、x > 3都是state function，但如果state function返回布尔值的话，称之为state predicate，例如x > 5。state predicate是state function的一种。在这一层只有temporal variables，当前状态，不包含prime。
• 第2层，转换变迁函数transition function，或transition predicate，即action。action就是Temporal Logic of Action的Action，是Lamport加进去的，因为Temporal Logic很复杂，他加了Action。它里面有next state。例如：x' = x + 1，就是一个transition function。transition function一般来说不是很有意义，transition predicate最有意义，因为它是布尔值的，一般也都返回布尔值。第2层包含了primed和unprimed之间的关系。

4.2.1.4 Transition Predicate Examples

这些都是action，都是transition predicate。

4.2.1.5 ENABLED

ENABLED的主要是action。对于一个action A来讲，A是个formula，ENABLED A也是个formula，它是一个state predicate，即只包含当前状态。A是一个action，A是个formula，里面肯定有x'和x，ENABLED A只需要x。就是说，对于当前状态里的那些变量，那些state predicate如果为真的话，ENABLED A为真。ENABLED A的意思是，如果A这个action要发生的话，s -> t要发生，那么当前状态s的这些变量满足什么条件才能发生，就是ENABLED A。A是s到t，现在只看s，s里肯定没有primed。如果A里不包含任何x的话，只有primed，没有非primed的话，ENABLED A永远为真。

图中的例子，x' = x / 2 \/ x' = -x / 2肯定不是state predicate。x % 2 = 为真的话，A就被enabled了。因为我们是在宇宙无穷的状态里选，只要ENABLED A为真肯定有next，只是找出来一个并不是创造出一个。Enabled A只要发生了，一定有s到t。s到t实现了一定ENABLED A，这两个是if and only if。ENABLED A为真，就有next step；next step存在，ENABLED A一定为真。

4.2.2 Temporal Formula

4.2.2.1 Formula Satisfied by Behavior

前面讲的一阶逻辑是关于一个状态的判断。我们说x > 2就是在当前状态下x大于2。temporal formula是关于行为的。TLA+的"+"静态部分是关于行为里的某一个状态的。现在要关注整个行为，想对整个行为做论断。

在S3下x = 5，这是一个普通的logic。我们用σ0、σ1、σ2 ……表示状态，σ是一个无穷的状态序列、一个行为。一个behavior就是一个状态序列。在σ里面，如果它有一个x，x永远等于3，那就是说对于σ中的每一个状态x都等于3。这就是对于行为的描述，就是temporal logic。

对于σ这样一个序列，如果里面有y，y最终肯定要等于0，但在哪个地方等于0我不管。这也是一个对于序列的论断。我没有指定某个状态，要么是所有状态，要么是我不指定某个状态。这用前面讲的逻辑是表达不了的。

时态逻辑的核心在于它是对一个行为的论断/谓词。

σ表示一个行为，对于行为中的每一个状态x都等于3。这句话用前面学的逻辑表达不了了，因为x一定指current state，最多两个状态x' = x + 3。这个逻辑假设不存在，要发明它，希望能对整体行为做论断，所以发明一个新的逻辑，起个名字叫temporal logic。

图中的σ0、σ1、σ2分别对应不同的时间，每个时间点状态的值都会变化，可以论断整个时间，也可以论断未来肯定有某个时间点y等于0，哪个时间点不管。

这个逻辑很有用，对并发程序写出非常有趣的属性Property。

做个记法，图中的σ+n(+n是右上角图标)，n是自然数。σ+n(+n是右上角图标)可以认为是σ的任意后缀，包含它本身(n = 0)。

如果不特殊说明，F都是指之前学过的formula，即正常逻辑的formula，不是时态逻辑的formula。"|="这个符号称之为满足(satisfy)，σ |= F表示行为σ满足F，这里的F就是之前学的公式。这里只是一个记法，后面会讲什么叫satisfy。如果F对这个行为为真的话，就说这个行为满足这个F。

什么叫公式对行为为真，还没有给它语义。可以先来看一下语法层面。

• 如果行为σ满足(F /\ G)，那么σ满足F且σ满足G。这是一个永真式。
• 如果行为σ满足¬F，那么σ不满足F。
• 如果行为σ满足(F => G)，那么σ满足F蕴含σ满足G。

什么叫一个行为满足一个公式，或者说这个公式对这个行为来说为真，现在给出严格的定义。x = 3是一个formula，是当前状态下x等于3。一个行为满足x = 3是什么意思呢？

• 如果P是一个state predicate，例如x = 3，那么它肯定是一个formula，我们说行为σ满足P这个state predicate当且仅当这个predicate被行为的第一个状态满足。如果行为的第一个状态满足x = 3，这个行为就满足x = 3。

给个序列，这个序列里只包含一个x。

σ: 5 -> 8 -> 10 -> ...

P: x = 3 -> FALSE，σ不满足P
P: x = 5 -> TRUE，σ满足P

因为这里的formula只能针对current state，但σ是个行为，所以我们只关心第一个状态。如果一个行为满足formula，或者说这个formula对这个行为为真，如果这个formula是state predicate的话，只关心第一个状态。

这是定义。根据这个定义可以导出x = 3 denotes ……。

x = 3这么一个formula，满足它的行为有多少？所有的行为，只要包含x，而且开始x等于3，都是满足这个公式的。所以x = 3其实是一个行为集合，这个集合里每一个行为的状态都有一个x，而且第一个状态的x一定等于3。

• 如果A是一个action，action里有prime和非prime，什么叫一个行为σ满足action呢？这个行为的前两个状态满足这个action。其实就是两个状态，一个prime、一个非prime。

σ: 5 -> 8 -> 10 -> ...

A: x' = x + 3 -> TRUE，σ满足A
P: x' = x + 4 -> FALSE，σ不满足A

x = 3 /\ x' = x + 1是一个Action，这个formula包含了哪些行为？第一个状态是3、第二个状态是4的所有行为。

x ∈ Nat /\ x' = x + 1，这个formula包含了哪些行为？第一个状态和第二个状态为连续两个自然数的所有行为。

把经典逻辑里的公式拿到行为上来看，原来看一个状态，现在看一个序列，给出一个最基本的定义。随便一个序列，只关心头两个状态，根据数学归纳法就可以推演出所有状态。思路是一样的，先把头两个状态定义好。

接下来正式进入Temporal Formula，我们引入两个Temporal Operator。

Temporal Logic有两个分支：Linear和Tree。Linear认为时间是单调增的，Tree认为有平行宇宙存在。Tree很复杂，但在动态离散系统里Linear就够了，不需要Tree。但相信在量子计算，肯定是需要Tree Temporal Logic。LTL就是Linear Temporal Logic。

4.2.2.2 Temporal Operator []

这个操作符叫box，ASCII写法就是两个中括号[]。它的意思是：F是一个一阶逻辑的formula，加一个修饰符Temporal Operator，即[]F，也是一个formula，如果一个行为σ满足[]F，即[]F对行为σ为真，任给n属于自然数，σ+n(+n是右上角图标)也是一个行为序列，当n等于0的时候，就是σ本身，≡右边的公式意思就是σ的所有后缀都满足F。

如果P是一个state predicate，σ的所有后缀的第一个元素都满足P，这个序列的每个状态P都为真，称之为[]P。就是前面讲的invariant，invariant如果用init/next写的话，就是之前的表达方式，如果用temporal formula写就是这个写法。

如果A是一个action，σ的所有后缀的前面两个元素满足A，那就是任给Si和Si+1属于σ，Si、Si+1都满足A，就是说A这个action对于σ这个序列里的任意两个相邻的状态都为真。

box也称为always，永远为真。

这样很自然地把一阶逻辑推演到时态逻辑了。

行为σ满足的公式的意思是什么？

这样我们可以从整体上考虑行为，我们可以根据定义推演一下。

• 第1步，根据[]的定义，任给n属于自然数，σ+n(+n是右上角图标)满足(x = 1) => [](y > 0)，把第1个[]先去掉了。
• 第2步，根据=>的定义，任给n属于自然数，如果σ+n(+n是右上角图标)满足(x = 1)，那么σ+n(+n是右上角图标)满足[](y > 0)。
• 第3步，根据[]的定义，把第二个[]去掉，任给m属于自然数，σ+n+m(+n和+m是右上角图标)满足(y > 0)。

假设σ序列包含两个状态x和y，做了什么断言？

假设n等于3的时候，x等于1，σ+n(+n是右上角图标)满足(x = 1)为TRUE，那么从3往后y大于0。如果在一个序列里，x曾经等于1，那么从此往后y永远大于0。

这就是如何描述"如果x等于某个值，y永远怎么样"这样的性质，在某个点上，我也不知道哪个点，x等于1，y肯定大于0，这个性质是保证的，可以这样去描述，工具可以帮你check。

觉得好像很含糊的含义，很简单地就能表达出来。在我们去验证属性的时候，特别是我不关心中间的步骤，只关心最终的全局属性的时候，... 【Faye：听不清】。

4.2.2.3 Temporal Operator <>

数学里很好玩，一般都会出现对偶的现象，或和与、任给和存在，这里也不例外。

这个操作符是不稳定的box(课上就说菱形)，ASCII写法就是尖括号<>。它的意思是：如果F是一个formula，<>F也是一个formula，我们这样定义，如图。如果把两个¬去掉，就是F永远为真，[]¬F的意思是F永远为假，¬[]¬F的意思是F不永远为假，那就是存在F为真。<>F的意思是"not always not F"，一般称之为eventually F，在序列的某一个点的状态上为真，哪个点我不关心。如果行为序列σ满足<>F的话，在这个序列的某个点上F为真，哪个点我不关心。这种描述非常适合我们去描述一个属性，知道它一定要发生，但什么时候发生我不关心。

以上是最基本的两个公式，通过这两个公式，我们可以非常生动地去描述行为的属性。我们就可以把一阶逻辑应用到整体的行为上去。

什么叫x永远都是3呢？[](x = 3)。y最终要等于256？<>(y = 256)

Temporal formula很容易写错，Lamport在此基础上加了很多约束、规范，告诉你如何去写，但还是会写错。正常情况下，大部分Specification都不需要写时态逻辑，如果关注正确性的话，大部分属性都不需要时态逻辑，前面用Init/Next，然后在Invariant里加上约束就足够了，这种check方法就足够了。除非写复杂的分布式并发系统，需要Safety和Liveness检查才需要写时态逻辑。

4.2.2.4 Temporal Formula with Operators

• <>[]F："eventually always F"，在某一个点之后F永远为真。
• []<>F："always eventually F"，存在无穷多个点F为真。有一个σ序列，任给一个后缀，总要包含一个F为真。
• F ~> G："F leads to G"，如果F在某个点上为真了，那么G一定在后面的某个点上为真。如果我收到一个用户的请求，系统一定在后面某个点上给用户回应，类似这种属性检查。一个处理用户请求的并发系统，这个系统对不对呢，这个系统对用户请求肯定有回应，如何保证呢，可以写一个属性，F定义成收到一个用户请求了，G定义成系统给回应了，F ~> G，如果在某个点上收到用户请求了，系统一定给回应。并没有说经过多少步骤，算法不一样，步骤不一样。

这三个是最常用且比较简单的公式，可以在现实世界里很完美地定义属性，解决现实问题。

通过时态逻辑operator和经典Operator(Faye：逻辑公式？)，就可以描述行为的属性。

4.2.2.5 Existential Temporal Quantifier

这个用得很少，稍微提一下。如果想引入Module，实现隐藏才会用到。

前面学过一个"存在"，是静态的。这里是Temporal存在符，它指的是，存在一个temporal variable x，temporal variable不是一个值，它有好多值，可以认为这个x在任意时刻都有个值，这个值可以让F为真。本来是一个值，现在是一个序列。x是一个序列，F是一个时态逻辑。

4.2.2.6 Hierarchy of Expression Levels

梳理一下，记得更牢。

表达式有几个层次。predicate就是逻辑表达式，那些非逻辑表达式最终都要拆到逻辑表达式中。所以我们一般关心predicate。

• constant predicate是state predicate的降级，因为没有temporal variables。
• state predicate是action的降级，因为没有prime。
• action是temporal formula的降级，因为action是两个状态，而temporal formula是整个状态序列、整个行为。

If the value of A is TRUE at some point in time, then []A is not the same as []TRUE. 假设A是个state predicate，A在某个点上为真，[]A和[]TRUE一样吗？

[]TRUE是universe的behavior，因为所有的行为都满足它。A在某个点上为真跟[]TRUE完全是两回事。[]A是指，存在一个行为，这个行为的任意两个状态，A永远为真。[]A只是某个行为，[]TRUE是整个universe。

4.3 A Digital System - A One-Bit Clock Again

4.3.1 Specifying it with one TEMPORAL Formula

回到原来的问题了，工具都交到大家手上了，怎么解决这个问题呢？

什么叫一个行为序列的初始状态是v = 0？什么叫v = 0开始的所有行为？ 我们称行为σ，σ满足一个P，P是v = 0。写一个v = 0就表示了v = 0开始的所有行为。但是不精确，太多了。v = 0在时态逻辑里就是包含了以v = 0开始的所有的行为序列。但是太多了，我只关心图上的序列。那怎么过滤呢？通过另外一个条件，另外一个条件跟v = 0是什么关系？与。

一个σ满足这个时态公式，第一个状态满足v = 0，并且任何两个相邻的状态都满足[](v' = (v + 1) mod 2)。就是前面图中的序列了。

其实并不是一个行为，还有好多行为，只是我们不关心，对我的属性来说不重要，不关心其他变量，不参与属性的check。

4.3.2 Actions are not Imperative Assignment Statement

actions是一个formula，不是赋值。赋值是创造行为的下一个状态，x = 2，下一个状态x = x + 3。而actions是过滤，行为已经存在了，过滤出所需要的行为。我描述出来我需要的行为，而不是说我创造一个行为。

想一想为什么程序会有Bug？ 我们编的程序都是在创造行为，写x = x + 5，创造了下一个比现在的值多5的状态。但现在我们描述我们想要什么行为，行为存在了，我想要什么样的行为呢，那就用逻辑表达式过滤。这是两个完全不同的思维。什么叫specification？你描述你想要什么，别人才能给你什么。而不是说我自己埋头干，不管我想要什么，先干出来再说，当然有bug了。

用":="来表示赋值。x := x + 1的时候觉得y没变。但action x' = x + 1，y可以为任意值，都是真的，这个公式蕴含了很多不确定性，这个不确定性是良性的，我们需要。x' = x + 1 /\ y' = y表示y不变，可以用UNCHANGED来表达。

要转换思维，别人什么都有，你要想清楚你想要什么，别人才能给你什么。而不是说你也不清楚你想要什么，就直接创造行为，而这个行为又不是你想要的。

任意一个整数开始的连续的整数，全部都在这个序列里。

4.4 A Two-Bit Clock

觉得temporal logic已经很不错了，但其实也引入了问题。当然这些问题不用我们自己去发现，Lamport已经改进好了。接下来讲，这些问题是什么，如何解决的。

4.4.1 A Two-Bit Clock

4.4.1.1 Problem

如上图所示，假设有一个设备，里面有个v，v不动，现在设备增加一个布尔w，w的跳变频率是v的两倍。现在系统里除了v，还有w。

做完抽象之后，如上图所示。这个状态序列如何描述呢？

序列如上图所示。w是每步都变化，v是两步一变。

假设有一个物理设备，一开始只有v时钟，后来又加了一个w时钟，加了w之后的v还是不是原来的v了？肯定认为v没区别，这是一个合理的认知。

忽略w，v还是原来的v。

问题是，把w去掉以后的v的序列已经不被之前的公式允许了。

这时有两种方法，一种是你觉得现实错了、我这没问题，另一种是描述有问题、现实是对的。如何解决呢？换个说法，这个问题更深层次的含义是什么？这是一个非常深刻、非常有价值的问题。

视角的问题。盯着v看的时候，0、1、0、1、……。假设电子表只看时、不看分，1点、2点、3点、……。把分拿出来看的话，你会发现时不变、分在变。公式是现实的解释与呈现。是视角问题。写Spec也一样，写图中的系统行为的时候，代表有其他的变量在变化，但目前的Spec容纳不了这种变化，我们希望Spec能够容纳这种变化，这样容纳性更强。对公式进行改造，改造完后，可以容纳从不同视角观察这个世界。盖上分钟、小时这样变，不盖上分钟、小时这样变————0、0、0、……，小时60个0跳1次。其实这是同样一个系统。希望引入一种方式能够容纳这种现实情况。

TLA能够具有抽象代数的结构就是因为这个引入。

4.4.1.2 Solution - Stuttering Steps

公式允许不改变v的步骤存在，这是一个很自然的想法，这样涵盖性更强了。

4.4.2 Stuttering

4.4.2.1 Stuttering Free

一个行为σ，我们定义♮σ(左上角)为stuttering-free form of σ。stuttering-free的意思是没有stuttering。

把σ中的所有连续重复状态的有限子序列替换成一个状态。图中的例子，3个b变成1个b了。无限的只能出现在最后，结尾无穷的重复不管。

这就是stuttering free的概念。给我一个行为，我扫一遍，把中间那些有限、连续的重复替换成一个状态。

4.4.2.2 Stuttering Equivalent

行为σ和τ在stuttering的情况下是equivalent的，当且仅当♮σ = ♮τ，它们的stuttering-free形式一样。a a b b b ...和a a a b b ...这两个行为stuttering-equivalent，因为它们的stuttering-free form是一样的。

数学里非常重要的一点就是定义什么叫相等。这应该是数学里最精华的部分，也是最难的部分。

4.4.2.3 Stuttering Invariance

对于任何公式F，F可能是一个temporal logic formula，定义S是所有满足F的行为的集合。我们说F在stuttering的情况下是不变的，如果对于S中的每一个行为，所有和它stuttering-equivalent的行为都属于S。如果σ属于S且σ和τ它俩stuttering-equivalent，那么τ也属于S。

这种stuttering-invariance formula不能区分两个stuttering-equivalent的行为。But那个页面的之前的one-bit clock的temporal formula是可以区分的。如何让这个formula变成stuttering-invariance formula？

要么(v + 1) mod 2，要么不变。

4.4.2.3 Stuttering Invariant Formula

我们如果这样写，就是允许v不变。

TLA里所有的formula都是stuttering invariant formula。

如果v一直等于0是否满足这个公式？满足。 第一个v = 0、后面全是1，是否满足这个公式？满足。

如果用TLC，会报一个stuttering steps错误，意思是后面都重复都一样。

这个问题我们后面会解决。

带有w时钟的系统的所有行为都是目前行为的子集。

4.4.2.4 What stuttering invariance buy us?

Init + Safty + Liveness

σ

http://kaelzhang81.github.io/2018/04/08/%E5%BD%A2%E5%BC%8F%E5%8C%96%E8%A7%84%E8%8C%83%E8%AF%AD%E8%A8%80TLA+/