标签：Instantiation 4.2 代换 INSTANCE TLA 实例 模块 text Data

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

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

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

4.2.1 实例化是一种代换（Instantiation Is Substitution）

考虑第30页$Channel$Channel模块中的$Next$Next的定义，我们可以将定义中的符号用该符号的定义来代替。例如，我们可以通过展开$Send$Send的定义来消除表达式$Send(d)$Send(d)，这个过程可以不断重复。表达式$1-@$1−@中出现的“$-$−”(通过展开$Send$Send的定义获得)可以通过使用$Naturals$Naturals模块中的“$-$−”定义来消除，重复这种方式，我们最终获得$Next$Next的定义，它只包含$TLA^+$TLA+的内建运算符和$Channel$Channel模块的参数$Data$Data和$chan$chan。我们认为这是$Channel$Channel模块$Next$Next的“真正”定义。

$InChan \triangleq \text{INSTANCE }Channel \text{ WITH } Data \leftarrow Message,chan \leftarrow in$InChan≜INSTANCE Channel WITH Data←Message,chan←in

上述$InnerFIFO$InnerFIFO模块中定义的$InChan!Next$InChan!Next是在$Next$Next的“真正”定义中用$Message$Message代换$Data$Data，$in$in代换$chan$chan之后得到的公式。这样定义的$InChan!Next$InChan!Next只有$TLA^+$TLA+的内置运算符和模块$InnerFIFO$InnerFIFO的参数$Message$Message和$in$in。

让我们考虑一条任意的$\text{INSTANCE}$INSTANCE语句：
$IM \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$Σ为模块$M$M中定义的符号，设$d$d为其“真实”定义。$\text{INSTANCE}$INSTANCE语句定义$IM!\Sigma$IM!Σ是通过对任一$i$i，将$d$d中的$p_{i}$pi​用$e_{i}$ei​替换得到表达式。$IM!\Sigma$IM!Σ的定义必须只包含当前模块的参数(已声明的常量和变量)，而不包含模块$M$M的参数。因此，$p_{i}$pi​必须包含模块$M$M的所有参数，$e_{i}$ei​必须是在当前模块中有意义的表达式。

4.2.2 参数化实例化(Parametrized Instantiation)

FIFO规约使用了$Channel$Channel模块的两个实例，一个用$in$in代换$chan$chan，另一个用$out$out代换$chan$chan。我们也可以使用一个单一的参数化实例，如：
$Chan(ch) \triangleq \text{INSTANCE }Channel \text{ WITH } Data \leftarrow Message,chan \leftarrow ch$Chan(ch)≜INSTANCE Channel WITH Data←Message,chan←ch

对于定义在$Channel$Channel模块中的任意符号$\Sigma$Σ和任意表达式$exp$exp，$Chan(exp)!\Sigma$Chan(exp)!Σ等价于在公式$\Sigma$Σ中用$Message$Message代换$Data$Data，用$exp$exp代换$chan$chan。在通道$in$in上的动作可以被记作$Chan(in)!Rcv$Chan(in)!Rcv，$Send(msg)$Send(msg)在$out$out通道上也可以记作$Chan(out)!Send(msg)$Chan(out)!Send(msg)。

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

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

4.2.3 隐式代换（Implicit Subsititutions）

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

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

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

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

4.2.4 无重命名的实例化（Instantiation Without Renaming）

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

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

上述$Channel$Channel的实例化语句没用重命名，但是使用了代换，它将$Rcv$Rcv定义为$Channel$Channel模块中的同名公式，只是其中用$D$D代换了$Data$Data，用$chan$chan代换了$x$x。在使用表达式代换实例化模块的参数之前必须先定义它，所以这个$\text{INSTANCE}$INSTANCE语句必须在$D$D和$x$x的定义或声明的范围之内。

• 点赞
• 收藏
• 分享
• • 文章举报

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

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

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。