Additional logging feature.

diff --git a/main.jpf b/main.jpf
index 4c3f7d91fcfd3d698a91b8a223e1c1f467560367..1fbebbcc4c103237e1f11babca9358a179d9527b 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -49,6 +49,7 @@ apps=App1,App2
 # Debug mode for StateReducer
 printout_state_transition=true
 #activate_state_reduction=false
+file_output=moreStatistics
 
 # Timeout in minutes (default is 0 which means no timeout)
 timeout=1440

diff --git a/moreStatistics b/moreStatistics
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 12bd44ff802e2547e86e1e22856f32ff6e31c6bf..6ba35e75d759fd305f72527ab82d1750932bf62e 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -28,8 +28,11 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
+import java.io.FileWriter;
 import java.io.PrintWriter;
 import java.util.*;
+import java.util.logging.Logger;
+import java.io.IOException;
 
 // TODO: Fix for Groovy's model-checking
 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
@@ -53,6 +56,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean verboseMode;
   private boolean stateReductionMode;
   private final PrintWriter out;
+  private PrintWriter fileWriter;
   private String detail;
   private int depth;
   private int id;
@@ -95,6 +99,13 @@ public class DPORStateReducer extends ListenerAdapter {
     } else {
       out = null;
     }
+    String outputFile = config.getString("file_output");
+    if (!outputFile.isEmpty()) {
+      try {
+        fileWriter = new PrintWriter(new FileWriter(outputFile, true), true);
+      } catch (IOException e) {
+      }
+    }
     isBooleanCGFlipped = false;
                numOfConflicts = 0;
                numOfTransitions = 0;
@@ -161,6 +172,8 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  static Logger log = JPF.getLogger("report");
+
   @Override
   public void searchFinished(Search search) {
     if (stateReductionMode) {
@@ -173,6 +186,12 @@ public class DPORStateReducer extends ListenerAdapter {
       out.println("\n==> DEBUG: Number of conflicts   : " + numOfConflicts);
       out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
+
+      fileWriter.println("==> DEBUG: State reduction mode  : " + stateReductionMode);
+      fileWriter.println("==> DEBUG: Number of conflicts   : " + numOfConflicts);
+      fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+      fileWriter.println();
+      fileWriter.close();
     }
   }