diff --git a/IncrementalMinimization/scripts/budget_graph.py b/IncrementalMinimization/scripts/budget_graph.py index 7f985e21..842592a9 100644 --- a/IncrementalMinimization/scripts/budget_graph.py +++ b/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" diff --git a/IncrementalMinimization/scripts/compare_data.py b/IncrementalMinimization/scripts/compare_data.py index 58afc8b4..9bec8795 100644 --- a/IncrementalMinimization/scripts/compare_data.py +++ b/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') diff --git a/IncrementalMinimization/scripts/generate_line_graph.py b/IncrementalMinimization/scripts/generate_line_graph.py index cafce5fc..32c613e0 100644 --- a/IncrementalMinimization/scripts/generate_line_graph.py +++ b/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 diff --git a/IncrementalMinimization/scripts/record_graph.py b/IncrementalMinimization/scripts/record_graph.py index ea42a26d..68538964 100644 --- a/IncrementalMinimization/scripts/record_graph.py +++ b/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) diff --git a/IncrementalMinimization/src/minimization/DebugException.java b/IncrementalMinimization/src/minimization/DebugException.java index 0cef7a85..6c805ef1 100644 --- a/IncrementalMinimization/src/minimization/DebugException.java +++ b/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) diff --git a/IncrementalMinimization/src/minimization/MinimizationAlgorithm.java b/IncrementalMinimization/src/minimization/MinimizationAlgorithm.java index 06785ff9..a1543a9b 100644 --- a/IncrementalMinimization/src/minimization/MinimizationAlgorithm.java +++ b/IncrementalMinimization/src/minimization/MinimizationAlgorithm.java @@ -6,5 +6,7 @@ import automata.sfa.SFA; public interface MinimizationAlgorithm
{ - public SFA
minimize() throws TimeoutException, DebugException; + //Interface for minimization algorithms, useful for testing + + public SFA
minimize() throws TimeoutException; } diff --git a/IncrementalMinimization/src/minimization/MooreMinimization.java b/IncrementalMinimization/src/minimization/MooreMinimization.java index 84cdeeab..8f6bfbb8 100644 --- a/IncrementalMinimization/src/minimization/MooreMinimization.java +++ b/IncrementalMinimization/src/minimization/MooreMinimization.java @@ -16,6 +16,9 @@ import automata.sfa.SFAMove; public class MooreMinimization
implements MinimizationAlgorithm
{ + //Adaptation of Moore's algorithm to SFAs + //Implemented as described in "Minimization of Symbolic Automata" by D'Antoni and Veanes + public static
SFA
mooreMinimize(SFA
aut, BooleanAlgebra
ba) throws TimeoutException { MooreMinimization
moore = new MooreMinimization
(aut, ba); @@ -147,7 +150,6 @@ public class MooreMinimization
implements MinimizationAlgorithm
{ SFAInputMove
newt = new SFAInputMove
(p, stateEquiv.get(t.to), t.guard); newTransitions.add(newt); - //System.out.println(newt); } } SFA
minAut = SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba); diff --git a/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java b/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java index 2c284a1f..880b3fea 100644 --- a/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java +++ b/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
extends IncrementalMinimization
diff --git a/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java b/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java index 324b40ed..7e4ebcb0 100644 --- a/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java +++ b/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java @@ -16,8 +16,21 @@ import automata.sfa.SFAInputMove; public class IncrWithDependencyChecks
extends IncrementalMinimization
{ + /* + * 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
extends IncrementalMinimization
List extends IncrementalMinimization
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;
diff --git a/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java b/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java
index f42234c0..f5e66b62 100644
--- a/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java
+++ b/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java
@@ -26,14 +26,20 @@ import automata.sfa.SFAMove;
public class IncrementalMinimization implements MinimizationAlgorithm
{
+ //Base class for incremental minimization; implements the most efficient variant of the incremental algorithm
- protected class EquivTest //tests for equality of two given states in the automata
+ protected class EquivTest
{
+ //tests for equality of two given states in the automata
+
protected class EquivRecord
{
+ //Contains info (comparison states and path) that is passed recursively to isEquiv in the recursive implementation
+
public final Integer pState;
public final Integer qState;
public final HashSet implements MinimizationAlgorithm
protected final DisjointSets implements MinimizationAlgorithm
this.maxDepth = 0;
}
- protected List pMove = outp.iterator().next();
P pGuard = pMove.guard;
for(SFAInputMove qMove : outq)
@@ -92,7 +99,7 @@ public class IncrementalMinimization implements MinimizationAlgorithm
EquivRecord start = new EquivRecord(pStart,qStart,path);
Stack implements MinimizationAlgorithm
{
maxDepth += 1;
}
- Collection pMove = nonDisjointGuards.get(0);
SFAInputMove qMove = nonDisjointGuards.get(1);
Integer pNextClass = equivClasses.find(pMove.to);
Integer qNextClass = equivClasses.find(qMove.to);
- List implements MinimizationAlgorithm
this.path = newPath;
return false;
}
- if (!newPath.contains(nextPair))
+ if (!newPath.contains(nextPair)) //path containing next pair indicates a cycle of equivalence tests - we can not prove that this next pair is inequivalent (yet)
{
+ //Record created for next pair of states (assuming equivalence not already known) and added to test stack
equiv.add(nextPair);
EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath);
testStack.push(nextTest);
@@ -131,6 +141,8 @@ public class IncrementalMinimization implements MinimizationAlgorithm
}
outp.remove(pMove);
outq.remove(qMove);
+
+ //local minterm is now removed from outp and outq
P newPGuard = ba.MkAnd(pMove.guard, ba.MkNot(qMove.guard));
if (ba.IsSatisfiable(newPGuard))
{
@@ -143,7 +155,7 @@ public class IncrementalMinimization implements MinimizationAlgorithm
}
}
}
- equiv.add(normalize(pStart, qStart));
+ equiv.add(normalize(pStart, qStart)); //if no non-equivalent has been found, we assume the pair to be equivalent
return true;
}
@@ -169,6 +181,8 @@ public class IncrementalMinimization implements MinimizationAlgorithm
protected class StateComparator implements Comparator implements MinimizationAlgorithm
protected final SFA aut;
protected final BooleanAlgebra ba;
- protected final int num_pairs;
+ protected final int num_pairs; //number of pairs of states in automaton
- protected HashSet aut, BooleanAlgebra ba) throws TimeoutException
@@ -202,10 +216,11 @@ public class IncrementalMinimization implements MinimizationAlgorithm
aut = aut.determinize(ba);
}
this.aut = aut.mkTotal(ba);
+
this.ba = ba;
this.debug=false;
this.num_pairs = aut.getStates().size() * aut.getStates().size();
- this.neq = new HashSet implements MinimizationAlgorithm
protected LinkedHashMap implements MinimizationAlgorithm
protected Integer getStateDistanceToFinal(Integer state)
{
+ //wrapper for getting distance from distanceToFinalMap.
+ //Necessary because sink states (i.e. states w/o path to accepting state) are not included
+
if(distanceToFinalMap.containsKey(state))
{
return distanceToFinalMap.get(state);
@@ -274,6 +294,10 @@ public class IncrementalMinimization implements MinimizationAlgorithm
protected boolean isKnownNotEqual(Integer p, Integer q)
{
+ //tests whether states are known to be inequivalent.
+ //Implemented instead of simply checking for inclusion in neq - avoids needing to iterate through all pairs
+ //of states in distanceToFinalMap in order to add to neq.
+
List implements MinimizationAlgorithm
protected SFA mergeSFAStates(DisjointSets implements MinimizationAlgorithm
protected void timeCheck(long endTime, DisjointSets curAut = mergeSFAStates(equivClasses);
double exceeded = (new Double(System.nanoTime()-endTime))/1000000;
- System.out.println(String.format("Exceeded by %f ms", exceeded));
+ System.out.println(String.format("Budget exceeded by %f ms", exceeded));
throw new TimeBudgetExceededException(curAut);
/* Current time budget implementation intended to test % of automata minimization given
* a set period of time. However, it does not necessarily return this mostly minimized
* automata exactly after the budget is met (this is definitely possible, just not with
* present implementation), i.e. there will likely be a delay between the exceeding of time
- * budget and the returning of a partially minimized automata.
+ * budget and the returning of a partially minimized automata. No additional minimization
+ * occurs within this extra time though.
*/
}
}
public SFA minimize(long budget, boolean recordMinimization, boolean debug)
- throws TimeoutException, DebugException
+ throws TimeoutException, DebugException
{
+ //Actual minimization algorithm - returns minimum SFA of aut passed to constructor.
+
this.startTime = System.nanoTime();
this.debug = debug;
long endTime = startTime + budget;
@@ -347,7 +376,7 @@ public class IncrementalMinimization implements MinimizationAlgorithm
{
endTime = Long.MAX_VALUE;
}
- if(aut.isEmpty())
+ if(aut.isEmpty()) //catches edge case where aut is empty, i.e. accepts no language
{
if(recordMinimization)
{
@@ -356,10 +385,13 @@ public class IncrementalMinimization implements MinimizationAlgorithm
return SFA.getEmptySFA(ba);
}
DisjointSets implements MinimizationAlgorithm
//Already found p,q equivalent
continue;
}
- //TODO: look into efficiency of HashSet operations, ideally should be O(1) for searching, inserting, removing
timeCheck(endTime, equivClasses);
EquivTest pEquiv = makeEquivTest(equivClasses);
- boolean isequiv = pEquiv.isEquiv(p, q);
+ boolean isequiv = pEquiv.isEquiv(p, q); //isEquiv(p,q) computes whether p,q are equivalent states
HashSet implements MinimizationAlgorithm
{
throw new DebugException("finished first equiv test", pEquiv.getMaxDepth());
}
- timeCheck(endTime, equivClasses);
}
else
{
+ //p,q found non-equivalent. Other pairs may have been found non-equivalent.
timeCheck(endTime, equivClasses);
- //p,q found non-equivalent. Other pairs may be found non-equivalent.
for(List implements MinimizationAlgorithm
return minAut;
}
+ @Override
public SFA minimize() throws TimeoutException
{
return minimize(Long.MAX_VALUE);
@@ -444,6 +476,8 @@ public class IncrementalMinimization implements MinimizationAlgorithm
public LinkedHashMap extends IncrementalMinimization
{
+ //Naive implementation of incremental algorithm based on upfront computation of minterms
+ //Uses non-recursive equiv test
private class EquivTestNaive extends EquivTest
{
diff --git a/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java b/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java
index b8f18f12..3b34574b 100644
--- a/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java
+++ b/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java
@@ -20,6 +20,10 @@ import automata.sfa.SFAInputMove;
public class IncrementalRecWithDeps extends IncrementalMinimization
{
+ //Recursive Equivalence Test with dependency checking
+
+ //See IncrWithDependencyChecks.java for more info.
+
private class EquivTestRecursive extends EquivTest
{
private DependencyGraph deps;
@@ -50,7 +54,6 @@ public class IncrementalRecWithDeps extends IncrementalMinimization
List pMove = nonDisjointGuards.get(0);
SFAInputMove qMove = nonDisjointGuards.get(1);
- //note: we don't actually need to generate a witness, only need to know pMove,qMove are non-disjoint
Integer pNextClass = equivClasses.find(pMove.to);
Integer qNextClass = equivClasses.find(qMove.to);
List extends IncrementalMinimization
int mergeResults = deps.mergeStates(equivClasses, path);
if(mergeResults > 0)
{
- System.out.println(String.format("Recursive alg merged %d pairs", mergeResults));
+ //Debug print to identify when dependency checking actually merges pairs not already found
+ System.out.println(String.format("Recursive dependency alg merged %d pairs", mergeResults));
}
}
return finalResult;
diff --git a/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java b/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java
index bdc72b6e..b6f437f0 100644
--- a/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java
+++ b/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java
@@ -20,6 +20,8 @@ import automata.sfa.SFAInputMove;
public class IncrementalRecursive extends IncrementalMinimization
{
+ //Incremental algorithm with intuitive, recursive equiv test.
+
private class EquivTestRecursive extends EquivTest
{
public EquivTestRecursive(DisjointSets
{
+ //Structure used to generate the minterm set for an automaton.
+ //Implemented as described in "Minimization of Symbolic Automata" by D'Antoni and Veanes
+
public static ArrayList generate_minterms(SFA aut, BooleanAlgebra ba) throws TimeoutException
{
+ //Returns minterm list for the given SFA and algebra
+
MintermTree tree = new MintermTree (ba, ba.True());
for(SFAInputMove p : aut.getInputMovesFrom(aut.getStates()))
{
diff --git a/IncrementalMinimization/src/test/TestDisjointSets.java b/IncrementalMinimization/src/test/TestDisjointSets.java
index 553bc128..cc4166da 100644
--- a/IncrementalMinimization/src/test/TestDisjointSets.java
+++ b/IncrementalMinimization/src/test/TestDisjointSets.java
@@ -1,13 +1,13 @@
package test;
-import static org.junit.Assert.*;
import junit.framework.Assert;
-import org.junit.Before;
import org.junit.Test;
import structures.DisjointSets;
-public class TestDisjointSets {
+public class TestDisjointSets
+{
+ //Unit tests for DisjointSets
DisjointSets minAut = null;
- try
- {
- minAut = minAlg.minimize();
- }
- catch (DebugException e)
- {
- //This should never happen here
- }
+ minAut = minAlg.minimize();
Double finishTime = ((double)(System.nanoTime() - startTime)/1000000);
- //System.out.println(stdMinAut);
- //System.out.println(minAut);
Assert.assertNotNull(minAut);
Assert.assertTrue(SFA.areEquivalent(minAut, stdMinAut, ba));
Assert.assertTrue(minAut.stateCount() <= stdMinAut.stateCount());
@@ -182,6 +181,8 @@ public class TestIncrementalMinimization
@Test
public void testDep() throws TimeoutException
{
+ //Specific test of minimizing automaton with dependency checking that has been found to often reach edge cases.
+
String regex = "(\\s*\\S*){2}(ipsum)(\\S*\\s*){2}";
UnaryCharIntervalSolver ba = new UnaryCharIntervalSolver();
SFA> curPath;
+ //path set isn't actually passed recursively in recursive algorithm but the way it is modified does assume recursive traversal
public EquivRecord(Integer p, Integer q, HashSet
> curPath)
{
@@ -50,10 +56,10 @@ public class IncrementalMinimization
> equiv;
- protected HashSet
> path;
+ protected HashSet
> equiv; //Set contains all pairs of states assumed to be equivalent.
+ protected HashSet
> path; //In recursive algorithm, tracks path from initial pair to current pair in recursive call tree.
- private int maxDepth;
+ private int maxDepth; //only used for testing
public EquivTest(DisjointSets
> equiv,
HashSet
> path)
@@ -64,11 +70,12 @@ public class IncrementalMinimization
> neq;
- protected StateComparator stateComp;
+ protected HashSet
> neq; //contains all pairs of states known not to be equivalent
+ protected StateComparator stateComp; //custom state comparator
private LinkedHashMap
>(num_pairs, 0.9f); //won't exceed initial capacity
+ this.neq = new HashSet
>(num_pairs, 0.9f); //shouldn't exceed initial capacity
this.distanceToFinalMap = generateDistanceToFinalMap();
this.stateComp = new StateComparator();
this.startTime = null;
@@ -235,6 +250,8 @@ public class IncrementalMinimization
> equiv = pEquiv.getEquiv();
HashSet
> path = pEquiv.getPath();
if(isequiv)
{
- //p,q found equivalent. Other pairs may be found equivalent.
+ //p,q found equivalent. Other pairs may have been found equivalent.
+ timeCheck(endTime, equivClasses);
for(List
> equiv,
diff --git a/IncrementalMinimization/src/structures/DependencyGraph.java b/IncrementalMinimization/src/structures/DependencyGraph.java
index 0cc3a82a..58de9b6f 100644
--- a/IncrementalMinimization/src/structures/DependencyGraph.java
+++ b/IncrementalMinimization/src/structures/DependencyGraph.java
@@ -11,8 +11,15 @@ import org.sat4j.specs.TimeoutException;
public class DependencyGraph
{
- protected class StatePair //Nodes in graph
+ /*
+ * Tracks dependency relation on pairs of states when testing for equivalence with dependency checking.
+ * Lots of room for optimization.
+ */
+
+ protected class StatePair
{
+ //Nodes in graph
+
public final List
,StatePair> pairLookup;
+ private HashMap
,StatePair> pairLookup; //pair of state integers mapped to node in graph
public DependencyGraph()
{
@@ -97,6 +104,8 @@ public class DependencyGraph
public void addDependency(List
> badPairs) throws TimeoutException
{
+ //Checks if all dependencies on the given pair has been satisfied. If so, merges them,
Queue
> badPath) throws TimeoutException
{
+ //Checks for all pairs of states that can be merged.
+ //Badpath represents path that an isEquiv test returns false on. Pairs in this path are necessarily non-equivalent.
+
int result = 0;
for(StatePair pairEntry : pairLookup.values())
{
diff --git a/IncrementalMinimization/src/structures/DisjointSets.java b/IncrementalMinimization/src/structures/DisjointSets.java
index b30f7da2..4eb97837 100644
--- a/IncrementalMinimization/src/structures/DisjointSets.java
+++ b/IncrementalMinimization/src/structures/DisjointSets.java
@@ -4,14 +4,13 @@ import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
-
public class DisjointSets