Alloy - comparing in first order logic

Question

How does one compare the equality of functions in Alloy? Something like:

--[(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))
}

It's not completely clear what your question is. Is the initial comment complete, or was some text lost at the end? — C. M. Sperberg-McQueen

Attila Karoly Attila Karoly · Accepted Answer · 2016-06-13T16:17:43

Here's an elementary version. Guessing by the '(All x)(All y)[R(x,y) -> R(y,x)]]' part, you've probably thought of something more special; in that case, please specify your question further.

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

Alloy - comparing in first order logic

1 Answers