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

*From*: dominik.tornow@xxxxxxxxx*Date*: Tue, 19 Feb 2019 11:03:48 -0800 (PST)*References*: <d886cf14-0d41-4136-af48-d0c0c9909a1a@googlegroups.com> <f8d7835c-7e73-4521-a6e5-f1b89a44fabe@googlegroups.com>

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.

**Follow-Ups**:**Re: [tlaplus] Re: Modeling a Hash***From:*Markus Kuppe

**References**:**[tlaplus] Modeling a Hash***From:*dominik . tornow

**[tlaplus] Re: Modeling a Hash***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs** - Next by Date:
**Re: [tlaplus] Re: Modeling a Hash** - Previous by thread:
**[tlaplus] Re: Modeling a Hash** - Next by thread:
**Re: [tlaplus] Re: Modeling a Hash** - Index(es):