このページの翻訳は最新ではありません。ここをクリックして、英語の最新版を参照してください。
形式的要件の評価順序の活用
Requirements Table ブロックでは、最初の要件から下位に向かって順番に要件を評価していきます。この動作を利用して、データに値を割り当ててから、そのデータを要件セットにリストされた後続の要件で使用することができます。
たとえば、ローカル データを他の要件の前提条件で参照する場合は次のようにします。
ローカル データの値を定義する要件をセットで先にリストします。
ローカル データを前提条件で必要とする要件をそれよりも後にリストします。
データの読み取りを書き込みの前に行っている要件がないことを確認します。
Simulink® Design Verifier™ がある場合は、要件を解析して、データの読み取りを書き込みの前に行っているインスタンスを検出できます。[テーブル] タブの [解析] セクションで [テーブルの解析] をクリックします。矛盾する形式的要件セットおよび不完全な形式的要件セットの特定を参照してください。
要件を定義する方法の詳細については、Requirements Table ブロックを使用した形式的要件の作成を参照してください。
前提条件で出力データを参照できるのは、[前提条件で出力を有効にする] プロパティが有効になっている場合、またはデータが getPrevious
演算子の引数である場合です。このプロパティを有効にするには、Requirements Table ブロックを開きます。[モデル化] タブの [データの設計] セクションで [プロパティ インスペクター] をクリックします。[プロパティ] タブで [前提条件で出力を有効にする] プロパティを有効にします。前提条件で出力を有効にするを参照してください。
要件の順序の使用例
この例では、Requirements Table ブロックで要件の順序がデータにどのように影響するかを示します。
要件の確認
Requirements Table ブロックを開きます。このブロックでは、入力データの sensorv
と sensor
を使用して、ローカル データ value
の値を判定します。その後、要件で value
を使用して、出力データ output
の値を判定します。
要件 3 と 4 を要件 1 と 2 よりも前に定義すると、要件で value
を定義する前に value
が必要になるため、シミュレーション時に書き込み前の読み取りのエラーが発生します。