合金在过河时的唯一对一个量词

Question

在 river crossing Alloy model ，这个谓词:

pred crossRiver [from, from', to, to': set Object] {
  one x: from | {
    from' = from - x - Farmer - from'.eats
    to' = to + x + Farmer
  }
}

模型过河:对象之一 x来自 from侧移至 to一边，随着农夫。

为了测试我的理解，我改了: one x: from至 lone x: from - Farmer --- 前者“完全是一件东西”过河，后者“至多是一件非农事”。

我认为后者更好地为问题建模:Farmer 在等式约束中被硬编码并且总是过河，而 lone应该更好地传达农民可以带着零或一件东西过河。

但是，在这个改动之后运行模型时，结果是无稽之谈:



这里的第二个状态实例显示了河流两岸的鸡和 Cereal ，而农民根本没有过河。

我错过了什么？
(这是在合金 4.2_2015-02-22 上运行的)

Answer 1

当您更改 one至 lone你让 Alloy 轻而易举地返回 true来自 crossRiver谓词，不管是什么near和 far看起来像。因此，该步骤的模型状态不受任何限制。因此，near 的所有可能值集和 far在 State合金完全没问题。

这并不意味着 Alloy 会以某种方式优化它并且永远不会限制。它将尝试 one (正确约束 near 和 far )，它只会 true不限制解。但是，两个解都必须在解空间中。显然，还有更多不受约束的解决方案，因此您可能会看到垃圾。

如果您使用 one , 然后合金 必须满足谓词，这意味着主体带有far和 near关系以这样一种方式受到约束，即在 State 中仅对有效的交叉进行建模。

把合金想象成一种石雕工具。你从一个巨大的状态块开始:near 中每个可能的原子组合和 far和 State在那里。但是，如果您跳过跟踪中的约束，那么您只会得到原子的随机组合。

发生类似事情的常见问题是:

  some f : Foo | no f

这看起来总是假的。唉，当没有 Foo 原子时，这是真的，因为从不看 body 。