diff --git a/IncrementalMinimization/src/IncrementalMinimization.java b/IncrementalMinimization/src/IncrementalMinimization.java index 1c03f236..c365dbdb 100644 --- a/IncrementalMinimization/src/IncrementalMinimization.java +++ b/IncrementalMinimization/src/IncrementalMinimization.java @@ -12,6 +12,7 @@ import theory.BooleanAlgebra; import theory.intervals.IntPred; import theory.intervals.IntegerSolver; +import utilities.Pair; import automata.sfa.SFA; import automata.sfa.SFAInputMove; import automata.sfa.SFAMove; @@ -33,7 +34,7 @@ public TimeBudgetExceeded(SFA returnAut) { this("Time budget exceeded", returnAut); } - + public SFA getReturnAut() { return returnAut; @@ -143,6 +144,158 @@ public HashSet> getPath() } } + private static class EquivTestUpfront + { + private static class MintermTree + { + private final BooleanAlgebra ba; + + private P root_pred; + private MintermTree left; + private MintermTree right; + + public MintermTree(BooleanAlgebra ba, P root_pred) + { + this.ba = ba; + this.root_pred = root_pred; + left = null; + right = null; + } + + public boolean isLeaf() + { + return (left == null); //no single children are ever added, so this is a sufficient check + } + + public void refine(P pred) throws TimeoutException + { + P predAnd = ba.MkAnd(root_pred, pred); + P predAndNot = ba.MkAnd(root_pred, ba.MkNot(pred)); + if (ba.IsSatisfiable(predAnd) && ba.IsSatisfiable(predAndNot)) + { + if (isLeaf()) + { + this.left = new MintermTree(ba, predAnd); + this.right = new MintermTree(ba, predAndNot); + } + else + { + left.refine(pred); + right.refine(pred); + } + } + } + + public ArrayList

getMinterms() + { + ArrayList

minterms = new ArrayList

(); + if (isLeaf()) + { + minterms.add(root_pred); + } + else + { + minterms.addAll(left.getMinterms()); + minterms.addAll(right.getMinterms()); + } + return minterms; + } + + } + + public static ArrayList

generate_minterms(SFA aut, BooleanAlgebra ba) throws TimeoutException + { + MintermTree tree = new MintermTree(ba, ba.True()); + for(SFAInputMove p : aut.getInputMovesFrom(aut.getStates())) + { + tree.refine(p.guard); + } + return tree.getMinterms(); + } + + private final SFA aut; + private final BooleanAlgebra ba; + private final DisjointSets equivClasses; + private final ArrayList

minterms; + + private HashSet> neq; + private HashSet> equiv; + private HashSet> path; + + public EquivTestUpfront(SFA aut, BooleanAlgebra ba, DisjointSets equivClasses, + ArrayList

minterms, HashSet> neq, HashSet> equiv, + HashSet> path) + { + this.aut = aut; + this.ba = ba; + this.equivClasses = equivClasses; + this.minterms = minterms; + this.neq = neq; + this.equiv = equiv; + this.path = path; + } + + private Integer mintermTransition(Integer state, P minterm) throws TimeoutException + { + Integer toState = null; + for (SFAInputMove t : aut.getInputMovesFrom(state)) + { + if (ba.IsSatisfiable(ba.MkAnd(minterm, t.guard))) + { + //aut is deterministic and complete. So, always one and exactly one transition per minterm. + toState = t.to; + break; + } + } + assert(toState != null); + return toState; + } + + public boolean isEquiv(Integer p, Integer q) throws TimeoutException, TimeBudgetExceeded + { + List pair = normalize(p,q); //Should already be normalized + if (neq.contains(pair)) + { + return false; + } + if (path.contains(pair)) + { + return true; + } + path.add(pair); + for (P minterm : minterms) + { + Integer pNextClass = equivClasses.find(mintermTransition(p, minterm)); + Integer qNextClass = equivClasses.find(mintermTransition(q, minterm)); + List nextPair = normalize(pNextClass, qNextClass); + if (!pNextClass.equals(qNextClass) && !equiv.contains(nextPair)) + { + equiv.add(nextPair); + if(!isEquiv(pNextClass, qNextClass)) + { + return false; + } + else + { + path.remove(nextPair); + } + } + } + equiv.add(pair); + return true; + } + + public HashSet> getEquiv() + { + return equiv; + } + + public HashSet> getPath() + { + return path; + } + } + private static List normalize(Integer p, Integer q) { List pair; @@ -181,9 +334,28 @@ private static SFA mergeSFAStates(DisjointSets equivClasses, return minAut; } - public static SFA minimize(SFA aut, BooleanAlgebra ba, long budget) + private static void timeCheck(SFA aut, BooleanAlgebra ba, + DisjointSets equivClasses, long endTime) throws TimeoutException + { + if(System.nanoTime() > endTime) + { + //Time Budget exceeded + SFA curAut = mergeSFAStates(equivClasses, aut, ba); + double exceeded = (new Double(System.nanoTime()-endTime))/1000000; + System.out.println(String.format("Exceeded by %f ms", exceeded)); + throw new TimeBudgetExceeded(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 deinitiely possible, just not with + * present implementation). + */ + } + } + + public static SFA minimize(SFA aut, BooleanAlgebra ba, long budget, boolean upfront) throws TimeoutException { + long endTime = System.nanoTime() + budget; if (endTime < 0) //indicates overflow { @@ -198,12 +370,17 @@ public static SFA minimize(SFA aut, BooleanAlgebra ba, l aut = aut.determinize(ba); } aut = aut.mkTotal(ba); + ArrayList

upfront_minterms = null; + if(upfront) + { + upfront_minterms = EquivTestUpfront.generate_minterms(aut, ba); + } + int num_pairs = aut.getStates().size() * aut.getStates().size(); //n^2 where n is # of states DisjointSets equivClasses = new DisjointSets(); for(Integer q : aut.getStates()) { equivClasses.make(q); } - int num_pairs = aut.getStates().size() * aut.getStates().size(); //n^2 where n is # of states HashSet> neq = new HashSet>(num_pairs, 0.9f); //set is given initial capacity of n^2, won't exceed this for(Integer p : aut.getFinalStates()) { @@ -233,32 +410,39 @@ else if(equivClasses.find(p) == equivClasses.find(q)) //TODO: look into efficiency of HashSet operations, ideally should be O(1) for searching, inserting, removing HashSet> equiv = new HashSet>(num_pairs,0.9f); HashSet> path = new HashSet>(num_pairs,0.9f); - EquivTest pEquiv = new EquivTest(aut, ba, equivClasses, neq, equiv, path); + timeCheck(aut, ba, equivClasses, endTime); boolean isequiv; - isequiv = pEquiv.isEquiv(p, q); + if(!upfront) + { + EquivTest pEquiv = new EquivTest(aut, ba, equivClasses, neq, equiv, path); + isequiv = pEquiv.isEquiv(p, q); + equiv = pEquiv.getEquiv(); + path = pEquiv.getPath(); + } + else + { + EquivTestUpfront pEquivUpfront = new EquivTestUpfront(aut, ba, equivClasses, + upfront_minterms, neq, equiv, path); + isequiv = pEquivUpfront.isEquiv(p,q); + equiv = pEquivUpfront.getEquiv(); + path = pEquivUpfront.getPath(); + } if(isequiv) { //p,q found equivalent. Other pairs may be found equivalent. - for(List equivPair : pEquiv.getEquiv()) + for(List equivPair : equiv) { - if(System.nanoTime() >= endTime) - { - //Time Budget exceeded - SFA curAut = mergeSFAStates(equivClasses, aut, ba); - throw new TimeBudgetExceeded(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 deinitiely possible, just not with - * present implementation). - */ - } equivClasses.union(equivPair.get(0), equivPair.get(1)); + //equivClasses.union(equivPair.get(0), equivPair.get(1)); } + timeCheck(aut, ba, equivClasses, endTime); + //after equiv merging for soft time budget? } else { + timeCheck(aut, ba, equivClasses, endTime); //p,q found non-equivalent. Other pairs may be found non-equivalent. - for(List pathPair : pEquiv.getPath()) + for(List pathPair : path) { neq.add(pathPair); } @@ -266,35 +450,15 @@ else if(equivClasses.find(p) == equivClasses.find(q)) } } - /* new SFA created with minimum states - HashMap> classes = equivClasses.getSets(); - Set newStates = classes.keySet(); - Collection> newTransitions = new LinkedList>(); - Collection newFinalStates = new HashSet(); - for (Integer p : newStates) - { - for (SFAInputMove t : aut.getInputMovesFrom(classes.get(p))) - { - newTransitions.add(new SFAInputMove(p, equivClasses.find(t.to), t.guard)); - } - if(aut.isFinalState(p)) - { - newFinalStates.add(p); - } - } - Integer newInitialState = equivClasses.find(aut.getInitialState()); - SFA minAut = SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba, false); - return minAut; */ - return mergeSFAStates(equivClasses, aut, ba); } - public static SFA incrementalMinimize(SFA aut, BooleanAlgebra ba, long budget) + public static SFA incrementalMinimize(SFA aut, BooleanAlgebra ba, long budget, boolean upfront) throws TimeoutException { try { - return minimize(aut, ba, budget); + return minimize(aut, ba, budget, upfront); } catch(TimeBudgetExceeded e) { @@ -302,9 +466,15 @@ public static SFA incrementalMinimize(SFA aut, BooleanAlgebra SFA incrementalMinimize(SFA aut, BooleanAlgebra ba, boolean upfront) throws TimeoutException + { + return incrementalMinimize(aut, ba, Long.MAX_VALUE, upfront); + } + public static SFA incrementalMinimize(SFA aut, BooleanAlgebra ba) throws TimeoutException { - return incrementalMinimize(aut, ba, Long.MAX_VALUE); //Default time budget 200+ years (i.e. there is none) + return incrementalMinimize(aut, ba, Long.MAX_VALUE, false); //Default time budget 200+ years (i.e. there is none) } + //TODO: refactor, make class instantiable with above as constructors. } diff --git a/IncrementalMinimization/src/TestIncrementalMinimization.java b/IncrementalMinimization/src/TestIncrementalMinimization.java index 823bcf3f..60da73fb 100644 --- a/IncrementalMinimization/src/TestIncrementalMinimization.java +++ b/IncrementalMinimization/src/TestIncrementalMinimization.java @@ -1,9 +1,13 @@ import static org.junit.Assert.*; import java.io.BufferedReader; +import java.io.BufferedWriter; import java.io.FileNotFoundException; +import java.io.FileOutputStream; import java.io.FileReader; import java.io.IOException; +import java.io.OutputStreamWriter; +import java.io.Writer; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -15,8 +19,6 @@ import org.junit.Test; import org.sat4j.specs.TimeoutException; -import com.google.common.base.Stopwatch; - import benchmark.SFAprovider; import theory.BooleanAlgebra; @@ -80,11 +82,16 @@ public void testMyAut() throws TimeoutException { SFA incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); SFA stdMinAut = aut.minimize(ba); //auts are equivalent but incrMin is not determinstic! + SFA upfrontMinAut = IncrementalMinimization.incrementalMinimize(aut, ba, true); + Assert.assertTrue(incrMinAut.isDeterministic(ba)); Assert.assertTrue(stdMinAut.isDeterministic(ba)); + Assert.assertTrue(upfrontMinAut.isDeterministic(ba)); Assert.assertTrue(incrMinAut.getStates().size() <= stdMinAut.getStates().size()); + Assert.assertTrue(upfrontMinAut.getStates().size() <= stdMinAut.getStates().size()); Assert.assertTrue(SFA.areEquivalent(incrMinAut, aut, ba)); Assert.assertTrue(SFA.areEquivalent(incrMinAut, stdMinAut, ba)); + Assert.assertTrue(SFA.areEquivalent(upfrontMinAut, stdMinAut, ba)); } @Test @@ -124,8 +131,12 @@ public void testCharPred() throws TimeoutException } @Test - public void testRegEx() throws TimeoutException, IOException + public void testCompare() throws TimeoutException, IOException { + System.out.println("========================"); + System.out.println("STARTING COMPARISON TEST"); + System.out.println("========================"); + //import list of regex. Heavily borrowed code from symbolic automata library FileReader regexFile = new FileReader("src/regexlib-SFA.txt"); BufferedReader read = new BufferedReader(regexFile); @@ -144,9 +155,25 @@ public void testRegEx() throws TimeoutException, IOException UnaryCharIntervalSolver ba = new UnaryCharIntervalSolver(); //System.out.println(regexList.size()); ArrayList messageList = new ArrayList(); + long timeout = 3600000; //determinization timeout = 1 hour for (String regex : regexList) { SFA aut = (new SFAprovider(regex, ba)).getSFA(); + try + { + aut = aut.determinize(ba, timeout); + aut = aut.mkTotal(ba); + } + catch(TimeoutException e) + { + continue; + } + catch(OutOfMemoryError e) + { + System.gc(); + continue; + } + System.out.println("Determinized"); //incremental minimization long incrStart = System.nanoTime(); @@ -166,24 +193,60 @@ public void testRegEx() throws TimeoutException, IOException continue; } Double incrTime = ((double)(System.nanoTime() - incrStart)/1000); + System.out.println("Incremental minimized."); + + //DFAized incremental minimization + long incrDFAStart = System.nanoTime(); + SFA upfrontMinAut; + try + { + upfrontMinAut = IncrementalMinimization.incrementalMinimize(aut, ba, true); + } + catch(TimeoutException e) + { + System.out.println("Skipping because of Timeout Exception"); //TODO Debug + continue; + } + catch(OutOfMemoryError e) + { + System.out.println("Skipping because out of heap space"); //TODO Debug + continue; + } + Double upfrontTime = ((double)(System.nanoTime() - incrDFAStart)/1000); + System.out.println("Upfront Incremental minimized."); //standard minimization long stdStart = System.nanoTime(); SFA stdMinAut; stdMinAut = aut.minimize(ba); Double stdTime = ((double)(System.nanoTime() - stdStart)/1000); + System.out.println("Standard minimized."); //moore minimization long mooreStart = System.nanoTime(); SFA mooreMinAut; mooreMinAut = MooreMinimization.mooreMinimize(aut, ba); Double mooreTime = ((double)(System.nanoTime() - mooreStart)/1000); + System.out.println("Moore minimized."); Assert.assertTrue(incrMinAut.isDeterministic(ba)); Assert.assertTrue(SFA.areEquivalent(incrMinAut, stdMinAut, ba)); Assert.assertTrue(incrMinAut.stateCount() <= stdMinAut.stateCount()); Assert.assertTrue(SFA.areEquivalent(mooreMinAut, stdMinAut, ba)); Assert.assertTrue(mooreMinAut.stateCount() <= stdMinAut.stateCount()); + Assert.assertTrue(incrMinAut.stateCount() <= stdMinAut.stateCount()); + Assert.assertTrue(SFA.areEquivalent(incrMinAut, stdMinAut, ba)); + try + { + Assert.assertTrue(upfrontMinAut.stateCount() == incrMinAut.stateCount()); + } + catch (AssertionError e) + { + System.out.println(stdMinAut.stateCount()); + System.out.println(incrMinAut.stateCount()); + System.out.println(upfrontMinAut.stateCount()); + } + Assert.assertTrue(SFA.areEquivalent(upfrontMinAut, stdMinAut, ba)); String initialStateCount = Integer.toString(aut.stateCount()); String transCount = Integer.toString(aut.getTransitionCount()); @@ -198,17 +261,154 @@ public void testRegEx() throws TimeoutException, IOException ArrayList predList = new ArrayList(predSet); String mintermCount = Integer.toString(ba.GetMinterms(predList).size()); - String message = "states: " + initialStateCount + " -> " + finalStateCount - + ", transition count: " + transCount + ", predicate count: " + predCount - + ", Minterms: " + mintermCount + ", incremental time: " + Double.toString(incrTime) - + ", Standard time: " + Double.toString(stdTime) - + ", moore time: " + Double.toString(mooreTime) + " (microsecs)"; + String message = String.format("%s, %s, %s, %s, %s, %s, %s, %s, %s", + initialStateCount, finalStateCount, transCount, predCount, mintermCount, + Double.toString(incrTime), Double.toString(stdTime), Double.toString(mooreTime), + Double.toString(upfrontTime)); + System.out.println(message); messageList.add(message); } + FileOutputStream file = new FileOutputStream("compare_test.txt"); + Writer writer = new BufferedWriter(new OutputStreamWriter(file)); + writer.write("initial states, final states, transition count, predicate count, minterm count," + + "incremental time, standard time, Moore time, upfront incremental time"); for (String msg : messageList) { + writer.write(msg + "\n"); + } + writer.close(); + } + + //@Test + public void testBudget() throws TimeoutException, IOException + { + //Similar to Regex test, but incremental minimization only given as long as + + System.out.println("========================="); + System.out.println("STARTING TIME BUDGET TEST"); + System.out.println("========================="); + + //import list of regex + FileReader regexFile = new FileReader("src/regexlib-SFA.txt"); + BufferedReader read = new BufferedReader(regexFile); + ArrayList regexList = new ArrayList(); + String line; + while(true) + { + line = read.readLine(); + if (line == null) + { + break; + } + regexList.add(line); + } + //regex converted to SFAs and minimized + UnaryCharIntervalSolver ba = new UnaryCharIntervalSolver(); + //System.out.println(regexList.size()); + ArrayList messageList = new ArrayList(); + long timeout = 3600000; //determinization timeout = 1 hour + for(String regex : regexList) + { + SFA aut = (new SFAprovider(regex, ba)).getSFA(); + try + { + aut = aut.determinize(ba, timeout); + aut = aut.mkTotal(ba); + } + catch(TimeoutException e) + { + continue; + } + catch(OutOfMemoryError e) + { + System.gc(); + continue; + } + System.out.println("Determinized."); + + //Standard minimiazation runs first + long stdStart = System.nanoTime(); + SFA stdMinAut; + long budget; + try + { + stdMinAut = aut.minimize(ba); + budget = System.nanoTime() - stdStart; + } + catch(TimeoutException e) + { + continue; + } + double bms = (new Double(budget))/1000000; + System.out.println(String.format("Standard minimization computed, budget: %f ms", bms)); + + //Incremental minimization runs with time budget of standard minimization + SFA incrMinAut; + SFA upfrontIncrAut; + try + { + incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba, budget, false); + System.out.println("Incremental minimized."); + upfrontIncrAut = IncrementalMinimization.incrementalMinimize(aut, ba, budget, true); + System.out.println("Upfront incremental minimized.."); + } + catch(TimeoutException e) + { + continue; + } + catch(OutOfMemoryError e) + { + continue; + } + + //TODO: negative percentages + + int initialCount = aut.stateCount(); + String initialStateCount = Integer.toString(initialCount); + int finalCount = stdMinAut.stateCount(); + String finalStateCount = Integer.toString(finalCount); + int incrCount = incrMinAut.stateCount(); + String incrStateCount= Integer.toString(incrCount); + int upfrontCount = upfrontIncrAut.stateCount(); + String upfrontStateCount = Integer.toString(upfrontCount); + + double incrPercentMinimized; + if (incrCount <= finalCount) + { + incrPercentMinimized = 1.; + } + else + { + incrPercentMinimized = ((double) initialCount - incrCount)/(initialCount - finalCount); + } + String incrPercent = Double.toString(incrPercentMinimized); + double upfPercentMinimized; + if (upfrontCount <= finalCount) + { + upfPercentMinimized = 1.; + } + else + { + upfPercentMinimized = ((double) initialCount - upfrontCount)/(initialCount - finalCount); + } + String upfPercent = Double.toString(upfPercentMinimized); + + String msg = String.format("%s, %s, %s, %s, %s, %s", + initialStateCount, finalStateCount, incrStateCount, upfrontCount, + incrPercent, upfPercent); + messageList.add(msg); System.out.println(msg); + Assert.assertTrue(incrPercentMinimized >= 0); + } + FileOutputStream file = new FileOutputStream("budget_test.txt"); + Writer writer = new BufferedWriter(new OutputStreamWriter(file)); + writer.write("initial states, final states, incremental states, upfront states" + + "incremental percent, upfront percent"); + for (String msg : messageList) + { + writer.write(msg + "\n"); } + writer.close(); } }