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

页Software Abstractions 293说，这两者是等价的：为什么多个Alloy声明不等价于嵌套的Alloy声明？

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次（银）结婚纪念日。

我在餐桌上创建了人的合金模型。该模型规定，有一个L：男，女：女人夫妇其中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

的情况下，合金分析仪生成的是我所期望的。

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

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

的合金分析仪所产生的相同的实例！

接下来，我写了一个声明，声称这两个版本是相同的：

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

来源

2017-10-08 Roger Costello

谓词太制约了有

合金模型有差别。

嵌套版和非嵌套版本之间的差异可以当例子修改了一下可以看出：让每个人要结婚，一组女：

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

，说恰好有一个L：男人，W：女人其中w是m的妻子之一，w的丈夫是m，m和w正在庆祝一个银色的周年纪念日。

以下是Alloy Analyzer生成的实例之一：Man1有妻子Woman1和Woman2。 Woman1有丈夫Man1。同样，Woman2有丈夫Man1。Woman1正与她的丈夫（Man1）庆祝25周年结婚纪念日。

这里是嵌套的版本：

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

，说正好有一个L：人为其约束是真实的，这里的约束是这样的：有一个女人就是女人是男人的妻子和他们已结婚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

来源

2017-10-08 19:44:30

您可以运行这些例子看出区别：

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

来源

2017-10-12 07:10:32 Grayswandyr

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

回答

相关问题