找不到名称“div”...嗯？为什么？

Question

在这个模块中，我使用合金“div”：

module test

one sig Test {
     t: Int
} {
   t = div[4,2]
}

run {}

执行效果很好。

我创建了另一个模块，它使用第一个模块：

module hope

open test

sig A {}

run {}

执行会导致以下错误消息：

找不到名称“div”。

为什么我会收到错误消息？如何解决？

Answer 1

这是一个已知的错误，有一个简单的解决方法。您需要在第一个模型中显式导入 util/integer 模块。

见Alloy built-in integer math functions don't work in imported files