alloy - 合金中的谓词和整数

Question

我知道合金中谓词的使用，但我对下面的描述有点惊讶：

pred locationConstraint(loc: Int -> Int){
    loc in (Int[0] + Int[1] + Int[2] + Int[3] + Int[4] + Int[5] + Int[6]) -> (Int[2] + Int[3])
 + (Int[2] + Int[3]) -> (Int[0] + Int[1] + Int[2] + Int[3] + Int[4] + Int[5])

}

有人可以向我解释上述内容。

Answer 1

添加run {}到您的模型中，然后{x,y:Int | locationConstraint[x->y]}在评估器中键入以获取结果：