Creating a hash-map in TLA+

[Aman Shaikh]

Hi

I'd like to create a hash in TLA+ that maps a key to its value where ..

key == expr1

val == expr2

Doing [key |-> val] creates a record with the field 'key'. What I want is [expr1 |-> expr2]. How do I achieve this?

thx

aman

 

[Haruki Okada]

[x \in {key} |-> val]

should work

2022年11月26日(土) 5:23 Aman Shaikh <amansh...@gmail.com>:

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/41e9a4b7-14a9-4e55-bce5-ba54b46b1a38n%40googlegroups.com.

--

========================

Okada Haruki

ocad...@gmail.com

========================

[Calvin Loncaric]

The TLC module has operators :> and @@ to make this even easier:

---- MODULE SmallMap ----

EXTENDS TLC

dictionary ==
    (10 :> "a") @@
    (20 :> "b") @@
    (10 :> "c")

ASSUME dictionary[10] = "a"
ASSUME dictionary[20] = "b"

====

Note that the @@ operator is "left-biased", so mappings on the left side take precedence over mappings on the right. That's why dictionary[10] /= "c".

(Also, a quick pedantic note, probably irrelevant to what you're trying to do: a hash map is a specific data structure that implements a dictionary on real hardware. TLA+ is not a programming language and it does not have hash maps. It has functions, which are mathematical objects that behave like dictionaries. Functions have a domain that acts like a dictionary's keys, and they map each element in their domain to a value in their range, just like how a dictionary maps each key to a value. You can read more about functions in Section 5.2 of Specifying Systems. Internally, TLC actually does not use hash maps to implement functions, so you should not expect functions to have the same performance characteristics as hash maps during model checking.)

--

Calvin

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHf4GKqRpmnHvqpr2Hf6Zduszgte8G02oNXBcFLSA8US42rXPg%40mail.gmail.com.

[Aman Shaikh]

Thanks Calvin and Haruki.

Calvin - Thanks for the note. Indeed, I'm aware of the fact that in TLA+ hash-maps, records, sequences are Mathematical functions. Also, I am not relying on a specific implementation (or performance) for these functions. My use of 'hash-map' was to easily explain what I was trying to do.

aman

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Ey7ykBRppTI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMgPSL9E02AkLT8ob9aBqE%3D6MSsUia16dvw6L-fPZYyCmA%40mail.gmail.com.