合金 - 一阶逻辑比较答案

【问题标题】：Alloy - comparing in first order logic合金 - 一阶逻辑比较
【发布时间】：2016-04-07 00:43:11
【问题描述】：

如何比较 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))
}

【问题讨论】：

不完全清楚你的问题是什么。最初的评论是完整的，还是最后丢失了一些文字？

标签： alloy first-order-logic

【解决方案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

【讨论】：