Fixing a few bugs in the statistics printout.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 64025773718083adcdc6917b3469a6c134cb7a70..7c6ed74929744a37854aac0af216df11a08ce072 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -45,6 +45,8 @@ import java.util.logging.Logger;
 public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   // Information printout fields for verbose mode
 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;
   private boolean verboseMode;
   private boolean stateReductionMode;
   private final PrintWriter out;


@@ -113,6 +115,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     stateToPredInfo = new HashMap<>();
     stateToUniqueTransMap = new HashMap<>();
     initializeStatesVariables();
     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
   }
 
   @Override


@@ -182,11 +188,23 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       int summaryOfUniqueTransitions = summarizeUniqueTransitions();
       out.println("\n==> DEBUG: ----------------------------------- search finished");
       out.println("\n==> DEBUG: State reduction mode                : " + stateReductionMode);
       int summaryOfUniqueTransitions = summarizeUniqueTransitions();
       out.println("\n==> DEBUG: ----------------------------------- search finished");
       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);
       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);

+      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.println("==> DEBUG: Number of transitions               : " + numOfTransitions);
       fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
       fileWriter.println();


@@ -284,6 +302,16 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 
   @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
     if (stateReductionMode) {
       if (!isEndOfExecution) {
         // Has to be initialized and it is a integer CG