[PExplicit] Convert run status to enum

p-org · Apr 15, 2024 · 61ef7c3 · 61ef7c3
1 parent d8fbfe3
commit 61ef7c3
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 11 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
@@ -1,6 +1,7 @@
 package pexplicit;
 
 import pexplicit.runtime.PExplicitGlobal;
+import pexplicit.runtime.STATUS;
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.logger.StatWriter;
 import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
@@ -55,7 +56,7 @@ private static void printStats() {
         double searchTime = TimeMonitor.stopInterval();
         scheduler.recordStats();
         if (PExplicitGlobal.getResult().equals("correct for any depth")) {
-            PExplicitGlobal.setStatus("verified");
+            PExplicitGlobal.setStatus(STATUS.VERIFIED);
         }
         StatWriter.log("time-search-seconds", String.format("%.1f", searchTime));
     }
@@ -82,7 +83,7 @@ private static void preprocess() {
     }
 
     private static void postprocess(boolean printStats) {
-        if (!PExplicitGlobal.getStatus().equals("cex")) {
+        if (PExplicitGlobal.getStatus() != STATUS.BUG_FOUND) {
             scheduler.updateResult();
         }
 
@@ -103,15 +104,14 @@ private static void process(boolean resume) throws Exception {
             future = executor.submit(timedCall);
             TimeMonitor.startInterval();
             runWithTimeout((long) PExplicitGlobal.getConfig().getTimeLimit());
-            PExplicitGlobal.setStatus("completed");
         } catch (TimeoutException e) {
-            PExplicitGlobal.setStatus("timeout");
+            PExplicitGlobal.setStatus(STATUS.TIMEOUT);
             throw new Exception("TIMEOUT", e);
         } catch (MemoutException | OutOfMemoryError e) {
-            PExplicitGlobal.setStatus("memout");
+            PExplicitGlobal.setStatus(STATUS.MEMOUT);
             throw new Exception("MEMOUT", e);
         } catch (BugFoundException e) {
-            PExplicitGlobal.setStatus("cex");
+            PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
             PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.schedule.getStepNumber()));
 
             postprocess(true);
@@ -121,15 +121,15 @@ private static void process(boolean resume) throws Exception {
             }
             throw e;
         } catch (InterruptedException e) {
-            PExplicitGlobal.setStatus("interrupted");
+            PExplicitGlobal.setStatus(STATUS.INTERRUPTED);
             throw new Exception("INTERRUPTED", e);
         } catch (RuntimeException e) {
-            PExplicitGlobal.setStatus("error");
+            PExplicitGlobal.setStatus(STATUS.ERROR);
             throw new Exception("ERROR", e);
         } finally {
             future.cancel(true);
             executor.shutdownNow();
-            postprocess(!PExplicitGlobal.getStatus().equals("cex"));
+            postprocess(PExplicitGlobal.getStatus() != STATUS.BUG_FOUND);
         }
     }
 

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java
@@ -38,7 +38,7 @@ public class PExplicitGlobal {
      **/
     @Getter
     @Setter
-    private static String status = "incomplete";
+    private static STATUS status = STATUS.INCOMPLETE;
 
     /**
      * Result of the run

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java
@@ -0,0 +1,12 @@
+package pexplicit.runtime;
+
+public enum STATUS {
+    INCOMPLETE,         // search still ongoing
+    SCHEDULEOUT,        // schedule limit reached
+    TIMEOUT,            // timeout reached
+    MEMOUT,             // memout reached
+    VERIFIED,           // full state space explored and no bug found
+    BUG_FOUND,          // found a bug
+    INTERRUPTED,        // interrupted by user
+    ERROR               // unexpected error encountered
+}
diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -4,6 +4,7 @@
 import lombok.Setter;
 import org.apache.commons.lang3.StringUtils;
 import pexplicit.runtime.PExplicitGlobal;
+import pexplicit.runtime.STATUS;
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.logger.ScratchLogger;
 import pexplicit.runtime.logger.StatWriter;
@@ -112,7 +113,10 @@ protected void runIteration() throws TimeoutException {
                 !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (schedule.getStepNumber() < PExplicitGlobal.getConfig().getMaxStepBound()),
                 "Step bound of " + PExplicitGlobal.getConfig().getMaxStepBound() + " reached.");
         if (PExplicitGlobal.getConfig().getMaxSchedules() > 0) {
-            isDoneIterating = (iteration >= PExplicitGlobal.getConfig().getMaxSchedules());
+            if (iteration >= PExplicitGlobal.getConfig().getMaxSchedules()) {
+                isDoneIterating = true;
+                PExplicitGlobal.setStatus(STATUS.SCHEDULEOUT);
+            }
         }
     }
 
@@ -326,6 +330,7 @@ public void updateResult() {
             } else {
                 result += String.format("partially correct up to step %d with %d choices remaining", maxStepNumber, numUnexplored);
             }
+
         }
         PExplicitGlobal.setResult(result);
     }