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

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

• 实例化本质上是一种代换，通过代换待实例化模块中的符号，最终得到的表达式只包含$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的定义或声明的范围之内。

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

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