TLA+：指定函数序列的每个元素的范围为{0}

Question

我正在尝试在 TLA+ 中指定一组内存单元，每个内存单元包含 256 个 32 位整数。我想指定在初始化时所有内存都清零。我凭直觉认为正确的方法类似于嵌套的 forall 语句，但我不知道如何在 TLA+ 中表达它。

---------------------------- MODULE combinators ----------------------------

EXTENDS Integers, FiniteSets, Sequences

CONSTANTS Keys, Values

VARIABLES Cells

TypeOK ==
    /\ Channels = 0 .. 255
    /\ Values = -2147483648 .. 2147483647
    /\ Cells \in Seq([Keys -> Values])

Init == ???

Answer 1

几件事。

如果 Values 是常量，请在 ASSUME 中指定它们的域，而不是在不变量中。 CONSTANT 表示任意输入；如果你的意思是实际常量，那么只需定义 Values == -2147483648 .. 2147483647.
Keys甚至可以是无限的；您必须始终为每个常量指定一个 ASSUME（甚至 IsFiniteSet）。
你没有声明Channels，但是，像Values一样，它似乎应该是一个简单的定义，而不是一个不变量。
您没有说开始时有多少 Cells。定义了TypeOK，Cells的个数每一步都可以变化，甚至可以为空。

但是假设您想要 N 个单元格，所以：

Cells = [c ∈ 1..N ↦ [k ∈ Keys ↦ 0]]

但是你写了 "domain" 并且这里 0 在范围内，所以我不确定我是否理解你的问题。您还提到了频道，所以也许您的意思是：

Cells = [c ∈ 1..N ↦ [k ∈ Channels ↦ 0]]

TLA+：指定函数序列的每个元素的范围为{0}

TLA+: specify that the range of each element of a sequence of functions is {0}

tla+