什么是 TLA+

• 数学

• 公里语义的形式化语言

• 系统规格定义语言

简单、实用、高表达力的设计语言

可调试、可自动穷尽式验证

一线工程师容易掌握

设计哲学

simple example

这段代码什么意思？

如何知道的？

机器模型： C 语言 -》 汇编语言 -》 机器指令

C 语言合适么？

为何不需要在机器层面上去理解这个程序的语义？

C 语言模型简单么？

C 语言合不合适对于计算进行形式化的描述呢？

• 刚开始学 C 语言的时候理解变量和数学领域里是不一样的

• 需要程序跑起来

• 从数学角度不是字包含解释的，需要机器模型

所以需要一个更简单的模型描述这个计算。

正确么？

调用一次 foo 后，y = 3，正确吗？

我们在脑子里计算了一下，其实脑子里有一幅图的：

所以 y=2

程序控制流

控制流状态显示化

状态空间

如何选出我们期望的状态序列？

• 如何找出 S1

• 如何通过 Si 找出 Si+1

其实也就是找出过滤条件。

精确的表达

初始状态的表达

是针对单一状态的变量的布尔表达式

状态迁移的规则

是针对两个状态的变量间关系的布尔表达式

数学语言的表达

TLA+的表达

结果

总结

状态机是通用的计算模型，任何其他计算形式都可以表述为状态机

我们没有实际去构造状态序列，而是描述了状态序列要满足的属性！！

• 状态变量的构成

• 每一步的大小

练习

-------------------------------- MODULE lec1 --------------------------------

EXTENDS Integers

VARIABLES x,y,pc

Init == y = 1 /\ x = 0 /\ pc = "L1"

Next1 == pc = "L1" /\ x' = y /\ y' = y /\ pc' = "L2"

Next2 == pc = "L2" /\ x' = x+1 /\ y' = y /\ pc' = "L3"

Next3 == pc = "L3" /\ x' = x /\ y' = y /\ pc' = "Done"

Next == Next1 \/ Next2 \/ Next3

=============================================================================

这是个模型的描述，我们现在要运行一下这个模型。

就是把这个模型满足的行为全部产生出来

TLC

deadlock

和常规理解的死锁不一样。是指当前的状态下，已经再也找不到。

即没有 NEXT 可以满足了。

invariant 不变性

所有状态都要满足的属性

例如：

y /= 2

ERROR Trace

整个状态跃迁过程

练习

Init == y \in 1..5 /\ x = 0 /\ pc = "L1"

invariant：y /= 6

-------------------------------- MODULE lec1 --------------------------------

EXTENDS Integers

VARIABLES x,y,pc

Init == y \in 1..5 /\ x = 0 /\ pc = "L1"

Next1 == pc = "L1" /\ x' = y /\ y' = y /\ pc' = "L2"

Next2 == pc = "L2" /\ x' = x+1 /\ y' = y /\ pc' = "L3"

Next3 == pc = "L3" /\ x' = x /\ y' = x /\ pc' = "Done"

Next == Next1 \/ Next2 \/ Next3

===============================================================

TLA+ 用到的数学

一阶逻辑和集合论(+的部分)

• 变量数据结构定义

• 状态机定义

• 定义不变性

时态逻辑

整体上定义行为和属性

一阶命题逻辑

集合操作

谓词逻辑

集合构造器

Simple Operaors

High Order Operators

Sets Filtering

Sets Mapping

Tuples

Sequences

Structures / Records

练习

Functions

Function Set

练习：汉诺塔

清晰的思考和表达

• 状态有哪些？如何表达？

• 如何定义行为？

• 如何定义不变性？

小总结

• 用代码来写，层次太低了

• 用自然语言来写，不精确，写出来其实并不一定想清楚

• TLA+会迫使你思考，输出对系统理解精确的表达

时态逻辑