Main Content

形式的要件の評価順序の活用

R2022a 以降

Requirements Table ブロックでは、最初の要件から下位に向かって順番に要件を評価していきます。この動作を利用して、データに値を割り当ててから、そのデータを要件セットにリストされた後続の要件で使用することができます。

たとえば、ローカル データを他の要件の前提条件で参照する場合は次のようにします。

  1. ローカル データの値を定義する要件をセットで先にリストします。

  2. ローカル データを前提条件で必要とする要件をそれよりも後にリストします。

  3. データの読み取りを書き込みの前に行っている要件がないことを確認します。

    • Simulink® Design Verifier™ がある場合は、要件を解析して、データの読み取りを書き込みの前に行っているインスタンスを検出できます。[テーブル] タブの [解析] セクションで [テーブルの解析] をクリックします。Detect Read-Before-Write Issuesを参照してください。

要件を定義する方法の詳細については、Requirements Table ブロックを使用した形式的要件の作成を参照してください。

前提条件で出力データを参照できるのは、[前提条件で出力を有効にする] プロパティが有効になっている場合、またはデータが getPrevious 演算子の引数である場合です。このプロパティを有効にするには、Requirements Table ブロックを開きます。[モデル化] タブの [データの設計] セクションで [プロパティ インスペクター] をクリックします。[プロパティ] タブで [前提条件で出力を有効にする] プロパティを有効にします。前提条件で出力を有効にするを参照してください。

要件の順序の使用例

この例では次を使用します。

モデルを開く

この例では、Requirements Table ブロックで要件の順序がデータにどのように影響するかを示します。

要件の確認

Requirements Table ブロックを開きます。このブロックでは、入力データの sensorv と sensor を使用して、ローカル データ value の値を判定します。その後、要件で value を使用して、出力データ output の値を判定します。

要件 3 と 4 を要件 1 と 2 よりも前に定義すると、要件で value を定義する前に value が必要になるため、シミュレーション時に書き込み前の読み取りのエラーが発生します。

参考

関連するトピック