小编lyn*_*ghk的帖子

在河流穿越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上运行的)