为什么多个 Alloy 声明不等同于嵌套 Alloy 声明？

Question

Software Abstractions 的第 293 页说这两者是等价的：

all x: X, y: Y | F

all x: X | all y: Y | F

但这两者并不等价：

one x: X, y: Y | F

one x: X | one y: Y | F

为什么后两者不等价？

我通过具体的例子学得最好，所以让我们举一个具体的例子。

上周我乘船去了阿拉斯加。晚餐时，我和另外五个人坐在一起。其中一对夫妇（杰森和丹妮丝）正在庆祝他们的第 25 个（银）结婚纪念日。

我创建了餐桌旁人的合金模型。该模型指定有一对 m: man, w: women 夫妇，其中 m 的妻子是 w，w 的丈夫是 m，m 和 w 正在庆祝银婚：

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

Alloy Analyzer 生成的实例符合我的预期。

然后我修改了表达式以使用嵌套表达式：

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

Alloy Analyzer 生成了相同的实例！

接下来，我写了一个断言，断言两个版本是等价的：

Version1 iff Version2

合金分析仪返回：未找到反例！

下面是我的模型。为什么这两个版本是等价的？我可以对模型进行一些小调整以显示嵌套版本和非嵌套版本之间的区别吗？

---

阿拉斯加游轮上的罗杰餐桌合金模型

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

您可以运行这些示例来查看差异：

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

谓词太受限制，以至于没有区别。

如果稍微修改一下例子就可以看出嵌套版本和非嵌套版本的区别：允许每个男人与一组女人结婚：

sig Man {
    wives: set Woman
}

将约束放松为：w in m.wives

这是新的非嵌套版本：

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

也就是说只有一个 m: Man, w: Woman，w 是 m 的妻子之一，w 的丈夫是 m，m 和 w 正在庆祝银婚纪念日。

这是合金分析器生成的实例之一：Man1 有妻子 Woman1 和 Woman2。女人 1 有丈夫男人 1。同样，Woman2 有丈夫 Man1。 Woman1 正在与丈夫 (Man1) 庆祝结婚 25 周年。

这是嵌套版本：

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

这就是说正好有一个 m: 约束为真的男人，约束是这样的：有一个女人是男人的妻子，他们结婚 25 年。可以有另一个人的约束是真实的。

这是合金分析器生成的实例之一：Man1 有妻子 Woman0 和 Woman1。 Man1 和 Woman1 结婚 25 年。 Man2 有妻子 Woman2。他们已经结婚 25 年了。

下面是合金模型。

多妻制男子合金模型

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