TLA+ 《Specifying Systems》翻译初稿——Section 4.0 A FIFO

2024-03-26 18:28:22

下一个例子是FIFO缓冲区，简称FIFO，它是一个装置，发送方进程使用它向接收方传输一系列的值。发送方和接收方使用 $in$ in和 $out$ out两个通道与缓冲区通信:

值的发送将遵循第30页图3.2中的 $Channel$ Channel模块指定的异步协议。该系统规约将允许下列行为：其步骤中具有四种非重叠步骤，即分别在 $in$ in通道和 $out$ out通道上的 $Send$ Send和 $Rcv$ Rcv步骤。