Better dependency checking

Various other small changes as well

IncrementalMinimization/scripts/budget_graph.py

@@ -11,8 +11,9 @@
 xIndex = int(sys.argv[2])
 percent1_index = int(sys.argv[3])
 percent2_index = int(sys.argv[4])
-increment = int(sys.argv[5])
-cutoff = int(sys.argv[6])
+#percent3_index = int(sys.argv[5]) #TODO: generalize to arbitrary number of indices
+increment = int(sys.argv[6])
+cutoff = int(sys.argv[7])
 
 def toNum(s):
     if s.isdigit():
@@ -34,6 +35,7 @@ def get_tick_from_point(point):
     tick_map = {}
     p1_data = []
     p2_data = []
+    p3_data = []
     for i in range(0, cutoff, increment):
         tick_start = i
         tick_end = (i + increment) - 1
@@ -46,6 +48,7 @@ def get_tick_from_point(point):
             break
         p1 = data[row][percent1_index]
         p2 = data[row][percent2_index]
+        #p3 = data[row][percent3_index]
         tick = ticks[cur_index]
         actual_tick = get_tick_from_point(x)
         while(tick != actual_tick):
@@ -57,18 +60,15 @@ def get_tick_from_point(point):
             count = 1
             p1_data.append(p1)
             p2_data.append(p2)
+            #p3_data.append(p3)
         else:
             count += 1
             p1_data[cur_index] += (p1 - p1_data[cur_index])/float(count)
             p2_data[cur_index] += (p2 - p2_data[cur_index])/float(count)
-    print(ticks)
-    print(len(ticks))
-    print(len(p1_data))
-    for i in range(0,len(ticks)):
-        print "{} : {} : {}".format(ticks[i], str(p1_data[i]), str(p2_data[i]))
+            #p3_data[cur_index] += (p3 - p3_data[cur_index])/float(count)
     assert(len(ticks) == len(p1_data))
     assert(len(p1_data) == len(p2_data))
-    return ticks, p1_data, p2_data
+    return ticks, p1_data, p2_data, p3_data
 
 with open(testsfile, "r") as f:
     fStrings = f.read().split('\n')
@@ -77,14 +77,16 @@ def get_tick_from_point(point):
 fData = [[toNum(datum) for datum in row.split(',') if datum]
          for row in fStrings[1:] if row]
 
-ticks, p1_data, p2_data = generate_data(fData, increment, cutoff)
+ticks, p1_data, p2_data, p3_data = generate_data(fData, increment, cutoff)
 
 p1_data = [p1*100 for p1 in p1_data]
 p2_data = [p2*100 for p2 in p2_data]
+#p3_data = [p3*100 for p3 in p3_data]
 fig, ax = pyplot.subplots(1,1)
 percent_format = mtick.FormatStrFormatter("%.0f%%")
-ax.bar([a - 0.15 for a in range(0,len(p1_data))], p1_data, width=0.30, label="Symbolic Incremental")
-ax.bar([b + 0.15 for b in range(0,len(p2_data))], p2_data, width=0.30, label="'Naive' Incremental")
+ax.bar([a - 0.15 for a in range(0,len(p1_data))], p1_data, width=0.20, label="Symbolic Incremental")
+ax.bar([b + 0.15 for b in range(0,len(p2_data))], p2_data, width=0.20, label="'Naive' Incremental")
+#ax.bar([c + 0.20 for c in range(0,len(p3_data))], p3_data, width=0.20, label ="Incremental with Dependency Check")
 pyplot.xticks(range(0, len(ticks)), ticks, fontsize=6)
 ax.yaxis.set_major_formatter(percent_format)
 pyplot.xlabel(xAxis)

IncrementalMinimization/scripts/generate_graph.py

@@ -4,6 +4,7 @@
 xAxis = "Number of States"
 yAxis = "Average Minimization Time (ms)"
 title = "Comparison of SFA Minimization Algorithms"
+scale = "log"
 
 testsfile = sys.argv[1]
 xIndex = int(sys.argv[2])
@@ -52,7 +53,7 @@ def mergeData(data, index):
 for i in graph_indices:
     graphData = [row[i] for row in fData[:len(xData)]]
     pyplot.plot(xData, graphData, label=title_row[i], linewidth=1.0)
-pyplot.yscale("log")
+pyplot.yscale(scale)
 pyplot.legend(loc=0)
 pyplot.xlabel(xAxis)
 pyplot.ylabel(yAxis)

IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java

@@ -140,61 +140,6 @@ public void addDependency(List<Integer> pair, List<Integer> dependency)
 				}
 				assert(depEntry != null);
 				pairEntry.addDependency(depEntry);
-
-
-				/*
-				//System.out.println("");
-				//System.out.println(String.format("Adding %s to %s", dependency.toString(), pair.toString()));
-				if(dependencies.containsKey(dependency) && !pair.equals(dependency))
-				{
-					//System.out.println("Already seen dependency");
-					//Dependency is transitive. So, we flatten the dependency list as much as possible before adding.
-					/*ArrayList<List<Integer>> flatDependencyList = new ArrayList<List<Integer>>();
-					Queue<List<Integer>> nestedDepQueue = new LinkedList<List<Integer>>();
-					nestedDepQueue.addAll(dependencies.get(dependency));
-					//System.out.println(String.format("Deps of dep: %s", nestedDepQueue.toString()));
-					HashSet<List<Integer>> debugTest = new HashSet<List<Integer>>(); //TODO: remove. using to check that no infinite loops exist.
-					while(!nestedDepQueue.isEmpty())
-					{
-						//System.out.println(nestedDepQueue);
-						System.out.println(String.format("ndq: %d / %d", debugTest.size(), num_pairs));
-						List<Integer> dep = nestedDepQueue.remove();
-						if(debugTest.contains(dep))
-						{
-							continue;
-						}
-						else if(dependencies.containsKey(dep))
-						{
-							nestedDepQueue.addAll(dependencies.get(dep));
-						}
-						else
-						{
-							flatDependencyList.add(dep);
-						}
-						debugTest.add(dep);
-					}
-					ArrayList<List<Integer>> flatDependencyList = dependencies.get(dependency);
-					if(!dependencies.containsKey(pair))
-					{
-						dependencies.put(pair, new ArrayList<List<Integer>>());
-					}
-					dependencies.get(pair).addAll(flatDependencyList);
-				}
-				else
-				{
-					if(!dependencies.containsKey(pair))
-					{
-						dependencies.put(pair, new ArrayList<List<Integer>>());
-					}
-					dependencies.get(pair).add(dependency);
-				}
-				System.out.println(dependency);
-				assert(dependencies.containsKey(dependency));
-				if(!dependencies.containsKey(pair))
-				{
-					dependencies.put(pair, new ArrayList<List<Integer>>());
-				}
-				dependencies.get(pair).add(dependency); */
 			}
 
 			public void addAllDependencies(List<Integer> pair, ArrayList<List<Integer>> dpairs)
@@ -205,7 +150,7 @@ public void addAllDependencies(List<Integer> pair, ArrayList<List<Integer>> dpai
 				}
 			}
 
-			private void mergePair(StatePair pairEntry, HashSet<List<Integer>> badPath)
+			private void mergePair(StatePair pairEntry, HashSet<List<Integer>> badPath) throws TimeoutException
 			{
 
 				Queue<StatePair> depQueue = new LinkedList<StatePair>();
@@ -232,11 +177,11 @@ private void mergePair(StatePair pairEntry, HashSet<List<Integer>> badPath)
 					assert(pairLookup.values().contains(dep));
 					depQueue.addAll(dep.getDependencies());
 				}
-				System.out.println("SQUIBLLITY DOOP BOP");
+				System.out.println("SQUIBLLITY DOOP BOP"); //unique string for debug purposes
 				equivClasses.union(pairEntry.pair.get(0), pairEntry.pair.get(1));
 			}
 
-			public void mergeStates(HashSet<List<Integer>> badPath)
+			public void mergeStates(HashSet<List<Integer>> badPath) throws TimeoutException
 			{
 				for(StatePair pairEntry : pairLookup.values())
 				{
@@ -258,6 +203,13 @@ else if(badPath.contains(pairEntry.pair))
 
 		private Dependencies deps;
 
+		public EquivTestDependency (DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv, 
+				HashSet<List<Integer>> path, Dependencies deps)
+		{
+			super(equivClasses, equiv, path);
+			this.deps = deps;
+		}
+
 		public EquivTestDependency (DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv, 
 				HashSet<List<Integer>> path)
 		{
@@ -272,7 +224,7 @@ public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
 			{
 				return false;
 			}
-			EquivRecord start = new EquivRecord(pStart,qStart,path,equiv);
+			EquivRecord start = new EquivRecord(pStart,qStart,path);
 			Stack<EquivRecord> testStack = new Stack<EquivRecord>();
 			testStack.add(start);
 			while (!testStack.isEmpty())
@@ -281,7 +233,6 @@ public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
 				Integer p = curEquivTest.pState;
 				Integer q = curEquivTest.qState;
 				HashSet<List<Integer>> curPath = curEquivTest.curPath;
-				HashSet<List<Integer>> curEquiv = curEquivTest.curEquiv;
 				List<Integer> pair = normalize(p,q);
 				HashSet<List<Integer>> newPath = new HashSet<List<Integer>>(curPath);
 				newPath.add(pair);
@@ -295,30 +246,30 @@ public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
 					Integer pNextClass = equivClasses.find(pMove.to);
 					Integer qNextClass = equivClasses.find(qMove.to);
 					List<Integer> nextPair = normalize(pNextClass, qNextClass);
-					if(!pNextClass.equals(qNextClass) && !equiv.contains(nextPair))
+					if(equiv.contains(nextPair) || path.contains(nextPair))
+					{
+						deps.addDependency(pair, nextPair);
+					}
+					else if(!pNextClass.equals(qNextClass))
 					{
 						if(isKnownNotEqual(pNextClass,qNextClass))
 						{
-
 							newPath.add(nextPair);
+							for(List<Integer> pathPair : path)
+							{
+								neq.add(pathPair); //TODO: remove this call from outer minimize method
+							}
 							this.path = newPath;
 							deps.mergeStates(newPath);
 							return false;
 						}
-						if (!newPath.contains(nextPair))
+						else
 						{
-							HashSet<List<Integer>> nextEquiv = new HashSet<List<Integer>>(curEquiv);
 							equiv.add(nextPair);
-							nextEquiv.add(nextPair); 
-							EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath, nextEquiv);
-							testStack.push(nextTest);
-							deps.addDependency(pair, nextPair);
+							EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath);
+							testStack.add(nextTest);
 						}
 					}
-					else if(equiv.contains(nextPair))
-					{
-						deps.addDependency(pair, nextPair);
-					}
 					outp.remove(pMove);
 					outq.remove(qMove);
 					P newPGuard = ba.MkAnd(pMove.guard, ba.MkNot(qMove.guard));
@@ -332,7 +283,6 @@ else if(equiv.contains(nextPair))
 						outq.add(new SFAInputMove<P,S>(qMove.from, qMove.to, newQGuard));
 					}
 				}
-				//deps.satisfyDependency(pair);
 			}
 			equiv.add(normalize(pStart, qStart));
 			return true;