使用模块重载在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，因此应该按照您希望的方式工作(根据我对您的问题的理解)。另请注意，值类层次结构已从包tlc2.value移至版本1.5.8中的tlc2.value.impl。

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