Clean up comments
authorBrian Demsky <bdemsky@uci.edu>
Tue, 17 Dec 2019 06:41:16 +0000 (22:41 -0800)
committerBrian Demsky <bdemsky@uci.edu>
Tue, 17 Dec 2019 06:41:16 +0000 (22:41 -0800)
src/main/gov/nasa/jpf/listener/ConflictTracker.java

index 56d4d67..a61da9c 100644 (file)
@@ -114,17 +114,21 @@ public class ConflictTracker extends ListenerAdapter {
     HashMap<IndexObject, Update> lastupdate = new HashMap<IndexObject, Update>();
     boolean changed = false;
     
+    //Go through each update on the current transition
     for(int i=0; i<edgeUpdates.size(); i++) {
       Update u = edgeUpdates.get(i);
       IndexObject io = u.getIndex();
       HashSet<Update> confupdates = null;
+
+      //See if we have already updated this device attribute
       if (lastupdate.containsKey(io)) {
         confupdates = new HashSet<Update>();
         confupdates.add(lastupdate.get(io));
       } else if (srcUpdates.containsKey(io)){
         confupdates = srcUpdates.get(io);
       }
-      //Check for conflict
+
+      //Check for conflict with the appropriate update set if we are not a manual transition
       if (confupdates != null && !e.isManual()) {
         for(Update u2: confupdates) {
           if (conflicts(u, u2)) {
@@ -135,6 +139,7 @@ public class ConflictTracker extends ListenerAdapter {
       lastupdate.put(io, u);
     }
     for(IndexObject io: srcUpdates.keySet()) {
+      //Only propagate src changes if the transition doesn't update the device attribute
       if (!lastupdate.containsKey(io)) {
         //Make sure destination has hashset in map
         if (!dstUpdates.containsKey(io))
@@ -153,6 +158,7 @@ public class ConflictTracker extends ListenerAdapter {
     return changed;
   }
 
+  //Method to check for conflicts between two updates
   //Have conflict if same device, same attribute, different app, different vaalue
   boolean conflicts(Update u, Update u2) {
     return (!u.getApp().equals(u2.getApp())) &&
@@ -172,6 +178,7 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   Edge createEdge(Node parent, Node current, Transition transition, boolean ismanual) {
+    //Check if this transition is explored.  If so, just skip everything
     if (transitions.contains(transition))
       return null;
 
@@ -210,6 +217,7 @@ public class ConflictTracker extends ListenerAdapter {
     }
   }
 
+  //Each Edge corresponds to a transition
   static class Edge {
     Node source, destination;
     Transition transition;
@@ -274,6 +282,7 @@ public class ConflictTracker extends ListenerAdapter {
       return value;
     }
 
+    //Gets an index object for indexing updates by just device and attribute
     IndexObject getIndex() {
       return new IndexObject(this);
     }
@@ -530,7 +539,6 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   private void writeWriterAndValue(String writer, String attribute, String value) {
-    // Update the temporary Set set.
     Update u = new Update(writer, "DEVICE", attribute, value);
     currUpdates.add(u);
   }
@@ -578,7 +586,7 @@ public class ConflictTracker extends ListenerAdapter {
             if (getWriter(ti.getStack(), manualSet) != null)
               manual = true;
             
-            // Update the temporary Set set.
+            // Update the current updates
             writeWriterAndValue(writer, var, value);
           }
         }