[Java Path Finder][JPF學習筆記][7]JPF輸出詳細程度設定

這篇日志是補充一下看到的一點點經驗。

這個頁面：http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/output 中介紹到，jpf的一次運作主要可以生成三類輸出：

1. application output

2. JPF logging

3. JPF reporting system

其實上面的頁面對這三種輸出已經講解得很詳細了，但是沒有介紹前兩種輸出在哪裡配置。

實際上就是在%JPF_HOME%\jpf-core\jpf.properties，打開這個檔案，我們可以發現從0-5共6類設定。其中vm.tree_output的設定是在第2部分，log.level的設定是在第3部分。

但是我還沒有找到哪裡有文檔完整介紹一下JPF reporting system的配置，隻知道按照JPF自己給出的例子，可以在.jpf檔案中設定諸如：

report.console.property_violation=error,trace,snapshot,output,statistics
           

的語句，而且上面這個頁面中說的：

"There is no standard transition topic yet (but it could be implemented in PublisherExtensions). "，也不太清楚具體是什麼意思，哪位大俠能指點一二？