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 e00663866..69138d97b 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitOptions.java @@ -297,7 +297,7 @@ public static PExplicitConfig ParseCommandlineArgs(String[] args) { config.setSearchStrategyMode(SearchStrategyMode.Random); break; case "astar": - config.setSearchStrategyMode (SearchStrategyMode.AStar); + config.setSearchStrategyMode(SearchStrategyMode.AStar); break; default: optionError( diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java index 0f26b770b..f30f2c005 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java @@ -5,7 +5,6 @@ import pexplicit.commandline.PExplicitConfig; import pexplicit.runtime.machine.PMachine; import pexplicit.runtime.scheduler.Scheduler; -import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategy; import pexplicit.runtime.scheduler.explicit.strategy.SearchStrategyMode; import java.util.*; 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 30fceee09..7fdc3e4c9 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 @@ -446,7 +446,9 @@ private void setChildTask(Choice choice, int choiceNum, SearchTask parentTask, b searchStrategy.addNewTask(newTask); } - /** Set next backtrack task with given orchestration mode */ + /** + * Set next backtrack task with given orchestration mode + */ public SearchTask setNextTask() { SearchTask nextTask = searchStrategy.setNextTask(); if (nextTask != null) { diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategy.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategy.java index 4c81d06a8..0f73960c9 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategy.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategy.java @@ -1,8 +1,6 @@ package pexplicit.runtime.scheduler.explicit.strategy; import lombok.Getter; -import pexplicit.runtime.PExplicitGlobal; -import pexplicit.runtime.logger.PExplicitLogger; import pexplicit.runtime.scheduler.Choice; import pexplicit.runtime.scheduler.explicit.SearchStatistics; @@ -42,13 +40,6 @@ public SearchTask createTask(Choice choice, int choiceNum, SearchTask parentTask return newTask; } - private void setCurrTask(SearchTask task) { - assert (pendingTasks.contains(task.getId())); - pendingTasks.remove(task.getId()); - currTaskId = task.getId(); - currTaskStartIteration = SearchStatistics.iteration; - } - public void createFirstTask() { assert (allTasks.size() == 0); SearchTask firstTask = createTask(null, 0, null); @@ -59,13 +50,18 @@ public SearchTask getCurrTask() { return getTask(currTaskId); } + private void setCurrTask(SearchTask task) { + assert (pendingTasks.contains(task.getId())); + pendingTasks.remove(task.getId()); + currTaskId = task.getId(); + currTaskStartIteration = SearchStatistics.iteration; + } public int getNumSchedulesInCurrTask() { return SearchStatistics.iteration - currTaskStartIteration; } - private boolean isValidTaskId(int id) { return (id < allTasks.size()); } @@ -93,7 +89,7 @@ public SearchTask setNextTask() { */ public int getNumPendingChoices() { int numUnexplored = 0; - for (Integer tid: pendingTasks) { + for (Integer tid : pendingTasks) { SearchTask task = getTask(tid); numUnexplored += task.getNumUnexploredScheduleChoices() + task.getNumUnexploredDataChoices(); } @@ -107,7 +103,7 @@ public int getNumPendingChoices() { */ public int getNumPendingDataChoices() { int numUnexplored = 0; - for (Integer tid: pendingTasks) { + for (Integer tid : pendingTasks) { SearchTask task = getTask(tid); numUnexplored += task.getNumUnexploredDataChoices(); } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java index bade55115..53126b7a5 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyAStar.java @@ -4,25 +4,25 @@ import java.util.concurrent.PriorityBlockingQueue; public class SearchStrategyAStar extends SearchStrategy { - private final PriorityBlockingQueue elements; + private final PriorityBlockingQueue elements; - public SearchStrategyAStar() { - elements = - new PriorityBlockingQueue( - 100, - new Comparator() { - public int compare(SearchTask a, SearchTask b) { - return Integer.compare(a.getCurrChoiceNumber(), b.getCurrChoiceNumber()); - } - }); - } + public SearchStrategyAStar() { + elements = + new PriorityBlockingQueue( + 100, + new Comparator() { + public int compare(SearchTask a, SearchTask b) { + return Integer.compare(a.getCurrChoiceNumber(), b.getCurrChoiceNumber()); + } + }); + } - public void addNewTask(SearchTask task) { - elements.offer(task); - } + public void addNewTask(SearchTask task) { + elements.offer(task); + } - public SearchTask popNextTask() { - assert (!elements.isEmpty()); - return elements.poll(); - } + public SearchTask popNextTask() { + assert (!elements.isEmpty()); + return elements.poll(); + } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java index e33f96627..8d3441428 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategyRandom.java @@ -5,27 +5,27 @@ import java.util.*; public class SearchStrategyRandom extends SearchStrategy { - private final List elementList; - private final Set elementSet; + private final List elementList; + private final Set elementSet; - public SearchStrategyRandom() { - elementList = new ArrayList<>(); - elementSet = new HashSet<>(); - } + public SearchStrategyRandom() { + elementList = new ArrayList<>(); + elementSet = new HashSet<>(); + } - public void addNewTask(SearchTask task) { - assert (!elementSet.contains(task)); - elementList.add(task); - elementSet.add(task); - } + public void addNewTask(SearchTask task) { + assert (!elementSet.contains(task)); + elementList.add(task); + elementSet.add(task); + } - public SearchTask popNextTask() { - assert (!elementList.isEmpty()); - Collections.shuffle( - elementList, new Random(RandomNumberGenerator.getInstance().getRandomLong())); - SearchTask result = elementList.get(0); - elementList.remove(0); - elementSet.remove(result); - return result; - } + public SearchTask popNextTask() { + assert (!elementList.isEmpty()); + Collections.shuffle( + elementList, new Random(RandomNumberGenerator.getInstance().getRandomLong())); + SearchTask result = elementList.get(0); + elementList.remove(0); + elementSet.remove(result); + return result; + } } 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 1e41083a4..c11fa2e18 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,126 +1,122 @@ package pexplicit.runtime.scheduler.explicit.strategy; +import lombok.Getter; +import pexplicit.runtime.scheduler.Choice; + import java.io.Serializable; import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; -import lombok.Getter; -import lombok.Setter; -import pexplicit.runtime.scheduler.Choice; - public class SearchTask implements Serializable { - @Getter - private final int id; - @Getter - private final SearchTask parentTask; - @Getter - private final List children = new ArrayList<>(); - @Getter - private final int currChoiceNumber; - - @Getter - private int numUnexploredScheduleChoices = 0; - @Getter - private int numUnexploredDataChoices = 0; - - - private final Choice currChoice; - private Map prefixChoices = new HashMap<>(); - private List suffixChoices = new ArrayList<>(); - - public SearchTask(int id, Choice choice, int choiceNum, SearchTask parentTask) { - this.id = id; - this.currChoice = choice; - this.currChoiceNumber = choiceNum; - this.parentTask = parentTask; - if (!isInitialTask()) { - numUnexploredScheduleChoices += choice.getUnexploredScheduleChoices().size(); - numUnexploredDataChoices += choice.getUnexploredDataChoices().size(); + @Getter + private final int id; + @Getter + private final SearchTask parentTask; + @Getter + private final List children = new ArrayList<>(); + @Getter + private final int currChoiceNumber; + private final Choice currChoice; + @Getter + private int numUnexploredScheduleChoices = 0; + @Getter + private int numUnexploredDataChoices = 0; + private final Map prefixChoices = new HashMap<>(); + private final List suffixChoices = new ArrayList<>(); + + public SearchTask(int id, Choice choice, int choiceNum, SearchTask parentTask) { + this.id = id; + this.currChoice = choice; + this.currChoiceNumber = choiceNum; + this.parentTask = parentTask; + if (!isInitialTask()) { + numUnexploredScheduleChoices += choice.getUnexploredScheduleChoices().size(); + numUnexploredDataChoices += choice.getUnexploredDataChoices().size(); + } } - } - - public boolean isInitialTask() { - return id == 0; - } - - public void addChild(SearchTask task) { - children.add(task); - } - public void cleanup() { - if (currChoice != null) { - currChoice.clearUnexplored(); + public boolean isInitialTask() { + return id == 0; } - suffixChoices.clear(); - } - public void addPrefixChoice(Choice choice, int choiceNum) { - assert (!choice.isUnexploredNonEmpty()); - prefixChoices.put(choiceNum, choice); - } + public void addChild(SearchTask task) { + children.add(task); + } - public void addSuffixChoice(Choice choice) { - // TODO: check if we need copy here - suffixChoices.add(choice); - numUnexploredScheduleChoices += choice.getUnexploredScheduleChoices().size(); - numUnexploredDataChoices += choice.getUnexploredDataChoices().size(); - } + public void cleanup() { + if (currChoice != null) { + currChoice.clearUnexplored(); + } + suffixChoices.clear(); + } - public List getAllChoices() { - List result = new ArrayList<>(suffixChoices); - result.add(0, currChoice); + public void addPrefixChoice(Choice choice, int choiceNum) { + assert (!choice.isUnexploredNonEmpty()); + prefixChoices.put(choiceNum, choice); + } - SearchTask task = this; - int i = currChoiceNumber-1; - while(i >= 0) { - Choice c = task.prefixChoices.get(i); - if (c == null) { - assert (!task.isInitialTask()); - task = task.parentTask; - } else { - result.add(0, c); - i--; - } + public void addSuffixChoice(Choice choice) { + // TODO: check if we need copy here + suffixChoices.add(choice); + numUnexploredScheduleChoices += choice.getUnexploredScheduleChoices().size(); + numUnexploredDataChoices += choice.getUnexploredDataChoices().size(); } - assert(result.size() == (currChoiceNumber + 1 + suffixChoices.size())); - return result; - } - @Override - public int hashCode() { - return this.id; - } + public List getAllChoices() { + List result = new ArrayList<>(suffixChoices); + result.add(0, currChoice); + + SearchTask task = this; + int i = currChoiceNumber - 1; + while (i >= 0) { + Choice c = task.prefixChoices.get(i); + if (c == null) { + assert (!task.isInitialTask()); + task = task.parentTask; + } else { + result.add(0, c); + i--; + } + } + assert (result.size() == (currChoiceNumber + 1 + suffixChoices.size())); + return result; + } - @Override - public boolean equals(Object obj) { - if (obj == this) return true; - else if (!(obj instanceof SearchTask)) { - return false; + @Override + public int hashCode() { + return this.id; } - return this.id == ((SearchTask) obj).id; - } - @Override - public String toString() { - return String.format("task%d", id); - } + @Override + public boolean equals(Object obj) { + if (obj == this) return true; + else if (!(obj instanceof SearchTask)) { + return false; + } + return this.id == ((SearchTask) obj).id; + } - public String toStringDetailed() { - if (isInitialTask()) { - return String.format("%s @0::0 (parent: null)", toString()); + @Override + public String toString() { + return String.format("task%d", id); } - if (currChoice.getChoiceStep() != null) { - return String.format("%s @%d::%d (parent: %s)", - toString(), - currChoice.getChoiceStep().getStepNumber(), - currChoiceNumber, - parentTask); + + public String toStringDetailed() { + if (isInitialTask()) { + return String.format("%s @0::0 (parent: null)", this); + } + if (currChoice.getChoiceStep() != null) { + return String.format("%s @%d::%d (parent: %s)", + this, + currChoice.getChoiceStep().getStepNumber(), + currChoiceNumber, + parentTask); + } + return String.format("%s @?::%d (parent: %s)", + this, + currChoiceNumber, + parentTask); } - return String.format("%s @?::%d (parent: %s)", - toString(), - currChoiceNumber, - parentTask); - } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PValue.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PValue.java index d3a5b6b2c..978545752 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PValue.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/values/PValue.java @@ -18,11 +18,6 @@ public abstract class PValue> implements Serializable { */ private String stringRep; - protected void initialize() { - stringRep = _asString(); - hashCode = Objects.hashCode(stringRep); - } - /** * Create a safe clone of the passed PValue * @@ -63,6 +58,11 @@ public static boolean notEqual(PValue val1, PValue val2) { return !isEqual(val1, val2); } + protected void initialize() { + stringRep = _asString(); + hashCode = Objects.hashCode(stringRep); + } + /** * Returns the hash code for the PValue *