合金中的xor操作

Question

是否有合金的xor操作,如果没有,我该如何定义它:

我想有一个名为xor的谓词,它将两个谓词作为参数,当它们的xor成立时它保持为真.

更精细的是,如果我有P1和P2,我知道我可以将P3定义为如下:

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

是P1和P2的xor,但我想定义xor(或任何其他公式连接词),将它放在库中并稍后使用它们.所以我希望我的P3得到谓词作为参数.这可能吗？

谢谢

Answer 1

不幸的是,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),但是当调用xor时,你需要将这些谓词的真值"转换"给Bool.

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

在我看来,这两个解决方案都是丑陋的.如果想要获得更好的解决方案,那就更好地了解您希望实现的目标.

Answer 2

该xor操作可以写为iff not。