合金-一阶逻辑中的比较

Question

如何比较Alloy中函数的相等性？类似于：

--[(All x)(Exists y)[R(x,y)] 
-- and (All x)(All y)[R(x,y) -> R(y,x)]] 
-- = 
-- (All x)[R(x,x)] and 
assert checkEquality{
    ( all m: Model, x:m.A| some y:m.A | (y in x.(m.R)) ) and
    ( all m: Model, x:m.A, y:m.A | (y in x.(m.R) -> x in y.(m.R)) ) =
    ( all m: Model, x:m.A | (x in x.(m.R))
}

Answer 1

这是一个基本版本。根据"（All x）（All y）[R（x，y）->R（y，x）]]"部分的猜测，你可能想到了更特别的东西；在这种情况下，请进一步说明你的问题。

sig Value {}
pred p1 [x, y: Value] {
    // ...
}
pred p2 [x, y: Value] {
    // ...    
}
assert equ_pred {
    all x, y: Value | p1 [x, y] <=> p2 [x, y]
}
check equ_pred