이 옵션을 사용자 정의 매개 변수의 이름으로 설정합니다. 이 매개 변수의 값은 mc_reports 디렉토리에서 파일 확장자가 .dsumm.html 및 .dsumm.xml인 상세 Modelcheck 보고서 파일에 표시됩니다.

보고서를 생성하려면 초기화 옵션 HTML_FILE_OUTPUT을 Y로 설정해야 합니다.