out = new PrintWriter(System.out, true);
debugMode = config.getBoolean("debug_mode", false);
- String[] conflictVars = config.getStringArray("variables");
- // We are not tracking anything if it is null
- if (conflictVars != null) {
- for (String var : conflictVars) {
- conflictSet.add(var);
+ if (!debugMode) {
+ String[] conflictVars = config.getStringArray("variables");
+ // We are not tracking anything if it is null
+ if (conflictVars != null) {
+ for (String var : conflictVars) {
+ conflictSet.add(var);
+ }
}
- }
- String[] apps = config.getStringArray("apps");
- // We are not tracking anything if it is null
- if (apps != null) {
- for (String var : apps) {
- appSet.add(var);
+ String[] apps = config.getStringArray("apps");
+ // We are not tracking anything if it is null
+ if (apps != null) {
+ for (String var : apps) {
+ appSet.add(var);
+ }
}
}
}
//Check for conflict with the appropriate update set if we are not a manual transition
- //If this is debug mode, then we do not report any conflicts
- if (!debugMode && confupdates != null && !u.isManual()) {
+ if (confupdates != null && !u.isManual()) {
for(Update u2: confupdates) {
if (conflicts(u, u2)) {
//throw new RuntimeException(createErrorMessage(u, u2));
out.println("The state is restored to state with id: "+id+", depth: "+depth);
// Update the parent node
- parentNode = getNode(id);
+ if (!debugMode) {
+ parentNode = getNode(id);
+ }
}
@Override
@Override
public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
- if (currentCG instanceof IntChoiceFromSet) {
- IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
- currentEvent = icsCG.getNextChoice();
+ if (!debugMode) {
+ if (currentCG instanceof IntChoiceFromSet) {
+ IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
+ currentEvent = icsCG.getNextChoice();
+ }
}
}
depth = search.getDepth();
operation = "forward";
- // Add the node to the list of nodes
- Node currentNode = getNode(id);
+ if (!debugMode) {
+ // Add the node to the list of nodes
+ Node currentNode = getNode(id);
- // Create an edge based on the current transition
- Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);
+ // Create an edge based on the current transition
+ Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);
- // Reset the temporary variables and flags
- currUpdates.clear();
- manual = false;
+ // Reset the temporary variables and flags
+ currUpdates.clear();
+ manual = false;
- // If we have a new Edge, check for conflicts
- if (newEdge != null)
- propagateChange(newEdge);
+ // If we have a new Edge, check for conflicts
+ if (newEdge != null)
+ propagateChange(newEdge);
- if (search.isNewState()) {
- detail = "new";
- } else {
- detail = "visited";
- }
+ if (search.isNewState()) {
+ detail = "new";
+ } else {
+ detail = "visited";
+ }
- if (search.isEndState()) {
- out.println("This is the last state!");
- theEnd = "end";
- }
+ if (search.isEndState()) {
+ out.println("This is the last state!");
+ theEnd = "end";
+ }
- out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
+ out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
- // Update the parent node
- parentNode = currentNode;
+ // Update the parent node
+ parentNode = currentNode;
+ }
}
@Override
out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
- // Update the parent node
- parentNode = getNode(id);
+ if (!debugMode) {
+ // Update the parent node
+ parentNode = getNode(id);
+ }
}
@Override
public void searchFinished(Search search) {
out.println("----------------------------------- search finished");
- //Comment out the following line to print the explored graph
- printGraph();
+ if (!debugMode) {
+ //Comment out the following line to print the explored graph
+ printGraph();
+ }
}
private String getValue(ThreadInfo ti, Instruction inst, byte type) {
}
}
- if (conflictFound) {
+ if (!debugMode) {
+ if (conflictFound) {
- StringBuilder sb = new StringBuilder();
- sb.append(errorMessage);
- Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
- ti.setNextPC(nextIns);
- } else {
+ StringBuilder sb = new StringBuilder();
+ sb.append(errorMessage);
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+ ti.setNextPC(nextIns);
+ } else {
- if (executedInsn instanceof WriteInstruction) {
- String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
- // Check if we have an update to isManualTransaction to update manual field
- if (varId.contains("isManualTransaction")) {
- byte type = getType(ti, executedInsn);
- String value = getValue(ti, executedInsn, type);
- System.out.println();
- manual = (value.equals("true"))?true:false;
- }
- for (String var : conflictSet) {
- if (varId.contains(var)) {
- // Get variable info
+ if (executedInsn instanceof WriteInstruction) {
+ String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+ // Check if we have an update to isManualTransaction to update manual field
+ if (varId.contains("isManualTransaction")) {
byte type = getType(ti, executedInsn);
String value = getValue(ti, executedInsn, type);
- String writer = getWriter(ti.getStack(), appSet);
-
- // Just return if the writer is not one of the listed apps in the .jpf file
- if (writer == null)
- return;
-
- // Update the current updates
- writeWriterAndValue(writer, var, value);
+ System.out.println();
+ manual = (value.equals("true"))?true:false;
+ }
+ for (String var : conflictSet) {
+ if (varId.contains(var)) {
+ // Get variable info
+ byte type = getType(ti, executedInsn);
+ String value = getValue(ti, executedInsn, type);
+ String writer = getWriter(ti.getStack(), appSet);
+
+ // Just return if the writer is not one of the listed apps in the .jpf file
+ if (writer == null)
+ return;
+
+ // Update the current updates
+ writeWriterAndValue(writer, var, value);
+ }
}
}
}