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
Andrew
On Monday, February 18, 2019 at 12:55:36 PM UTC-8, Dominik Tornow wrote:
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