Skip to content

Commit 53c5d15

Browse files
aman-goelaman-goel
committed
[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
1 parent 122dc53 commit 53c5d15

File tree

15 files changed

+373
-274
lines changed

15 files changed

+373
-274
lines changed

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

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,11 @@
1313
import pexplicit.runtime.machine.PMonitor;
1414
import pexplicit.runtime.machine.State;
1515
import pexplicit.runtime.machine.events.PContinuation;
16-
import pexplicit.runtime.scheduler.choice.Choice;
16+
import pexplicit.runtime.scheduler.Schedule;
17+
import pexplicit.runtime.scheduler.choice.DataChoice;
1718
import pexplicit.runtime.scheduler.choice.ScheduleChoice;
19+
import pexplicit.runtime.scheduler.choice.ScheduleSearchUnit;
20+
import pexplicit.runtime.scheduler.choice.SearchUnit;
1821
import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
1922
import pexplicit.runtime.scheduler.explicit.SearchStatistics;
2023
import pexplicit.runtime.scheduler.explicit.StateCachingMode;
@@ -207,48 +210,48 @@ public static void logFinishedIteration(int step) {
207210
/**
208211
* Log when backtracking to a new choice
209212
*
210-
* @param choice Choice to which backtracking to
213+
* @param searchUnit Choice to which backtracking to
211214
*/
212-
public static void logBacktrack(Choice choice) {
215+
public static void logBacktrack(SearchUnit searchUnit) {
213216
if (verbosity > 1) {
214217
log.info(String.format(" Backtracking to %s choice @%d::%d",
215-
((choice instanceof ScheduleChoice) ? "schedule" : "data"),
216-
choice.getStepNumber(),
217-
choice.getChoiceNumber()));
218+
((searchUnit instanceof ScheduleSearchUnit) ? "schedule" : "data"),
219+
searchUnit.getStepNumber(),
220+
searchUnit.getChoiceNumber()));
218221
}
219222
}
220223

221-
public static void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
224+
public static void logNewScheduleChoice(List<ScheduleChoice> choices, int step, int idx) {
222225
if (verbosity > 1) {
223226
log.info(String.format(" @%d::%d new schedule choice: %s", step, idx, choices));
224227
}
225228
}
226229

227-
public static void logNewDataChoice(List<PValue<?>> choices, int step, int idx) {
230+
public static void logNewDataChoice(List<DataChoice> choices, int step, int idx) {
228231
if (verbosity > 1) {
229232
log.info(String.format(" @%d::%d new data choice: %s", step, idx, choices));
230233
}
231234
}
232235

233-
public static void logRepeatScheduleChoice(PMachine choice, int step, int idx) {
236+
public static void logRepeatScheduleChoice(ScheduleChoice choice, int step, int idx) {
234237
if (verbosity > 2) {
235238
log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice));
236239
}
237240
}
238241

239-
public static void logCurrentScheduleChoice(PMachine choice, int step, int idx) {
242+
public static void logCurrentScheduleChoice(ScheduleChoice choice, int step, int idx) {
240243
if (verbosity > 2) {
241244
log.info(String.format(" @%d::%d %s", step, idx, choice));
242245
}
243246
}
244247

245-
public static void logRepeatDataChoice(PValue<?> choice, int step, int idx) {
248+
public static void logRepeatDataChoice(DataChoice choice, int step, int idx) {
246249
if (verbosity > 2) {
247250
log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice));
248251
}
249252
}
250253

251-
public static void logCurrentDataChoice(PValue<?> choice, int step, int idx) {
254+
public static void logCurrentDataChoice(DataChoice choice, int step, int idx) {
252255
if (verbosity > 2) {
253256
log.info(String.format(" @%d::%d %s", step, idx, choice));
254257
}

‎Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
import lombok.Getter;
44
import pexplicit.runtime.PExplicitGlobal;
55
import pexplicit.runtime.machine.PMachine;
6+
import pexplicit.runtime.scheduler.choice.DataChoice;
7+
import pexplicit.runtime.scheduler.choice.ScheduleChoice;
68
import pexplicit.utils.misc.Assert;
79
import pexplicit.values.PBool;
810
import pexplicit.values.PInt;
@@ -42,22 +44,22 @@ private static void logComment(String message) {
4244
logIdx++;
4345
}
4446

45-
public static void logDataChoice(PValue<?> choice) {
47+
public static void logDataChoice(DataChoice choice) {
4648
Class type = choice.getClass();
47-
if (choice instanceof PBool boolChoice) {
49+
if (choice.getValue() instanceof PBool boolChoice) {
4850
logComment("boolean choice");
4951
log(boolChoice.getValue() ? "True" : "False");
50-
} else if (choice instanceof PInt intChoice) {
52+
} else if (choice.getValue() instanceof PInt intChoice) {
5153
logComment("integer choice");
5254
log(intChoice.toString());
5355
} else {
5456
assert false;
5557
}
5658
}
5759

58-
public static void logScheduleChoice(PMachine choice) {
60+
public static void logScheduleChoice(ScheduleChoice choice) {
5961
logComment("schedule choice");
60-
log(String.format("(%d)", choice.getInstanceId()));
62+
log(String.format("(%d)", PExplicitGlobal.getGlobalMachine(choice.getValue()).getInstanceId()));
6163
}
6264

6365
public static void logHeader() {

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package pexplicit.runtime.machine;
22

33
import lombok.Getter;
4+
import pexplicit.runtime.scheduler.choice.ScheduleChoice;
45

56
@Getter
67
public class PMachineId {
@@ -11,4 +12,20 @@ public PMachineId(Class<? extends PMachine> t, int tid) {
1112
type = t;
1213
typeId = tid;
1314
}
15+
16+
@Override
17+
public String toString() {
18+
return String.format("%s<%d>", type.getSimpleName(), typeId);
19+
}
20+
21+
@Override
22+
public boolean equals(Object obj) {
23+
if (obj == this)
24+
return true;
25+
else if (!(obj instanceof PMachineId)) {
26+
return false;
27+
}
28+
PMachineId rhs = (PMachineId) obj;
29+
return this.type == rhs.type && this.typeId == rhs.typeId;
30+
}
1431
}

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

Lines changed: 42 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,11 @@
11
package pexplicit.runtime.scheduler;
22

3+
import lombok.Data;
34
import lombok.Getter;
45
import lombok.Setter;
56
import pexplicit.runtime.PExplicitGlobal;
6-
import pexplicit.runtime.machine.PMachine;
77
import pexplicit.runtime.machine.PMachineId;
8-
import pexplicit.runtime.scheduler.choice.Choice;
9-
import pexplicit.runtime.scheduler.choice.DataChoice;
10-
import pexplicit.runtime.scheduler.choice.ScheduleChoice;
8+
import pexplicit.runtime.scheduler.choice.*;
119
import pexplicit.runtime.scheduler.explicit.StepState;
1210
import pexplicit.values.PValue;
1311

@@ -20,11 +18,11 @@
2018
*/
2119
public class Schedule implements Serializable {
2220
/**
23-
* List of choices
21+
* List of current choices
2422
*/
2523
@Getter
2624
@Setter
27-
private List<Choice> choices = new ArrayList<>();
25+
private List<SearchUnit> searchUnits = new ArrayList<>();
2826

2927
/**
3028
* Step state at the start of a scheduler step.
@@ -45,8 +43,8 @@ public Schedule() {
4543
* @param idx Choice depth
4644
* @return Choice at depth idx
4745
*/
48-
public Choice getChoice(int idx) {
49-
return choices.get(idx);
46+
public SearchUnit getChoice(int idx) {
47+
return searchUnits.get(idx);
5048
}
5149

5250
/**
@@ -55,8 +53,8 @@ public Choice getChoice(int idx) {
5553
* @param idx Choice depth
5654
*/
5755
public void clearChoice(int idx) {
58-
choices.get(idx).clearCurrent();
59-
choices.get(idx).clearUnexplored();
56+
searchUnits.get(idx).clearCurrent();
57+
searchUnits.get(idx).clearUnexplored();
6058
}
6159

6260
/**
@@ -65,7 +63,7 @@ public void clearChoice(int idx) {
6563
* @param choiceNum Choice depth
6664
*/
6765
public void removeChoicesAfter(int choiceNum) {
68-
choices.subList(choiceNum + 1, choices.size()).clear();
66+
searchUnits.subList(choiceNum + 1, searchUnits.size()).clear();
6967
}
7068

7169
/**
@@ -75,7 +73,7 @@ public void removeChoicesAfter(int choiceNum) {
7573
*/
7674
public int getNumUnexploredChoices() {
7775
int numUnexplored = 0;
78-
for (Choice<?> c : choices) {
76+
for (SearchUnit<?> c : searchUnits) {
7977
numUnexplored += c.getUnexplored().size();
8078
}
8179
return numUnexplored;
@@ -88,8 +86,8 @@ public int getNumUnexploredChoices() {
8886
*/
8987
public int getNumUnexploredDataChoices() {
9088
int numUnexplored = 0;
91-
for (Choice<?> c : choices) {
92-
if (c instanceof DataChoice) {
89+
for (SearchUnit<?> c : searchUnits) {
90+
if (c instanceof DataSearchUnit) {
9391
numUnexplored += c.getUnexplored().size();
9492
}
9593
}
@@ -104,17 +102,17 @@ public int getNumUnexploredDataChoices() {
104102
* @param current Machine to set as current schedule choice
105103
* @param unexplored List of machine to set as unexplored schedule choices
106104
*/
107-
public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current, List<PMachineId> unexplored) {
108-
if (choiceNum == choices.size()) {
109-
choices.add(null);
105+
public void setScheduleChoice(int stepNum, int choiceNum, ScheduleChoice current, List<ScheduleChoice> unexplored) {
106+
if (choiceNum == searchUnits.size()) {
107+
searchUnits.add(null);
110108
}
111-
assert (choiceNum < choices.size());
109+
assert (choiceNum < searchUnits.size());
112110
if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()
113111
&& stepNum != 0) {
114112
assert (stepBeginState != null);
115-
choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, stepBeginState));
113+
searchUnits.set(choiceNum, new ScheduleSearchUnit(stepNum, choiceNum, current, unexplored, stepBeginState));
116114
} else {
117-
choices.set(choiceNum, new ScheduleChoice(stepNum, choiceNum, current, unexplored, null));
115+
searchUnits.set(choiceNum, new ScheduleSearchUnit(stepNum, choiceNum, current, unexplored, null));
118116
}
119117
}
120118

@@ -126,12 +124,12 @@ public void setScheduleChoice(int stepNum, int choiceNum, PMachineId current, Li
126124
* @param current PValue to set as current schedule choice
127125
* @param unexplored List of PValue to set as unexplored schedule choices
128126
*/
129-
public void setDataChoice(int stepNum, int choiceNum, PValue<?> current, List<PValue<?>> unexplored) {
130-
if (choiceNum == choices.size()) {
131-
choices.add(null);
127+
public void setDataChoice(int stepNum, int choiceNum, DataChoice current, List<DataChoice> unexplored) {
128+
if (choiceNum == searchUnits.size()) {
129+
searchUnits.add(null);
132130
}
133-
assert (choiceNum < choices.size());
134-
choices.set(choiceNum, new DataChoice(stepNum, choiceNum, current, unexplored));
131+
assert (choiceNum < searchUnits.size());
132+
searchUnits.set(choiceNum, new DataSearchUnit(stepNum, choiceNum, current, unexplored));
135133
}
136134

137135
/**
@@ -140,9 +138,9 @@ public void setDataChoice(int stepNum, int choiceNum, PValue<?> current, List<PV
140138
* @param idx Choice depth
141139
* @return Current schedule choice
142140
*/
143-
public PMachineId getCurrentScheduleChoice(int idx) {
144-
assert (choices.get(idx) instanceof ScheduleChoice);
145-
return ((ScheduleChoice) choices.get(idx)).getCurrent();
141+
public ScheduleChoice getCurrentScheduleChoice(int idx) {
142+
assert (searchUnits.get(idx) instanceof ScheduleSearchUnit);
143+
return ((ScheduleSearchUnit) searchUnits.get(idx)).getCurrent();
146144
}
147145

148146
/**
@@ -151,9 +149,9 @@ public PMachineId getCurrentScheduleChoice(int idx) {
151149
* @param idx Choice depth
152150
* @return Current data choice
153151
*/
154-
public PValue<?> getCurrentDataChoice(int idx) {
155-
assert (choices.get(idx) instanceof DataChoice);
156-
return ((DataChoice) choices.get(idx)).getCurrent();
152+
public DataChoice getCurrentDataChoice(int idx) {
153+
assert (searchUnits.get(idx) instanceof DataSearchUnit);
154+
return ((DataSearchUnit) searchUnits.get(idx)).getCurrent();
157155
}
158156

159157
/**
@@ -162,10 +160,10 @@ public PValue<?> getCurrentDataChoice(int idx) {
162160
* @param idx Choice depth
163161
* @return List of machines, or null if index is invalid
164162
*/
165-
public List<PMachineId> getUnexploredScheduleChoices(int idx) {
163+
public List<ScheduleChoice> getUnexploredScheduleChoices(int idx) {
166164
if (idx < size()) {
167-
assert (choices.get(idx) instanceof ScheduleChoice);
168-
return ((ScheduleChoice) choices.get(idx)).getUnexplored();
165+
assert (searchUnits.get(idx) instanceof ScheduleSearchUnit);
166+
return ((ScheduleSearchUnit) searchUnits.get(idx)).getUnexplored();
169167
} else {
170168
return new ArrayList<>();
171169
}
@@ -177,22 +175,22 @@ public List<PMachineId> getUnexploredScheduleChoices(int idx) {
177175
* @param idx Choice depth
178176
* @return List of PValue, or null if index is invalid
179177
*/
180-
public List<PValue<?>> getUnexploredDataChoices(int idx) {
178+
public List<DataChoice> getUnexploredDataChoices(int idx) {
181179
if (idx < size()) {
182-
assert (choices.get(idx) instanceof DataChoice);
183-
return ((DataChoice) choices.get(idx)).getUnexplored();
180+
assert (searchUnits.get(idx) instanceof DataSearchUnit);
181+
return ((DataSearchUnit) searchUnits.get(idx)).getUnexplored();
184182
} else {
185183
return new ArrayList<>();
186184
}
187185
}
188186

189-
public ScheduleChoice getScheduleChoiceAt(Choice choice) {
190-
if (choice instanceof ScheduleChoice scheduleChoice) {
187+
public ScheduleSearchUnit getScheduleChoiceAt(SearchUnit searchUnit) {
188+
if (searchUnit instanceof ScheduleSearchUnit scheduleChoice) {
191189
return scheduleChoice;
192190
} else {
193-
for (int i = choice.getChoiceNumber() - 1; i >= 0; i--) {
194-
Choice c = choices.get(i);
195-
if (c instanceof ScheduleChoice scheduleChoice) {
191+
for (int i = searchUnit.getChoiceNumber() - 1; i >= 0; i--) {
192+
SearchUnit c = searchUnits.get(i);
193+
if (c instanceof ScheduleSearchUnit scheduleChoice) {
196194
return scheduleChoice;
197195
}
198196
}
@@ -206,7 +204,7 @@ public ScheduleChoice getScheduleChoiceAt(Choice choice) {
206204
* @param idx Choice depth
207205
*/
208206
public void clearCurrent(int idx) {
209-
choices.get(idx).clearCurrent();
207+
searchUnits.get(idx).clearCurrent();
210208
}
211209

212210
/**
@@ -215,6 +213,6 @@ public void clearCurrent(int idx) {
215213
* @return Number of choices in the schedule
216214
*/
217215
public int size() {
218-
return choices.size();
216+
return searchUnits.size();
219217
}
220218
}

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

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import pexplicit.runtime.machine.PMachine;
88
import pexplicit.runtime.machine.PMachineId;
99
import pexplicit.runtime.machine.PMonitor;
10+
import pexplicit.runtime.scheduler.choice.DataChoice;
1011
import pexplicit.runtime.scheduler.explicit.StepState;
1112
import pexplicit.utils.exceptions.BugFoundException;
1213
import pexplicit.utils.exceptions.NotImplementedException;
@@ -118,7 +119,7 @@ protected void reset() {
118119
*
119120
* @return PValue as data choice
120121
*/
121-
protected abstract PValue<?> getNextDataChoice(List<PValue<?>> input_choices);
122+
protected abstract PValue<?> getNextDataChoice(List<DataChoice> input_choices);
122123

123124
public void updateLogNumber() {
124125
stepNumLogs += 1;
@@ -133,9 +134,9 @@ public void updateLogNumber() {
133134
* @return boolean data choice
134135
*/
135136
public PBool getRandomBool() {
136-
List<PValue<?>> choices = new ArrayList<>();
137-
choices.add(PBool.PTRUE);
138-
choices.add(PBool.PFALSE);
137+
List<DataChoice> choices = new ArrayList<>();
138+
choices.add(new DataChoice(PBool.PTRUE));
139+
choices.add(new DataChoice(PBool.PFALSE));
139140
return (PBool) getNextDataChoice(choices);
140141
}
141142

@@ -146,7 +147,7 @@ public PBool getRandomBool() {
146147
* @return integer data choice
147148
*/
148149
public PInt getRandomInt(PInt bound) {
149-
List<PValue<?>> choices = new ArrayList<>();
150+
List<DataChoice> choices = new ArrayList<>();
150151
int boundInt = bound.getValue();
151152
if (boundInt > 10000) {
152153
throw new BugFoundException(String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", boundInt));
@@ -155,7 +156,7 @@ public PInt getRandomInt(PInt bound) {
155156
boundInt = 1;
156157
}
157158
for (int i = 0; i < boundInt; i++) {
158-
choices.add(new PInt(i));
159+
choices.add(new DataChoice(new PInt(i)));
159160
}
160161
return (PInt) getNextDataChoice(choices);
161162
}

0 commit comments

Comments
 (0)