將此選項設定為使用者定義參數的名稱。此參數的值會顯示在 mc_reports 目錄內檔案副檔名為 .dsumm.html 與 .dsumm.xml 的詳細 Modelcheck 報告檔案中。

必須將初始化選項 HTML_FILE_OUTPUT 設定為 Y，才會產生報告。