Main Content

無効なプロパティを含むプロパティ証明

この例では、Simulink Design Verifier のプロパティ証明解析を使用した、無効なプロパティの検索方法を示します。これは、現在の入力値および以前の 6 つの入力値の合計が 6 より大きい場合、出力が 2 と等しいことを証明しようとします。この場合、単一の大きな入力値 (255 など) によって合計が 6 より大きくなるため、プロパティは無効です。Simulink Design Verifier はこの違反を示す反例を生成します。

open_system('sldvdemo_debounce_falseprop');