Simulink Design Verifier データファイルの管理

データファイルの生成

Simulink^® Design Verifier™ は解析の完了時にデータファイルを生成します。データファイルは、sldvData という名前の構造体が含まれる MAT ファイルです。この構造体には、このソフトウェアが解析時に収集および生成するすべてのデータが格納されます。同じデータはハーネスモデルにはグラフィカルに、さらにレポートにも表示されますが、独自の解析の実行やカスタムレポートの生成にこのデータファイルを使用できます。

`sldvData` 構造体のコンテンツ

Simulink Design Verifier はその解析を完了すると、sldvData という名前の構造体を含む MAT ファイルを生成します。sldvData 構造体のコンテンツは、以下の手順により確認します。

sldvdemo_flipflop モデルのテストケースを生成します。
```
sldvdemo_flipflop;
sldvrun('sldvdemo_flipflop');
```
次のコマンドを入力して MATLAB^® プロンプトでデータファイルを読み込みます。
```
load('sldv_output\sldvdemo_flipflop\sldvdemo_flipflop_sldvdata.mat')
```
MATLAB ソフトウェアにより sldvData 構造体がそのワークスペースに読み込まれます。この構造体には、sldvdemo_flipflop モデルの Simulink Design Verifier の解析結果が含まれています。

MATLAB コマンドラインで「sldvData」と入力して、構造体を構成するフィールド名を表示します。

sldvData = 

       ModelInformation: [1x1 struct]
    AnalysisInformation: [1x1 struct]
           ModelObjects: [1x2 struct]
            Constraints: []
             Objectives: [1x12 struct]
              TestCases: [1x4 struct]
                Version: '2.1'

`sldvData` のモデル情報フィールド

以下の節では、sldvData 構造体のフィールドについて説明します。

ModelInformation フィールド
AnalysisInformation フィールド
ModelObjects フィールド
Constraints フィールド
Objectives フィールド
TestCases フィールド / CounterExamples フィールド
Version フィールド
DeadLogic フィールド

ModelInformation フィールド

sldvData 構造体の ModelInformation フィールドには、解析したモデルに関する情報が含まれます。次の表では、ModelInformation フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`Name`	モデル名。
`Version`	モデル番号。
`Author`	ユーザー名。
`TimeStamp`	モデルの最終更新日時。
`SubsystemPath`	解析されたサブシステムがある場合、その絶対パス名。
`ExtractedModel`	`SubsystemPath` でサブシステムが指定されている場合、その解析用に抽出されたモデルがあれば、その名前。
`ReplacementModel`	ブロック置換を含むモデルがある場合、その名前。
`HarnessOwnerModel`	解析している Simulink Test™ のテストハーネスの所有者モデルがある場合、その名前。

AnalysisInformation フィールド

sldvData 構造体の AnalysisInformation フィールドには、個々の解析オプションと関連情報の設定がリストされます。次の表では、AnalysisInformation フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`Status`	Simulink Design Verifier 解析の完了ステータス。
`AnalysisTime`	解析の長さを秒単位で示す double。
`Options`	解析時に使用される Simulink Design Verifier オプションオブジェクトのディープコピー。
`InputPortInfo`	最上位システムの各 Inport ブロックに関する情報を示す構造体の cell 配列。
`OutputPortInfo`	最上位システムの各 Outport ブロックに関する情報を示す構造体の cell 配列。
`SampleTimes`	内部使用専用。
`Parameters`	内部使用専用。
`AbstractedBlocks`	内部使用専用。
`Approximations`	解析時に実行される近似を記述する構造体。近似の詳細は、近似を参照してください。
`ReplacementInfo`	内部使用専用。
`PreProcessingTime`	モデル表現を作成または再利用する時間 (秒単位) を指定する double。
`ModelRepresentationInfo`	解析に使用するモデル表現の日付と時刻。

ModelObjects フィールド

sldvData 構造体の ModelObjects フィールドには、モデルの項目とそれに関連付けられたオブジェクティブがリストされます。次の表では、ModelObjects フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`descr`	Stateflow^® チャートのオブジェクトなど、モデルオブジェクトの絶対パス。
`typeDesc`	モデルオブジェクトのブロックタイプ。
`slPath`	Simulink モデルオブジェクトの絶対パス。
`sfObjType`	Stateflow オブジェクトのタイプ。例: ステートは `S`、遷移は `T`。
`sfObjNum`	Stateflow オブジェクトの一意の識別子を表す整数。
`sid`	内部使用専用。
`designSid`	内部使用専用。
`replacementSid`	内部使用専用。
`objectives`	モデルオブジェクトに関連付けられたオブジェクティブのインデックスを表す整数ベクトル。

Constraints フィールド

sldvData 構造体の Constraints フィールドには、モデルの入力端子に指定された最小値および最大値がある場合、それに関する情報がリストされます。次の表では、Constraints フィールドのサブフィールドについて説明します。

サブフィールド名	説明
`DesignMinMax`	値が指定されている各入力端子の名前、最小値および最大値を含む構造体の cell 配列。

Objectives フィールド

sldvData 構造体の Objectives フィールドには、タイプ、ステータス、説明など、それぞれのオブジェクティブに関する情報がリストされます。次の表では、Objectives フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`type`	オブジェクティブのタイプ。
`status`	オブジェクティブのステータス。
`descr`	オブジェクティブの説明。
`label`	オブジェクティブのラベル。
`outcomeValue`	オブジェクティブの結果を示す整数。
`coveragePointIdx`	オブジェクティブが関連付けられているカバレッジポイントのインデックスを表す整数。
`linkInfo`	内部使用専用。
`range`	内部使用専用。
`detectability`	オブジェクティブの検出可能性ステータス。このフィールドは、解析モードが `[テスト生成]` に設定され、モデルカバレッジオブジェクティブが `[Enhanced MCDC]` に設定されているときに、データファイルに表示されます。
`detectionSites`	検出可能オブジェクティブの、検出サイトの Simulink 識別子 (SID) の配列。オブジェクティブは、いずれかの検出サイトで検出可能です。このフィールドは、解析モードが `[テスト生成]` に設定され、モデルカバレッジオブジェクティブが `[Enhanced MCDC]` に設定されているときに、データファイルに表示されます。
`modelObjectIdx`	オブジェクティブが関連付けられているモデルオブジェクトのインデックスを表す整数。
`analysistime`	オブジェクトの解析時間を表す整数。
`testCaseIdx`	オブジェクティブを扱うテストケースまたは反例のインデックスを表す整数。

TestCases フィールド / CounterExamples フィールド

sldvData 構造体では、構造体では、このフィールドはチェックのタイプに応じて 2 つの名前をもつことができます。

[モード] パラメーターを [設計エラー検出] に設定すると、CounterExamples フィールドに整数オーバーフローまたはゼロ除算エラーとなる各テストケースに関する情報がリストされます。
[モード] パラメーターを [テスト生成] に設定すると、TestCases フィールドにその信号値や達成するテストオブジェクティブなど、各テストケースに関する情報がリストされます。
[モード] パラメーターを [プロパティ証明] に設定すると、CounterExamples フィールドに反例とそれによって反証される証明オブジェクティブの情報が個々にリストされます。

次の表では、TestCases / CounterExamples フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`timeValues`	テストケースまたは反例の信号に関連付けられた時間値を示すベクトル。
`dataValues`	テストケースまたは反例の信号に関連付けられたデータ値を示す cell 配列。
`paramValues`	テストケースまたは反例に関連付けられたパラメーター値を示す構造体。この構造体には以下のフィールドがあります。 `name` — パラメーター名。 `value` — パラメーターの値を示す数値。 `noEffect` — パラメーターの値がオブジェクティブに影響するかどうかを示す論理値。
`stepValues`	テストケースまたは反例の信号を構成するタイムステップ数を示すベクトル。
`objectives`	テストケースまたは反例で扱われるオブジェクティブを示す構造体。この構造体には以下のフィールドがあります。 `objectiveIdx` — テストケースが達成するオブジェクティブまたは反例が反証するオブジェクティブのインデックスを表す整数。 `atTime` — テストケースがオブジェクティブを達成するとき、あるいは反例がオブジェクティブを反証するときの時間値。 `atStep` — テストケースがオブジェクティブを達成するとき、あるいは反例がオブジェクティブを反証するときのタイムステップ。
`dataNoEffect`	信号のデータ値がオブジェクティブに影響するかどうかを示す logical ベクトルの cell 配列。ベクトルは信号のデータ値がオブジェクティブに影響しないことを `1` により示し、それ以外には `0` を使用します。
`expectedOutput`	テストケースの信号を使用したモデルのシミュレーションから得られた出力値を示すベクトルの cell 配列。それぞれのセルは、最上位システムの個々の Outport ブロックに関連付けられた出力値を表します。[期待される出力値を含める] が選択されている場合、このサブフィールドにデータが格納されます。

Version フィールド

sldvData 構造体の Version フィールドでは、モデルを解析した Simulink Design Verifier のバージョンを指定します。

DeadLogic フィールド

モデルのデッドロジックを解析すると、sldvData 構造体の DeadLogic フィールドに、デッドロジックとなった各オブジェクティブについての情報がリストされます。

次の表では、DeadLogic フィールドの各サブフィールドについて説明します。

サブフィールド名	説明
`label`	デッドロジックとなったオブジェクティブの説明。
`descr`	Stateflow チャートのオブジェクトなど、モデルオブジェクトの絶対パス。
`modelObjIdx`	オブジェクティブに関連付けられているモデルオブジェクトのインデックスを表す整数。
`coverageType`	カバレッジオブジェクティブのタイプ。
`coverageIdx`	オブジェクティブに関連付けられているカバレッジポイントのインデックスを表す整数。
`ObjectiveIdx`	モデルオブジェクトに関連付けられているオブジェクティブのインデックスを表す整数。

データファイルを使用したモデルのシミュレーション

関数 sldvruntest は、Simulink Design Verifier データファイル内のテストケースまたは反例を使用してモデルをシミュレートします。

sldvdemo_flipflop モデルをシミュレートし、テストケースを生成します。
```
sldvdemo_flipflop
```
モデルを解析した後、生成されたデータファイルの位置を保存します。
```
sldvDataFile = 'sldv_output\sldvdemo_flipflop\sldvdemo_flipflop_sldvdata.mat'
```
関数 sldvruntest を使用して、データファイルのテストケース 2 で sldvdemo_flipflop モデルをシミュレートします。
```
[ outdata ] = sldvruntest('sldvdemo_flipflop', sldvDataFile, 2)
```
sldvruntest からの出力は、Simulink.SimulationOutput オブジェクトの配列です。

Simulink.SimulationOutput オブジェクトのメソッドを使用して、最初のテストケースの出力データを調べます。

tout_sldvruntest = outdata(1).find('tout_sldvruntest');
xout_sldvruntest = outdata(1).find('xout_sldvruntest');
yout_sldvruntest = outdata(1).find('yout_sldvruntest');
logsout_sldvruntest = outdata(1).find('logsout_sldvruntest');

データファイルからの結果の読み込み

モデルの以前の解析結果をデータファイルから読み込むことができます。詳細は以前の結果の読み込みと sldvloadresults を参照してください。