[tlaplus] Re: Modeling a Hash

[dominik.tornow@xxxxxxxxx]

Apologies, I forgot to mention the Hash should be a String as the algorithm also depends on String concatenation.

Best, D


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.