From: rtrimana <rtrimana@uci.edu>
Date: Mon, 20 Apr 2020 19:29:48 +0000 (-0700)
Subject: Additional logging feature.
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=cdcc6e222b85a2daa355cf1a1dd29054411910fa

Additional logging feature.
---

diff --git a/main.jpf b/main.jpf
index 4c3f7d9..1fbebbc 100644
--- 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
index 0000000..e69de29
diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 12bd44f..6ba35e7 100644
--- 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();
     }
   }