/*
sig a {
}
sig b {
}
*/
pred rel_test(r : univ -> univ) {
# r = 1
}
run {
some r : univ -> univ {
rel_test [r]
}
} for 2
运行这个小测试，$r 在每个生成的实例中都包含一个元素。但是，当 sig a 和 sig b 未注释时，第一个实例是：
在我的解释中，$r 在这里仍然有 9 个元组，要求单元组关系的谓词成功。我哪里错了？
一个辅助问题：这两个声明是否等价？
pred rel_test(r : univ -> univ)
pred rel_test(r : set univ -> univ)
【问题讨论】：
标签： alloy
问题在于，如果将“禁止溢出”选项设置为“否”，Alloy 中的整数语义将被环绕，并且默认范围为 3（位），然后实际上是 9=1，正如您可以在评估器中确认的那样。
有了签名a和b的注释，范围2可以生成的最大关系有4个元组（因为univ的最大大小是2），所以不会出现问题。
它也不会出现在最新版本中，因为我相信它带有默认设置为“是”的“禁止溢出”选项，并且使用该选项，整数的语义排除了发生溢出的情况，这正是您计算与 9 个元组的关系的大小。有关这种替代整数语义的更多详细信息，请参阅 Aleksandar Milicevic 和 Daniel Jackson 的论文“Preventing算术溢出在合金中”。
【讨论】：
关于主要问题：您使用的是什么版本的合金？我无法复制您描述的行为（在 OS X 10.6.8 上使用 2015 年 2 月 22 日的 Alloy 4.2）。
关于辅助问题：看起来是这样。 （语言参考并不像人们希望的那样明确，但它以“如果右手表达式表示一元关系......”和（在我认为的上下文中）开始了它对多重性的讨论的一部分如此定义）“默认多重性为一”；如果默认多重性始终为一，则条件将毫无意义。
另一方面，相同的解释逻辑会得出这样的结论，即语言参考认为一元多重性关键字只允许在表示一元关系的表达式之前使用（这似乎使r: set univ -> univ 不合语法）。但是 Alloy 接受该表达式并将其解析为 set (univ -> univ)。 （替代解析，(set univ) -> univ，将很难赋予其含义。）
【讨论】：