Use module overloading to implement a hash function in TLA+

The module overloading mechanism is explained in the Tower of Hanoi sample here. It enables you to implement TLA+ operators in Java, for improved model-checking performance.

I've struggled for a while to define a useful hash function in TLA+ (no, the identity function does not work for my purposes) and am thinking module overloading might be the way to do it. The hash function would accept a TLA+ object (a record, for example) and use Java's hashCode() method on the object's string representation to deterministically derive its hash value. This value would be returned to the TLA+ spec.

Is this possible? What would the Java override code look like? Do any other module override code samples exist?

Solution

import tlc2.value.impl.IntValue;
import tlc2.value.impl.Value;

public class TLCHash {
    
    public static Value Hash(Value v) {
        return IntValue.gen(v.hashCode());
    }
}

------------------------------ MODULE TLCHash ------------------------------
EXTENDS Integers

Hash(val) == CHOOSE n \in Int : TRUE


ASSUME(Hash(<<"a","b","c">>) = Hash(<<"a","b","c">>))
ASSUME(Hash(<<"a","b","c">>) # Hash(<<"c","b","a">>))

ASSUME(Hash({"a","b","c"}) = Hash({"b","c","a", "c"}))

=============================================================================

Note that TLC's implementation of Value#hashCode delegates to Value#fingerprint and thus should work the way you want it to (from my understanding of your question). Also note that the Value class hierarchy has been moved from the package tlc2.value to tlc2.value.impl in version 1.5.8.

https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754 shows a real-world application of module overwrites and might inspire a solution. Lastly, the only aspect of TLC's built-in standard modules that actually turns them into standard modules is the tlc2.module package/namespace.