[PEx] Revamps tracking unexplored choices, changes schedule choice (#745

)

* [PEx] Change schedule choice from PMachine to PMachineId

* [PEx] Major revamping of Choice: 1/n

Old schedule/data choice changed to schedule/data SearchUnit

Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?>

TODO: clean up Schedule with new class structure

* Revert "[PEx] Major revamping of Choice: 1/n"

This reverts commit 53c5d15.

* [PEx] Separates unexplored choices from schedule

* [PEx] Cleanup and minor corrections to recent changes to SearchTask

* [PEx] Minor correction

* [PEx] Corrections to new backtracking logic

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

@@ -4,6 +4,7 @@
 import lombok.Setter;
 import pexplicit.commandline.PExplicitConfig;
 import pexplicit.runtime.machine.PMachine;
+import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.Scheduler;
 import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode;
 
@@ -60,19 +61,18 @@ public class PExplicitGlobal {
     /**
      * Get a machine of a given type and index if exists, else return null.
      *
-     * @param type Machine type
-     * @param idx  Machine index
+     * @param pid Machine pid
      * @return Machine
      */
-    public static PMachine getGlobalMachine(Class<? extends PMachine> type, int idx) {
-        List<PMachine> machinesOfType = machineListByType.get(type);
+    public static PMachine getGlobalMachine(PMachineId pid) {
+        List<PMachine> machinesOfType = machineListByType.get(pid.getType());
         if (machinesOfType == null) {
             return null;
         }
-        if (idx >= machinesOfType.size()) {
+        if (pid.getTypeId() >= machinesOfType.size()) {
             return null;
         }
-        PMachine result = machineListByType.get(type).get(idx);
+        PMachine result = machineListByType.get(pid.getType()).get(pid.getTypeId());
         assert (machineSet.contains(result));
         return result;
     }

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

@@ -9,11 +9,14 @@
 import pexplicit.runtime.PExplicitGlobal;
 import pexplicit.runtime.STATUS;
 import pexplicit.runtime.machine.PMachine;
+import pexplicit.runtime.machine.PMachineId;
 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;
 import pexplicit.runtime.scheduler.explicit.SearchStatistics;
 import pexplicit.runtime.scheduler.explicit.StateCachingMode;
@@ -204,20 +207,21 @@ public static void logFinishedIteration(int step) {
     }
 
     /**
-     * Log when backtracking to a new choice
+     * Log when backtracking to a search unit
      *
-     * @param choice Choice to which backtracking to
+     * @param stepNum Step number
+     * @param choiceNum Choice number
+     * @param unit Search unit to which backtracking to
      */
-    public static void logBacktrack(Choice choice) {
+    public static void logBacktrack(int stepNum, int choiceNum, SearchUnit unit) {
         if (verbosity > 1) {
             log.info(String.format("  Backtracking to %s choice @%d::%d",
-                    ((choice instanceof ScheduleChoice) ? "schedule" : "data"),
-                    choice.getStepNumber(),
-                    choice.getChoiceNumber()));
+                    ((unit instanceof ScheduleSearchUnit) ? "schedule" : "data"),
+                    stepNum, choiceNum));
         }
     }
 
-    public static void logNewScheduleChoice(List<PMachine> choices, int step, int idx) {
+    public static void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
         if (verbosity > 1) {
             log.info(String.format("    @%d::%d new schedule choice: %s", step, idx, choices));
         }

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

@@ -28,7 +28,7 @@ public abstract class PMachine implements Serializable, Comparable<PMachine> {
     private static final Map<String, PMachine> nameToMachine = new HashMap<>();
     protected static int globalMachineId = 1;
     @Getter
-    protected final int typeId;
+    protected final PMachineId pid;
     @Getter
     protected final String name;
     private final Set<State> states;
@@ -72,7 +72,8 @@ public PMachine(String name, int id, State startState, State... states) {
         // initialize name, ids
         this.name = name;
         this.instanceId = ++globalMachineId;
-        this.typeId = id;
+        this.pid = new PMachineId(this.getClass(), id);
+        this.pid.setName(this.toString());
         nameToMachine.put(toString(), this);
 
         // initialize states

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

@@ -0,0 +1,36 @@
+package pexplicit.runtime.machine;
+
+import lombok.Getter;
+import lombok.Setter;
+
+@Getter
+public class PMachineId {
+    Class<? extends PMachine> type;
+    int typeId;
+    @Setter
+    String name;
+
+    public PMachineId(Class<? extends PMachine> t, int tid) {
+        type = t;
+        typeId = tid;
+        name = null;
+    }
+
+
+    @Override
+    public String toString() {
+        return name;
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (obj == this)
+            return true;
+        else if (!(obj instanceof PMachineId)) {
+            return false;
+        }
+        PMachineId rhs = (PMachineId) obj;
+        return this.type == rhs.type && this.typeId == rhs.typeId;
+    }
+
+}

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

@@ -3,7 +3,7 @@
 import lombok.Getter;
 import lombok.Setter;
 import pexplicit.runtime.PExplicitGlobal;
-import pexplicit.runtime.machine.PMachine;
+import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.choice.Choice;
 import pexplicit.runtime.scheduler.choice.DataChoice;
 import pexplicit.runtime.scheduler.choice.ScheduleChoice;
@@ -48,51 +48,15 @@ public Choice getChoice(int idx) {
         return choices.get(idx);
     }
 
-    /**
-     * Clear choice at a choice depth
-     *
-     * @param idx Choice depth
-     */
-    public void clearChoice(int idx) {
-        choices.get(idx).clearCurrent();
-        choices.get(idx).clearUnexplored();
-    }
-
     /**
      * Remove choices after a choice depth
      *
      * @param choiceNum Choice depth
      */
     public void removeChoicesAfter(int choiceNum) {
-        choices.subList(choiceNum + 1, choices.size()).clear();
-    }
-
-    /**
-     * Get the number of unexplored choices in this schedule
-     *
-     * @return Number of unexplored choices
-     */
-    public int getNumUnexploredChoices() {
-        int numUnexplored = 0;
-        for (Choice<?> c : choices) {
-            numUnexplored += c.getUnexplored().size();
+        if ((choiceNum + 1) < choices.size()) {
+            choices.subList(choiceNum + 1, choices.size()).clear();
         }
-        return numUnexplored;
-    }
-
-    /**
-     * Get the number of unexplored data choices in this schedule
-     *
-     * @return Number of unexplored data choices
-     */
-    public int getNumUnexploredDataChoices() {
-        int numUnexplored = 0;
-        for (Choice<?> c : choices) {
-            if (c instanceof DataChoice) {
-                numUnexplored += c.getUnexplored().size();
-            }
-        }
-        return numUnexplored;
     }
 
     /**
@@ -101,19 +65,18 @@ public int getNumUnexploredDataChoices() {
      * @param stepNum    Step number
      * @param choiceNum  Choice number
      * @param current    Machine to set as current schedule choice
-     * @param unexplored List of machine to set as unexplored schedule choices
      */
-    public void setScheduleChoice(int stepNum, int choiceNum, PMachine current, List<PMachine> unexplored) {
+    public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) {
         if (choiceNum == choices.size()) {
             choices.add(null);
         }
         assert (choiceNum < choices.size());
         if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
                 && stepNum != 0) {
             assert (stepBeginState != null);
-            choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, stepBeginState));
+            choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, stepBeginState));
         } else {
-            choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, null));
+            choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, null));
         }
     }
 
@@ -123,14 +86,13 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachine current, List
      * @param stepNum    Step number
      * @param choiceNum  Choice number
      * @param current    PValue to set as current schedule choice
-     * @param unexplored List of PValue to set as unexplored schedule choices
      */
-    public void setDataChoice(int stepNum, int choiceNum, PValue<?> current, List<PValue<?>> unexplored) {
+    public void setDataChoice(int stepNum, int choiceNum, PValue<?> current) {
         if (choiceNum == choices.size()) {
             choices.add(null);
         }
         assert (choiceNum < choices.size());
-        choices.set(choiceNum, new DataChoice(stepNum, choiceNum, current, unexplored));
+        choices.set(choiceNum, new DataChoice(current));
     }
 
     /**
@@ -139,7 +101,7 @@ public void setDataChoice(int stepNum, int choiceNum, PValue<?> current, List<PV
      * @param idx Choice depth
      * @return Current schedule choice
      */
-    public PMachine getCurrentScheduleChoice(int idx) {
+    public PMachineId getCurrentScheduleChoice(int idx) {
         assert (choices.get(idx) instanceof ScheduleChoice);
         return ((ScheduleChoice) choices.get(idx)).getCurrent();
     }
@@ -155,57 +117,24 @@ public PValue<?> getCurrentDataChoice(int idx) {
         return ((DataChoice) choices.get(idx)).getCurrent();
     }
 
-    /**
-     * Get unexplored schedule choices at a choice depth.
-     *
-     * @param idx Choice depth
-     * @return List of machines, or null if index is invalid
-     */
-    public List<PMachine> getUnexploredScheduleChoices(int idx) {
-        if (idx < size()) {
-            assert (choices.get(idx) instanceof ScheduleChoice);
-            return ((ScheduleChoice) choices.get(idx)).getUnexplored();
-        } else {
-            return new ArrayList<>();
-        }
-    }
-
-    /**
-     * Get unexplored data choices at a choice depth.
-     *
-     * @param idx Choice depth
-     * @return List of PValue, or null if index is invalid
-     */
-    public List<PValue<?>> getUnexploredDataChoices(int idx) {
-        if (idx < size()) {
-            assert (choices.get(idx) instanceof DataChoice);
-            return ((DataChoice) choices.get(idx)).getUnexplored();
-        } else {
-            return new ArrayList<>();
-        }
-    }
-
-    public ScheduleChoice getScheduleChoiceAt(Choice choice) {
-        if (choice instanceof ScheduleChoice scheduleChoice) {
-            return scheduleChoice;
-        } else {
-            for (int i = choice.getChoiceNumber() - 1; i >= 0; i--) {
-                Choice c = choices.get(i);
-                if (c instanceof ScheduleChoice scheduleChoice) {
-                    return scheduleChoice;
-                }
+    public ScheduleChoice getScheduleChoiceAt(int choiceNum) {
+        for (int i = choiceNum; i >= 0; i--) {
+            if (choiceNum >= choices.size()) {
+                continue;
+            }
+            Choice c = choices.get(i);
+            if (c instanceof ScheduleChoice scheduleChoice) {
+                return scheduleChoice;
             }
         }
         return null;
     }
 
     /**
-     * Clear current choices at a choice depth
-     *
-     * @param idx Choice depth
+     * Clear current choices
      */
-    public void clearCurrent(int idx) {
-        choices.get(idx).clearCurrent();
+    public void clear() {
+        choices.clear();
     }
 
     /**

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

@@ -5,6 +5,7 @@
 import pexplicit.runtime.PExplicitGlobal;
 import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.machine.PMachine;
+import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.machine.PMonitor;
 import pexplicit.runtime.scheduler.explicit.StepState;
 import pexplicit.utils.exceptions.BugFoundException;
@@ -271,8 +272,8 @@ public PMachine allocateMachine(
             Function<Integer, ? extends PMachine> constructor) {
         // get machine count for given type from schedule
         int machineCount = stepState.getMachineCount(machineType);
-
-        PMachine machine = PExplicitGlobal.getGlobalMachine(machineType, machineCount);
+        PMachineId pid = new PMachineId(machineType, machineCount);
+        PMachine machine = PExplicitGlobal.getGlobalMachine(pid);
         if (machine == null) {
             // create a new machine
             machine = constructor.apply(machineCount);