10.1 组合两个规范

以时钟为例，研究两个时钟组合而成的系统。如果我们把两个时钟的规范通过合取连接，经过化简后，“两时钟”系统会多出一个 next 步，表示两个时钟同时发生改变，这种规范叫做非交错规范。与其相对的交错规范指的是子组件不同时改变的规范。

如果我们想要“两时钟”系统是一个交错规范，可以通过下面两种方式之一解决：

  1. 让每个时钟的 next 动作显式合取另一个时钟的变量保持不变

  2. 依然合取原始的单个时钟的规范，但是再合取[][(x' = x) \/ (y' = y)]_<<x, y>>，其中x、y是两个时钟的小时值

10.2 组合多个规范

在涉及组合多个规范的交错规范时，上一节的方式 1 就变得不合适了，因为让子组件去限制其他所有组件比较复杂。我们将方法 2 进行泛化：

[][\E k \in C: \A i \in C \ {k}: vi' = vi]_<<v>>

这个公式表示只有vk在改变，其他vi都不变。

回到时钟的例子。如果是多个时钟的组合而成的子系统，其中hr[k]表示第k个时钟显示的小时的数组。上面公式的v能否用hr替代呢？答案是不能。因为hr没有被限定定义域，因此可能在意料之外的定义域上有未预期的行为。解决这个问题有两种方式：

  1. 用hrfcn == [k \in Clock |-> hr[k]]代替v

  2. 合取一个运算符[]IsFcnOn(hr, Clock)，其中IsFcnOn(f, S) == f = [x \in S |-> f[x]]

另外，我们可以利用EXCEPT进一步简化组合规范N(k) == hrfcn' = [hrfcn EXCEPT ![k] = (hr[k] + 1) % 12]

10.3 FIFO

FIFO 模块的自由变量是in、out两个Channel，以及Message消息集合。FIFO 由如下三个组件组合而成：Sender 影响in.val、in.rdy，Buffer 影响in.ack、q、out.val、out.rdy，Receiver 影响out.ack。我们可以注意到有的初始化公式是跨组件的：(in.ack = in.rdy) /\ (out.ack = out.rdy)。对于跨组件的公式有如下三种处理方法：

  1. 在公式涉及的所有组件的初始化公式中，重复地声明该公式

  2. 选择一个组件，在它的初始化公式中声明该公式

  3. 在所有组件的外部独立声明该公式。

在描述开系统时，需要使用后两种方法。

10.4 带有共享状态的组合

10.4.1 显式状态变化

把上面的 FIFO 规范中的 Buffer 组件进行简化，用一个普通的buf序列代替，FIFO 就只剩下了 Sender 和 Receiver 两个组件，并且它们共同修改buf变量。这里的buf就是组件间的共享变量。我们尝试把整体的 FIFO 规范逆向分拆成两组件规范，Sender 和 Receiver 的步如下：

Sndr == \/ /\ buf' = Append(buf, ...)
           /\ SCommunicate
           /\ UNCHANGED r
        \/ /\ SCompute
           /\ UNCHANGED <<buf, r>>

Rcvr == \/ /\ buf /= <<>>
           /\ buf' = Tail(buf)
           /\ RCommunicate
           /\ UNCHANGED s
        \/ /\ RCompute
           /\ UNCHANGED <<buf, s>>

两个组件的初始状态容易指定，但是Next步比较难分拆。我们使用NS、NR表示 Sender 和 Receiver 的 Next步

NS == Sndr \/ (sigma /\ (s' = s))
NR == Rcvr \/ (rho   /\ (r' = r))

其中sigma和rho是仅关于共享变量buf的动作，更准确地说，是不由自己引起的buf变化。

我们尝试从分离的NS和NR合取得到组合系统的规范，即

[][NS]_<<buf, s>> /\ [][NR]_<<buf, r>> <=> [][Sndr \/ Rcvr]_<<buf, s, r>>

首先对上式左边进行化简：

[][
    /\ Sndr \/ ((sigma /\ (s' = s)) \/ UNCHANGED <<buf, s>>)
    /\ Rcvr \/ ((rho   /\ (r' = r)) \/ UNCHANGED <<buf, r>>)
]
==
[][
    \/ Sndr /\ Rcvr
    \/ Sndr /\ ((rho /\ (r' = r)) \/ UNCHANGED <<buf, r>>)
    \/ Rcvr /\ ((sigma /\ (s' = s)) \/ UNCHANGED <<buf, s>>)

    \/ s' = s /\ r' = r /\ buf' = buf                         \* if (sigma /\ rho) => (buf' = buf)
    \/ FALSE
    \/ FALSE
    \/ UNCHANGED <<buf, s, r>>
]

对于Sndr /\ ((rho /\ (r' = r)) \/ UNCHANGED <<buf, r>>)，可以看到Sndr的第二个子动作蕴含UNCHANGED <<buf, r>>，因此如果第一个子动作蕴含rho，该式即可化简为Sndr。对于Rcvr /\ ((sigma /\ (s' = s)) \/ UNCHANGED <<buf, s>>)也是同理。因此如果有下面三个假设：

  • \A d: (buf' = Append(buf, d)) => rho

  • (buf /= <<>>) /\ (buf' = Tail(buf)) => sigma

  • (sigma /\ rho) => (buf' = buf)

整个左边就可以化简为[][Sndr \/ Rcvr]_<<buf, s, r>>。即完成了从分离的NS和NR合取得到组合系统的规范。

上面三个假设只需要取合理的sigma和rho即可。一种（很强的）取法是

sigma == (buf /= <<>>) /\ (buf' = Tail(buf))
rho   == \E d: (buf' = Append(buf, d))

另一种（更弱的）取法是sigma不变，rho == ~sigma。

上面即为一个交错规范。

接下来考虑一种非交错规范，同时允许SCompute和RCompute并保持buf不变。我们定义SSndr和RRcvr为不描述对方组件不变的公式，即

Sndr <=> SSndr /\ (r' = r)
Rcvr <=> RRcvr /\ (s' = s)

因此组合而成的系统的 next 步是Sndr \/ Rcvr \/ (SSndr /\ RRcvr /\ (buf' = buf))。我们又可以按照上面的方式定义NS、NR，并找到满足的sigma和rho。实际上sigma和rho与上面一致。

这种技巧可以推广到多个组件在共享变量的状态下进行组合：集合C由表示组件，共享变量是w，N_k第k个组件的Next步，动作mu_k表示由第k个组件以外的组件对w产生的所有改变，v_k是第k个组件的私有状态。下面是交错规范的共享状态组合法则：

如下的 4 个条件

  1. (\A k \in C: v_k' = v_k) <=> (v' = v)

  2. \A i, k \in C: N_k /\ (i /= k) => (v_i' = v_i)

  3. \A i, k \in C: N_k /\ (w' = w) /\ (i /= k) => mu_i

  4. (\A \in C: mu_k) <=> (w' = w)，表示在所有的组件以外，不存在改变w的组件，反之也成立

蕴含组件的合取等价于完整规范：

(\A k \in C: I_k /\ [][N_k \/ (mu_k /\ (v_k' = v_k))]_<<w, v_k>>)
<=>
(\A k \in C: I_k) /\ [][\E k \in C: N_k]_<<w, v>>

10.4.2 联合动作的组合

对于某些组合，一些动作可能会不得不由多个组件共同完成，于是我们可以把动作拆分为前提、多组件共有的子动作、组件私有状态的变化等更细粒度，分配给多个组件进行描述。显然“多组件共有的子动作”需要出现在每个组件的动作中。

10.5 一个简短的回顾

10.5.1 组合的分类

  • 交错规范与非交错规范

  • 分离式状态与共享式状态：分离式状态即系统的状态可以完整分拆为，若干个单独由某组件影响的子状态变量。

  • 联合动作与分离动作：联合动作规范是一种非交错规范，其中一些步会在多个组件上同时发生。不属于联合动作规范即为分离动作规范。

10.5.2 有关交错的思考

在对真实系统的抽象上，交错与否并没有限制。但是非交错规范通常不能蕴含交错规范，因此为了实现一个抽象规范，通常需要写交错规范。通过合取限制交错的公式，非交错规范很容易转化为交错规范。

10.5.3 有关联合动作的思考

“组合”就是为了把系统进行简化、分拆，但是联合动作阻止了这种分拆。一般而言，应当尽量减少联合动作，但是为了描述多组件的通信，为了把发送、接受两个动作抽象为一个动作，就需要联合动作以及增加辅助变量。

10.6 活跃性和隐藏变量

10.6.1 活跃性和状态机闭包

本章的组合表示了由组件的安全性构造系统的安全性，那么活跃性也可以由组件的活跃性构造出吗？按照前文的建议，活跃性的描述应当使用弱公平性和强公平性，首先要注意公平性的下标，选择私有变量或者全部变量正确描述系统。

接下来考虑如果组件是状态机绑定的，整个系统是否也是状态机绑定的。这个问题也没有通用答案，依然要使用 8.9.2 节的经验，如果公平性描述的动作是Next步的子动作，这个系统就是状态机绑定的。因此在交错规范中，如果组件的公平性描述的动作是整个系统Next步的子动作，系统是状态机绑定的。非交错规范的组件会相互影响，往往不是状态机绑定的，例如第 9 章芝诺式规范可以看作是有联合动作的组件相互影响从而不满足状态机绑定。

10.6.2 隐藏变量

前文中我们介绍过使用\EE隐藏中间变量，对于组合而成的系统是否也可以这么做呢？按照定义，如果组件之间访问了共享变量，那么对各组件分别应用\EE，无法为共享变量建立跨组件的联系。如果（有限个）组件之间没有访问任何共享变量，对各组件隐藏变量就等价于对系统隐藏变量。

在交错规范中，如果组件 i 访问了其他组件 j 变量，但是这种访问仅是UNCHANGED v_j，那么也有上面的等价关系。

10.7 开系统规范

第 4 章介绍了开系统，本章我们可以从组合的角度进一步明确什么是开系统。前文中的规范是包含了系统与环境的闭系统，例如 FIFO 缓冲区规范中，缓冲区可以看作是系统，发送、接收方可以看作环境。开系统仅描述系统M本身，因此从组件的角度，似乎“环境E蕴含系统M”可以将开系统作为组件并与相应环境组合，形成一个闭系统规范。但这种描述太弱了，因为如果系统M主动破坏了规范导致E为假，E => M仍然成立。

为了限制上面的情况，引入新的运算符：E -+-> M表示

  • 环境E蕴含系统M

  • 对于任意自然数 n，如果行为的前 n 个状态满足E，那么前 n+1 个状态满足M。也即M不主动破坏了规范

对于一个闭系统规范，将其按照系统与环境拆分为组件，对同时与两者交互的公式分配给一方，以及提取不单独描述组件、仅描述组合而成的系统的公式（例如IsFcnOn），即可利用-+->转化为系统组件与环境组件。

10.8 接口微调

接口微调指的是对高抽象层级的规范进行调整，得到低抽象层级的规范。

10.8.1 二进制时钟

本节给出一个接口微调的例子。以前文时钟为基础，描述一个二进制序列表示小时值的时钟。对于一个二进制序列转十进制的函数BitArrayVal，除了用它来作为实例化的hr映射之外，为了避免该函数无意间将未定义的输入转化为了合法的小时值，还要确定函数的定义域。

HourVal(b) == IF b \in [(0..3) -> {0, 1}] THEN BitArrayVal(b)
                                          ELSE 99              \* any value doesn't satisfy HC!Init
B == INSTANCE HourClock WITH hr <- HourVal(bits)

另一种不使用实例化的方式是，\EE hr: [](hr = HourVal(bits)) /\ HC

10.8.2 微调一个信道

本节继续通过接口微调把一个信道转换为发送二进制值的信道。由于信道有发送-确认的机制，这里需要实例化两个信道，分别将可发送的数据指定为自然数和二进制，并通过一个中间缓冲区计算二进制到十进制的转化，以及在累积到若干二进制位后执行十进制信道的发送、确认步。

10.8.3 通用的接口微调

对于更通用场景而言，假如有一个高抽象层次的规范HSpec，想对它的接口进行调整实现一个更具体的规范LSpec，可以使用如下的公式：

LSpec == \EE h: IR /\ HSpec

其中h是HSpec的自由变量，IR模块将LSpec的l与h建立转化关系，l、h可能是长度不相等的元组。IR模块就起到了接口微调的作用。

对于HSpec与LSpec状态一一对应就能完成h与l的转换（例如 10.8.1），IR实际上只是[]表示的表达转换的单状态公式，这叫做数据微调。如果是多个状态才能决定h与l的转换（例如 10.8.2），IR就会表示得更加复杂。

10.8.4 开系统规范的接口微调

开系统在进行接口微调时需要注意系统与环境两部分，依然以h与l为例，l的变化需要正确地归纳到系统或者环境中。

当开系统有活跃性描述时，例如 10.8.2，当l因为环境的不正确而阻塞时，h因为无法累积而阻塞，就会导致LSpec下系统正确、环境不正确影响了HSpec的活跃性，从而影响了HSpec的正确。为了避免这种情况，IR中也要包含合取子式描述LSpec的活跃性。

10.9 应当使用组合吗？

通常而言，写整体的规范或者组合而成的规范差别并不大。