頁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