このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
Proof Assumption
モデルのプロパティを証明する場合に、信号値を制限する
ライブラリ:
Simulink Design Verifier /
Objectives and Constraints
説明
プロパティ証明モードで動作する場合、Simulink® Design Verifier™ ソフトウェアは、モデルのプロパティが指定された基準を満たしていることを証明します (プロパティ証明とはを参照)。このモードでは、Proof Assumption ブロックを使って、モデル内の信号の前提を定義できます。[値] パラメーターを使用すると、プロパティ証明時の信号値に関する制限を指定できます。このブロックは、指定された [値] パラメーターを入力信号に適用します。Simulink Design Verifier ソフトウェアは、モデルのプロパティが指定された基準を満たしていることを証明または反証します。
このブロックのパラメーター ダイアログ ボックスでは、以下の操作も実行できます。
前提を有効または無効にします。
Simulink エディターで、ブロックの [値] パラメーターを表示するように指定します。
ブロックの出力端子を表示するように指定します。
メモ
Simulink と Simulink Coder™ ソフトウェアは、それぞれモデルのシミュレーション時とコード生成時に、Proof Assumption ブロックを無視します。Simulink Design Verifier ソフトウェアは、モデル プロパティの証明時にだけ Proof Assumption ブロックを使用します。
[値] パラメーターを使って、プロパティ証明の信号値を制限できます。詳細については、パラメーター コンフィギュレーション ファイルの使用を参照してください。
例
端子
入力
出力
パラメーター
バージョン履歴
R2007a で導入