diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java index ce28c7f38..ca5e6663d 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java +++ b/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; diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java index 3aa4da04f..8d9a6d8b6 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java +++ b/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 { 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 index 3591e725f..bba0ec8b2 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java +++ b/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; @@ -71,7 +72,7 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current) { 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)); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/Choice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/Choice.java index 00fd47431..7fd891e67 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/Choice.java +++ b/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(); } \ No newline at end of file diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataChoice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataChoice.java index 4f2dbe754..47ed48285 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/DataChoice.java +++ b/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); } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java index 8ad0a0147..4231cf487 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/choice/ScheduleChoice.java @@ -2,6 +2,7 @@ import lombok.Getter; import lombok.Setter; +import pexplicit.commandline.PExplicitConfig; import pexplicit.runtime.machine.PMachineId; import pexplicit.runtime.scheduler.explicit.StepState; @@ -32,8 +33,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 diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java index c233ca8d8..26d09b629 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -193,7 +193,7 @@ protected void runStep() throws TimeoutException { return; } - if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled() + if (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() != StatefulBacktrackingMode.None && stepNumber != 0) { schedule.setStepBeginState(stepState.copyState()); } @@ -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(); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StatefulBacktrackingMode.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StatefulBacktrackingMode.java new file mode 100644 index 000000000..b304696a4 --- /dev/null +++ b/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 +} diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java index 597b116bc..a27e6c7b0 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java @@ -1,8 +1,10 @@ package pexplicit.runtime.scheduler.explicit.strategy; import lombok.Getter; +import pexplicit.runtime.PExplicitGlobal; import pexplicit.runtime.machine.PMachineId; import pexplicit.runtime.scheduler.choice.*; +import pexplicit.runtime.scheduler.explicit.StatefulBacktrackingMode; import pexplicit.values.PValue; import java.io.Serializable; @@ -41,7 +43,8 @@ public void cleanup() { } public void addPrefixChoice(Choice choice) { - prefixChoices.add(choice.copyCurrent()); + boolean copyState = (PExplicitGlobal.getConfig().getStatefulBacktrackingMode() == StatefulBacktrackingMode.All); + prefixChoices.add(choice.copyCurrent(copyState)); } public void addSuffixSearchUnit(int choiceNum, SearchUnit unit) {