[tlaplus] Re: How to represent Memory in TLA+?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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

On Friday, December 9, 2022 at 3:21:42 AM UTC-5 amjad.h...@xxxxxxxxx wrote:

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)]

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9f269cc0-c0eb-4cbd-adf9-809b909c3b87n%40googlegroups.com.