alloy - 合金中的异或运算

Question

合金中是否有异或运算，如果没有，我该如何定义它:

我想要一个名为 xor 的谓词，它以两个谓词作为参数，并且当它们的 xor 为真时它也为真。

更详细地说，如果我有 P1 和 P2，我知道我可以将 P3 定义如下:

pred P3(){
   (P1 and (not P2)) or ((not P1) and P2)
}

成为 P1 和 P2 的异或，但我想定义异或(或任何其他公式连接词)，将其放入库中并稍后使用。所以我希望我的 P3 get 谓词作为参数。这可能吗？

谢谢

Answer 1

不幸的是，Alloy 没有 bool 类型。如果没有正确的类型，就不能为谓词声明参数。因此，您的方法似乎是一个失败的原因。

我可以想到两个丑陋的技巧，它们都涉及使用 util/boolean 或您自己的 bool 定义来使事情​​发挥作用。

在这两种技巧中，您的 XOR 谓词都应采用两个 Bool 参数。

pred xor[ x,y:Bool){
   x != y
} 

第一招 ，将您的所有命题表示为单例签名(例如 P1 和 P2)而不是谓词。让这些签名声明一个 Bool 类型字段(例如 bool)，并使用您将放入谓词 P1 和 P2 的公式将此字段设置在签名事实中。

然后调用您的谓词 xor 如下:

xor[P1.bool ,P2.bool]

第二招
您将命题表示为谓词(P1 和 P2)，但是在调用 xor 时，您需要将这些谓词的真值“转换”为 Bool。

xor[(P1 implies True else False ),(P2 implies True else False )]

再次在我看来，这两种解决方案都很丑陋。最好能更广泛地了解您想要实现的目标，以便提供更好的解决方案。