sldv.assume

Stateflow チャートおよび MATLAB Function ブロックについて証明の前提となる関数

構文

sldv.assume(expr)

sldv.assume(expr) は、プロパティの証明時に expr がすべての評価に対して真であることを指定します。expr には有効な論理式を使用します。

この関数はなにも出力しないため、expr を評価する間接的な副作用があるだけで、親関数には影響を与えません。MATLAB^® コマンドラインからこの関数を実行しても、効果はありません。

MATLAB コード内に sldv.assume の証明の前提を組み入れるか、前提を分離して検証スクリプトに入れます。

[プロパティ証明] ペインの [証明の前提] オプションは、関数 sldv.assume および Proof Assumption ブロックによって表現される証明の前提に適用されます。

MATLAB Function ブロックを使用して、sldvdemo_sbr_verification モデルのプロパティ証明オブジェクティブおよび証明の前提を指定します。

sldvdemo_sbr_verification モデルを開き、ex_sldvdemo_sbr_verification として保存します。

Safety Properties サブシステムを開きます。

MATLAB Function ブロックである MATLAB Property ブロックを開きます。

関数 check_reminder の定義の最後に sldv.assume(Inputs.KEY==0 | 1); を追加します。この関数定義の最後の 2 行は次のようになります。

sldv.prove(implies(activeCond, SeatBeltIcon));
sldv.assume(Inputs.KEY==0 | 1);

更新したコードを保存するには、[エディター] タブで [保存] をクリックして、エディターを閉じます。

安全性のプロパティを証明するには、Simulink^® エディターで Safety Properties サブシステムを選択します。[Design Verifier] タブで、[プロパティの証明] をクリックします。

または、Simulink エディターで Safety Properties サブシステムを右クリックし、[Design Verifier] 、 [サブシステムのプロパティを検証] を選択することもできます。

MATLAB 式。たとえば、x > 0。

関数 sldv.assume を使用する代わりに、Proof Assumption ブロックをモデルに挿入できます。Proof Assumption ブロックの代わりに sldv.assume を使用すると、プロパティ証明とはで説明されているとおり、いくつかの利点があります。

MATLAB をコードの生成に使用してモデルを証明する場合、関数 sldv.assume を使用せずに信号値を制限することもできます。コードの生成に MATLAB を直接使用するのではなく、sldv.assume を使用すると、次の処理が不要になります。

R2009b で導入