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

Question

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

我在test.als中有另一种合金模型.该模型导入avlTree(使用"open avlTree"),然后对avlTree模型中的关系进行一些断言.但是当我尝试在Alloy Analyzer GUI中运行这些断言时,我收到以下消息:

发生语法错误:

无法找到名称"加号".

并且语法错误的链接将我带到了我的avlTree模型.因此,当我自己运行该模型时,似乎avlTree模型对整数数学的使用工作正常,但是当我尝试将其导入另一个模型时,它会中断.有没有解决这个问题？

我正在运行Alloy 4.2.

Answer 1

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

open util/integer

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