Alloy で整数を使う際のビット幅の件

結論としては、
・　デフォルトではビット幅が 3 ( -4 〜 3 ) になっている（デフォルトのスコープが Int にも適用される）
・　指定のビット幅の範囲を超える整数についての式は結果が不定（？）
・　特にエラー、警告は出ない。
ということのようである。
※Alloy Analyzer 4.2 での話。
ビット幅の件はp132参照。

なお、明示的に Int シグネチャを指定せず、濃度制約等で整数を定数として使用してもアウトらしい。

sig B {}
sig A {
rel : set B
}

このモデルで、

pred show {
#rel > 8
}
run show

とやると、デフォルトのスコープが3なので、Aが3個、Bが3個で rel が9個になるインスタンスのみが真になるはずだが、解析の結果そうでないものが大量に引っかかる。

pred show {
#rel > 8
}
run show for 3 but 5 Int

とやると、A 3, B3, rel 9 のインスタンスのみが引っかかる。