[tlaplus] Re: Modeling a Hash

[dominik.tornow@xxxxxxxxx]

Thank you Andrew for sharing your experience. I tend to prefer option 3, I guess it's time to dust off javac. I will update this thread in case I have a working solution.

Thanks again. D

On Monday, February 18, 2019 at 1:14:45 PM UTC-8, Andrew Helwer wrote:
> 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

-- 
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.