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

[tlaplus] Re: Modeling a Hash

Hey, Dominik! I've also taken a crack at this problem. There are three solutions I've come up with:

First, if the data structure you're hashing doesn't itself include a hash, you can just use the identity function. A hash of a record is just the record itself. Easy-peasy. However, this doesn't work when you're specifying recursive data structures that point to other elements with hashes.

Second, you can assign hashes from a pool of values as they are requested. You might have a variable SequenceNumber which is a number that is returned then incremented every time you call Hash(), plus you keep track of past assigned hashes and return those if you've already assigned a hash to the val. This runs into problems like being only able to calculate a single hash per step, since you have to modify a variable in order to assign the hash. Another drawback as that this looks "messy"; you have these extra variables which detract from understanding of the spec. This can to some degree be solved through hiding the hash function implementation in a separate "model check" spec which includes your main spec, as outlined here: https://stackoverflow.com/q/49600307/2852699

The final approach (which I haven't yet accomplished) is to use module overrides and actually write your hash function in Java using the built-in hashing capabilities of the language. See here: https://stackoverflow.com/q/53908653/2852699


On Monday, February 18, 2019 at 12:55:36 PM UTC-8, Dominik Tornow wrote:


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.