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

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

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

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

标签：4.0,步骤,FIFO,ininin,发送,TLA,缓冲区,outoutout
来源： https://blog.csdn.net/robinhzp/article/details/104077440