Checking Sig Equality in Alloy

Question

In the following Alloy model I want to check the equality of two instances of a sig with Bool field type:

module test

open util/boolean as bool


sig Info {
    active: Bool
}

assert assertion {
    all x1, x2: Info |
        x1.active = True && x2.active = True implies x1 = x2
}

check assertion for 10

This model checks for equality of x_1 and x_2 if both have True as their active field. Alloy comes back with a counterexample, however, in the counterexample, both x_1 and x_2 are structurally equal but for some reason Alloy considers them not equal.

Edit:

One suggestion is to use subtyping as follows:

sig Info {}

sig ActiveInfo in Info {}

-- i is inactive if i in (Info - ActiveInfo) 

However, this is not suitable for my model.

Quote from the Software Abstractions book:

" Is equality structural equality or reference equality?

A relation has no identity distinct from its value, so this distinction, based on programming notions, doesn’t make sense here. If two relations have the same set of tuples, they aren’t two relations: they’re just one and the same relation. An atom is nothing but its identity; two atoms are equal when they are the same atom. If you have a set of atoms that represent composite objects (using some relations to map the atoms to their contents), you can define any notion of structural equality you want explicitly, by introducing a new relation. (And for those C++ programmers out there: no, you can’t redefine the equals symbol in Alloy.)"

I don't quite understand this paragraph. I appreciate explanation on how equality works in Alloy. Particularly on how to check equalities of atoms with different identities but same values?

Answer 1

I know that equality in Alloy is based on values.

This is not true. x1 and x2 have the same value for active, but are different atoms in the signature. It's similar to how in a lot of OOP languages, two objects can have the same structural values but have different identities.

Incidentally, I'd recommend using subtypes to represent booleans. You could do

sig Info {}

sig ActiveInfo in Info {}

-- i is inactive if i in (Info - ActiveInfo) 

Answer 2

You can think of a field in a signature as "belonging" to an atom of that signature if you like, but it's better just to think of fields as relations. You wouldn't expect two persons to be the same if they have the same mother:

sig Person {mother: Parent} 

But if you want your signature to have the property that no two distinct members have the same fields, you can just add that as a fact:

sig Coordinate {x, y: Value}
fact {all c, c': Coordinate | (c.x = c'.x and c.y = c'.y) implies c = c'}