0

我试图在 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 == ???
4

1 回答 1

1

一些东西。

  1. 如果Values是常量，则在 中指定它们的域ASSUME，而不是在不变量中。CONSTANT表示一些任意输入；如果您的意思是实际常量，那么只需定义Values == -2147483648 .. 2147483647.

  2. Keys甚至可以是无限的；您必须始终ASSUME为每个常量（偶数IsFiniteSet）指定一个。

  3. 你没有声明Channels，但是，Values看起来它应该是一个简单的定义，而不是一个不变量。

  4. 你没有说Cells你从多少开始。被TypeOK定义，每一步的数量都Cells可以改变，甚至可以为空。

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

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

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

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

于 2019-11-28T20:43:09.040 回答