[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



mem' = [mem EXCEPT ![2][7] = 1]  

Memory in the next state is equal to memory in the current state except for [2][7] which is changed to 1

The ! quoting Dr Lamport’s video lectures “…is just syntax. It doesn't mean anything…”

On Sat, Dec 10, 2022 at 1:21 PM Amjad Ali <amjad.hamdi.ali@xxxxxxxxx> wrote:

Thank you for your answer. Can you please elaborate on what EXCEPT and ! mean in mem' = [mem EXCEPT ![2][7] = 1] 
On Friday, December 9, 2022 at 2:10:12 PM UTC-6 andrew...@xxxxxxxxx wrote:
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/ebdd71e0-fddb-4b80-a045-b2bc87c4629an%40googlegroups.com.
--
Jeremy

--
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/CAC2JkJvFwKKMq5%3Dcz9hwfDAJSBONcEen%2BM7O1hKVGPhh7T_Aag%40mail.gmail.com.