使用模块重载在TLA +中实现哈希函数

Question

模块重载机制在河内塔样本here中解释。它使您能够在Java中实现TLA +运算符，以提高模型检查性能。

我已经挣扎了一段时间来在TLA +中定义一个有用的哈希函数（不，身份函数不能用于我的目的）并且我认为模块重载可能是这样做的方法。哈希函数将接受TLA +对象（例如，记录），并在对象的字符串表示上使用Java的hashCode()方法来确定性地派生其哈希值。该值将返回到TLA +规范。

这可能吗？ Java覆盖代码会是什么样的？是否存在任何其他模块覆盖代码示例？

Answer 1

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"}))

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

请注意，TLC的Value＃hashCode实现委托给Value＃fingerprint，因此应该按照您希望的方式工作（根据我对您的问题的理解）。另请注意，Value类层次结构已从版本1.5.8中的包tlc2.value移至tlc2.value.impl。

https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754展示了模块覆盖的真实应用，并可能激发解决方案。最后，TLC的built-in standard modules实际上将它们转换为标准模块的唯一方面是tlc2.module包/命名空间。