[PEx] Add support to serialize and deserialize search tasks in/from file

Author: aman-goel

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/ForeignFunctionInterface.java

@@ -5,24 +5,24 @@
 import java.util.function.Function;
 
 public class ForeignFunctionInterface {
-  /**
-   * Invoke a foreign function with a void return type
-   *
-   * @param fn function to invoke
-   * @param args arguments
-   */
-  public static void accept(Consumer<List<Object>> fn, Object... args) {
-    fn.accept(List.of(args));
-  }
+    /**
+     * Invoke a foreign function with a void return type
+     *
+     * @param fn   function to invoke
+     * @param args arguments
+     */
+    public static void accept(Consumer<List<Object>> fn, Object... args) {
+        fn.accept(List.of(args));
+    }
 
-  /**
-   * Invoke a foreign function with a non-void return type
-   *
-   * @param fn function to invoke
-   * @param args arguments
-   * @return the return value of the function
-   */
-  public static Object apply(Function<List<Object>, Object> fn, Object... args) {
-    return fn.apply(List.of(args));
-  }
+    /**
+     * Invoke a foreign function with a non-void return type
+     *
+     * @param fn   function to invoke
+     * @param args arguments
+     * @return the return value of the function
+     */
+    public static Object apply(Function<List<Object>, Object> fn, Object... args) {
+        return fn.apply(List.of(args));
+    }
 }

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java

@@ -13,8 +13,6 @@
 import pexplicit.runtime.machine.PMonitor;
 import pexplicit.runtime.machine.State;
 import pexplicit.runtime.machine.events.PContinuation;
-import pexplicit.runtime.scheduler.choice.Choice;
-import pexplicit.runtime.scheduler.choice.ScheduleChoice;
 import pexplicit.runtime.scheduler.choice.ScheduleSearchUnit;
 import pexplicit.runtime.scheduler.choice.SearchUnit;
 import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
@@ -155,7 +153,7 @@ public static void logEndTask(SearchTask task, int numSchedules) {
      * @param task Next search task
      */
     public static void logNextTask(SearchTask task) {
-        if (verbosity > 1) {
+        if (verbosity > 0) {
             log.info(String.format("  Next task: %s", task.toStringDetailed()));
         }
     }
@@ -171,6 +169,29 @@ public static void logNewTasks(List<SearchTask> tasks) {
         }
     }
 
+    /**
+     * Log when serializing a task
+     *
+     * @param task    Task to serialize
+     * @param szBytes Bytes written
+     */
+    public static void logSerializeTask(SearchTask task, long szBytes) {
+        if (verbosity > 1) {
+            log.info(String.format("      %,.1f MB  written in %s", (szBytes / 1024.0 / 1024.0), task.getSerializeFile()));
+        }
+    }
+
+    /**
+     * Log when deserializing a task
+     *
+     * @param task Task that is deserialized
+     */
+    public static void logDeserializeTask(SearchTask task) {
+        if (verbosity > 1) {
+            log.info(String.format("      Reading %s from %s", task, task.getSerializeFile()));
+        }
+    }
+
     /**
      * Log at the start of an iteration
      *
@@ -209,9 +230,9 @@ public static void logFinishedIteration(int step) {
     /**
      * Log when backtracking to a search unit
      *
-     * @param stepNum Step number
+     * @param stepNum   Step number
      * @param choiceNum Choice number
-     * @param unit Search unit to which backtracking to
+     * @param unit      Search unit to which backtracking to
      */
     public static void logBacktrack(int stepNum, int choiceNum, SearchUnit unit) {
         if (verbosity > 1) {

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachineId.java

@@ -3,8 +3,10 @@
 import lombok.Getter;
 import lombok.Setter;
 
+import java.io.Serializable;
+
 @Getter
-public class PMachineId {
+public class PMachineId implements Serializable {
     Class<? extends PMachine> type;
     int typeId;
     @Setter

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/buffer/MessageQueue.java

@@ -3,7 +3,6 @@
 import lombok.Getter;
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.utils.exceptions.PExplicitRuntimeException;
-import pexplicit.utils.misc.Assert;
 import pexplicit.values.PMessage;
 
 import java.io.Serializable;

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java

@@ -63,9 +63,9 @@ public void removeChoicesAfter(int choiceNum) {
     /**
      * Set the schedule choice at a choice depth.
      *
-     * @param stepNum    Step number
-     * @param choiceNum  Choice number
-     * @param current    Machine to set as current schedule choice
+     * @param stepNum   Step number
+     * @param choiceNum Choice number
+     * @param current   Machine to set as current schedule choice
      */
     public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) {
         if (choiceNum == choices.size()) {
@@ -84,9 +84,9 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) {
     /**
      * Set the data choice at a choice depth.
      *
-     * @param stepNum    Step number
-     * @param choiceNum  Choice number
-     * @param current    PValue to set as current schedule choice
+     * @param stepNum   Step number
+     * @param choiceNum Choice number
+     * @param current   PValue to set as current schedule choice
      */
     public void setDataChoice(int stepNum, int choiceNum, PValue<?> current) {
         if (choiceNum == choices.size()) {

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/SchedulerInterface.java

@@ -2,6 +2,7 @@
 
 import pexplicit.values.*;
 
+import java.io.IOException;
 import java.io.Serializable;
 import java.util.concurrent.TimeoutException;
 
@@ -13,7 +14,7 @@ public interface SchedulerInterface extends Serializable {
     /**
      * Perform the search
      */
-    void run() throws TimeoutException, InterruptedException;
+    void run() throws TimeoutException, InterruptedException, IOException;
 
     /**
      * Return a random PBool based on the search and strategy.

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataSearchUnit.java

@@ -5,7 +5,7 @@
 import java.util.ArrayList;
 import java.util.List;
 
-public class DataSearchUnit extends SearchUnit<PValue<?>>{
+public class DataSearchUnit extends SearchUnit<PValue<?>> {
     /**
      * Constructor
      */

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java

@@ -2,7 +2,6 @@
 
 import lombok.Getter;
 import lombok.Setter;
-import pexplicit.commandline.PExplicitConfig;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.explicit.StepState;
 

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleSearchUnit.java

@@ -1,7 +1,6 @@
 package pexplicit.runtime.scheduler.choice;
 
 import pexplicit.runtime.machine.PMachineId;
-import pexplicit.runtime.scheduler.explicit.StepState;
 
 import java.util.ArrayList;
 import java.util.List;

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java

@@ -12,7 +12,6 @@
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.Scheduler;
-import pexplicit.runtime.scheduler.choice.Choice;
 import pexplicit.runtime.scheduler.choice.ScheduleChoice;
 import pexplicit.runtime.scheduler.choice.SearchUnit;
 import pexplicit.runtime.scheduler.explicit.strategy.*;
@@ -112,9 +111,9 @@ public void run() throws TimeoutException {
                 runIteration();
                 postProcessIteration();
             }
+            PExplicitLogger.logEndTask(searchStrategy.getCurrTask(), searchStrategy.getNumSchedulesInCurrTask());
             addRemainingChoicesAsChildrenTasks();
             endCurrTask();
-            PExplicitLogger.logEndTask(searchStrategy.getCurrTask(), searchStrategy.getNumSchedulesInCurrTask());
 
             if (searchStrategy.getPendingTasks().isEmpty() || PExplicitGlobal.getStatus() == STATUS.SCHEDULEOUT) {
                 // all tasks completed or schedule limit reached
@@ -431,7 +430,7 @@ private void postProcessIteration() {
     private void addRemainingChoicesAsChildrenTasks() {
         SearchTask parentTask = searchStrategy.getCurrTask();
         int numChildrenAdded = 0;
-        for (int i: parentTask.getSearchUnitKeys(false)) {
+        for (int i : parentTask.getSearchUnitKeys(false)) {
             SearchUnit unit = parentTask.getSearchUnit(i);
             // if search unit at this depth is non-empty
             if (!unit.getUnexplored().isEmpty()) {
@@ -462,7 +461,7 @@ private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask,
         newTask.addSuffixSearchUnit(choiceNum, unit);
 
         if (!isExact) {
-            for (int i: parentTask.getSearchUnitKeys(false)) {
+            for (int i : parentTask.getSearchUnitKeys(false)) {
                 if (i > choiceNum) {
                     if (i > maxChoiceNum) {
                         maxChoiceNum = i;
@@ -476,6 +475,7 @@ private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask,
             newTask.addPrefixChoice(schedule.getChoice(i));
         }
 
+        newTask.serializeTask();
         parentTask.addChild(newTask);
         searchStrategy.addNewTask(newTask);
     }
@@ -494,11 +494,11 @@ public SearchTask setNextTask() {
     }
 
     public int getNumUnexploredChoices() {
-        return searchStrategy.getCurrTask().getNumUnexploredChoices() + searchStrategy.getNumPendingChoices();
+        return searchStrategy.getCurrTask().getCurrentNumUnexploredChoices() + searchStrategy.getNumPendingChoices();
     }
 
     public int getNumUnexploredDataChoices() {
-        return searchStrategy.getCurrTask().getNumUnexploredDataChoices() + searchStrategy.getNumPendingDataChoices();
+        return searchStrategy.getCurrTask().getCurrentNumUnexploredDataChoices() + searchStrategy.getNumPendingDataChoices();
     }
 
     /**
@@ -518,7 +518,7 @@ public double getUnexploredDataChoicesPercent() {
 
     private void postIterationCleanup() {
         SearchTask task = searchStrategy.getCurrTask();
-        for (int cIdx: task.getSearchUnitKeys(true)) {
+        for (int cIdx : task.getSearchUnitKeys(true)) {
             SearchUnit unit = task.getSearchUnit(cIdx);
             if (unit.getUnexplored().isEmpty()) {
                 task.clearSearchUnit(cIdx);