alloy - 排序谓词不可满足

Question

ff_next关于这个合金模型的排序谓词的第一个分支，我似乎有些不明白。

open util/ordering[Exposure]
open util/ordering[Tile]
open util/ordering[Point]

sig Exposure {}

sig Tile {}

sig Point {
    ex: one Exposure,
    tl: one Tile
} fact {
    // Uncommenting the line below makes the model unsatisfiable
    // Point.ex = Exposure  
    Point.tl = Tile
}

pred ff_next[p, p': Point] {
    (p.tl = last) => (p'.ex = next[p.ex] and p'.tl = first)
    else (p'.ex = p.ex and p'.tl = next[p.tl])
}

fact ff_ordering {
    first.ex = first
    first.tl = first
    all p: Point - last | ff_next[p, next[p]]
}

run {}

这里的直觉是我有很多次曝光，每一次我都想在多个图块位置执行。考虑制作全景图像，然后将它们拼接在一起，但使用不同的相机设置多次执行此操作。

注释掉注释行后，我得到的第一个实例是：

这相当于在一张曝光的情况下通过全景图，然后将其他曝光放在地板上。

这个问题似乎是 in 之后的第一个分支=>，ff_next但我不明白出了什么问题。该分支永远不会满足，它将移动到下一次曝光和全景图的开始。如果我取消注释该行Point.ex = Exposure，模型将变得无法满足，因为它需要该分支。

关于为什么该分支不能满足的任何帮助？

标签： alloyformal-methods

Answer 1

看起来您试图表达“在我们移动到下一次曝光之前，每个图块都必须对应于当前曝光的点。” 问题是一个主要的陷阱ordering：它强制签名准确。如果你写

run {} for 6 but 3 Tile, 2 Exposure

然后按预期工作。时只有模型#Point = #Exposure * #Tile。ordering如果这对您来说是个问题，您可以编写自己的简化版本。