[tlaplus] How to represent Memory in TLA+?

[Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>]

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/dd434e7c-036c-450f-bed7-a6c50a5dfdcbn%40googlegroups.com.