覆盖合金中的对象

Question

我一直在努力让我的项目更具动态性，所以我决定编写一个 add 函数，我从他们在 Alloy 网站上的这个示例中得到启发：

pred add [b, b': Book, n: Name, t: Target] {
  b'.addr = b.addr + n->t 
}

但我想要做的是覆盖两个对象“b”和“b'”（就像我想添加到同一个对象一样）但我似乎无法找到一种方法来做到这一点。

如果有人有想法，我将不胜感激

Answer 1

你没有错过任何东西。您找不到“添加到同一个对象”的方法的原因是您做不到。合金没有突变；您不能更改模型中的任何对象。

涉及突变的应用程序通常像您在示例中为 add 建模一样建模：两个参数显示前状态和后状态。在这样的模型中，当且仅当存在一些 n, t 使得 add[b1, b2, n, t] 成立。