Fixing a few bugs in the statistics printout.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducerWithSummary.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index a750c4d9763d2d9653e8c228c064767b1ff0fda3..7c6ed74929744a37854aac0af216df11a08ce072 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -22,6 +22,7 @@ import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.jvm.bytecode.INVOKEINTERFACE;
 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
+import gov.nasa.jpf.report.Publisher;
 import gov.nasa.jpf.search.Search;
 import gov.nasa.jpf.vm.*;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
@@ -44,6 +45,8 @@ import java.util.logging.Logger;
 public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   // Information printout fields for verbose mode
+  private long startTime;
+  private long timeout;
   private boolean verboseMode;
   private boolean stateReductionMode;
   private final PrintWriter out;
@@ -66,7 +69,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
   private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
   private HashSet<FieldInfo> relevantFields;    // Field info objects of relevant fields
-  private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+  private HashMap<Integer, HashSet<Integer>> stateToEventMap;       // Map state ID to events
   // Data structure to analyze field Read/Write accesses and conflicts
   private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
@@ -84,6 +87,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   // Statistics
   private int numOfTransitions;
+  private HashMap<Integer, HashSet<Integer>> stateToUniqueTransMap;
 
   public DPORStateReducerWithSummary(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
@@ -109,7 +113,12 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     relevantFields = new HashSet<>();
     restorableStateMap = new HashMap<>();
     stateToPredInfo = new HashMap<>();
+    stateToUniqueTransMap = new HashMap<>();
     initializeStatesVariables();
+
+    // Timeout input from config is in minutes, so we need to convert into millis
+    timeout = config.getInt("timeout", 0) * 60 * 1000;
+    startTime = System.currentTimeMillis();
   }
 
   @Override
@@ -176,13 +185,28 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   @Override
   public void searchFinished(Search search) {
     if (verboseMode) {
+      int summaryOfUniqueTransitions = summarizeUniqueTransitions();
       out.println("\n==> DEBUG: ----------------------------------- search finished");
-      out.println("\n==> DEBUG: State reduction mode  : " + stateReductionMode);
-      out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+      out.println("\n==> DEBUG: State reduction mode                : " + stateReductionMode);
+      if (choices != null) {
+        out.println("\n==> DEBUG: Number of events                    : " + choices.length);
+      } else {
+        // Without DPOR we don't have choices being assigned with a CG
+        out.println("\n==> DEBUG: Number of events                    : 0");
+      }
+      out.println("\n==> DEBUG: Number of transitions               : " + numOfTransitions);
+      out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 
-      fileWriter.println("==> DEBUG: State reduction mode  : " + stateReductionMode);
-      fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+      fileWriter.println("==> DEBUG: State reduction mode                : " + stateReductionMode);
+      if (choices != null) {
+        fileWriter.println("==> DEBUG: Number of events                    : " + choices.length);
+      } else {
+        // Without DPOR we don't have choices being assigned with a CG
+        fileWriter.println("==> DEBUG: Number of events                    : 0");
+      }
+      fileWriter.println("==> DEBUG: Number of transitions               : " + numOfTransitions);
+      fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
       fileWriter.println();
       fileWriter.close();
     }
@@ -259,7 +283,9 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         if (choiceCounter > 0 && terminateCurrentExecution()) {
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
+          // We only count IntChoiceFromSet CGs
           numOfTransitions++;
+          countUniqueTransitions(vm.getStateId(), icsCG.getNextChoice());
         }
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
@@ -267,12 +293,25 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         choiceCounter++;
       }
     } else {
-      numOfTransitions++;
+      // We only count IntChoiceFromSet CGs
+      if (currentCG instanceof IntChoiceFromSet) {
+        numOfTransitions++;
+      }
     }
   }
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+    // Check the timeout
+    if (timeout > 0) {
+      if (System.currentTimeMillis() - startTime > timeout) {
+        StringBuilder sbTimeOut = new StringBuilder();
+        sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+        Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
+        ti.setNextPC(nextIns);
+      }
+    }
+
     if (stateReductionMode) {
       if (!isEndOfExecution) {
         // Has to be initialized and it is a integer CG
@@ -797,6 +836,34 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     return transition;
   }
 
+  // --- Functions related to statistics counting
+  // Count unique state IDs
+  private void countUniqueTransitions(int stateId, int nextChoiceValue) {
+    HashSet<Integer> events;
+    // Get the set of events
+    if (!stateToUniqueTransMap.containsKey(stateId)) {
+      events = new HashSet<>();
+      stateToUniqueTransMap.put(stateId, events);
+    } else {
+      events = stateToUniqueTransMap.get(stateId);
+    }
+    // Insert the event
+    if (!events.contains(nextChoiceValue)) {
+      events.add(nextChoiceValue);
+    }
+  }
+
+  // Summarize unique state IDs
+  private int summarizeUniqueTransitions() {
+    // Just count the set size of each of entry map and sum them up
+    int numOfUniqueTransitions = 0;
+    for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueTransMap.entrySet()) {
+      numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
+    }
+
+    return numOfUniqueTransitions;
+  }
+
   // --- Functions related to cycle detection and reachability graph
 
   // Detect cycles in the current execution/trace