Why are multiple Alloy declarations not equivalent to nested Alloy declarations?

Question

Page 293 of Software Abstractions says that these two are equivalent:

all x: X, y: Y | F

all x: X | all y: Y | F

but these two are not equivalent:

one x: X, y: Y | F

one x: X | one y: Y | F

Why are the latter two not equivalent?

I learn best with concrete examples, so let’s take a concrete example.

Last week I took a cruise to Alaska. At dinner I was seated with five other people. One of the couples (Jason and Denise) were celebrating their 25th (silver) wedding anniversary.

I created an Alloy model of the people at the dining table. The model specifies that there is one m: man, w: woman couple for which m's wife is w, w's husband is m, and m and w are celebrating a silver anniversary:

one m: Man, w: Woman |
    m.wife = w and 
    w.husband = m and 
    m.anniversary = Silver and
    w.anniversary = Silver

The instances that the Alloy Analyzer generated are what I expected.

Then I modified the expression to use nested expressions:

one m: Man |
    one w: Woman |
        m.wife = w and 
        w.husband = m and 
        m.anniversary = Silver and
        w.anniversary = Silver

The Alloy Analyzer generated the same instances!

Next, I wrote an assertion, asserting that the two versions are equivalent:

Version1 iff Version2

The Alloy Analyzer returned: No counterexamples found!

Below is my model. Why are the two versions equivalent? Is there a small tweak that I could make to the model to show a difference between the nested version and the non-nested version?

---

Alloy Model of Roger's Dining Table on the Cruise to Alaska

abstract sig Man {
    wife: lone Woman,
    anniversary: lone Anniversary
}
one sig Roger extends Man {}
one sig Jason extends Man {}

abstract sig Woman {
    husband: lone Man,
    anniversary: lone Anniversary
}
one sig Faye extends Woman {}
one sig Nina extends Woman {}
one sig Claudia extends Woman {}
one sig Denise extends Woman {}

abstract sig Anniversary {}
one sig Silver extends Anniversary {}

pred v1_One_couple_celebrating_25th_wedding_anniversary {
    one m: Man, w: Woman | m.wife = w and w.husband = m and 
                           m.anniversary = Silver and w.anniversary = Silver }

pred v2_One_couple_celebrating_25th_wedding_anniversary {
    one m: Man | 
        one w: Woman | 
            m.wife = w and w.husband = m and 
            m.anniversary = Silver and w.anniversary = Silver }

assert Both_versions_are_identical {
    v1_One_couple_celebrating_25th_wedding_anniversary 
    iff
    v2_One_couple_celebrating_25th_wedding_anniversary
}
check Both_versions_are_identical

Answer 1

You may run these examples to see the difference:

sig Man {}

sig Woman { 
    // married is a relation Woman set -> set Man
    married : set Man 
}

// there is exactly one married couple
run { one w : Woman, m : Man | w->m in married } for 5

// there is exactly one woman that has exactly one husband;
// apart from that, several men may share a wife, and vice-versa
run { one w : Woman | one m : Man | w->m in married } for 5

Answer 2

The predicate is too constraining for there to be a difference.

The difference between the nested version and the non-nested version can be seen if the example is modified a bit: Allow each man to be married to a set of women:

sig Man {
    wives: set Woman
}

Loosen the constraint to this: w in m.wives

Here is the new, non-nested version:

one m: Man, w: Woman |
    w in m.wives and
    w.husband = m and
    w.anniversary = Silver

That says there is exactly one m: Man, w: Woman for which w is one of m's wives, w's husband is m, and m and w are celebrating a silver anniversary.

Here’s one of the instances that the Alloy Analyzer generates: Man1 has wives Woman1 and Woman2. Woman1 has husband Man1. Likewise, Woman2 has husband Man1. Woman1 is celebrating a 25th wedding anniversary with her husband (Man1).

Here is the nested version:

one m: Man |
    one w: Woman | 
        w in m.wives and 
        w.husband = m and
        w.anniversary = Silver

That says there is exactly one m: Man for which the constraint is true, where the constraint is this: there is one woman for which the woman is the man’s wife and they have been married 25 years. There can be another man for which the constraint is true.

Here’s one of the instances that the Alloy Analyzer generates: Man1 has wives Woman0 and Woman1. Man1 and Woman1 have been married 25 years. Man2 has wife Woman2. They have been married 25 years.

Below is the Alloy model.

Alloy Model of Men Married to Multiple Wives

sig Man {
    wives: set Woman
}

sig Woman {
    husband: lone Man,
    anniversary: lone Anniversary
}

abstract sig Anniversary {}
one sig Silver extends Anniversary {}

pred v1_One_couple_celebrating_25th_wedding_anniversary {
    one m: Man, w: Woman | w in m.wives and w.husband = m and 
                           w.anniversary = Silver 
}

pred v2_One_couple_celebrating_25th_wedding_anniversary {
   one m: Man |
        one w: Woman | 
            w in m.wives and w.husband = m and w.anniversary = Silver 
}

assert Both_versions_are_identical {
    v1_One_couple_celebrating_25th_wedding_anniversary 
    iff
    v2_One_couple_celebrating_25th_wedding_anniversary
}   
check Both_versions_are_identical