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
,模型将变得无法满足,因为它需要该分支。
关于为什么该分支不能满足的任何帮助?