alloy - 原始整数运算

Question

我正在尝试比较由二元关系相关的两组元素，其效果是

#set1 = #set0 + 2 

显然在这个表达式中 2 被解释为{}，这是评估者告诉我的，所以表达式返回true。书中说+算术运算符是自动检测的。但显然问题更多是关于如何用算术表示 2。在书中，我看到了一个正是我想做的例子。

此外，当我计算#Set包含set1+set0评估器的 时，返回一个负值。

有人对此有想法吗？

提前致谢。

Answer 1

尝试这个：

sig A {}
sig B {}

pred show{ #A = add[#B, 2]}

run show for 5

据我了解，有添加整数的特殊功能。让我知道我是否理解正确。