合金中的谓词和整数

【问题标题】：Predicates and Int in alloy合金中的谓词和整数
【发布时间】：2012-11-17 16:53:49
【问题描述】：

我知道合金中谓词的用法，但我对以下描述感到有些惊讶：

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])

}

谁能给我解释一下上面的内容。

【问题讨论】：

对于否决这个问题的人来说，这对您来说可能是一个愚蠢的问题，但 SO 对 Alloy 信息的了解如此之少，每一点都有帮助。

标签： alloy

【解决方案1】：

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

【讨论】：

2 个小问题。 Int[0] 是什么意思？您如何解释表达式 (Int[0] + Int[1]) -> (Int[2] + Int[3])。您能否以文字形式解释上述内容。非常感谢:)
Int[0] 表示 Int 的原子的单例集，表示值为零。 Int[0] + Int[1] 是两个这样的单例集的并集，即包含原子 0 和 1 的 Int 的子集。
对你的第二个问题 {a+b+c} -> {d+e+f} 表示 {a,b,c} 和 {d,e,f 的集合之间的二元关系} 其中包含所有可能的对，即它是两组的笛卡尔积。换句话说，它是两个顶点集 {a,b,c} 和 {d,e,f} 的完整二部有向图 (q.v.)。