}
boolean propagateTheChange(Node currentNode) {
- HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
- HashMap<Node, HashSet<Node>> parentQueueMap = new HashMap<Node, HashSet<Node>>();
- HashSet<Node> parents = new HashSet<Node>();
- parents.add(currentNode);
+ HashSet<Node> changed = new HashSet<Node>();
+ boolean isChanged = false;
- for (Node node : currentNode.getSuccessors()) {
- parentQueueMap.put(node, parents);
- }
+ // Add the current node to the changed set
+ changed.add(currentNode);
while(!changed.isEmpty()) {
// Get the first element of the changed set and remove it
Node nodeToProcess = changed.iterator().next();
changed.remove(nodeToProcess);
- // Update the changed parents
- parents.clear();
- parents = parentQueueMap.get(nodeToProcess);
- boolean isChanged = false;
-
- for (Node node : parents) {
- // Update the edge
- isChanged |= updateTheOutSet(node, nodeToProcess);
- }
-
- // All the changes in current parents are propagated
- parentQueueMap.get(nodeToProcess).clear();
-
- // Check if the node has changed or not
- if (isChanged) {
- // Check for a conflict in all the transition out of this node
- if (checkAllSuccForConflict(nodeToProcess))
- return true;
-
- // Update the parents list for the successors of the current node
- parents.clear();
- parents.add(nodeToProcess);
-
- // For all the successors of the current node
- for (Node i : nodeToProcess.getSuccessors()) {
- if (!changed.contains(i))
- changed.add(i);
-
- // Update the list of updated parents for the current node
- if (parentQueueMap.containsKey(i))
- parentQueueMap.get(i).add(nodeToProcess);
- else
- parentQueueMap.put(i, parents);
- }
+ // Update all the successors of the node
+ for (Node node : nodeToProcess.getSuccessors()) {
+ isChanged = false;
+ isChanged = updateTheOutSet(nodeToProcess, node);
+ if (isChanged) {
+ changed.add(node);
+ if (checkAllSuccForConflict(node))
+ return true;
+ }
}
}
return false;
}
boolean updateTheOutSet(Node parentNode, Node currentNode) {
- HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
+ Edge edge = parentNode.getOutgoingEdges().get(currentNode);
+ HashMap<Transition, ArrayList<NameValuePair>> setSets = edge.getSetSetMap();
HashSet<String> updatedVarNames = new HashSet<String>();
- Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
- HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
- HashMap<String, String> lastValue = currentEdge.getLastValue();
- HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
+ HashSet<String> outSetVarMap = new HashSet<String>();
boolean isChanged = false;
for (Map.Entry mapElement : setSets.entrySet()) {
}
for (NameValuePair i : parentNode.getOutSet()) {
- outSetVarMap.put(i.getVarName(), i.getAppNum());
+ outSetVarMap.add(i.getVarName());
if (!updatedVarNames.contains(i.getVarName()))
isChanged |= currentNode.getOutSet().add(i);
}
+ ArrayList<NameValuePair> lastSetSet = setSets.get(edge.getFinalTransition());
- for (Map.Entry mapElement : setSets.entrySet()) {
- ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
-
- for (int i = 0;i < setSet.size();i++) {
- String varName = setSet.get(i).getVarName();
- Integer writer = lastWriter.get(varName);
- String value = lastValue.get(varName);
-
- if (setSet.get(i).getAppNum().equals(writer)
- && setSet.get(i).getValue().equals(value)) {
- if (outSetVarMap.containsKey(varName)) {
- Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
- varName.hashCode();
- currentNode.getOutSet().remove(hashCode);
- }
- isChanged |= currentNode.getOutSet().add(setSet.get(i));
- }
+ for (int i = 0;i < lastSetSet.size();i++) {
+ String var = lastSetSet.get(i).getVarName();
+
+ if (outSetVarMap.contains(var)) {
+ currentNode.getOutSet().remove(lastSetSet.get(i));
}
+ isChanged |= currentNode.getOutSet().add(lastSetSet.get(i));
}
return isChanged;
}
void updateTheEdge(Node currentNode, Transition transition) {
if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
- if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
- if (manual)
- currentEdge.getSetSetMap().put(transition, tempSetSet);
- else
- currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
- } else { // Add a new transition
- currentEdge.getSetSetMap().put(transition, tempSetSet);
- }
+ if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
+ if (manual)
+ currentEdge.getSetSetMap().put(transition, tempSetSet);
+ else
+ currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
+ } else { // Add a new transition
+ currentEdge.getSetSetMap().put(transition, tempSetSet);
+ }
+ currentEdge.setFinalTransition(transition);
} else {
parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
currentEdge.getSetSetMap().put(transition, tempSetSet);
- }
-
- // Update the last writer and last value for this edge for each varName
- Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
- ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
- for (int i = 0;i < setSet.size();i++) {
- NameValuePair nameValuePair = setSet.get(i);
- currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
- currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
+ currentEdge.setFinalTransition(transition);
}
}
-
-
static class Node {
Integer id;
HashSet<Node> predecessors = new HashSet<Node>();
static class Edge {
Node source, destination;
+ Transition finalTransition;
HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
HashMap<String, String> lastValue = new HashMap<String, String>();
HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
return destination;
}
+ Transition getFinalTransition() {
+ return finalTransition;
+ }
+
+ void setFinalTransition(Transition transition) {
+ finalTransition = transition;
+ }
+
HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
return setSetMap;
}
// Update the outset of the current node and check if it is changed or not to propagate the change
boolean isChanged = updateTheOutSet(parentNode, currentNode);
-
+
// Check if the outSet of this state has changed, update all of its successors' sets if any
if (isChanged)
conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode);
if (getWriter(ti.getStack(), manualSet) != null)
manual = true;
-
+
// Update the temporary Set set.
writeWriterAndValue(writer, value, var);
}
projects / jpf-core.git / blobdiff