Adding more documentation to code

IncrementalMinimization/scripts/budget_graph.py

@@ -1,8 +1,11 @@
 import matplotlib.pyplot as pyplot
 import matplotlib.ticker as mtick
-
 import sys
 
+'''
+Generates bar graph for budget graph.
+'''
+
 xAxis = "Number of States"
 yAxis = "Average Amount of Minimization Completed"
 title = "Comparison of Incremental Minimization Rates"

IncrementalMinimization/scripts/compare_data.py

@@ -1,5 +1,9 @@
 import sys
 
+'''
+Script used to compare separate runs of the same test to compare for improvement.
+'''
+
 file1 = sys.argv[1]
 file2 = sys.argv[2]
 base_index = int(sys.argv[3])
@@ -24,7 +28,8 @@ f1Data = [[toNum(datum) for datum in row.split(',') if datum]
 f2Data = [[toNum(datum) for datum in row.split(',') if datum]
           for row in f2[1:] if row]
 
-good = 0
+
+"""good = 0
 bad = 0
 for row in f1Data:
     if row[0] > 50 and row[1] < 150 and row[0] == row[1]:
@@ -33,19 +38,18 @@ for row in f1Data:
         else:
             bad +=1
 print(good)
-print(bad)
+print(bad)"""
 
 
 f1Average = 0
 f2Average = 0
 f1Min = max([row[base_index] for row in f1Data])
-print("adsadad")
 f1Max = 0
-negs = []
+pos = []
 count = 0.0
 for row in range(0,min(len(f1Data),len(f2Data))):
-    if f1Data[row][0] < 50:
-        continue
+    if (f1Data[row][0] < 320 or f1Data[row][0] > 400):
+	continue
     count += 1
     if f1Data[row][:4] != f2Data[row][:4]:
         if len(f1Data) > len(f2Data):
@@ -61,18 +65,18 @@ for row in range(0,min(len(f1Data),len(f2Data))):
         f1Min = f1Comp
     if f1Comp > f1Max:
         f1Max = f1Comp
-    if f1Comp <= 0:
-        negs.append(f1Data[row])
+    if f1Comp > 0:
+    	pos.append(f1Data[row])
     if count == 0:
         f1Average = f1Comp
         f2Average = f2Comp
     else:
-        count += 1.0
         f1Average += (f1Comp - f1Average)/count
         f2Average += (f2Comp - f2Average)/count
-        
-for n in negs:
+
+for n in pos:
     print n
+print(len(pos))
 print('avg')
 print(f1Average)
 print('min')

IncrementalMinimization/scripts/generate_line_graph.py

@@ -1,9 +1,14 @@
 import matplotlib.pyplot as pyplot
 import sys
 
+'''
+Generates standard line graph for comparison of runtimes.
+Could be improved for better/smoother visualization
+'''
+
 xAxis = "Number of States"
 yAxis = "Average Minimization Time (ms)"
-title = "Comparison of Incremental SFA Minimization Algorithms"
+title = "Comparison of Incremental Algorithms"
 scale = "log"
 
 testsfile = sys.argv[1]
@@ -15,7 +20,7 @@ def toNum(s):
     if s.isdigit():
         return int(s)
     else:
-        return float(s)
+        return float(s)/1000
 
 def mergeData(data, index):
     data.sort(key = lambda x: x[index])
@@ -49,7 +54,7 @@ print(sum(average_mins)/len(average_mins))
 
 fData = mergeData(fData, xIndex)
 
-lineStyles = ['-','--','-.',':'] #Different line style markers
+lineStyles = ['-','--',':',':'] #Different line style markers
 
 xData = [row[xIndex] for row in fData if row[xIndex] <= cutoff]
 style_num = 0

IncrementalMinimization/scripts/record_graph.py

@@ -1,12 +1,15 @@
 import numpy
 import matplotlib.pyplot as pyplot
 import matplotlib.colors as colors
-
 import sys
 
+'''
+Script generates record/heatmap graph.
+'''
+
 xAxis = "Percentage of Automata Minimized"
-yAxis = "Number of States"
-title = "Progress of Naive Incremental Minimization"
+yAxis = "Number of States in Automaton"
+title = "Progress of Efficient Incremental Minimization"
 
 testsfile = sys.argv[1]
 
@@ -33,6 +36,8 @@ for row in fStrings[1:]:
 	maxTime = toNum(row[-2])
         for time in row[1:-1]:
             percent = toNum(time)/maxTime*100
+            if time == maxTime:
+                 assert(percent==100)
             z.append(percent)
             y.append(states)
 

IncrementalMinimization/src/minimization/DebugException.java

@@ -2,6 +2,9 @@ package minimization;
 
 public class DebugException extends Exception
 {
+	//Exception used for debug and testing purposes.
+	//Specifically, used for depth test
+
 	private final Integer maxDepth;
 
 	public DebugException (String message, Integer maxDepth)

IncrementalMinimization/src/minimization/MinimizationAlgorithm.java

@@ -6,5 +6,7 @@ import automata.sfa.SFA;
 
 public interface MinimizationAlgorithm <P,S>
 {
-	public SFA<P,S> minimize() throws TimeoutException, DebugException;
+	//Interface for minimization algorithms, useful for testing
+
+	public SFA<P,S> minimize() throws TimeoutException;
 }

IncrementalMinimization/src/minimization/MooreMinimization.java

@@ -16,6 +16,9 @@ import automata.sfa.SFAMove;
 
 public class MooreMinimization<P,S> implements MinimizationAlgorithm<P,S>
 {
+	//Adaptation of Moore's algorithm to SFAs
+	//Implemented as described in "Minimization of Symbolic Automata" by D'Antoni and Veanes
+
 	public static <P,S> SFA<P,S> mooreMinimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba) throws TimeoutException
 	{
 		MooreMinimization<P,S> moore = new MooreMinimization<P,S>(aut, ba);
@@ -147,7 +150,6 @@ public class MooreMinimization<P,S> implements MinimizationAlgorithm<P,S>
 			{
 				SFAInputMove<P,S> newt = new SFAInputMove<P,S>(p, stateEquiv.get(t.to), t.guard);
 				newTransitions.add(newt);
-				//System.out.println(newt);
 			}
 		}
 		SFA<P,S> minAut = SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba);

IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java

@@ -10,10 +10,10 @@ import theory.BooleanAlgebra;
 import automata.sfa.SFA;
 
 /*
- * CLASS FOR TESTING PURPOSES ONLY
- * 
  * This class uses a naive non-equivalence check that initially only checks
  * whether or not the given pair contains one final and one non-final state.
+ * 
+ * Class for comparison purposes only
  */
 
 public class IncrSimpleNEQ<P,S> extends IncrementalMinimization<P,S>

IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java

@@ -16,8 +16,21 @@ import automata.sfa.SFAInputMove;
 
 public class IncrWithDependencyChecks<P,S> extends IncrementalMinimization<P,S>
 {
+	/*
+	 * Non-recursive incremental minimization with dependency checking
+	 * 
+	 * Key idea: whenever a pair of states (p,q) is tested in an equivalence test, if it does not return false
+	 * then for all successor pairs (p',q') either we already know p'=q' or we have (p',q') in equiv or 
+	 * (p',q') in path. In the cases where p'=/=q', we have that the equivalence of (p,q) is "dependent" on
+	 * the equivalence of (p',q'). By keeping track of this dependency relation in a directed graph, we may be
+	 * able to identify when a pair of states has been found to be equivalent even if the initial pair of states
+	 * tested are not equivalent.
+	 * 
+	 *   Currently not as efficient as non-recursive incremental minimization without dependency checking
+	 *   (given in IncrementalMinimization.java) but there is a lot of room for improvement and optimization.
+	 */
 
-	protected class EquivTestDependency extends EquivTest //tests for equality of two given states in the automata
+	protected class EquivTestDependency extends EquivTest
 	{
 
 		private DependencyGraph deps;
@@ -60,6 +73,8 @@ public class IncrWithDependencyChecks<P,S> extends IncrementalMinimization<P,S>
 					List<Integer> nextPair = normalize(pNextClass, qNextClass);
 					if(equiv.contains(nextPair) || curPath.contains(nextPair))
 					{
+						//Dependencies may be added to the dependency graph more often than is necessary to check for equivalence. 
+						//TODO: look into
 						deps.addDependency(pair, nextPair);
 					}
 					else if(!pNextClass.equals(qNextClass))
@@ -74,7 +89,8 @@ public class IncrWithDependencyChecks<P,S> extends IncrementalMinimization<P,S>
 							int result = deps.mergeStates(equivClasses, newPath);
 							if(result > 0)
 							{
-								System.out.println(String.format("Non-recursive alg merged %d pairs", result));
+								//Debug print, indicates when dependency checking actually merges pairs that would not have been found otherwise
+								System.out.println(String.format("Non-recursive dependency alg merged %d pairs", result));
 							}
 							this.path.clear();
 							return false;