Skip to content

Commit

Permalink
Various improvements related to testing
Browse files Browse the repository at this point in the history
Discrete data structures class optimized, minimization via moore's algorithm implemented for comparison, incremental minimization on a time budget implemented (but not yet tested), and misc other fixes
  • Loading branch information
jah12014 committed Jan 23, 2018
1 parent bc9f939 commit 4f90094
Show file tree
Hide file tree
Showing 10 changed files with 4,633 additions and 55 deletions.
Binary file modified IncrementalMinimization/lib/symbolicautomata.jar
Binary file not shown.
2,145 changes: 2,145 additions & 0 deletions IncrementalMinimization/results/large_test_output

Large diffs are not rendered by default.

Binary file not shown.
Binary file not shown.
63 changes: 36 additions & 27 deletions IncrementalMinimization/src/DisjointSets.java
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
Expand All @@ -7,19 +8,23 @@ public class DisjointSets <E>
{
//TODO: rewrite or find an implementation using "rooted trees" for optimization

//naive implementation inspired from http://www.cs.cornell.edu/~wdtseng/icpc/notes/graph_part4.pdf
//implementation inspired from https://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-046j-design-and-analysis-of-algorithms-spring-2012/lecture-notes/MIT6_046JS12_lec16.pdf
//parentMap contains a forest of implicit trees with the identifiers of the sets at the root, every element in parentMap is mapped to its parent in its tree



private HashMap<E, E> parentMap;
private HashMap<E, Integer> rankMap;

public DisjointSets()
{
parentMap = new HashMap<E, E>();
rankMap = new HashMap<E, Integer>();
}

public DisjointSets(Collection<E> identifiers)
{
parentMap = new HashMap<E, E>();
rankMap = new HashMap<E, Integer>();
for(E identifier : identifiers)
{
make(identifier);
Expand All @@ -31,6 +36,7 @@ public void make(E identifier) throws IllegalArgumentException
if(!parentMap.containsKey(identifier))
{
parentMap.put(identifier, null);
rankMap.put(identifier, 1);
}
else
{
Expand All @@ -40,53 +46,56 @@ public void make(E identifier) throws IllegalArgumentException

public E find(E element) throws IllegalArgumentException
{
if(parentMap.containsKey(element))
if (!parentMap.containsKey(element))
{
E parent = parentMap.get(element);
if(parent == null)
{
return element;
}
else
{
return find(parent);
}
throw new IllegalArgumentException("Element not found in any disjoint set");
}
else
ArrayList<E> path = new ArrayList<E>(53); //height of tree will not exceed 53 with less than 1024 TB of available memory
while(parentMap.get(element) != null)
{
throw new IllegalArgumentException("Element not found in any disjoint set");
path.add(element);
element = parentMap.get(element);

}
for(E pathMember : path) //path is compressed
{
if (pathMember != element)
{
parentMap.put(pathMember, element);
}
}
return element;
}

public E union(E elem1, E elem2)
{
E iden1 = find(elem1);
E iden2 = find(elem2);
E union_iden;
if(iden1 == iden2)
if(iden1.equals(iden2))
{
union_iden = iden1;
}
else
{
try //if E extends comparable, the lesser element will always be new identifier
int rank1 = rankMap.get(iden1);
int rank2 = rankMap.get(iden2);
if (rank1 == rank2)
{
if (((Comparable) iden1).compareTo((Comparable) iden2) <= 0)
{
parentMap.put(iden2, iden1);
union_iden = iden1;
}
else
{
parentMap.put(iden1, iden2);
union_iden = iden2;
}
parentMap.put(iden2, iden1);
rankMap.put(iden1, rank1+1);
union_iden = iden1;
}
catch(Exception e)
else if (rank1 > rank2)
{
parentMap.put(iden2, iden1);
union_iden = iden1;
}
else
{
parentMap.put(iden1, iden2);
union_iden = iden2;
}
}
return union_iden;
}
Expand Down
112 changes: 100 additions & 12 deletions IncrementalMinimization/src/IncrementalMinimization.java
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,28 @@

public class IncrementalMinimization
{
@SuppressWarnings("rawtypes") // Extensions of Throwable class can not be generic
private static class TimeBudgetExceeded extends TimeoutException
{
private 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 static class EquivTest<P,S>
{
private final SFA<P,S> aut;
Expand All @@ -39,7 +61,8 @@ public EquivTest(SFA<P,S> aut, BooleanAlgebra<P,S> ba, DisjointSets<Integer> equ
this.path = path;
}

private List<SFAInputMove<P,S>> findNonDisjointMoves(Collection<SFAInputMove<P, S>> outp, Collection<SFAInputMove<P, S>> outq) throws TimeoutException
private List<SFAInputMove<P,S>> findNonDisjointMoves(Collection<SFAInputMove<P, S>> outp,
Collection<SFAInputMove<P, S>> outq) throws TimeoutException
{
//TODO: look into local minterm generation, can be more efficient?
assert(!outp.isEmpty() && !outq.isEmpty()); //TODO: remove assertions
Expand Down Expand Up @@ -134,28 +157,61 @@ private static List<Integer> normalize(Integer p, Integer q)
return pair;
}

public static <P, S> SFA<P, S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba) throws TimeoutException
private static <P,S> SFA<P,S> mergeSFAStates(DisjointSets<Integer> equivClasses,
SFA<P,S> originalAut, BooleanAlgebra<P,S> ba) throws TimeoutException
{
//new SFA created with minimum states
HashMap<Integer, HashSet<Integer>> classes = equivClasses.getSets();
Set<Integer> newStates = classes.keySet();
Collection<SFAMove<P, S>> newTransitions = new LinkedList<SFAMove<P, S>>();
Collection<Integer> newFinalStates = new HashSet<Integer>();
for (Integer p : newStates)
{
for (SFAInputMove<P,S> t : originalAut.getInputMovesFrom(classes.get(p)))
{
newTransitions.add(new SFAInputMove<P,S>(p, equivClasses.find(t.to), t.guard));
}
if(originalAut.isFinalState(p))
{
newFinalStates.add(p);
}
}
Integer newInitialState = equivClasses.find(originalAut.getInitialState());
SFA<P,S> minAut = SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba, false);
return minAut;
}

public static <P, S> SFA<P, S> minimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba, long budget)
throws TimeoutException
{
long endTime = System.nanoTime() + budget;
if (endTime < 0) //indicates overflow
{
endTime = Long.MAX_VALUE;
}
if(aut.isEmpty())
{
return SFA.getEmptySFA(ba);
}
aut = aut.determinize(ba).mkTotal(ba); //TODO: normalizes?
if (!aut.isDeterministic())
{
aut = aut.determinize(ba);
}
aut = aut.mkTotal(ba);
DisjointSets<Integer> equivClasses = new DisjointSets<Integer>();
for(Integer q : aut.getStates())
{
equivClasses.make(q);
}
Integer num_pairs = aut.getStates().size() * aut.getStates().size(); //n^2 where n is # of states
HashSet<List<Integer>> neq = new HashSet<List<Integer>>(num_pairs, 1); //set is given initial capacity of n^2, won't exceed this
int num_pairs = aut.getStates().size() * aut.getStates().size(); //n^2 where n is # of states
HashSet<List<Integer>> neq = new HashSet<List<Integer>>(num_pairs, 0.9f); //set is given initial capacity of n^2, won't exceed this
for(Integer p : aut.getFinalStates())
{
for(Integer q : aut.getNonFinalStates())
{
neq.add(normalize(p,q));
}
}

for(Integer p : aut.getStates())
{
for(Integer q : aut.getStates())
Expand All @@ -175,14 +231,27 @@ 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<List<Integer>> equiv = new HashSet<List<Integer>>(num_pairs,1);
HashSet<List<Integer>> path = new HashSet<List<Integer>>(num_pairs,1);
HashSet<List<Integer>> equiv = new HashSet<List<Integer>>(num_pairs,0.9f);
HashSet<List<Integer>> path = new HashSet<List<Integer>>(num_pairs,0.9f);
EquivTest<P,S> pEquiv = new EquivTest<P,S>(aut, ba, equivClasses, neq, equiv, path);
if(pEquiv.isEquiv(p,q))
boolean isequiv;
isequiv = pEquiv.isEquiv(p, q);
if(isequiv)
{
//p,q found equivalent. Other pairs may be found equivalent.
for(List<Integer> equivPair : pEquiv.getEquiv())
{
if(System.nanoTime() >= endTime)
{
//Time Budget exceeded
SFA<P,S> 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));
}
}
Expand All @@ -197,8 +266,7 @@ else if(equivClasses.find(p) == equivClasses.find(q))
}
}

//new SFA created with minimum states
//TODO verify that this merges transitions correctly.
/* new SFA created with minimum states
HashMap<Integer, HashSet<Integer>> classes = equivClasses.getSets();
Set<Integer> newStates = classes.keySet();
Collection<SFAMove<P, S>> newTransitions = new LinkedList<SFAMove<P, S>>();
Expand All @@ -216,7 +284,27 @@ else if(equivClasses.find(p) == equivClasses.find(q))
}
Integer newInitialState = equivClasses.find(aut.getInitialState());
SFA<P,S> minAut = SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba, false);
return minAut;
return minAut; */

return mergeSFAStates(equivClasses, aut, ba);
}

public static <P,S> SFA<P,S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba, long budget)
throws TimeoutException
{
try
{
return minimize(aut, ba, budget);
}
catch(TimeBudgetExceeded e)
{
return e.getReturnAut();
}
}

public static <P,S> SFA<P,S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba) throws TimeoutException
{
return incrementalMinimize(aut, ba, Long.MAX_VALUE); //Default time budget 200+ years (i.e. there is none)
}

}
Loading

0 comments on commit 4f90094

Please sign in to comment.