Main Content

Proof Assumption

モデルのプロパティを証明する場合に、信号値を制限する

このページをすべて展開する
  • Proof Assumption block

ライブラリ:
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 ブロックを使用します。

[値] パラメーターを使って、プロパティ証明の信号値を制限できます。詳細については、パラメーター コンフィギュレーション ファイルの使用を参照してください。

例

Assumption ブロックによるプロパティ証明

Assumption ブロックによるプロパティ証明

この例では、Proof Assumption ブロックを使用した、Simulink® Design Verifier™ のプロパティ証明の実行方法を示します。これは、現在の入力値および以前の 6 つの入力値の合計が 6 より大きい場合、出力が 2 と等しいことを証明しようとします。モデルには入力を 0 または 1 に制約する Proof Assumption ブロックが含まれます。Simulink Design Verifier は 20 以下のタイム ステップの違反を検索します。仮定に基づいてプロパティが有効であるため、違反を見つけることはできません。

スクリプトを開く

端子

入力

すべて展開する

Proof Assumption ブロックは、Simulink ソフトウェアがサポートするすべての組み込みデータ型の信号を受け入れます。Simulink ソフトウェアがサポートするデータ型の詳細は、Simulink でサポートされているデータ型を参照してください。このブロックは、複素数入力信号をサポートしていません。

データ型: single | double | int8 | int16 | int32 | int64 | uint8 | uint16 | uint32 | uint64 | Boolean | fixed point | enumerated | bus

出力

すべて展開する

Proof Assumption ブロックは、Simulink ソフトウェアがサポートするすべての組み込みデータ型の信号を返します。サポートされているデータ型の詳細については、Simulink でサポートされているデータ型を参照してください。

データ型: single | double | int8 | int16 | int32 | int64 | uint8 | uint16 | uint32 | uint64 | Boolean | fixed point | enumerated | bus

パラメーター

すべて展開する

このブロックが有効かどうかを指定します。選択すると (既定の設定)、Simulink Design Verifier ソフトウェアはモデルのプロパティの証明時にこのブロックを使用します。このオプションをオフにすると、ブロックが無効になります。すなわち、Simulink Design Verifier ソフトウェアは Proof Assumption ブロックが存在しないかのように動作します。選択されていない場合は、Simulink エディターでこのブロックがグレー表示になります。

ブロックが Proof Assumption ブロックまたは Test Condition ブロックのどちらとして動作するかを指定します。[テスト条件] を選択すると、Proof Assumption ブロックが Test Condition ブロックに変換されます。

[値] パラメーターを使って、テスト ケースの信号値を制限します。MATLAB® の cell 配列形式で、スカラー値と間隔の組み合わせを指定します。詳細については、パラメーター コンフィギュレーション ファイルの使用を参照してください。

Simulink エディターで、ブロックが [値] パラメーターの内容を表示するかどうかを指定します。

選択すると、ブロックは出力端子を表示し、入力信号をブロックの出力へパス スルーすることができます。選択されていない場合は、ブロックは出力端子を非表示にして、入力信号を終了します。

例: 次の図は、各ケースのブロックの外観を示しています。

パス スルー スタイル (出力端子を表示): 選択した場合

パス スルー スタイル (出力端子を表示): 選択しない場合

バージョン履歴

R2007a で導入

参考

|