diff --git a/IncrementalMinimization/src/minimization/MooreMinimization.java b/IncrementalMinimization/src/minimization/MooreMinimization.java index 75517552..84cdeeab 100644 --- a/IncrementalMinimization/src/minimization/MooreMinimization.java +++ b/IncrementalMinimization/src/minimization/MooreMinimization.java @@ -25,7 +25,7 @@ public static SFA mooreMinimize(SFA aut, BooleanAlgebra ba) private SFA aut; private BooleanAlgebra ba; - private MooreMinimization(SFA aut, BooleanAlgebra ba) + public MooreMinimization(SFA aut, BooleanAlgebra ba) { this.aut = aut; this.ba = ba; diff --git a/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java b/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java new file mode 100644 index 00000000..2c284a1f --- /dev/null +++ b/IncrementalMinimization/src/minimization/incremental/IncrSimpleNEQ.java @@ -0,0 +1,61 @@ +package minimization.incremental; + +import java.util.Comparator; +import java.util.LinkedHashMap; +import java.util.List; + +import org.sat4j.specs.TimeoutException; + +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. + */ + +public class IncrSimpleNEQ extends IncrementalMinimization +{ + protected class StateComparatorSimple extends StateComparator + { + @Override + public int compare(Integer a, Integer b) + { + return a-b; + } + } + + public IncrSimpleNEQ(SFA aut, BooleanAlgebra ba) throws TimeoutException + { + super(aut, ba); + this.stateComp = new StateComparatorSimple(); + for(Integer p : aut.getFinalStates()) + { + for(Integer q : aut.getNonFinalStates()) + { + neq.add(normalize(p,q)); + } + } + } + + @Override + protected LinkedHashMap generateDistanceToFinalMap() + { + return null; + } + + @Override + protected Integer getStateDistanceToFinal(Integer state) + { + return 0; + } + + @Override + protected boolean isKnownNotEqual(Integer p, Integer q) + { + List normalizedPair = normalize(p,q); + return neq.contains(normalizedPair); + } +} diff --git a/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java b/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java index f6a8e87b..e73228f2 100644 --- a/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java +++ b/IncrementalMinimization/src/minimization/incremental/IncrWithDependencyChecks.java @@ -1,19 +1,14 @@ package minimization.incremental; import java.util.ArrayList; -import java.util.Arrays; import java.util.Collection; -import java.util.HashMap; import java.util.HashSet; -import java.util.LinkedList; import java.util.List; -import java.util.Queue; import java.util.Stack; -import minimization.incremental.IncrementalMinimization.EquivTest; - import org.sat4j.specs.TimeoutException; +import structures.DependencyGraph; import structures.DisjointSets; import theory.BooleanAlgebra; import automata.sfa.SFA; @@ -25,196 +20,13 @@ public class IncrWithDependencyChecks extends IncrementalMinimization protected class EquivTestDependency extends EquivTest //tests for equality of two given states in the automata { - protected class Dependencies //tracks the pairs of states that an equivalence result depends on within our algorithm. - { - protected class StatePair - { - public final List pair; - private boolean isTested; - private LinkedList deps; - - public StatePair(List pair, boolean isTested) - { - this.pair = pair; - this.isTested = isTested; - this.deps = new LinkedList(); - } - - public StatePair(List pair) - { - this(pair, true); - } - - public void addDependency(StatePair dep) - { - assert(dep != null); - deps.add(dep); - } - - public LinkedList getDependencies() - { - return deps; - } - - public boolean isTested() - { - return isTested; - } - - public void setTested(boolean b) - { - isTested = b; - } - - @Override - public boolean equals(Object other) - { - if(other == null || (other.getClass() != getClass())) - { - return false; - } - StatePair otherPair = (StatePair) other; - if(pair.equals((otherPair.pair))) - { - assert(deps.equals(otherPair.getDependencies())); - return true; - } - else - { - return false; - } - } - - @Override - public int hashCode() - { - return pair.hashCode(); - } - - @Override - public String toString() - { - return String.format("%s | %s ", pair.toString(), Boolean.toString(isTested)); - } - - public String toStringLong() - { - return String.format("%s | %s | %s", pair.toString(), Boolean.toString(isTested), deps.toString()); - } - } - - - private HashMap,StatePair> pairLookup; - - public Dependencies() - { - this.pairLookup = new HashMap,StatePair>(num_pairs); - } - - public void addDependency(List pair, List dependency) - { - if(pair.equals(dependency)) - { - return; - } - StatePair pairEntry; - if(pairLookup.containsKey(pair)) - { - pairEntry = pairLookup.get(pair); - pairEntry.setTested(true); - } - else - { - pairEntry = new StatePair(pair, true); - pairLookup.put(pair, pairEntry); - } - StatePair depEntry; - if(pairLookup.containsKey(dependency)) - { - depEntry = pairLookup.get(dependency); - } - else - { - depEntry = new StatePair(dependency, false); - pairLookup.put(dependency, depEntry); - } - assert(depEntry != null); - pairEntry.addDependency(depEntry); - } - - public void addAllDependencies(List pair, ArrayList> dpairs) - { - for(List dpair : dpairs) - { - addDependency(pair, dpair); - } - } - - private void mergePair(StatePair pairEntry, HashSet> badPath) throws TimeoutException - { - - Queue depQueue = new LinkedList(); - depQueue.addAll(pairEntry.getDependencies()); - //HashSet> debugTest = new HashSet>(); - HashSet seenPairs = new HashSet(); - while(!depQueue.isEmpty()) - { - StatePair dep = depQueue.remove(); - assert(! (dep == null)); - if(seenPairs.contains(dep)) - { - continue; - } - seenPairs.add(dep); - if(!dep.isTested()) - { - return; - } - if(badPath.contains(dep.pair)) - { - return; - } - assert(pairLookup.values().contains(dep)); - depQueue.addAll(dep.getDependencies()); - } - 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> badPath) throws TimeoutException - { - for(StatePair pairEntry : pairLookup.values()) - { - if(!pairEntry.isTested) - { - continue; - } - else if(badPath.contains(pairEntry.pair)) - { - continue; - } - else - { - mergePair(pairEntry,badPath); - } - } - } - } - - private Dependencies deps; - - public EquivTestDependency (DisjointSets equivClasses, HashSet> equiv, - HashSet> path, Dependencies deps) - { - super(equivClasses, equiv, path); - this.deps = deps; - } + private DependencyGraph deps; public EquivTestDependency (DisjointSets equivClasses, HashSet> equiv, HashSet> path) { super(equivClasses, equiv, path); - this.deps = new Dependencies(); + this.deps = new DependencyGraph(); } @Override @@ -234,19 +46,19 @@ public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException Integer q = curEquivTest.qState; HashSet> curPath = curEquivTest.curPath; List pair = normalize(p,q); - HashSet> newPath = new HashSet>(curPath); - newPath.add(pair); Collection> outp = new ArrayList>(aut.getInputMovesFrom(p)); Collection> outq = new ArrayList>(aut.getInputMovesFrom(q)); while(!outp.isEmpty() && !outq.isEmpty()) { + HashSet> newPath = new HashSet>(curPath); + newPath.add(pair); List> nonDisjointGuards = findNonDisjointMoves(outp, outq); SFAInputMove pMove = nonDisjointGuards.get(0); SFAInputMove qMove = nonDisjointGuards.get(1); Integer pNextClass = equivClasses.find(pMove.to); Integer qNextClass = equivClasses.find(qMove.to); List nextPair = normalize(pNextClass, qNextClass); - if(equiv.contains(nextPair) || path.contains(nextPair)) + if(equiv.contains(nextPair) || curPath.contains(nextPair)) { deps.addDependency(pair, nextPair); } @@ -259,8 +71,8 @@ else if(!pNextClass.equals(qNextClass)) { neq.add(pathPair); //TODO: remove this call from outer minimize method } - this.path = newPath; - deps.mergeStates(newPath); + deps.mergeStates(equivClasses, newPath); + this.path.clear(); return false; } else @@ -268,6 +80,7 @@ else if(!pNextClass.equals(qNextClass)) equiv.add(nextPair); EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath); testStack.add(nextTest); + deps.addDependency(pair, nextPair); } } outp.remove(pMove); diff --git a/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java b/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java index ded282b3..f42234c0 100644 --- a/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java +++ b/IncrementalMinimization/src/minimization/incremental/IncrementalMinimization.java @@ -167,7 +167,7 @@ public Integer getMaxDepth() throws DebugException } } - private class StateComparator implements Comparator + protected class StateComparator implements Comparator { public int compare(Integer a, Integer b) { @@ -188,8 +188,8 @@ public int compare(Integer a, Integer b) protected final int num_pairs; protected HashSet> neq; + protected StateComparator stateComp; private LinkedHashMap distanceToFinalMap; //maps states to distance from final state, does not contain sink states - private StateComparator stateComp; private Long startTime; private LinkedHashMap record; //maps time stamps to number of states private Long singularRecord = null; @@ -212,7 +212,28 @@ public IncrementalMinimization(SFA aut, BooleanAlgebra ba) throws Time this.record = new LinkedHashMap(); } - private LinkedHashMap generateDistanceToFinalMap() + 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) + { + pair = Arrays.asList(p,q); + } + else + { + pair = Arrays.asList(q,p); + } + return pair; + } + + protected LinkedHashMap generateDistanceToFinalMap() { LinkedHashMap distanceMap = new LinkedHashMap(); Queue stateQueue = new LinkedList(); @@ -239,27 +260,6 @@ private LinkedHashMap generateDistanceToFinalMap() return distanceMap; } - 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) - { - pair = Arrays.asList(p,q); - } - else - { - pair = Arrays.asList(q,p); - } - return pair; - } - protected Integer getStateDistanceToFinal(Integer state) { if(distanceToFinalMap.containsKey(state)) diff --git a/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java b/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java new file mode 100644 index 00000000..b8f18f12 --- /dev/null +++ b/IncrementalMinimization/src/minimization/incremental/IncrementalRecWithDeps.java @@ -0,0 +1,115 @@ +package minimization.incremental; + +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 minimization.incremental.IncrementalMinimization.EquivTest; + +import org.sat4j.specs.TimeoutException; + +import structures.DependencyGraph; +import structures.DisjointSets; +import theory.BooleanAlgebra; +import automata.sfa.SFA; +import automata.sfa.SFAInputMove; + + +public class IncrementalRecWithDeps extends IncrementalMinimization +{ + private class EquivTestRecursive extends EquivTest + { + private DependencyGraph deps; + + public EquivTestRecursive(DisjointSets equivClasses, HashSet> equiv, + HashSet> path) + { + super(equivClasses, equiv, path); + this.deps = new DependencyGraph(); + } + + public boolean isEquivRecursive(Integer p, Integer q) throws TimeoutException + { + if (isKnownNotEqual(p,q)) + { + return false; + } + List pair = normalize(p,q); + if (path.contains(pair)) + { + return true; + } + path.add(pair); + Collection> outp = new ArrayList>(aut.getInputMovesFrom(p)); + Collection> outq = new ArrayList>(aut.getInputMovesFrom(q)); + 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(equiv.contains(nextPair) || path.contains(nextPair)) + { + deps.addDependency(pair, nextPair); + } + if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair)) + { + equiv.add(nextPair); + if (!isEquivRecursive(pNextClass, qNextClass)) + { + return false; + } + } + 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)); + } + } + path.remove(pair); + equiv.add(pair); + return true; + } + + @Override + public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException + { + boolean finalResult = isEquivRecursive(pStart, qStart); + if(!finalResult) + { + int mergeResults = deps.mergeStates(equivClasses, path); + if(mergeResults > 0) + { + System.out.println(String.format("Recursive alg merged %d pairs", mergeResults)); + } + } + return finalResult; + } + } + + public IncrementalRecWithDeps(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/minimization/incremental/IncrementalRecursive.java b/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java index add945cb..bdc72b6e 100644 --- a/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java +++ b/IncrementalMinimization/src/minimization/incremental/IncrementalRecursive.java @@ -11,6 +11,7 @@ import org.sat4j.specs.TimeoutException; +import structures.DependencyGraph; import structures.DisjointSets; import theory.BooleanAlgebra; import automata.sfa.SFA; @@ -21,141 +22,26 @@ 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 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 + public boolean isEquivRecursive(Integer p, Integer q) throws TimeoutException { if (isKnownNotEqual(p,q)) { - return new ResultDependencies(false); + return false; } List pair = normalize(p,q); if (path.contains(pair)) { - ResultDependencies r = new ResultDependencies(true); - r.addDependency(pair); - return r; + return true; } 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); @@ -168,36 +54,9 @@ public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutE if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair)) { equiv.add(nextPair); - equivDepends.put(nextPair, null); - if(path.contains(nextPair)) + if (!isEquivRecursive(pNextClass, qNextClass)) { - 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); + return false; } } outp.remove(pMove); @@ -213,25 +72,16 @@ else if(!pair.equals(nextPair)) 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; + path.remove(pair); + equiv.add(pair); + return true; } @Override public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException { - ResultDependencies finalResult = isEquivRecursive(pStart, qStart); - return finalResult.isEquiv(); + boolean finalResult = isEquivRecursive(pStart, qStart); + return finalResult; } } diff --git a/IncrementalMinimization/src/structures/DependencyGraph.java b/IncrementalMinimization/src/structures/DependencyGraph.java new file mode 100644 index 00000000..7628f2ae --- /dev/null +++ b/IncrementalMinimization/src/structures/DependencyGraph.java @@ -0,0 +1,185 @@ +package structures; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Queue; + +import org.sat4j.specs.TimeoutException; + +public class DependencyGraph +{ + protected class StatePair //Nodes in graph + { + public final List pair; + private boolean isTested; + private LinkedList deps; //successor nodes, i.e. pairs that this pair is dependent on + + public StatePair(List pair, boolean isTested) + { + this.pair = pair; + this.isTested = isTested; + this.deps = new LinkedList(); + } + + public StatePair(List pair) + { + this(pair, true); + } + + public void addDependency(StatePair dep) + { + assert(dep != null); + deps.add(dep); + } + + public LinkedList getDependencies() + { + return deps; + } + + public boolean isTested() + { + return isTested; + } + + public void setTested(boolean b) + { + isTested = b; + } + + @Override + public boolean equals(Object other) + { + if(other == null || (other.getClass() != getClass())) + { + return false; + } + StatePair otherPair = (StatePair) other; + if(pair.equals((otherPair.pair))) + { + assert(deps.equals(otherPair.getDependencies())); + return true; + } + else + { + return false; + } + } + + @Override + public int hashCode() + { + return pair.hashCode(); + } + + @Override + public String toString() + { + return String.format("%s | %s ", pair.toString(), Boolean.toString(isTested)); + } + + public String toStringLong() + { + return String.format("%s | %s | %s", pair.toString(), Boolean.toString(isTested), deps.toString()); + } + } + + + private HashMap,StatePair> pairLookup; + + public DependencyGraph() + { + this.pairLookup = new HashMap,StatePair>(); + } + + public void addDependency(List pair, List dependency) + { + if(pair.equals(dependency)) + { + return; + } + StatePair pairEntry; + if(pairLookup.containsKey(pair)) + { + pairEntry = pairLookup.get(pair); + pairEntry.setTested(true); + } + else + { + pairEntry = new StatePair(pair, true); + pairLookup.put(pair, pairEntry); + } + StatePair depEntry; + if(pairLookup.containsKey(dependency)) + { + depEntry = pairLookup.get(dependency); + } + else + { + depEntry = new StatePair(dependency, false); + pairLookup.put(dependency, depEntry); + } + assert(depEntry != null); + pairEntry.addDependency(depEntry); + } + + public void addAllDependencies(List pair, ArrayList> dpairs) + { + for(List dpair : dpairs) + { + addDependency(pair, dpair); + } + } + + private int mergePair(StatePair pairEntry, DisjointSets equivClasses, HashSet> badPath) throws TimeoutException + { + + Queue depQueue = new LinkedList(); + depQueue.addAll(pairEntry.getDependencies()); + HashSet seenPairs = new HashSet(); + while(!depQueue.isEmpty()) + { + StatePair dep = depQueue.remove(); + if(seenPairs.contains(dep)) + { + continue; + } + seenPairs.add(dep); + if(!dep.isTested()) + { + return 0; + } + if(badPath.contains(dep.pair)) + { + return 0; + } + depQueue.addAll(dep.getDependencies()); + } + equivClasses.union(pairEntry.pair.get(0), pairEntry.pair.get(1)); + return 1; + } + + public int mergeStates(DisjointSets equivClasses, HashSet> badPath) throws TimeoutException + { + int result = 0; + for(StatePair pairEntry : pairLookup.values()) + { + if(!pairEntry.isTested) + { + continue; + } + else if(badPath.contains(pairEntry.pair)) + { + continue; + } + else + { + result += mergePair(pairEntry,equivClasses,badPath); + } + } + return result; + } +} diff --git a/IncrementalMinimization/src/test/TestIncrementalMinimization.java b/IncrementalMinimization/src/test/TestIncrementalMinimization.java index 2e079f84..e529de5e 100644 --- a/IncrementalMinimization/src/test/TestIncrementalMinimization.java +++ b/IncrementalMinimization/src/test/TestIncrementalMinimization.java @@ -26,10 +26,13 @@ import minimization.DebugException; +import minimization.MinimizationAlgorithm; import minimization.MooreMinimization; +import minimization.incremental.IncrSimpleNEQ; import minimization.incremental.IncrWithDependencyChecks; import minimization.incremental.IncrementalMinimization; import minimization.incremental.IncrementalNaive; +import minimization.incremental.IncrementalRecWithDeps; import minimization.incremental.IncrementalRecursive; import minimization.incremental.TimeBudgetExceededException; @@ -53,6 +56,7 @@ public class TestIncrementalMinimization { public static final String REGEXLIB_FILE = "regex/regexlib-SFA.txt"; + public static final int TRIAL_COUNT = 10; @Test public void testMyAut() throws TimeoutException @@ -153,6 +157,57 @@ public void testCharPred() throws TimeoutException Assert.assertTrue(incrMinAut.stateCount() <= stdMinAut.stateCount()); } + private Double testMin(MinimizationAlgorithm minAlg, SFA stdMinAut, BooleanAlgebra ba, + Long startTime) throws TimeoutException + { + SFA minAut = null; + try + { + minAut = minAlg.minimize(); + } + catch (DebugException e) + { + //This should never happen here + } + 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()); + Assert.assertTrue(minAut.isDeterministic(ba)); + return finishTime; + } + + @Test + public void testDep() throws TimeoutException + { + String regex = "(\\s*\\S*){2}(ipsum)(\\S*\\s*){2}"; + UnaryCharIntervalSolver ba = new UnaryCharIntervalSolver(); + SFA aut = (new SFAprovider(regex, ba)).getSFA(); + aut = aut.determinize(ba); + aut = aut.mkTotal(ba); + SFA stdMinAut = aut.minimize(ba); + long startTime = System.nanoTime(); + IncrementalMinimization depMin = new IncrWithDependencyChecks(aut,ba); + Double finishTime = testMin(depMin, stdMinAut, ba, startTime); + System.out.println(finishTime.toString()); + } + + private double arrayAvg(double[] arr) + { + if (arr.length <= 0) + { + throw new IllegalArgumentException("Array must be non-empty"); + } + double sum = 0.0; + for(double i : arr) + { + sum += i; + } + return sum/arr.length; + } + private void compareRuntimeFromRegex(List regexList, String outfile) throws TimeoutException, IOException { //Given a list of regex, runs all minimization algorithms on each and output results to the given file. @@ -178,147 +233,103 @@ private void compareRuntimeFromRegex(List regexList, String outfile) thr System.gc(); continue; } - System.out.println("Determinized"); - - //standard minimization - long stdStart = System.nanoTime(); - SFA stdMinAut; - stdMinAut = aut.minimize(ba); - Double stdTime = ((double)(System.nanoTime() - stdStart)/1000000); - System.out.println("Standard minimized."); - - //moore minimization - long mooreStart = System.nanoTime(); - SFA mooreMinAut; - mooreMinAut = MooreMinimization.mooreMinimize(aut, ba); - Double mooreTime = ((double)(System.nanoTime() - mooreStart)/1000000); - Assert.assertTrue(SFA.areEquivalent(mooreMinAut, stdMinAut, ba)); - Assert.assertTrue(mooreMinAut.stateCount() <= stdMinAut.stateCount()); - System.out.println("Moore minimized."); - //incremental minimization - System.out.println("Starting incremental minimization"); - long incrStart = System.nanoTime(); - SFA incrMinAut; - try + if(aut.stateCount() > 400) { - 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) - { - 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)); - Assert.assertTrue(incrMinAut.stateCount() <= stdMinAut.stateCount()); - System.out.println("Incremental minimized."); - + System.out.println("Determinized"); - //DFAized incremental minimization - System.out.println("Starting upfront incremental"); - long incrDFAStart = System.nanoTime(); - SFA upfrontMinAut; - try + System.out.println("Standard minimizing..."); + double[] stdTimes = new double[TRIAL_COUNT]; + SFA stdMinAut = null; + for(int i = 0; i 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) - { - 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)); - Assert.assertEquals(upfrontMinAut.stateCount(), incrMinAut.stateCount()); - /*try - { - Assert.assertTrue(upfrontMinAut.stateCount() == incrMinAut.stateCount()); + long stdStart = System.nanoTime(); + stdMinAut = aut.minimize(ba); + double trialTime = ((double)(System.nanoTime() - stdStart)/1000000); + stdTimes[i] = trialTime; } - catch(AssertionError e) - { - System.out.println(upfrontMinAut.stateCount()); - System.out.println(incrMinAut.stateCount()); - throw(e); - }*/ - Assert.assertTrue(SFA.areEquivalent(upfrontMinAut, stdMinAut, ba)); - System.out.println("Upfront Incremental minimized."); + Assert.assertNotNull(stdMinAut); + Double stdTime = arrayAvg(stdTimes); - //recursive incremental - System.out.println("Starting Recursive incremental w/ dependency check"); - long recStart = System.nanoTime(); - SFA recursiveMinAut; - try + System.out.println("Moore minimizing..."); + double[] mooreTimes = new double[TRIAL_COUNT]; + for(int i = 0; i incrRec = new IncrementalRecursive(aut, ba); - recursiveMinAut = incrRec.minimize(); - } - catch(TimeoutException e) - { - System.out.println("Skipping because of Timeout Exception"); //TODO: does this come up? - continue; + long mooreStart = System.nanoTime(); + MinimizationAlgorithm mooreMin = new MooreMinimization(aut, ba); + double trialTime = testMin(mooreMin, stdMinAut, ba, mooreStart); + mooreTimes[i] = trialTime; } - Double recTime = ((double)(System.nanoTime() - recStart)/1000000); - Assert.assertTrue(recursiveMinAut.stateCount() <= stdMinAut.stateCount()); - try - { - Assert.assertTrue(SFA.areEquivalent(recursiveMinAut, stdMinAut, ba)); - } - catch(AssertionError e) + Double mooreTime = arrayAvg(mooreTimes); + + //incremental minimization + System.out.println("Starting incremental minimization..."); + double[] incrTimes = new double[TRIAL_COUNT]; + for(int i = 0; i incrMin = new IncrementalMinimization(aut, ba); + double trialTime = testMin(incrMin, stdMinAut, ba, incrStart); + incrTimes[i] = trialTime; } - Assert.assertTrue(SFA.areEquivalent(recursiveMinAut, incrMinAut, ba)); - Assert.assertEquals(recursiveMinAut.stateCount(), incrMinAut.stateCount()); + Double incrTime = arrayAvg(incrTimes); - //standard incremental w/ dependency check - System.out.println("Starting standard incremental w/ dependency check"); - long depStart = System.nanoTime(); - SFA depMinAut; - try + System.out.println("Starting naive incremental..."); + double[] upfrontTimes = new double[TRIAL_COUNT]; + for(int i = 0; i incrDep = new IncrWithDependencyChecks(aut, ba); - depMinAut = incrDep.minimize(); + long naiveStart = System.nanoTime(); + MinimizationAlgorithm naiveMin = new IncrementalNaive(aut, ba); + double trialTime = testMin(naiveMin,stdMinAut, ba, naiveStart); + upfrontTimes[i] = trialTime; } - catch(TimeoutException e) + Double upfrontTime = arrayAvg(upfrontTimes); + + System.out.println("Starting recursive incremental..."); + double[] recTimes = new double[TRIAL_COUNT]; + for(int i = 0; i recMin = new IncrementalRecursive(aut, ba); + double trialTime = testMin(recMin, stdMinAut, ba, recStart); + recTimes[i] = trialTime; } - catch(OutOfMemoryError e) + Double recTime = arrayAvg(recTimes); + + System.out.println("Starting recursive incremental w/ dependency check..."); + double[] recDepTimes = new double[TRIAL_COUNT]; + for(int i = 0; i recMin = new IncrementalRecWithDeps(aut, ba); + double trialTime = testMin(recMin, stdMinAut, ba, recDepStart); + recDepTimes[i] = trialTime; } - Double depTime = ((double)(System.nanoTime() - depStart)/1000000); - Assert.assertTrue(depMinAut.stateCount() <= stdMinAut.stateCount()); - try + Double recDepTime = arrayAvg(recDepTimes); + + System.out.println("Starting standard incremental w/ dependency check..."); + double[] depTimes = new double[TRIAL_COUNT]; + for(int i = 0; i depMin = new IncrWithDependencyChecks(aut, ba); + double trialTime = testMin(depMin, stdMinAut, ba, depStart); + depTimes[i] = trialTime; } - catch(AssertionError e) + Double depTime = arrayAvg(depTimes); + + System.out.println("Starting incremental w/ simple neq initialization..."); + double[] neqTimes = new double[TRIAL_COUNT]; + for(int i = 0; i neqMin = new IncrSimpleNEQ(aut, ba); + double trialTime = testMin(neqMin, stdMinAut, ba, neqStart); + neqTimes[i] = trialTime; } - Assert.assertTrue(SFA.areEquivalent(depMinAut, incrMinAut, ba)); - Assert.assertEquals(depMinAut.stateCount(), incrMinAut.stateCount()); + Double neqTime = arrayAvg(neqTimes); String initialStateCount = Integer.toString(aut.stateCount()); String transCount = Integer.toString(aut.getTransitionCount()); @@ -333,10 +344,11 @@ private void compareRuntimeFromRegex(List regexList, String outfile) thr ArrayList predList = new ArrayList(predSet); String mintermCount = Integer.toString(ba.GetMinterms(predList).size()); - String message = String.format("%s, %s, %s, %s, %s, %s, %s, %s, %s, %s, %s", + String message = String.format("%s, %s, %s, %s, %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), Double.toString(recTime), Double.toString(depTime)); + Double.toString(upfrontTime), Double.toString(recTime), Double.toString(recDepTime), + Double.toString(depTime), Double.toString(neqTime)); System.out.println(message); System.out.println(""); messageList.add(message); @@ -345,7 +357,8 @@ private void compareRuntimeFromRegex(List regexList, String outfile) thr 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, " + - "recursive symbolic incremental, With Dependency check \n"); + "recursive symbolic incremental, Rec w/ Dependency check, Stdrd q/ Dependency check," + + " With simple neq \n"); for (String msg : messageList) { writer.write(msg + "\n"); @@ -964,7 +977,5 @@ public void testDepth() throws IOException, TimeoutException writer.close(); } - - }