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

Question

I am trying to specify a collection of memory cells in TLA+, each holding 256 32-bit integers. I would like to specify that at initialization time all the memory is zeroed out. I intuit that the correct approach is something like nested forall statements, but I don't know how to express that in 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

A few things.

1. If Values are constants, specify their domain in an ASSUME, not in an invariant. CONSTANT means some arbitray input; if you meant actual constants, then just define Values == -2147483648 .. 2147483647.

2. Keys could even be infinite; you must always specify an ASSUME for each constant (even IsFiniteSet).

3. You didn't declare Channels, but, like Values it seems like it should be a simple definition, not an invariant.

4. You didn't say how many Cells you're starting out with. The TypeOK is defined, the number of Cells can change at each step, and even be empty.

But suppose you want N cells for some N, so:

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

But you wrote "domain" and here 0 is in the range, so I'm not sure I understand your question. You also mention channels so perhaps you meant:

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