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

[tlaplus] Modeling a Hash


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


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.