alloy - 合金の述語とInt

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]}、エバリュエーターに入力して結果を取得します。