projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
58dc349
)
Fix a bug in ConflictTracker.java
author
amiraj
<amiraj.95@uci.edu>
Thu, 14 Nov 2019 19:21:53 +0000
(11:21 -0800)
committer
amiraj
<amiraj.95@uci.edu>
Thu, 14 Nov 2019 19:21:53 +0000
(11:21 -0800)
src/main/gov/nasa/jpf/listener/ConflictTracker.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 435a29a0a7505850384781699ab9d9b1d3cab8b7..fa940012e2194e18587fdd5b143f5a87bee7762b 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/
src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@
-128,6
+128,7
@@
public class ConflictTracker extends ListenerAdapter {
HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
+
// Update the valueMap
for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
// Update the valueMap
for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
@@
-174,12
+175,10
@@
public class ConflictTracker extends ListenerAdapter {
boolean updateEdge(Node parentNode, Node currentNode) {
ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
HashSet<String> updatedVarNames = new HashSet<String>();
boolean updateEdge(Node parentNode, Node currentNode) {
ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
HashSet<String> updatedVarNames = new HashSet<String>();
- HashMap<String, Integer> lastWriter = new HashMap<String, Integer>(); // Store the last writer of each variable
boolean isChanged = false;
for (int i = 0;i < setSet.size();i++) {
updatedVarNames.add(setSet.get(i).getVarName());
boolean isChanged = false;
for (int i = 0;i < setSet.size();i++) {
updatedVarNames.add(setSet.get(i).getVarName());
- lastWriter.put(setSet.get(i).getVarName(), setSet.get(i).getAppNum());
}
for (NameValuePair i : parentNode.getOutSet()) {
}
for (NameValuePair i : parentNode.getOutSet()) {
@@
-188,8
+187,7
@@
public class ConflictTracker extends ListenerAdapter {
}
for (int i = 0;i < setSet.size();i++) {
}
for (int i = 0;i < setSet.size();i++) {
- if (setSet.get(i).getAppNum().equals(lastWriter.get(setSet.get(i).getVarName()))) // Add the last writer of each variable to outSet
- isChanged |= currentNode.getOutSet().add(setSet.get(i));
+ isChanged |= currentNode.getOutSet().add(setSet.get(i));
}
return isChanged;
}
return isChanged;
@@
-342,11
+340,10
@@
public class ConflictTracker extends ListenerAdapter {
depth = search.getDepth();
operation = "forward";
depth = search.getDepth();
operation = "forward";
- // Check for the conflict in this new transition
- conflictFound = checkForConflict(parentNode);
+ // Add the node to the list of nodes
+ if (nodes.get(id) == null)
+ nodes.put(id, new Node(id));
- // Add the node to the list of nodes
- nodes.put(id, new Node(id));
Node currentNode = nodes.get(id);
// Update the setSet for this new node
Node currentNode = nodes.get(id);
// Update the setSet for this new node
@@
-386,6
+383,9
@@
public class ConflictTracker extends ListenerAdapter {
// Update the edge and check if the outset of the current node is changed or not to propagate the change
boolean isChanged = updateEdge(parentNode, currentNode);
// Update the edge and check if the outset of the current node is changed or not to propagate the change
boolean isChanged = updateEdge(parentNode, currentNode);
+ // Check for the conflict in this edge
+ conflictFound = checkForConflict(currentNode);
+
// Check if the outSet of this state has changed, update all of its successors' sets if any
if (isChanged)
conflictFound = conflictFound || propagateTheChange(currentNode);
// Check if the outSet of this state has changed, update all of its successors' sets if any
if (isChanged)
conflictFound = conflictFound || propagateTheChange(currentNode);