Given
CONSTANTS MemLength, MemWidth
VARIABLE mem
Where MemLength is the largest index possible in the memory, MemWidth is the number of bits at each location, and mem is the current memory state, you can define:
Memory == [0 .. (MemLength - 1) -> [0 .. (MemWidth - 1) -> {0, 1}]]
Init == mem = [0 .. (MemLength - 1) |-> [0 .. (MemWidth - 1) |-> 0]]
TypeInvariant == mem \in Memory
It's a good idea to parameterize this with constants because you can probably do the math to figure out the Memory set is absolutely enormous, on the order of 2^(MemLength * MemWidth). So you'd probably want to top out at 3 x 4 or something at most.
You can read a specific bit by double-indexing, like
mem[2][7]
And you can update a bit like
Next == mem' = [mem EXCEPT ![2][7] = 1]
Andrew
I would like to specify a large chunk of Memory with binary values.
Memory[i] should output an 8 byte datatype like so:
For example, assume the number 2 in binary form is in memory location 0.
Then,
Memory[0] should output
[i \in 0..63 |-> (i=1)]
Assume 129 is in location 400,
Then,
Memory[400] should output
[i \in 0..63 |-> (i=0) /\ (i=7)]
Also, I would like to be able to assign values to specific memory locations. Say, writing 4 to memory location 2.
Memory[2] == [i \in 0..63 |-> (i=2)]