alloy - Alloy 内置整数数学函数在导入的文件中不起作用

Question

我在 avlTree.als 中有一个合金模型。该模型使用整数运算，特别是加号和减号函数。这个模型中有一些断言，我可以使用 Alloy Analyzer GUI 很好地运行这些断言。

我在 test.als 中有另一个合金模型。该模型导入 avlTree（使用“open avlTree”），然后对 avlTree 模型中的关系进行一些断言。但是当我尝试在 Alloy Analyzer GUI 中运行这些断言时，我收到以下消息：

发生语法错误：

找不到名称“加号”。

语法错误的链接将我带到我的 avlTree 模型。因此，当我自己运行该模型时，似乎 avlTree 模型对整数数学的使用效果很好，但是当我尝试将其导入另一个模型时它会中断。有解决办法吗？

我正在运行合金 4.2。

Answer 1

是的，这是一个错误，但有一个快速的解决方法，即显式打开整数模块，通过编写

open util/integer

在 avlTree.als 文件的开头。之后，您将能够打开 avlTree 并从其他模块检查其断言。