合金奇怪的行爲？

Question

abstract sig S {} 
one sig S1, S2 in S {} 
fact {S1 != S2} 
run {-1 < S1.(S2 -> 1)} 

當我打開情況下，我得到了

integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7} 
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, S$0, S$1} 
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7} 
seq/Int={0, 1, 2, 3} 
String={} 
none={} 
this/S={S$0, S$1} 
this/S1={S$1} 
this/S2={S$0} 

從評價者，

（1）S1（S2 - > 1），計算結果爲{}

（ 2）none = S1（S2 - > 1）求值爲真

（3）-1 < S1。（S2 - > 1）求值爲真//爲什麼整數少 比空集？

（4）-1 < none給出類型錯誤//這看起來不錯，但給（3），爲什麼 這給出類型錯誤？

（5）0 < = S1。（S2-> 1）評估爲true

（6）0> = S1。（S2-> 1）評估爲true

（7）0 = S1。（S2-> 1）評估爲假//給定（5）（6），似乎 S1。（S2-> 1）評估爲0，但事實並非如此。

（8）0 =無評估爲假

（9）0 < =無給類型錯誤//（8）（9）似乎是有趣的，因爲 「=」 不被解釋爲整數比較。

任何人都可以解釋爲什麼（1） - （9）發生？有錯誤嗎？

Answer 1

（1）這應該是顯而易見的，爲什麼：這是一個關係加入，S1是不一樣的S2

（2）none計算結果爲空集，所以給出的（1）它是有道理的none = S1.(S2->1)

（3）這裏沒有類型錯誤，因爲-1的類型是int，並且S1.(S2->1)的類型是S.(S->int)，它是int。這個問題只是爲什麼-1小於一些整數類型表達式的計算結果爲空集。首先，表達式-1 < S1.(S2->1)必須被評估爲某種東西（即，不能像在編程語言中那樣拋出異常）。此外，這是一個布爾表達式，因此它必須評估爲true或false。因此，Alloy爲了評估<運算符，必​​須將雙方轉換爲單個（標量）整數，即使雙方實際上是整數集合（一切都是Alloy中的集合/關係），並且它通過總結每組中存在的所有原子來做到這一點。所以只是爲了算術比較,S1.(S2->1)評估爲0。

（4）應當清楚現在-1 < none確實是一個類型的錯誤，因爲左手側的類型是int和右手側的類型是none

（5）， （6）相同的說明作爲（3）

（7）0 = S1.(S2->1)是假的，因爲=是總是一組比較，不是整數的比較。如果你嘗試類似1 + 2 = 3的東西，你會得到false，因爲集合{1,2}不是{3}。

（8）同樣的事情，=是一組比較

（9）相同的解釋爲（4）