[PExplicit] Correct stateful backtracking with complex data choices

p-org · May 6, 2024 · 994be9f · 994be9f
1 parent 3069833
commit 994be9f
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java
@@ -109,8 +109,8 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachine current, List
         }
         assert (choiceNum < choices.size());
         if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
-                && stepBeginState != null
                 && stepNum != 0) {
+            assert (stepBeginState != null);
             choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, stepBeginState));
         } else {
             choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, null));

diff --git a/...mes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java b/...mes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java
@@ -26,17 +26,15 @@ public ScheduleChoice(int stepNum, int choiceNum, PMachine c, List<PMachine> u,
      */
     public void clearUnexplored() {
         unexplored.clear();
-        choiceState = null;
     }
 
     public Choice copyCurrent() {
-        return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, new ArrayList<>(), null);
+        return new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, new ArrayList<>(), this.choiceState);
     }
 
     public Choice transferChoice() {
         ScheduleChoice newChoice = new ScheduleChoice(this.stepNumber, this.choiceNumber, this.current, this.unexplored, this.choiceState);
         this.unexplored = new ArrayList<>();
-        this.choiceState = null;
         return newChoice;
     }
 

diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -506,6 +506,8 @@ private void postIterationCleanup() {
                     if (scheduleChoice != null && scheduleChoice.getChoiceState() != null) {
                         assert ((scheduleChoice == choice) || (scheduleChoice.getStepNumber() == (choice.getStepNumber() - 1)));
                         newStepNumber = scheduleChoice.getStepNumber();
+                    } else {
+                        assert (choice.getStepNumber() == 0);
                     }
                 }
                 if (newStepNumber == 0) {

diff --git a/...ntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java b/...ntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java
@@ -59,9 +59,9 @@ public void resetToZero() {
     }
 
     public void setTo(StepState input) {
-        machineListByType = input.machineListByType;
-        machineSet = input.machineSet;
-        machineLocalStates = input.machineLocalStates;
+        machineListByType = new HashMap<>(input.machineListByType);
+        machineSet = new TreeSet<>(input.machineSet);
+        machineLocalStates = new HashMap<>(input.machineLocalStates);
         assert (machineSet.size() == machineLocalStates.size());
 
         for (PMachine machine : PExplicitGlobal.getMachineSet()) {