ファクト（合金）で働いていない数を使用してください

Question

私は合金の初心者です（MITによって作られたモデリング言語）。私は合金の2ベッドルームのアパートのリースをモデル化しようとしています。私は、各賃貸アパートの人数が4人以下であるような事実を追加しようとしています。しかし、実行中に生成されたインスタンスは、10人の居住者を持つ唯一の2ベッドルームリースアパートを示しています。私は間違って何をしていますか？また可能ならMITのウェブサイト上のチュートリアルとは別に、Alloyを学ぶための良いリソースを指し示すことができますか？ありがとう。デフォルトでは

abstract sig apartment {} 

sig twoLeased extends apartment { 
occupants: some People 
} { #occupants < 5 } 

sig twoUnleased extends apartment { 

} 

sig People {} 

run {} for 3 but 4 twoLeased, 10 People 

Answer 1

整数を表すために使用されるビット幅は4ので、あなたのインスタンスが-8から7の範囲の整数が含まれています。占有者の数が10の場合、整数オーバフローが発生し（10>8）、#occupantsは負の数を返します。したがって、5よりも劣り、したがって不変量を満たします。

この問題を解決するには、Alloy Analyzerの設定で整数オーバフローを禁止するか、整数を表すビット幅を大きくします（例：run {} for 6 Int）。