述語の比較

Question

ポスターは、合金の機能を比較する方法を尋ねました。小さな例（関数の代わりに述語を比較する）をテストしながら、質問に答えるために、私は次のような動作に気付きました。

アナライザは、チェックコマンドの境界が3より大きく、ファクト 'f1'がアクティブである場合に反例を検出しません。事実を不活性化すると、アナライザは期待どおりに動作します。なぜ冗長な事実 'f1'はアナライザの動作を変更するのですか？また境界が3よりも大きいのはなぜですか？

open util/ordering [V] 
sig V {} 

fact f1 { 
    # V > 0 
} 

pred p1 [x: V] { 
    x = last 
} 

pred p2 [x: V] { 
    x = first 
} 

assert a1 { 
    all x: V | p1[x] <=> p2[x] 
} 

check a1 for 3 

いつでもチェック境界が4以上であると「F1は」アクティブアナライザーレポート「0 VARSであることが表示されます。 0プライマリヴァース。 0句。

Answer 1

詳細を調べることができませんが、合金の整数が非常に狭いという事実に基づいてオーバーフロー現象が発生しているようです（デフォルトでは4ビットと思われます）。 2の補数の整数なので、オーバーフローは定期的に発生します。

いくつかの変更は、それらが動作に影響を与えるかどうかを知るために、個別に、または一緒に教えることがあります。

• scopeコマンドを使用してのIntのための明示的なビット幅を提供し、「禁止するオーバーフロー」オプション
• にsome V
• ターンで実際にF1を交換する（他の署名のために、スコープの数はインスタンスの最大数を指定します; Intの場合はビット幅を指定します）

LoïcGammaitoniは別の質問に「ここでは合金で数値を使用するときは常に注意が必要です」と述べています。