合金の奇妙な行動？

Question

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

Iインスタンスを開くと、Iは、評価者から

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 <何もタイプエラーが発生しません。//これはうまく見えますが、（3）を与える理由、 これはタイプエラーですか？

（5）0 < = S1（S2-> 1）に評価真

（6）0> = S1（S2-> 1）に評価真

（7）0 = S1（S2→1）が偽に評価される//（5）（6）が与えられた場合、 S1（S2→1）は0と評価されますが、そうではありません。 （9）0 < =いずれも型エラーを与えない

（8）0 =なしが偽

に評価//（8）（9） "=" 整数比較として解釈されないような興味深いものに見えます。

（1） - （9）の原因は誰でも説明できますか？バグはありますか？

Answer 1

（1）これは、なぜ明らかにする必要があります：それは参加リレーショナルだとS1は（2）noneはそう考えると、空のセットに評価（1）それはnone = S1.(S2->1)

という意味があります S2

と同じではありません

（3）-1のタイプがintであり、S1.(S2->1)のタイプがS.(S->int)のタイプがintであるため、タイプエラーはありません。問題は、-1が空のセットに評価される整数型の式よりも小さい理由だけです。まず、式-1 < S1.(S2->1)は何かを評価する必要があります（つまり、プログラミング言語のように例外をスローすることはできません）。さらに、これはブール式なので、trueまたはfalseのいずれかに評価する必要があります。だから、Alloyは、<演算子を評価するために、両辺が実際に整数の集合（すべてが合金の集合/関係）であっても、両辺を単一（スカラー）整数に変換しなければなりません。各セットに存在するすべての原子を合計することによってそうする。したがって、算術比較のためだけに、S1.(S2->1)は0と評価されます。

（4）は、左側のタイプがintあり、右側のタイプは、none

（5）であるため-1 < noneは、実際型エラーであることが明らかであるべきです=は常にセットの比較ではなく、整数比較あるため、（6）（3）

用と同じ説明は、（7）0 = S1.(S2->1)は偽です。 1 + 2 = 3のようなものを試すと、セット{1,2}が{3}ではないので、falseが得られます。

（8）同じことを、=が設定された比較

（9）と同じ説明は、（4）

するためのものです