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

Question

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

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

A syntax error has occurred:

The name "plus" cannot be found.

语法错误的链接将我带到我的 avlTree 模型。因此，当我单独运行该模型时，avlTree 模型对整数数学的使用似乎工作正常，但当我尝试将其导入另一个模型时，它会崩溃。有解决办法吗？

我正在运行 Alloy 4.2。

Answer 1

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

open util/integer

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