--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/report/ConsolePublisher.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,392 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.report;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.Error;
+import gov.nasa.jpf.util.Left;
+import gov.nasa.jpf.vm.ClassInfo;
+import gov.nasa.jpf.vm.ClassLoaderInfo;
+import gov.nasa.jpf.vm.Instruction;
+import gov.nasa.jpf.vm.VM;
+import gov.nasa.jpf.vm.MethodInfo;
+import gov.nasa.jpf.vm.Path;
+import gov.nasa.jpf.vm.Step;
+import gov.nasa.jpf.vm.Transition;
+
+import java.io.FileNotFoundException;
+import java.io.FileOutputStream;
+import java.io.PrintWriter;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.TreeMap;
+
+public class ConsolePublisher extends Publisher {
+
+  // output destinations
+  String fileName;
+  FileOutputStream fos;
+
+  String port;
+
+  // the various degrees of information for program traces
+  protected boolean showCG;
+  protected boolean showSteps;
+  protected boolean showLocation;
+  protected boolean showSource;
+  protected boolean showMethod;
+  protected boolean showCode;
+
+  public ConsolePublisher(Config conf, Reporter reporter) {
+    super(conf, reporter);
+
+    // options controlling the output destination
+    fileName = conf.getString("report.console.file");
+    port = conf.getString("report.console.port");
+
+    // options controlling what info should be included in a trace
+    showCG = conf.getBoolean("report.console.show_cg", true);
+    showSteps = conf.getBoolean("report.console.show_steps", true);
+    showLocation = conf.getBoolean("report.console.show_location", true);
+    showSource = conf.getBoolean("report.console.show_source", true);
+    showMethod = conf.getBoolean("report.console.show_method", false);
+    showCode = conf.getBoolean("report.console.show_code", false);
+  }
+
+  @Override
+  public String getName() {
+    return "console";
+  }
+
+  @Override
+  protected void openChannel(){
+
+    if (fileName != null) {
+      try {
+        fos = new FileOutputStream(fileName);
+        out = new PrintWriter( fos);
+      } catch (FileNotFoundException x) {
+        // fall back to System.out
+      }
+    } else if (port != null) {
+      // <2do>
+    }
+
+    if (out == null){
+      out = new PrintWriter(System.out, true);
+    }
+  }
+
+  @Override
+  protected void closeChannel() {
+    if (fos != null){
+      out.close();
+    }
+  }
+
+  @Override
+  public void publishTopicStart (String topic) {
+    out.println();
+    out.print("====================================================== ");
+    out.println(topic);
+  }
+
+  @Override
+  public void publishTopicEnd (String topic) {
+    // nothing here
+  }
+
+  @Override
+  public void publishStart() {
+    super.publishStart();
+
+    if (startItems.length > 0){ // only report if we have output for this phase
+      publishTopicStart("search started: " + formatDTG(reporter.getStartDate()));
+    }
+  }
+
+  @Override
+  public void publishFinished() {
+    super.publishFinished();
+
+    if (finishedItems.length > 0){ // only report if we have output for this phase
+      publishTopicStart("search finished: " + formatDTG(reporter.getFinishedDate()));
+    }
+  }
+
+  @Override
+  protected void publishJPF() {
+    out.println(reporter.getJPFBanner());
+    out.println();
+  }
+
+  @Override
+  protected void publishDTG() {
+    out.println("started: " + reporter.getStartDate());
+  }
+
+  @Override
+  protected void publishUser() {
+    out.println("user: " + reporter.getUser());
+  }
+
+  @Override
+  protected void publishJPFConfig() {
+    publishTopicStart("JPF configuration");
+
+    TreeMap<Object,Object> map = conf.asOrderedMap();
+    Set<Map.Entry<Object,Object>> eSet = map.entrySet();
+
+    for (Object src : conf.getSources()){
+      out.print("property source: ");
+      out.println(conf.getSourceName(src));
+    }    
+    
+    out.println("properties:");
+    for (Map.Entry<Object,Object> e : eSet) {
+      out.println("  " + e.getKey() + "=" + e.getValue());
+    }
+  }
+
+  @Override
+  protected void publishPlatform() {
+    publishTopicStart("platform");
+    out.println("hostname: " + reporter.getHostName());
+    out.println("arch: " + reporter.getArch());
+    out.println("os: " + reporter.getOS());
+    out.println("java: " + reporter.getJava());
+  }
+
+
+  @Override
+  protected void publishSuT() {
+    publishTopicStart("system under test");
+    out.println( reporter.getSuT());
+  }
+
+  @Override
+  protected void publishError() {
+    Error e = reporter.getCurrentError();
+
+    publishTopicStart("error " + e.getId());
+    out.println(e.getDescription());
+
+    String s = e.getDetails();
+    if (s != null) {
+      out.println(s);
+    }
+
+  }
+
+  @Override
+  protected void publishConstraint() {
+    String constraint = reporter.getLastSearchConstraint();
+    publishTopicStart("search constraint");
+    out.println(constraint);  // not much info here yet
+  }
+
+  @Override
+  protected void publishResult() {
+    List<Error> errors = reporter.getErrors();
+
+    publishTopicStart("results");
+
+    if (errors.isEmpty()) {
+      out.println("no errors detected");
+    } else {
+      for (Error e : errors) {
+        out.print("error #");
+        out.print(e.getId());
+        out.print(": ");
+        out.print(e.getDescription());
+
+        String s = e.getDetails();
+        if (s != null) {
+          s = s.replace('\n', ' ');
+          s = s.replace('\t', ' ');
+          s = s.replace('\r', ' ');
+          out.print(" \"");
+          if (s.length() > 50){
+            out.print(s.substring(0,50));
+            out.print("...");
+          } else {
+            out.print(s);
+          }
+          out.print('"');
+        }
+
+        out.println();
+      }
+    }
+  }
+
+  /**
+   * this is done as part of the property violation reporting, i.e.
+   * we have an error
+   */
+  @Override
+  protected void publishTrace() {
+    Path path = reporter.getPath();
+    int i=0;
+
+    if (path.size() == 0) {
+      return; // nothing to publish
+    }
+
+    publishTopicStart("trace " + reporter.getCurrentErrorId());
+
+    for (Transition t : path) {
+      out.print("------------------------------------------------------ ");
+      out.println("transition #" + i++ + " thread: " + t.getThreadIndex());
+
+      if (showCG){
+        out.println(t.getChoiceGenerator());
+      }
+
+      if (showSteps) {
+        String lastLine = null;
+        MethodInfo lastMi = null;
+        int nNoSrc=0;
+
+        for (Step s : t) {
+          if (showSource) {
+            String line = s.getLineString();
+            if (line != null) {
+              if (!line.equals(lastLine)) {
+                if (nNoSrc > 0){
+                  out.println("      [" + nNoSrc + " insn w/o sources]");
+                }
+
+                out.print("  ");
+                if (showLocation) {
+                  out.print(Left.format(s.getLocationString(),30));
+                  out.print(" : ");
+                }
+                out.println(line.trim());
+                nNoSrc = 0;
+
+              }
+            } else { // no source
+              nNoSrc++;
+            }
+            
+            lastLine = line;
+          }
+
+          if (showCode) {
+            Instruction insn = s.getInstruction();
+            if (showMethod){
+              MethodInfo mi = insn.getMethodInfo();
+              if (mi != lastMi) {
+                ClassInfo mci = mi.getClassInfo();
+                out.print("    ");
+                if (mci != null) {
+                  out.print(mci.getName());
+                  out.print(".");
+                }
+                out.println(mi.getUniqueName());
+                lastMi = mi;
+              }
+            }
+            out.print("      ");
+            out.println(insn);
+          }
+        }
+
+        if (showSource && !showCode && (nNoSrc > 0)) {
+          out.println("      [" + nNoSrc + " insn w/o sources]");
+        }
+      }
+    }
+  }
+
+  @Override
+  protected void publishOutput() {
+    Path path = reporter.getPath();
+
+    if (path.size() == 0) {
+      return; // nothing to publish
+    }
+
+    publishTopicStart("output " + reporter.getCurrentErrorId());
+
+    if (path.hasOutput()) {
+      for (Transition t : path) {
+        String s = t.getOutput();
+        if (s != null){
+          out.print(s);
+        }
+      }
+    } else {
+      out.println("no output");
+    }
+  }
+
+  @Override
+  protected void publishSnapshot() {
+    VM vm = reporter.getVM();
+
+    // not so nice - we have to delegate this since it's using a lot of internals, and is also
+    // used in debugging
+    publishTopicStart("snapshot " + reporter.getCurrentErrorId());
+
+    if (vm.getPathLength() > 0) {
+      vm.printLiveThreadStatus(out);
+    } else {
+      out.println("initial program state");
+    }
+  }
+
+  public static final String STATISTICS_TOPIC = "statistics";
+  
+  // this is useful if somebody wants to monitor progress from a specialized ConsolePublisher
+  public synchronized void printStatistics (PrintWriter pw){
+    publishTopicStart( STATISTICS_TOPIC);
+    printStatistics( pw, reporter);
+  }
+  
+  // this can be used outside a publisher, to show the same info
+  public static void printStatistics (PrintWriter pw, Reporter reporter){
+    Statistics stat = reporter.getStatistics();
+    
+    pw.println("elapsed time:       " + formatHMS(reporter.getElapsedTime()));
+    pw.println("states:             new=" + stat.newStates + ",visited=" + stat.visitedStates
+            + ",backtracked=" + stat.backtracked + ",end=" + stat.endStates);
+    pw.println("search:             maxDepth=" + stat.maxDepth + ",constraints=" + stat.constraints);
+    pw.println("choice generators:  thread=" + stat.threadCGs
+            + " (signal=" + stat.signalCGs + ",lock=" + stat.monitorCGs + ",sharedRef=" + stat.sharedAccessCGs
+            + ",threadApi=" + stat.threadApiCGs + ",reschedule=" + stat.breakTransitionCGs
+            + "), data=" + stat.dataCGs);
+    pw.println("heap:               " + "new=" + stat.nNewObjects
+            + ",released=" + stat.nReleasedObjects
+            + ",maxLive=" + stat.maxLiveObjects
+            + ",gcCycles=" + stat.gcCycles);
+    pw.println("instructions:       " + stat.insns);
+    pw.println("max memory:         " + (stat.maxUsed >> 20) + "MB");
+
+    pw.println("loaded code:        classes=" + ClassLoaderInfo.getNumberOfLoadedClasses() + ",methods="
+            + MethodInfo.getNumberOfLoadedMethods());
+  }
+  
+  @Override
+  public void publishStatistics() {
+    printStatistics(out);
+  }
+
+}