这篇日志是补充一下看到的一点点经验。
这个页面：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). "，也不太清楚具体是什么意思，哪位大侠能指点一二？