合金中是否有异或运算，如果没有，如何定义：
我想要一个名为 xor 的谓词，它将两个谓词作为参数，并且当它们的 xor 成立时它成立。
更详细地说，如果我有 P1 和 P2，我知道我可以将 P3 定义如下：
pred P3(){
(P1 and (not P2)) or ((not P1) and P2)
}
要成为 P1 和 P2 的异或，但我想定义异或（或任何其他公式连接词），将其放入库中并稍后使用它们。所以我希望我的 P3 将谓词作为参数。这可能吗？
谢谢
【问题讨论】：
标签： alloy
不幸的是，Alloy 没有布尔类型。如果没有正确的类型，就不能为谓词声明参数。因此，您的方法似乎是一个失败的原因。
我可以想到两个丑陋的技巧，都涉及使用 util/boolean 或您自己的布尔定义来使事情正常进行。
在这两种技巧中，您的 XOR 谓词都应采用两个 Bool 参数。
pred xor[ x,y:Bool){
x != y
}
在第一个技巧中，将所有命题表示为单例签名（例如 P1 和 P2）而不是谓词。让这些签名声明一个 Bool 类型字段（例如 bool），并使用您在谓词 P1 和 P2 中放入的公式将此字段设置为签名事实。
然后调用你的谓词 xor 如下：
xor[P1.bool ,P2.bool]
在第二招 您将命题表示为谓词（P1 和 P2），但在调用异或时，您需要将这些谓词的真值“转换”为 Bool。
xor[(P1 implies True else False ),(P2 implies True else False )]
在我看来，这两种解决方案都很丑陋。最好能更广泛地了解您想要实现的目标，以便提供更好的解决方案。
【讨论】：
xor 操作可以写成iff not。
【讨论】：