scope - Alloy で単純な整数の反例が発生しないのはなぜですか?

Question

数値変数とブール変数の間の関係をモデル化しようとしています。数値変数が特定の範囲内にある場合、ブール変数は値を変更します。私は合金を初めて使用し、明らかな反例を生成するのに十分な範囲を制限する方法を理解するのに苦労しています。私のコードは次のとおりです。

open util/boolean 

one sig Object {
    discrete : one Bool,
    integer : one Int
}

fact { all o : Object | o.integer > 0 and o.integer < 10 }
fact { all o : Object | o.integer > 5 iff o.discrete = False }

assert discreteCondition { all o : Object | o.discrete = True }

check discreteCondition for 1000

o.integerは整数値であり、範囲は 0 から 10 であるため、10 の異なる選択肢のうちの 1 つにすぎません。そして、それぞれが oneと oneObjectのみを持つように指定しました。したがって、ここでチェックするケースは実際には 10 個しかないというのが理にかなっているように思えます。それでも、1000ケースでも、integerdiscreteinteger

反例は見つかりませんでした。

変数と関連する事実を削除するintegerと、反例がすぐに見つかります。また、他のソルバーを使用して、オプションでさまざまな深度とメモリの値を増やしてみましたが、これは役に立ちませんでした。明らかに私のコードに問題があります。

Alloy が反例を見つけられるようにスコープを制限するにはどうすればよいですか ( の可能な値を反復処理することによってinteger)? ありがとう！