Impostate questa opzione sul nome di un parametro definito dall'utente. Il valore di tale parametro verrà visualizzato nei file report dettagliati di Modelcheck nella directory mc_reports con le estensioni file .dsumm.html e .dsumm.xml.

Affinché i report siano generati, l'opzione di inizializzazione HTML_FILE_OUTPUT deve essere impostata su Y.