In Alloy, assertions are used to check the correctness of logic sentences (properties of your model), not to specify properties that should always hold in your model. So you didn't specify that
there will be some ~r iff x not in y and y not in x
you instead asked Alloy whether it is true that for all binary relations r
, some ~r iff x not in y and y not in x [...]
, and Alloy answered that it is not true, and gave you a concrete example (counterexample) in which that property doesn't hold.
A couple other points
some ~r
doesn't mean "r is symmetric"; it simply means that the transpose ofr
is non-empty, which is not the same. A binary relation is symmetric if it is equal to its transpose, so you can writer = ~r
to express that;instead of
some x, y: univ | x not in y and y not in x and [...]
you can equivalently writesome disj x, y: univ | [...]
;however, that
some
expression doesn't really express the symmetry property, because all it says is that "there are some x, y such that both x->y and y->x are in r"; instead, you want to say something like "for all x, y, if x->y is in r, then y->x is in r too".