时序属性

Termination

最简单的时序属性是Termination，Termination是算法终止的要求，如果算法崩溃或者死锁或者进入一个无限循环，那么久违反了Termination规范。

假设有一辆车在过交通灯时，有红灯和绿灯两种选择，绿灯行，红灯停，红绿灯交替亮起。

NextColor(c) == CASE c = "red" -> "green"[] c = "green" -> "red"(*--algorithm traffic
variablesat_light = TRUE,light = "red";process light = "light"
beginCycle:while at_light dolight := NextColor(light);end while;
end process;process car = "car"
beginDrive:when light = "green";at_light := FALSE;
end process;
end algorithm;*)

上述代码在TLC中运行时，如果在Model Overview > What to Check? > Properties, 不选中Termination,则不会报错，选中Termination，运行时会报错Temporal properties were violated.查看Error-trace，发现有个Stuffering。

Stuffering && liveness

TLA+是动作的时序逻辑，Model的每一步检查都代表着时间上的一个动作，TLC的工作原理是查看每一步中所有启用的标签，并选择一个执行，然而TLC还有另外一种选择，即不执行任何动作，这种情况称之为stuffering。大多数情况下，stuffering不会改变规范，既然没有动作发生，那就什么都不会改变。但是如果一直stuffering,就好像是动作执行被阻塞的一样，状态不会改变。

所有的不变量的检查都是安全的，用来检查不会到达一个无效状态。由于有效状态下的stuffering还是一种有效状态，因此TLC通常不会尝试stuffering。然而在大多数时序属性用来进行活性检查，活性检查（liveness check）是验证系统最终能够按照期望运行。上述例子中，由于stuffering，规范运行将不会终止。

stuffering是有用的，它可以表示服务器崩溃或者进程超时，或者信号量永远等不到。如果要明确的排除stuffering，就需要增加fairness。

Fairness

fairness有两种：弱（weak）,强（strong ）。只要声明了fair的动作保持启用，就能达到弱公平性（weakly fair）。为上述例子添加fairness：

fair process light = "light"  \* 通过fair关键字添加fairness
beginCycle:while at_light dolight := NextColor(light);end while;
end process;fair process car = "car"
beginDrive:when light = "green";at_light := FALSE;
end process;

如果上述例子中只给进程car添加fair，运行Model check，仍然stuffering，light不会循环变更；如果只给进程light添加fair，运行Model check，发现car永远不会Drive。如果两个进程都添加fair，运行后还是会出错。出现问题的原因是如果light在green和red之间循环，那car进程的Drive也将不断在禁用和启用之间变更。因此为了保证Car能够完成Drive，需要light保持green。

这时候强公平性就起作用了，如果一个强公平性的动作反复启动和禁用，那该动作一定会发生。可以通过fair+ 来将进程变成强公平性。如：

fair+ process car = "car"
beginDrive:when light = "green";at_light := FALSE;
end process;

重新执行model check，这次将按照预期进行，不会出现错误。需要注意的是，在Car为fair+的情况下，仍然需要light为fair。

上述fairness的强弱都是针对进程的，fairness的强弱也可以针对算法或者标签。

 --fair algorithm    \* 针对算法A:+                 \* 针对标签A，如果A本来是unfair,添加+后，A将变为weakly fair\* 如果A本来是wf，则添加+后，A将变为string fair

时序操作符

首先定义P和Q为布尔语句

[]

[]等价于always。[]P意味着对于动作中的所有状态，P都是TRUE。

<>

<>等价于eventually,<>P意味着对于动作中的所有状态，至少存在一个状态是的P为TRUE或者最终态P为TRUE。

Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* 可以理解为最终所有的process状态都是Done

~>

~>等价于 leads-to。 P ~>Q 意思是如果在某个状态P为true，那么Q也为true或者Q在未来的某个状态为true。leads-to是不可逆的，一旦发生，即使P之后是false，那Q也必须出现为true的情况。

L == (light = "green") ~> ~at_light
\* 当light为green时，一定会导致at_light变更。前后具有因果关系。

[]<> and <>[]

[]<>P意思是P总是最后为true； <>[]P意思是P最后总是为true。对于有限的规范来说，这两个是相同的意思，P在终止是为true。但对于无限的规范来说，<>[]P意思是在某个状态上P为true，并永远保持true。而[]<>P意思是如果P变为false，P最终会再次变成true。

THE END!

通过例子学TLA+(十五)--时序属性相关推荐

通过例子学TLA+(十四)--宏，过程与标签
宏,过程与标签 TLA+在多进程之间复用代码,最简单的方法是使用宏和过程. 宏宏是通用的代码内联器,格式为 nacro Name(var1,...) begin\* stuff end macro; ...
通过例子学TLA+(十二)-- 函数与实例
函数和实例函数 TLA+中除了数字,字符串,布尔值,模型值 4种基本类型外,还有两种复杂类型,分别为集合和函数.函数构成了所有实用复杂类型的基础. 函数的形式看起来跟之前介绍过的操作符是一样的.函 ...
通过例子学TLA+(十)--集合
集合集合用大括号来表示,如{1,2},对于连续的数字集合有种特殊的表示方式,如 1-3 表示集合{1,2,3} 下表是集合的常见操作 Operator example 备注 \in 1 \in {1 ...
通过例子学TLA+(五)--FIFO Sequences
FIFO 本例子是一个先进先出FIFO的Buffer.Sender向Buff发送数据,Buffer接收数据存储在Sequence中,然后,Buffer将Sequence中第一个数据取出发送给Recei ...
通过例子学TLA+（一）-- HourClock
前言刚接触TLA+,将学习过程中的理解整理记录下来,用于加深理解和备忘.有对TLA+感兴趣的可以私信我,一起学习. TLA+简介 TLA+ 是一门形式规格说明语言(formal specificat ...
通过例子学TLA+(十三)--多进程与await
多进程之前使用的例子都是单进程的,现在用多进程来描述多个逻辑同时发生,TLA+中的多进程可以理解为其他高级语言中的多线程.为了方便理解,使用Pluscal语言来描述,TLA+ Toolbox可以将p ...
通过例子学TLA+(八)--表达式
表达式在之前的例子中,已经多次用到了表达式,常见的表达式中会用到大于,小于,等于,不等于等这样条件判断.还有一些其他的用法,比如逻辑连接,IF-ELSE 等逻辑连接逻辑连接在之前的例子中是用过 ...
通过例子学TLA+(二) -- DieHard
第二个例子DieHard 这是一个倒水的例子,初始一个3升容量的桶,一个5升容量的桶,水不限,如何倒出一个容量刚好是4升的水.在一部老电影DieHard中主角就面临这个问题,这里就将module名命名 ...
通过例子学TLA+（四）-- Send Rev Print
Send & Rev 稍微复杂点的程序中都会涉及数据的发送与接收,本例子基于发送器Sender与接收器Receiver来实现数据的变更.假设Sender发送一个数据给Receiver,Rece ...

通过例子学TLA+(十五)--时序属性