本章介绍一个先进先出 FIFO 系统。 4.1 内部结构的规范 一个 FIFO 队列内部是一个缓冲区，对外提供单个消息的入队与出队接口。对于外部接口，TLA+ 可以复用之前的模块，这类似于面向对象编程中实例的概念。我们复用上一章的模块 Channel InChan == INSTANCE Channel WITH Data <- Message, chan <- in InChan 现在是一个 Channel ，除了 Data 和 chan 通过相应的新标识符访问，其余标识符（以及运算符）通过 InChan!symbol 访问。 缓冲区用 TLA+ 的内置数据结构 Sequences 进行表示。 Sequences 表示一个有限序列，字面量用元组表示，并有如下的与之相关的标识符： Seq(S) 表示 S 集合能组成的所有有限序列。 Head(S) 、 Tail(S) 表示序列的首元素及剩余序列。 Append(S) 、 S \o T 表示序列与元素、另一个序列连接。 Len(S) 表示序列的长度。 了解上述语法后，可以把 FIFO 描述为三个组件：依次相连的入队接口、内部先进先出缓冲区、出队接口。FIFO 的状态转移将由相连两组件各自的状态转移以及两组件交互组成。 4.2 实例化的细节 与 EXTENDS 不同，实例化需要导入的所有符号（主要是 CONSTANT 、 VARIABLE 等关键词定义的标识符）都指定本模块中对应标识符。有以下几个方面需要注意。 4.2.1 实例化即替换 TLA+ 的实例化是进行表达式展开和替换。为了满足语法，原模块替换完成后，所有符号在本模块中都要有定义，这可以通过 EXTENDS 引入运算符等符号以及使用 <- 为原模块未匹配的符号指定本模块的标识符、表达式等符号来满足。 4.2.2 实例化的参数化 实例化时可以包含参数，即 InChan == INSTANCE Channel WITH Data <- Message, chan <- in OutChan == INSTANCE Channel WITH Data <- Message, chan <- out 可以使用 Chan(ch) ...
评论
发表评论