以下示例显示了两个看起来等效的检查，但第二个检查找到了一个反例，而第二个检查没有发现反例。当设置“防止溢出”到“否”，都返回相同的结果： sig A {
x : Int,
y : Int
}
pred f1[a:A] {
y = x ++ (a -> ((a.x).add[1]))
}
pred f2[a:A] {
a.y = (a.x).add
下面是签名 one sig Library {
books: set Book,
patrons: set Patron,
circulation: Patron lone -> some Book
}
sig Book { }
sig Patron {
curbooks: set Book
}
问题 - >我想
我是Alloy的初学者。这是我使用合金分析仪的第一个模型。我现在正在为Travel in Alloy建立一个通用模型。在这个模型中，一个用户（我在这个模型中使用sig请求）可以请求'住宿'（包括'hotel'或'apartment'或'hostel'）; '飞行';或'旅游'（该请求可以是其中的一个或它们的任意组合，例如酒店和旅游）。它们中的每一个都是“资源”的子集。现在，我只坚持只有一个目的地的
即使在简单的示例中，我也无法使Alloy的基数运算符（#）按预期工作。 例如，下面的合金文件... sig Y {}
sig X {r : Y -> Y} {
//#r = 2
}
run {} for exactly 1 X, 3 Y
...给我，恰好包含2个r -edges溶液（见下图）。但是，如果我取消#r = 2这一行的注释，Alloy就不会找到解决方案！我究竟做错了什么？