一个时钟的例子
尝试用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(不变式),即不变式。
- 比如:HCInit断言hr是1到12的整数, []HCinit断言HCInit始终都是true,也就是说对于任何满足HCSpec的behavior,[]HCInit都是true,
- 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的不变式;