[tlaplus] Modeling a Hash

[dominik.tornow@xxxxxxxxx]

Hello,

I am attempting to model an algorithm that employed hashes to determine equality. I am looking for a way to model a has function so that

Hash(rec-1) = Hash(rec-2) <=> rec-1 = rec-2

e.g.

Hash([foo |-> "bar"]) = Hash([foo |-> "bar"]) but
Hash([foo |-> "bar"]) # Hash([foo |-> "baz"])

So far the only idea in my mind is to create an additional variable to manually track rec-1, rec-2 and their "hashes" (rec-3, ... rec-n can be created dynamically, so no constant).

However, since in most implementations a hash is an inherent property of a data record, an explicit modeling and manual tracking feels like communicating the wrong idea.

Any idea how I could alternatively model an inherent hash value in tla+?

Thanks and best, Dominik 

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.