[PEx] Adds hybrid stateful backtracking, improves storing search tasks

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java

@@ -4,6 +4,7 @@
 import lombok.Setter;
 import pexplicit.runtime.machine.buffer.BufferSemantics;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 /**
@@ -52,9 +53,9 @@ public class PExplicitConfig {
     // state caching mode
     @Setter
     StateCachingMode stateCachingMode = StateCachingMode.Murmur3_128;
-    // use stateful backtracking
+    // stateful backtracking mode
     @Setter
-    boolean statefulBacktrackEnabled = true;
+    StatefulBacktrackingMode statefulBacktrackingMode = StatefulBacktrackingMode.IntraTask;
     // search strategy mode
     @Setter
     SearchStrategyMode searchStrategyMode = SearchStrategyMode.Random;

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java

@@ -2,6 +2,7 @@
 
 import org.apache.commons.cli.*;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
 import java.io.PrintWriter;
@@ -165,13 +166,15 @@ public class PExplicitOptions {
         addHiddenOption(stateCachingMode);
 
         // whether or not to disable stateful backtracking
-        Option backtrack =
+        Option backtrackMode =
                 Option.builder()
-                        .longOpt("no-backtrack")
-                        .desc("Disable stateful backtracking")
-                        .numberOfArgs(0)
+                        .longOpt("stateful-backtrack")
+                        .desc("Stateful backtracking mode: none, intra-task, all (default: intra-task)")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("Backtrack Mode (string)")
                         .build();
-        addHiddenOption(backtrack);
+        addHiddenOption(backtrackMode);
 
         // max number of schedules to explore per search task
         Option maxSchedulesPerTask =
@@ -363,8 +366,22 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) {
                                     String.format("Unrecognized state caching mode, got %s", option.getValue()));
                     }
                     break;
-                case "no-backtrack":
-                    config.setStatefulBacktrackEnabled(false);
+                case "stateful-backtrack":
+                    switch (option.getValue()) {
+                        case "none":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.None);
+                            break;
+                        case "intra-task":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.IntraTask);
+                            break;
+                        case "all":
+                            config.setStatefulBacktrackingMode(StatefulBacktrackingMode.All);
+                            break;
+                        default:
+                            optionError(
+                                    option,
+                                    String.format("Unrecognized stateful backtrack mode, got %s", option.getValue()));
+                    }
                     break;
                 case "schedules-per-task":
                     try {

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

@@ -7,6 +7,7 @@
 import pexplicit.runtime.scheduler.choice.Choice;
 import pexplicit.runtime.scheduler.choice.DataChoice;
 import pexplicit.runtime.scheduler.choice.ScheduleChoice;
+import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode;
 import pexplicit.runtime.scheduler.explicit.StepState;
 import pexplicit.values.PValue;
 
@@ -62,16 +63,16 @@ 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()) {
             choices.add(null);
         }
         assert (choiceNum < choices.size());
-        if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
+        if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None
                 && stepNum != 0) {
             assert (stepBeginState != null);
             choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, stepBeginState));
@@ -83,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;
 

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

@@ -29,7 +29,7 @@ public void clearCurrent() {
      *
      * @return Choice object with the copied current choice
      */
-    abstract public Choice copyCurrent();
+    abstract public Choice copyCurrent(boolean copyState);
 
     abstract public String toString();
 }

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

@@ -14,7 +14,7 @@ public DataChoice(PValue<?> c) {
         super(c);
     }
 
-    public Choice copyCurrent() {
+    public Choice copyCurrent(boolean copyState) {
         return new DataChoice(this.current);
     }
 

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

@@ -32,8 +32,12 @@ public ScheduleChoice(int stepNum, int choiceNum, PMachineId c, StepState s) {
         this.choiceState = s;
     }
 
-    public Choice copyCurrent() {
-        return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, this.choiceState);
+    public Choice copyCurrent(boolean copyState) {
+        if (copyState) {
+            return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, this.choiceState);
+        } else {
+            return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, null);
+        }
     }
 
     @Override

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
@@ -193,7 +192,7 @@ protected void runStep() throws TimeoutException {
             return;
         }
 
-        if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
+        if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None
                 && stepNumber != 0) {
             schedule.setStepBeginState(stepState.copyState());
         }
@@ -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);
@@ -528,7 +528,7 @@ private void postIterationCleanup() {
             backtrackChoiceNumber = cIdx;
             int newStepNumber = 0;
             ScheduleChoice scheduleChoice = null;
-            if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()) {
+            if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None) {
                 scheduleChoice = schedule.getScheduleChoiceAt(cIdx);
                 if (scheduleChoice != null && scheduleChoice.getChoiceState() != null) {
                     newStepNumber = scheduleChoice.getStepNumber();

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

@@ -0,0 +1,7 @@
+package pexplicit.runtime.scheduler.explicit;
+
+public enum StatefulBacktrackingMode {
+    None,
+    IntraTask,
+    All
+}