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

几件事。

如果

1. 是常量，则在ASSUME中指定其域，而不是在不变量中指定。Values == -2147483648 .. 2147483647.
2. Keys意味着一些仲裁输入；如果您指的是实际的常量，那么定义IsFiniteSet).
3. You甚至可以是无限的；您必须始终为每个常量指定一个ASSUME (甚至IsFiniteSet).
4. You也没有声明Channels，但是，就像Values一样，它似乎应该是一个简单的定义，而不是invariant.
5. You没有说明您开始使用多少Cells。定义了TypeOK，Cells的数量在每一步都可以改变，甚至是空的。

但是假设你想要N个细胞来做一些N，那么：

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

但是你写了“域”，这里0在范围内，所以我不确定我是否理解你的问题。你还提到了频道，所以你的意思是：

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