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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Fri, 9 Dec 2022 12:10:12 -0800 (PST)*References*: <dd434e7c-036c-450f-bed7-a6c50a5dfdcbn@googlegroups.com>

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.

**Follow-Ups**:**[tlaplus] Re: How to represent Memory in TLA+?***From:*Amjad Ali

**References**:**[tlaplus] How to represent Memory in TLA+?***From:*Amjad Ali

- Prev by Date:
**[tlaplus] How to represent Memory in TLA+?** - Next by Date:
**[tlaplus] Re: How to represent Memory in TLA+?** - Previous by thread:
**[tlaplus] How to represent Memory in TLA+?** - Next by thread:
**[tlaplus] Re: How to represent Memory in TLA+?** - Index(es):