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

Question

模块重载机制在此处的河内塔示例中进行了说明。它使您能够在 Java 中实现 TLA+ 运算符，以提高模型检查性能。

我一直在努力在 TLA+ 中定义一个有用的哈希函数（不，身份函数不适用于我的目的）并且我认为模块重载可能是实现它的方法。散列函数将接受一个 TLA+ 对象（例如，一条记录），并使用 JavahashCode()对对象的字符串表示的方法来确定性地导出其散列值。该值将返回给 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 ，因此应该按照您希望的方式工作（根据我对您问题的理解）。另请注意，在版本 1.5.8 中，值类层次结构已从包 tlc2.value 移动到 tlc2.value.impl。

https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754显示了模块覆盖的真实应用，可能会激发解决方案。最后，TLC 的内置标准模块唯一真正将它们变成标准模块的方面是 tlc2.module 包/命名空间。