本节描述了异步接口的另一种写作方式,引入了记录的概念及其书写格式,在描述
next−state动作时引入了两种书写方式,并引入两个代指符号。
- 记录:类似C/C++语言的结构,Python的字典。
- 记录的书写方式
[r.val↦d,r.rdy↦1−chan.rdy,r.ack↦chan.ack]
-
next−state动作:
Send(d)≜∧chan.rdy=chan.ack∧chan′=[r.val↦d,r.rdy↦1−chan.rdy,r.ack↦chan.ack]
Send(d)≜∧chan.rdy=chan.ack∧chan′=[chan EXCEPT !.val=d,!.rdy=1−@]其中
!指代新记录,
@指代旧记录中的原值。
模块
AsynchInterface是对异步接口及其握手协议的详细描述,不过,目前它对调用该接口的其他系统不大友好,让我们以某种形式重写这个接口规约,以更方便地将其用作更大的规约的一部分。
原始规约的第一个问题是它使用三个变量来描述单个接口,其他系统可能调用接口的多个不同实例,为避免变量激增,我们用单个变量
chan(
channel的缩写)替换三个变量
val,
rdy和
ack。数学家可以通过将
chan的值设为有序三元组(例如用
[chan=⟨−1/2,0,1⟩] 代替
val=−1/2,rdy=0,ack=1。)不过程序员在编码过程中发现,使用这样的元组经常会出错,因为很容易忘记
ack是由第二个还是第三个元素表示。因此,TLA+除了提供更常规的数学符号外,还提供“记录”(
record)。
让我们用
val,
rdy和
ack字段将通道的状态表示为记录。如果
r是记录,则
r.val是其
val字段。我们可以定义类型不变量,声明
chan的值是所有此类记录
r的集合的元素:其中
r.val是集合
Data的元素,
r.rdy和
r.ack是集合
{0,1}的元素,该集合记做:
[val:Data,rdy:{0,1},ack:{0,1}]
记录的字段是不保序的,因此我们以何种顺序书写它们都无关紧要。同一组记录也可以写为
[ack:{0,1},val:Data,rdy:{0,1}]
在初始态,
chan可以等于该集合中
ack和
rdy字段相等的任何元素,因此初始谓词是类型不变量和条件
chan.ack=chan.rdy的合取。
调用该接口的系统可能执行以下操作:发送数值
d并执行其他一些依赖于
d的变更操作。我们想将这种操作表示为一个动作,该动作是两个单独动作的合取:一个描述
d的发送,另一个描述其他变更。因此,我们定义发送数据值
d的动作为
Send(d),而不是定义为发送一些未指定数值的动作
Send。“下一个状态”动作由
Send(d)步骤(对于
Data集中的某个
d)或
Rcv步骤满足。(
Rcv步骤收到的值等于
chan.val。)我们说
Send(d)步骤是一个关于
Data中某个
d的步骤,则意味着存在
Data中一个
d使得该步骤满足
Send(d)——换句话说,是个
∃d∈Data:Send(d) 步骤,因此我们定义
Next≜(∃d∈Data:Send(d))∨Rcv
Send(d)动作声明
chan′等于记录
r,其中
r.val=dr.rdy=1−chan.rdyr.ack=chan.ack该记录在TLA+中记做:
[r.val↦d,r.rdy↦1−chan.rdy,r.ack↦chan.ack](该符号在ASCII版本中记做“|->”。)由于记录的字段是无序的,因此也可以将该记录记做:
[r.ack↦chan.ack,r.val↦d,r.rdy↦1−chan.rdy]
Send(d)的使能条件是
rdy和
ack值相等,因此我们可以这样定义:
Send(d)≜∧chan.rdy=chan.ack∧chan′=[r.val↦d,r.rdy↦1−chan.rdy,r.ack↦chan.ack]
这样定义
Send(d)就很完美了,不过我更喜欢下面稍微不同的这个,我们可以说
chan′的值和
chan的值相等,除了
val等于
d且
rdy等于
1−chan.rdy之外。在TLA+中,我们可以将之记做
[chan EXCEPT !.val=d,!.rdy=1−chan.rdy]用
!代表新记录,用
EXCEPT 表达式描述对
chan的修改,则该表达式读作:“新纪录
!与
chan相等,除了
!.val等于
d,且
!.rdy等于
1−chan.rdy”,
在表达式
!.rdy=1−chan.rdy 中,用符号
@表示
chan.rdy,我们可以将之改写为:
[chan EXCEPT !.val=d,!.rdy=1−@]通常,对于任何记录
r,表达式
[r EXCEPT !.c1=e1,…,!.cn=en]
是通过对
i∈1..n中的每个
i用
ei替换
r.ci而获得的记录。用
@代替
ei,我们得到定义:
Send(d)≜∧chan.rdy=chan.ack∧chan′=[chan EXCEPT !.val=d,!.rdy=1−@]
Rcv的定义很简单直接,当
chan.rdy不等于
chan.ack时,可以接收一个值,且收到该值后要转置
chan.ack:
Rcv≜∧chan.rdy=chan.ack∧chan′=[chan EXCEPT !.ack=1−@]完整的规约如下图3.2: