其他分享
首页 > 其他分享> > TLA+ 《Specifying Systems》翻译初稿——Section 4.2 Instantiation Examined(审视实例化)

TLA+ 《Specifying Systems》翻译初稿——Section 4.2 Instantiation Examined(审视实例化)

作者:互联网

本节详细说明了模块实例化的几个方面:

  • 实例化本质上是一种代换,通过代换待实例化模块中的符号,最终得到的表达式只包含TLA+TLA^+TLA+的内建运算符和当前模块定义的常量和参数;
  • 也可以将实例作为入参,这样只需要一条实例化定义语句即可;
  • 一条INSTANCE\text{INSTANCE}INSTANCE语句必须对待实例化模块的每个参数都有代换。如果有些参数ppp没有显式的代换,那么必然有一个隐式的代换ppp \leftarrow pp←p;
  • 只需要模块的一个实例时,可以不对实例重命名,如果有代换,则必须在参数的声明或定义的范围内定义INSTANCE\text{INSTANCE}INSTANCE语句;

在实际中除了用于隐藏变量这种习惯用法外,其实很少用到INSTANCE\text{INSTANCE}INSTANCE语句。所以,大多数读者可以跳过这一部分,直接翻到第4.3节。

4.2.1 实例化是一种代换(Instantiation Is Substitution)

考虑第30页ChannelChannelChannel模块中的NextNextNext的定义,我们可以将定义中的符号用该符号的定义来代替。例如,我们可以通过展开SendSendSend的定义来消除表达式Send(d)Send(d)Send(d),这个过程可以不断重复。表达式1@1-@1−@中出现的“-−”(通过展开SendSendSend的定义获得)可以通过使用NaturalsNaturalsNaturals模块中的“-−”定义来消除,重复这种方式,我们最终获得NextNextNext的定义,它只包含TLA+TLA^+TLA+的内建运算符和ChannelChannelChannel模块的参数DataDataData和chanchanchan。我们认为这是ChannelChannelChannel模块NextNextNext的“真正”定义。
在这里插入图片描述

InChanINSTANCE Channel WITH DataMessage,chaninInChan \triangleq \text{INSTANCE }Channel \text{ WITH } Data \leftarrow Message,chan \leftarrow inInChan≜INSTANCE Channel WITH Data←Message,chan←in

上述InnerFIFOInnerFIFOInnerFIFO模块中定义的InChan!NextInChan!NextInChan!Next是在NextNextNext的“真正”定义中用MessageMessageMessage代换DataDataData,ininin代换chanchanchan之后得到的公式。这样定义的InChan!NextInChan!NextInChan!Next只有TLA+TLA^+TLA+的内置运算符和模块InnerFIFOInnerFIFOInnerFIFO的参数MessageMessageMessage和ininin。

让我们考虑一条任意的INSTANCE\text{INSTANCE}INSTANCE语句:
IMINSTANCE M WITH p1e1,,pnenIM \triangleq \text{INSTANCE } M \text{ WITH }p_{1} \leftarrow e_{1},\cdots,p_{n} \leftarrow e_{n}IM≜INSTANCE M WITH p1​←e1​,⋯,pn​←en​

Σ\SigmaΣ为模块MMM中定义的符号,设ddd为其“真实”定义。INSTANCE\text{INSTANCE}INSTANCE语句定义IM!ΣIM!\SigmaIM!Σ是通过对任一iii,将ddd中的pip_{i}pi​用eie_{i}ei​替换得到表达式。IM!ΣIM!\SigmaIM!Σ的定义必须只包含当前模块的参数(已声明的常量和变量),而不包含模块MMM的参数。因此,pip_{i}pi​必须包含模块MMM的所有参数,eie_{i}ei​必须是在当前模块中有意义的表达式。

4.2.2 参数化实例化(Parametrized Instantiation)

FIFO规约使用了ChannelChannelChannel模块的两个实例,一个用ininin代换chanchanchan,另一个用outoutout代换chanchanchan。我们也可以使用一个单一的参数化实例,如:
Chan(ch)INSTANCE Channel WITH DataMessage,chanchChan(ch) \triangleq \text{INSTANCE }Channel \text{ WITH } Data \leftarrow Message,chan \leftarrow chChan(ch)≜INSTANCE Channel WITH Data←Message,chan←ch

对于定义在ChannelChannelChannel模块中的任意符号Σ\SigmaΣ和任意表达式expexpexp,Chan(exp)!ΣChan(exp)!\SigmaChan(exp)!Σ等价于在公式Σ\SigmaΣ中用MessageMessageMessage代换DataDataData,用expexpexp代换chanchanchan。在通道ininin上的动作可以被记作Chan(in)!RcvChan(in)!RcvChan(in)!Rcv,Send(msg)Send(msg)Send(msg)在outoutout通道上也可以记作Chan(out)!Send(msg)Chan(out)!Send(msg)Chan(out)!Send(msg)。

上述实例化定义了Chan!SendChan!SendChan!Send为有两个入参的运算符。用Chan(out)!Send(msg)Chan(out)!Send(msg)Chan(out)!Send(msg)取代Chan!Send(out,msg)Chan!Send(out,msg)Chan!Send(out,msg)只是语法的一种特性,它看起来和中缀运算符的语法一样奇怪。(中缀运算符要求我们写a+ba + ba+b而不是+(a,b)+(a,b)+(a,b)。)

参数化实例化仅在TLA+TLA^+TLA+语言中用于变量隐藏,在后面的第4.3节中有描述。你可以在不了解它的情况下使用它,不了解任何有关参数化实例化的知识也没关系。

4.2.3 隐式代换(Implicit Subsititutions)

因为我们之前在异步ChannelChannelChannel规约中的使用了命名DataDataData,在FIFO规约中使用MessageMessageMessage作为传输数值集合的名称就有点奇怪了,假设我们使用DataDataData代代替MessageMessageMessage作为InnerFIFOInnerFIFOInnerFIFO模块的常量参数,第一条实例化语句应该是:
InChanINSTANCE Channel WITH DataData,chaninInChan \triangleq \text{INSTANCE }Channel \text{ WITH } Data \leftarrow Data,chan \leftarrow inInChan≜INSTANCE Channel WITH Data←Data,chan←in

DataDataData \leftarrow DataData←Data代换表示用当前模块的表达式DataDataData代换实例化ChannelChannelChannel模块的常量参数DataDataData。TLA+TLA^+TLA+允许我们删除任何形式的代换ΣΣ\Sigma \leftarrow \SigmaΣ←Σ。因此,上面的表述可以写成
InChanINSTANCE Channel WITH chaninInChan \triangleq \text{INSTANCE }Channel \text{ WITH } chan \leftarrow inInChan≜INSTANCE Channel WITH chan←in

我们知道存在一个隐含的DataDataData \leftarrow DataData←Data代换是因为一条INSTANCE\text{INSTANCE}INSTANCE语句必须对实例化模块的每个参数都有代换。如果有些参数ppp没有显式的代换,那么必然有一个隐式的代换ppp \leftarrow pp←p。这意味着INSTANCE\text{INSTANCE}INSTANCE声明必须在符号ppp的声明或者定义的范围内。

用隐式代换进行实例化操作是比较常见的。通常,每个参数都有一个隐式代换,在这种情况下,显式代换列表是空的,WITH\text{WITH}WITH语句可以被省略。

4.2.4 无重命名的实例化(Instantiation Without Renaming)

到目前为止,我们使用的所有实例化都与重命名有关。例如,ChannelChannelChannel模块的第一条实例化语句将定义的符号SendSendSend重命名为InChan!SendInChan!SendInChan!Send。如果要使用模块的多个实例或单个参数化实例,则需要使用这种重命名。模块InnerFIFOInnerFIFOInnerFIFO中的InChan!InitInChan!InitInChan!Init和OutChan!InitOutChan!InitOutChan!Init是不同的公式,它们需要不同的命名。

有时我们只需要模块的一个实例。例如,假设我们要定义的系统只有一个异步通道,则我们只需要一个ChannelChannelChannel实例,因此不必重命名。在这种情况下,我们可以这样写:
INSTANCE Channel WITH DataD,chanx\text{INSTANCE }Channel \text{ WITH }Data \leftarrow D,chan \leftarrow xINSTANCE Channel WITH Data←D,chan←x

上述ChannelChannelChannel的实例化语句没用重命名,但是使用了代换,它将RcvRcvRcv定义为ChannelChannelChannel模块中的同名公式,只是其中用DDD代换了DataDataData,用chanchanchan代换了xxx。在使用表达式代换实例化模块的参数之前必须先定义它,所以这个INSTANCE\text{INSTANCE}INSTANCE语句必须在DDD和xxx的定义或声明的范围之内。

知之为知知 发布了4 篇原创文章 · 获赞 1 · 访问量 5599 私信 关注

标签:Instantiation,4.2,代换,INSTANCE,TLA,实例,模块,text,Data
来源: https://blog.csdn.net/robinhzp/article/details/104091930