TLA+ Specifying System (3)

一个时钟的例子

尝试用TLA描述小时级别的时序逻辑

[hr=11] -> [hr=12] -> [hr=1] -> [hr=2]

hr=11 状态的值为11

[hr=11] -> [hr=12]，一对连续的状态，称为一个step

要描述一个小时粒度的时钟，只需要描述所有的状态

HCInit == hr \in 1..12
HCNext == hr’ = IF hr = 12 THEN hr + 1 ELSE 1
HCSpec == HCInit /\ _hr

• HCNext是一个普通的formula，描述的是：old state到new state的转换，这是一个step
• 像HCNext这种的formula包含了：primed和unprimed变量的，称为action
• 一个action的值为true或者false
• []HCNext 表示HCNext always为true
• HCSpect描述的是: 对于任意的behavior，HCInit为true，并且每一个Next值always为true，也就是说HCSpect是这个系统的spec。

Stuttering steps

• Stuttering steps：允许某些behavior中state值不变。

考虑这样一个场景：当某个事件发生时，时钟就定格了，也就是在某个state之后state不会再更改。比如[hr=12] -> [hr=11] -> [hr=11] ，这个时钟系统在11的时候被stop了，也就说系统允许在任何hr的值退出。

这个formula可以表示为：HCNext / (hr’ = hr)，注意：这里的hr’ = hr说明系统允许在任何hr的值退出，因为TLA每次宽度遍历都进入hr’ = hr的话，那么state的值就一直是hr了。

TLA+中简称为：[HCNext]_hr，表明在可达的behavior中hr允许stuttering的behavior。

一个无限长的状态序列。比如：[hr=11] -> [hr=“abc”] -> [hr=0.12] -> [hr=e] -> …

一个behavior描述的是状态序列的空间中的一个可能。可以想象成深度遍历的解空间，一个behavior就是其中一个遍历路径。

• Temporal formula：是关于所有behavior的断言。是所有为true的behavior，合法的behavior
  比如：HCSpec == HCInit /\ [][HCNext]_hr 描述所有符合HCNet约束的behavior。HCSpec称为这个时钟系统的specification
• theorem：在任何behavior下都为true的formula称为theorem（不变式），即不变式。

1. 比如：HCInit断言hr是1到12的整数, []HCinit断言HCInit始终都是true，也就是说对于任何满足HCSpec的behavior，[]HCInit都是true，
2. HCSpec => []HCInit，在任何合法的behavior下都成立，因此是一个theorem。

完整的TLA+

----------------------------- MODULE hour ------------------------------
EXTENDS Naturals
VARIABLES hr
HCInit == hr \in 1..12
HCNext == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HCSpec == HCInit /\ _hr
THEOREM HCSpec => [] HCInit

• TLA+提供了一些基础的模块比如：Naturals（提供加法，减法等，用可以自己定义加法，比如两个矩阵的加法）， Sequence（列表数据结构）。
• TLA+中操作的任何变量都必须是声明过。
• 有一堆减号连接起来的横线，可以出现在任何地方，仅仅用来分割较为完整逻辑的一小段代码
• THEOREM HCSpec => [] HCInit 断言了由hour模块，Naturals模块和rules ofTLA+推断出来的一个formula（推论）
• HCInit，HCNext，HCSpec都是definition，TLA+是一门方便书写数学定义和推理的语言

总结

• 要描述一个小时粒度的时钟，只需要描述状态转变规则；
• stuttering steps允许状态机停留在任一点；
• behavior是状态序列；
• temporal formula是对所有behavior的断言；
• theorem是spec的不变式；