このオプションにはユーザー定義パラメータの名前を設定します。このパラメータの値は mc_reports ディレクトリ内のファイル拡張子 .dsumm.html または .dsumm.xml が付いた詳細 Modelcheck レポートファイルに表示されます。

レポートが生成されるためには、初期化オプション HTML_FILE_OUTPUT が Y に設定されている必要があります。