diff --git a/IncrementalMinimization/src/IncrementalMinimization.java b/IncrementalMinimization/src/IncrementalMinimization.java index 669a3285..053f2c8f 100644 --- a/IncrementalMinimization/src/IncrementalMinimization.java +++ b/IncrementalMinimization/src/IncrementalMinimization.java @@ -21,30 +21,7 @@ public class IncrementalMinimization { - @SuppressWarnings("rawtypes") //Throwable subclasses can not be made generic - private static class TimeBudgetExceeded extends TimeoutException - { - - private final SFA returnAut; - - public TimeBudgetExceeded(String message, SFA returnAut) - { - super(message); - this.returnAut = returnAut; - } - - public TimeBudgetExceeded(SFA returnAut) - { - this("Time budget exceeded", returnAut); - } - - public SFA getReturnAut() - { - return returnAut; - } - } - - private 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 { @@ -178,307 +155,9 @@ public Integer getMaxDepth() throws DebugException throw new DebugException("Not in debug"); } } - - private class EquivTestRecursive extends EquivTest - { - private class ResultDependencies - { - private boolean result; - private boolean isindependent; - private HashMap, Boolean> dependencyTest; //List of pairs of states that must be equivalent for current result to hold. - private HashSet> dependencies; - - public ResultDependencies(boolean result) - { - this.result = result; - this.isindependent = true; - this.dependencyTest = new HashMap, Boolean>(); - this.dependencies = new HashSet>(); - } - - public ResultDependencies(boolean result, List dependency) - { - this(result); - addDependency(dependency); - this.isindependent = false; - } - - public boolean resultIsIndependent() - { - return isindependent; - } - - public void addDependency(List pair) - { - if (isEquiv()) - { - dependencyTest.put(pair, false); - dependencies.add(pair); - isindependent = false; - } - else - { - throw new IllegalStateException("False result has no dependencies"); - } - } - - public void removeDependency(List pair) - { - dependencyTest.put(pair, true); - dependencies.remove(pair); - if (dependencies.isEmpty()) - { - isindependent = true; - } - } - - public boolean isDependency(List pair) - { - return dependencies.contains(pair); - } - - public void combineWithResult(ResultDependencies other) - { - result = result && other.isEquiv(); - if(!result) - { - dependencies.clear(); - } - else - { - HashMap, Boolean> otherDepends = other.getDependencyTests(); - for (List pair : otherDepends.keySet()) - { - Boolean otherSatisfied = otherDepends.get(pair); - if(otherSatisfied) - { - removeDependency(pair); - } - else - { - if(!dependencyTest.containsKey(pair)) - { - addDependency(pair); - } - else - { - if(!dependencyTest.get(pair)) - { - assert(isDependency(pair)); - } - } - } - } - } - } - - public boolean isEquiv() - { - return result; - } - - public HashMap, Boolean> getDependencyTests() - { - return dependencyTest; - } - - public void updateDepenencies() - { - List> checked = new LinkedList>(); - for (List pair : dependencies) - { - if(!path.contains(pair)) - { - dependencyTest.put(pair, true); - checked.add(pair); - } - } - dependencies.removeAll(checked); - } - } - - private HashMap, ResultDependencies> equivDepends; - public EquivTestRecursive(DisjointSets equivClasses, HashSet> equiv, - HashSet> path) - { - super(equivClasses, equiv, path); - this.equivDepends = new HashMap, ResultDependencies>(); - } - - public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutException - { - if (isKnownNotEqual(p,q)) - { - return new ResultDependencies(false); - } - List pair = normalize(p,q); - if (path.contains(pair)) - { - ResultDependencies r = new ResultDependencies(true); - r.addDependency(pair); - return r; - } - path.add(pair); - Collection> outp = new ArrayList>(aut.getInputMovesFrom(p)); - Collection> outq = new ArrayList>(aut.getInputMovesFrom(q)); - ResultDependencies thisResult = new ResultDependencies(true); - while (!outp.isEmpty() && !outq.isEmpty()) - { - List> nonDisjointGuards = findNonDisjointMoves(outp,outq); - SFAInputMove 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 nextPair = normalize(pNextClass, qNextClass); - if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair)) - { - equiv.add(nextPair); - equivDepends.put(nextPair, null); - if(path.contains(nextPair)) - { - thisResult.addDependency(nextPair); - } - else - { - ResultDependencies nextResult = isEquivRecursive(pNextClass, qNextClass); - if(!nextResult.isEquiv()) - { - return nextResult; - } - else - { - equivDepends.put(nextPair, nextResult); - path.remove(nextPair); - thisResult.combineWithResult(nextResult); - } - } - } - else if (equiv.contains(nextPair)) - { - ResultDependencies dependencies = equivDepends.get(nextPair); - if (dependencies == null && !pair.equals(nextPair)) - { - thisResult.addDependency(nextPair); - } - else if(!pair.equals(nextPair)) - { - thisResult.combineWithResult(dependencies); - } - } - outp.remove(pMove); - outq.remove(qMove); - P newPGuard = ba.MkAnd(pMove.guard, ba.MkNot(qMove.guard)); - if (ba.IsSatisfiable(newPGuard)) - { - outp.add(new SFAInputMove(pMove.from, pMove.to, newPGuard)); - } - P newQGuard = ba.MkAnd(qMove.guard, ba.MkNot(pMove.guard)); - if (ba.IsSatisfiable(newQGuard)) - { - outq.add(new SFAInputMove(qMove.from, qMove.to, newQGuard)); - } - } - thisResult.removeDependency(pair); - thisResult.updateDepenencies(); - if(thisResult.resultIsIndependent()) - { - equivClasses.union(p,q); - } - else - { - equiv.add(pair); - equivDepends.put(pair, thisResult); - } - return thisResult; - } - - @Override - public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException - { - ResultDependencies finalResult = isEquivRecursive(pStart, qStart); - return finalResult.isEquiv(); - } - } - - private class EquivTestUpfront extends EquivTest - { - - private final ArrayList

minterms; - - public EquivTestUpfront(DisjointSets equivClasses, ArrayList

minterms, - HashSet> equiv, HashSet> path) - { - super(equivClasses, equiv, path); - this.minterms = minterms; - } - - 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; - } - - @Override - public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException, TimeBudgetExceeded - { - if (isKnownNotEqual(pStart,qStart)) - { - return false; - } - EquivRecord start = new EquivRecord(pStart,qStart,path); - Stack testStack = new Stack(); - testStack.add(start); - while (!testStack.isEmpty()) - { - EquivRecord curEquivTest = testStack.pop(); - Integer p = curEquivTest.pState; - Integer q = curEquivTest.qState; - HashSet> curPath = curEquivTest.curPath; - List pair = normalize(p,q); - HashSet> newPath = new HashSet>(curPath); - newPath.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(isKnownNotEqual(pNextClass, qNextClass)) - { - return false; - } - if(!newPath.contains(nextPair)) - { - equiv.add(nextPair); - EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath); - testStack.push(nextTest); - } - } - } - } - equiv.add(normalize(pStart, qStart)); - return true; - } - - } - private class StateComparator implements Comparator { - public int compare(Integer a, Integer b) { int diff = distanceToFinalMap.get(a) - distanceToFinalMap.get(b); @@ -491,54 +170,11 @@ public int compare(Integer a, Integer b) return diff; } } - } - @SuppressWarnings("unchecked") - public static SFA incrementalMinimize(SFA aut, BooleanAlgebra ba, long budget, boolean upfront) - throws TimeoutException - { - try - { - IncrementalMinimization min = new IncrementalMinimization(aut, ba, false); - return min.minimize(budget, upfront, false, false); - } - catch(TimeBudgetExceeded e) - { - return e.getReturnAut(); - } - catch(DebugException e) - { - throw new RuntimeException(e); //impossible to get here. - } - } - - public static 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, false); //Default time budget 200+ years (i.e. there is none) - } - - public static SFA incrRecursiveMin(SFA aut, BooleanAlgebra ba) throws TimeoutException - { - IncrementalMinimization recMin = new IncrementalMinimization(aut,ba, false); - try - { - return recMin.minimize(Long.MAX_VALUE, false, false, true); - } - catch (DebugException e) - { - throw new RuntimeException(e); - } - } - - private final SFA aut; - private final BooleanAlgebra ba; - private final int num_pairs; + protected final SFA aut; + protected final BooleanAlgebra ba; + protected final int num_pairs; private HashSet> neq; private LinkedHashMap distanceToFinalMap; @@ -548,7 +184,7 @@ public static SFA incrRecursiveMin(SFA aut, BooleanAlgebra private Long singularRecord = null; private boolean debug; - public IncrementalMinimization(SFA aut, BooleanAlgebra ba, boolean debug) throws TimeoutException + public IncrementalMinimization(SFA aut, BooleanAlgebra ba) throws TimeoutException { if (!aut.isDeterministic()) { @@ -556,7 +192,7 @@ public IncrementalMinimization(SFA aut, BooleanAlgebra ba, boolean deb } this.aut = aut.mkTotal(ba); this.ba = ba; - this.debug=debug; + this.debug=false; this.num_pairs = aut.getStates().size() * aut.getStates().size(); this.neq = new HashSet>(num_pairs, 0.9f); //won't exceed initial capacity this.distanceToFinalMap = generateDistanceToFinalMap(); @@ -621,7 +257,14 @@ public String toString() return distanceMap; } - private List normalize(Integer p, Integer q) + protected EquivTest makeEquivTest(DisjointSets equivClasses) + { + HashSet> equiv = new HashSet>(num_pairs,0.9f); + HashSet> path = new HashSet>(num_pairs,0.9f); + return new EquivTest(equivClasses, equiv, path); + } + + protected List normalize(Integer p, Integer q) { List pair; if(stateComp.compare(p, q) < 0) @@ -635,12 +278,7 @@ private List normalize(Integer p, Integer q) return pair; } - private boolean isSinkState(Integer p) - { - return distanceToFinalMap.get(p) == Integer.MAX_VALUE; - } - - private boolean isKnownNotEqual(Integer p, Integer q) + protected boolean isKnownNotEqual(Integer p, Integer q) { List normalizedPair = normalize(p,q); if (neq.contains(normalizedPair)) @@ -658,7 +296,7 @@ else if (!distanceToFinalMap.get(p).equals(distanceToFinalMap.get(q))) } } - private SFA mergeSFAStates(DisjointSets equivClasses) throws TimeoutException + protected SFA mergeSFAStates(DisjointSets equivClasses) throws TimeoutException { //new SFA created with minimum states HashMap> classes = equivClasses.getSets(); @@ -681,13 +319,13 @@ private SFA mergeSFAStates(DisjointSets equivClasses) throws Timeo return minAut; } - private void updateRecord(DisjointSets equivClasses) + protected void updateRecord(DisjointSets equivClasses) { Long time = System.nanoTime(); record.put(time, equivClasses.getSets().size()); } - private void timeCheck(long endTime, DisjointSets equivClasses) throws TimeoutException + protected void timeCheck(long endTime, DisjointSets equivClasses) throws TimeoutException { if(System.nanoTime() > endTime) { @@ -695,7 +333,7 @@ private void timeCheck(long endTime, DisjointSets equivClasses) throws SFA curAut = mergeSFAStates(equivClasses); double exceeded = (new Double(System.nanoTime()-endTime))/1000000; System.out.println(String.format("Exceeded by %f ms", exceeded)); - throw new TimeBudgetExceeded(curAut); + 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 @@ -705,10 +343,11 @@ private void timeCheck(long endTime, DisjointSets equivClasses) throws } } - public SFA minimize(long budget, boolean upfront, boolean recordMinimization, boolean recursive) + public SFA minimize(long budget, boolean recordMinimization, boolean debug) throws TimeoutException, DebugException { this.startTime = System.nanoTime(); + this.debug = debug; long endTime = startTime + budget; if (endTime < 0) //indicates overflow { @@ -722,11 +361,6 @@ public SFA minimize(long budget, boolean upfront, boolean recordMinimizati } return SFA.getEmptySFA(ba); } - ArrayList

upfront_minterms = null; - if(upfront) - { - upfront_minterms = MintermTree.generate_minterms(aut, ba); - } DisjointSets equivClasses = new DisjointSets(); for(Integer q : aut.getStates()) { @@ -757,26 +391,11 @@ else if(equivClasses.find(p) == equivClasses.find(q)) continue; } //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); timeCheck(endTime, equivClasses); - EquivTest pEquiv; - if(upfront) - { - pEquiv = new EquivTestUpfront(equivClasses, upfront_minterms, equiv, path); - - } - else if (recursive) - { - pEquiv = new EquivTestRecursive(equivClasses, equiv, path); - } - else - { - pEquiv = new EquivTest(equivClasses, equiv, path); - } + EquivTest pEquiv = makeEquivTest(equivClasses); boolean isequiv = pEquiv.isEquiv(p, q); - equiv = pEquiv.getEquiv(); - path = pEquiv.getPath(); + HashSet> equiv = pEquiv.getEquiv(); + HashSet> path = pEquiv.getPath(); if(isequiv) { //p,q found equivalent. Other pairs may be found equivalent. @@ -809,6 +428,26 @@ else if (recursive) return mergeSFAStates(equivClasses); } + public SFA minimize(long budget) throws TimeoutException + { + SFA minAut = null; + try + { + minAut = minimize(budget, false, false); + } + catch (DebugException e) + { + //We never get a debug exception here. + } + assert(minAut != null); + return minAut; + } + + public SFA minimize() throws TimeoutException + { + return minimize(Long.MAX_VALUE); + } + public LinkedHashMap getRecord() throws TimeoutException { LinkedHashMap actualRecord = new LinkedHashMap(); diff --git a/IncrementalMinimization/src/IncrementalNaive.java b/IncrementalMinimization/src/IncrementalNaive.java new file mode 100644 index 00000000..93eda39b --- /dev/null +++ b/IncrementalMinimization/src/IncrementalNaive.java @@ -0,0 +1,101 @@ +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Stack; + +import org.sat4j.specs.TimeoutException; + +import theory.BooleanAlgebra; +import automata.sfa.SFA; +import automata.sfa.SFAInputMove; + + +public class IncrementalNaive extends IncrementalMinimization +{ + + private class EquivTestNaive extends EquivTest + { + + public EquivTestNaive(DisjointSets equivClasses, HashSet> equiv, + HashSet> path) + { + super(equivClasses, equiv, 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; + } + + @Override + public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException + { + if (isKnownNotEqual(pStart,qStart)) + { + return false; + } + EquivRecord start = new EquivRecord(pStart,qStart,path); + Stack testStack = new Stack(); + testStack.add(start); + while (!testStack.isEmpty()) + { + EquivRecord curEquivTest = testStack.pop(); + Integer p = curEquivTest.pState; + Integer q = curEquivTest.qState; + HashSet> curPath = curEquivTest.curPath; + List pair = normalize(p,q); + HashSet> newPath = new HashSet>(curPath); + newPath.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(isKnownNotEqual(pNextClass, qNextClass)) + { + return false; + } + if(!newPath.contains(nextPair)) + { + equiv.add(nextPair); + EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath); + testStack.push(nextTest); + } + } + } + } + equiv.add(normalize(pStart, qStart)); + return true; + } + } + + private final ArrayList

minterms; + + public IncrementalNaive(SFA aut, BooleanAlgebra ba) throws TimeoutException + { + super(aut,ba); + minterms = MintermTree.generate_minterms(aut, ba); + } + + @Override + protected EquivTest makeEquivTest(DisjointSets equivClasses) + { + HashSet> equiv = new HashSet>(num_pairs,0.9f); + HashSet> path = new HashSet>(num_pairs,0.9f); + return new EquivTestNaive(equivClasses, equiv, path); + } +} diff --git a/IncrementalMinimization/src/IncrementalRecursive.java b/IncrementalMinimization/src/IncrementalRecursive.java new file mode 100644 index 00000000..d9b3a069 --- /dev/null +++ b/IncrementalMinimization/src/IncrementalRecursive.java @@ -0,0 +1,252 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; + +import org.sat4j.specs.TimeoutException; + +import theory.BooleanAlgebra; +import automata.sfa.SFA; +import automata.sfa.SFAInputMove; + + +public class IncrementalRecursive extends IncrementalMinimization +{ + private class EquivTestRecursive extends EquivTest + { + private class ResultDependencies + { + private boolean result; + private boolean isindependent; + private HashMap, Boolean> dependencyTest; //List of pairs of states that must be equivalent for current result to hold. + private HashSet> dependencies; + + public ResultDependencies(boolean result) + { + this.result = result; + this.isindependent = true; + this.dependencyTest = new HashMap, Boolean>(); + this.dependencies = new HashSet>(); + } + + public ResultDependencies(boolean result, List dependency) + { + this(result); + addDependency(dependency); + this.isindependent = false; + } + + public boolean resultIsIndependent() + { + return isindependent; + } + + public void addDependency(List pair) + { + if (isEquiv()) + { + dependencyTest.put(pair, false); + dependencies.add(pair); + isindependent = false; + } + else + { + throw new IllegalStateException("False result has no dependencies"); + } + } + + public void removeDependency(List pair) + { + dependencyTest.put(pair, true); + dependencies.remove(pair); + if (dependencies.isEmpty()) + { + isindependent = true; + } + } + + public boolean isDependency(List pair) + { + return dependencies.contains(pair); + } + + public void combineWithResult(ResultDependencies other) + { + result = result && other.isEquiv(); + if(!result) + { + dependencies.clear(); + } + else + { + HashMap, Boolean> otherDepends = other.getDependencyTests(); + for (List pair : otherDepends.keySet()) + { + Boolean otherSatisfied = otherDepends.get(pair); + if(otherSatisfied) + { + removeDependency(pair); + } + else + { + if(!dependencyTest.containsKey(pair)) + { + addDependency(pair); + } + else + { + if(!dependencyTest.get(pair)) + { + assert(isDependency(pair)); + } + } + } + } + } + } + + public boolean isEquiv() + { + return result; + } + + public HashMap, Boolean> getDependencyTests() + { + return dependencyTest; + } + + public void updateDepenencies() + { + List> checked = new LinkedList>(); + for (List pair : dependencies) + { + if(!path.contains(pair)) + { + dependencyTest.put(pair, true); + checked.add(pair); + } + } + dependencies.removeAll(checked); + } + } + + private HashMap, ResultDependencies> equivDepends; + + public EquivTestRecursive(DisjointSets equivClasses, HashSet> equiv, + HashSet> path) + { + super(equivClasses, equiv, path); + this.equivDepends = new HashMap, ResultDependencies>(); + } + + public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutException + { + if (isKnownNotEqual(p,q)) + { + return new ResultDependencies(false); + } + List pair = normalize(p,q); + if (path.contains(pair)) + { + ResultDependencies r = new ResultDependencies(true); + r.addDependency(pair); + return r; + } + path.add(pair); + Collection> outp = new ArrayList>(aut.getInputMovesFrom(p)); + Collection> outq = new ArrayList>(aut.getInputMovesFrom(q)); + ResultDependencies thisResult = new ResultDependencies(true); + while (!outp.isEmpty() && !outq.isEmpty()) + { + List> nonDisjointGuards = findNonDisjointMoves(outp,outq); + SFAInputMove 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 nextPair = normalize(pNextClass, qNextClass); + if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair)) + { + equiv.add(nextPair); + equivDepends.put(nextPair, null); + if(path.contains(nextPair)) + { + thisResult.addDependency(nextPair); + } + else + { + ResultDependencies nextResult = isEquivRecursive(pNextClass, qNextClass); + if(!nextResult.isEquiv()) + { + return nextResult; + } + else + { + equivDepends.put(nextPair, nextResult); + path.remove(nextPair); + thisResult.combineWithResult(nextResult); + } + } + } + else if (equiv.contains(nextPair)) + { + ResultDependencies dependencies = equivDepends.get(nextPair); + if (dependencies == null && !pair.equals(nextPair)) + { + thisResult.addDependency(nextPair); + } + else if(!pair.equals(nextPair)) + { + thisResult.combineWithResult(dependencies); + } + } + outp.remove(pMove); + outq.remove(qMove); + P newPGuard = ba.MkAnd(pMove.guard, ba.MkNot(qMove.guard)); + if (ba.IsSatisfiable(newPGuard)) + { + outp.add(new SFAInputMove(pMove.from, pMove.to, newPGuard)); + } + P newQGuard = ba.MkAnd(qMove.guard, ba.MkNot(pMove.guard)); + if (ba.IsSatisfiable(newQGuard)) + { + outq.add(new SFAInputMove(qMove.from, qMove.to, newQGuard)); + } + } + thisResult.removeDependency(pair); + thisResult.updateDepenencies(); + if(thisResult.resultIsIndependent()) + { + equivClasses.union(p,q); + } + else + { + equiv.add(pair); + equivDepends.put(pair, thisResult); + } + return thisResult; + } + + @Override + public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException + { + ResultDependencies finalResult = isEquivRecursive(pStart, qStart); + return finalResult.isEquiv(); + } + } + + public IncrementalRecursive(SFA aut, BooleanAlgebra ba) throws TimeoutException + { + super(aut,ba); + } + + @Override + protected EquivTest makeEquivTest(DisjointSets equivClasses) + { + HashSet> equiv = new HashSet>(num_pairs,0.9f); + HashSet> path = new HashSet>(num_pairs,0.9f); + return new EquivTestRecursive(equivClasses, equiv, path); + } +} diff --git a/IncrementalMinimization/src/TestIncrementalMinimization.java b/IncrementalMinimization/src/TestIncrementalMinimization.java index 31bee3ba..3cfcb4a0 100644 --- a/IncrementalMinimization/src/TestIncrementalMinimization.java +++ b/IncrementalMinimization/src/TestIncrementalMinimization.java @@ -40,7 +40,8 @@ public class TestIncrementalMinimization { @Test - public void testMyAut() throws TimeoutException { + public void testMyAut() throws TimeoutException + { //our algebra is constructed IntegerSolver ba = new IntegerSolver(); IntPred neg = new IntPred(null, new Integer(0)); @@ -86,9 +87,11 @@ public void testMyAut() throws TimeoutException { //SFA is defined SFA aut = SFA.MkSFA(transitions, 0, Arrays.asList(7,8), ba); - SFA incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); + IncrementalMinimization incr = new IncrementalMinimization(aut,ba); + SFA incrMinAut = incr.minimize(); SFA stdMinAut = aut.minimize(ba); //auts are equivalent but incrMin is not determinstic! - SFA upfrontMinAut = IncrementalMinimization.incrementalMinimize(aut, ba, true); + IncrementalNaive naive = new IncrementalNaive(aut,ba); + SFA upfrontMinAut = naive.minimize(); Assert.assertTrue(incrMinAut.isDeterministic(ba)); Assert.assertTrue(stdMinAut.isDeterministic(ba)); @@ -127,7 +130,8 @@ public void testCharPred() throws TimeoutException SFA aut = SFA.MkSFA(transitions, 9, Arrays.asList(3,4), ba); aut = aut.determinize(ba).mkTotal(ba); - SFA incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); + IncrementalMinimization incr = new IncrementalMinimization(aut,ba); + SFA incrMinAut = incr.minimize(); System.out.println(incrMinAut.getStates()); SFA stdMinAut = aut.minimize(ba); System.out.println(stdMinAut.getStates()); @@ -203,18 +207,19 @@ public void testCompare() throws TimeoutException, IOException SFA incrMinAut; try { - incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); + IncrementalMinimization incrMin = new IncrementalMinimization(aut, ba); + incrMinAut = incrMin.minimize(); } catch(TimeoutException e) { System.out.println("Skipping because of Timeout Exception"); //TODO Debug continue; } - catch(OutOfMemoryError e) + /*catch(OutOfMemoryError e) { System.out.println("Skipping because out of heap space"); //TODO Debug continue; - } + }*/ Double incrTime = ((double)(System.nanoTime() - incrStart)/1000000); Assert.assertTrue(incrMinAut.isDeterministic(ba)); Assert.assertTrue(SFA.areEquivalent(incrMinAut, stdMinAut, ba)); @@ -228,18 +233,19 @@ public void testCompare() throws TimeoutException, IOException SFA upfrontMinAut; try { - upfrontMinAut = IncrementalMinimization.incrementalMinimize(aut, ba, true); + IncrementalNaive naiveMin = new IncrementalNaive(aut, ba); + upfrontMinAut = naiveMin.minimize(); } catch(TimeoutException e) { System.out.println("Skipping because of Timeout Exception"); //TODO Debug continue; } - catch(OutOfMemoryError e) + /*catch(OutOfMemoryError e) { System.out.println("Skipping because out of heap space"); //TODO Debug continue; - } + }*/ Double upfrontTime = ((double)(System.nanoTime() - incrDFAStart)/1000000); Assert.assertTrue(upfrontMinAut.stateCount() <= stdMinAut.stateCount()); Assert.assertTrue(SFA.areEquivalent(upfrontMinAut, stdMinAut, ba)); @@ -263,7 +269,8 @@ public void testCompare() throws TimeoutException, IOException SFA recursiveMinAut; try { - recursiveMinAut = IncrementalMinimization.incrRecursiveMin(aut, ba); + IncrementalRecursive incrRec = new IncrementalRecursive(aut, ba); + recursiveMinAut = incrRec.minimize(); } catch(TimeoutException e) { @@ -272,7 +279,16 @@ public void testCompare() throws TimeoutException, IOException } Double recTime = ((double)(System.nanoTime() - recStart)/1000000); Assert.assertTrue(recursiveMinAut.stateCount() <= stdMinAut.stateCount()); - Assert.assertTrue(SFA.areEquivalent(recursiveMinAut, stdMinAut, ba)); + try + { + Assert.assertTrue(SFA.areEquivalent(recursiveMinAut, stdMinAut, ba)); + } + catch(AssertionError e) + { + System.out.println(recursiveMinAut); + System.out.println(stdMinAut); + throw e; + } Assert.assertTrue(SFA.areEquivalent(recursiveMinAut, incrMinAut, ba)); Assert.assertEquals(recursiveMinAut.stateCount(), incrMinAut.stateCount()); @@ -374,21 +390,36 @@ public void testBudget() throws TimeoutException, IOException 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.."); + IncrementalMinimization incrMin = new IncrementalMinimization(aut,ba); + incrMinAut = incrMin.minimize(budget); + } + catch(TimeBudgetExceededException e) + { + incrMinAut = e.getReturnAut(); } catch(TimeoutException e) { continue; } - catch(OutOfMemoryError e) + System.out.println("Incremental minimized."); + try + { + IncrementalNaive naiveMin = new IncrementalNaive(aut, ba); + upfrontIncrAut = naiveMin.minimize(budget); + } + catch(TimeBudgetExceededException e) + { + upfrontIncrAut = e.getReturnAut(); + } + catch(TimeoutException e) { continue; } - - //TODO: negative percentages + /*catch(OutOfMemoryError e) + { + continue; + }*/ + System.out.println("Naive incremental minimized.."); int initialCount = aut.stateCount(); String initialStateCount = Integer.toString(initialCount); @@ -522,23 +553,30 @@ public void testRecord() throws IOException, DebugException } System.out.println("Determinized."); - SFA incrMinAut; - LinkedHashMap record; + SFA incrMinAut =null; + LinkedHashMap record = null; try { - IncrementalMinimization recordMin = - new IncrementalMinimization(aut, ba, false); - incrMinAut = recordMin.minimize(Long.MAX_VALUE, false, true, false); - record = recordMin.getRecord(); + IncrementalMinimization incrMin = + new IncrementalMinimization(aut, ba); + incrMinAut = incrMin.minimize(Long.MAX_VALUE, true, false); + record = incrMin.getRecord(); } catch(TimeoutException e) { continue; } - catch(OutOfMemoryError e) + catch(DebugException e) { - continue; + //This will never occur + Assert.fail(); } + /*catch(OutOfMemoryError e) + { + continue; + }*/ + Assert.assertTrue(incrMinAut != null); + Assert.assertTrue(record != null); System.out.println("Minimized."); if(record.size()<=1) { @@ -744,12 +782,12 @@ public void testDepth() throws IOException, TimeoutException int depthSum = 0; for (int i = 0; i < tests; i++) { - IncrementalMinimization dbgTest = new IncrementalMinimization(aut, ba, true); + IncrementalMinimization dbgTest = new IncrementalMinimization(aut, ba); Integer maxDepth = null; SFA minAut = null; try { - minAut = dbgTest.minimize(Long.MAX_VALUE, false, false, false); + minAut = dbgTest.minimize(Long.MAX_VALUE, false, true); } catch (DebugException e) { diff --git a/IncrementalMinimization/src/TimeBudgetExceededException.java b/IncrementalMinimization/src/TimeBudgetExceededException.java new file mode 100644 index 00000000..2f1f27fa --- /dev/null +++ b/IncrementalMinimization/src/TimeBudgetExceededException.java @@ -0,0 +1,25 @@ +import org.sat4j.specs.TimeoutException; + +import automata.sfa.SFA; + +@SuppressWarnings("rawtypes") //throwable subclasses can not be made generic +public class TimeBudgetExceededException extends TimeoutException +{ + private final SFA returnAut; + + public TimeBudgetExceededException(String message, SFA returnAut) + { + super(message); + this.returnAut = returnAut; + } + + public TimeBudgetExceededException(SFA returnAut) + { + this("Time budget exceeded", returnAut); + } + + public SFA getReturnAut() + { + return returnAut; + } +}