合金在河流穿越时与单个量词相对

Question

在河流穿越Alloy模型中,这个谓词:

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---前移动"只有一个东西"隔江相望,后者运动"最多一个非农民的事".

我认为后者更好地模拟了这个问题:农民在平等约束中被硬编码并且总是穿越河流,并且lone应该更好地传达农民可以在河对岸采取零或一件事.

但是,在此更改后运行模型时,结果是无意义的:

在这里,第二个州的实例显示了河流两侧的鸡肉和谷物,而农民根本没有穿过.

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

Answer 1

当您更改oneto时，您允许 Alloy从谓词中lone轻松返回，而不管 和是什么样子。因此，该步骤的模型状态不受任何限制。因此，每组可能的值 for和in对于 Alloy 来说都是完全可以的。truecrossRivernearfarnearfarState

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

如果您使用one，则 Alloy必须满足谓词，这意味着具有 thefar和near关系的主体受到限制，使得只有有效的交叉才会在 State 中建模。

只要将合金视为石雕工具即可。你从一个巨大的状态块开始：每一种可以想象的原子组合都在near其中。但是，如果您跳过跟踪中的约束，那么您只会得到原子的随机组合。farState

发生类似情况的常见问题是：

  some f : Foo | no f

这看起来总是错误的。唉，当没有 Foo 原子时，这是真的，因为身体从未被观察过。