doc/devel/report.md

   1 # The JPF Report API #
   2 The JPF report system consists of three major components:
   3
   4   - the `Reporter`
   5   - any number of format specific `Publisher` objects
   6   - any number of tool-, property-, Publisher-specific `PublisherExtension` objects
   7
   8 Here is the blueprint:
   9
  10 ![Figure: JPF Report System](../graphics/report.svg){align=center width=800}
  11
  12 The `Reporter` is the data collector. It also manages and notifies `Publisher` extensions when a certain output phase is reached. The `Publishers` are the format (e.g. text, XML) specific output producers, the most prominent one being the `ConsolePublisher` (for normal, readable text output on consoles). `PublisherExtensions` can be registered for specific `Publishers` at startup time, e.g. from Listeners implementing properties or analysis modes such as `DeadlockAnalyzer`. This is so common that the `ListenerAdapter` actually implements all the required interface methods so that you just have to override the ones you are interested in.
  13
  14 Configuration is quite easy, and involves only a handful of JPF properties that are all in the report category. The first property specifies the Reporter class itself, but is not likely to be redefined unless you have to implement different data collection modes.
  15
  16 ~~~~~~~~ {.bash}
  17 report.class=gov.nasa.jpf.report.Reporter
  18 ~~~~~~~~
  19
  20 The next setting specifies a list of Publisher instances to use, using symbolic names:
  21
  22 ~~~~~~~~ {.bash}
  23 report.publisher=console,xml
  24 ~~~~~~~~
  25
  26 Each of these symbolic names has to have a corresponding class name defined:
  27
  28 ~~~~~~~~ {.bash}
  29 report.console.class=gov.nasa.jpf.report.ConsolePublisher
  30 ~~~~~~~~
  31
  32 Finally, we have to specify for each symbolic publisher name and output phase what topics should be processed in which order, e.g.
  33
  34 ~~~~~~~~ {.bash}
  35 report.console.property_violation=error,trace,snapshot
  36 ~~~~~~~~
  37
  38 Again, the order of these topics matters, and gives you complete control over the report format. As usual, please refer to `defaults.properties` for default values.
  39
  40 Publisher classes can have their own, additional properties. For instance, the `ConsolePublisher` implementation can be further configured with respect to the information that is included in traces (bytecodes, method names etc.), and to redirect output (file, socket). Please refer to the constructor of this class for further details.
  41
  42 ~~~~~~~~ {.bash}
  43 # save report to file
  44 report.console.file=My_JPF_report
  45 ~~~~~~~~
  46
  47 All of the involved core classes and interfaces reside in the `gov.nasa.jpf.report` package. The most common way to extend the system is to use your own `PublisherExtension` implementation, which involves two steps:
  48
  49   - implement the required phase and format specific methods
  50   - register the extension for a specific Publisher class
  51
  52
  53 The `DeadlockAnalyzer` (which is a listener to analyze concurrency defects) can be used as an example of how to do this:
  54
  55 ~~~~~~~~ {.java}
  56 public class DeadlockAnalyzer extends ListenerAdapter {
  57   ...
  58   public DeadlockAnalyzer (Config config, JPF jpf){
  59     jpf.addPublisherExtension(ConsolePublisher.class, this);  // (1)
  60     ...
  61   }
  62   ...
  63   public void publishPropertyViolation (Publisher publisher) { // (2)
  64     PrintWriter pw = publisher.getOut();
  65     publisher.publishTopicStart("thread ops " + publisher.getLastErrorId());
  66
  67     ... // use 'pw' to generate the output
  68   }
  69 }
  70 ~~~~~~~~