Adding framework for incremental minimization, not yet complete

IncrementalMinimization/.gitignore

@@ -0,0 +1,5 @@
+bin/
+.metadata/
+.settings/
+.classpath
+.project

IncrementalMinimization/src/DisjointSets.java

@@ -0,0 +1,121 @@
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+
+
+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
+	//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;
+
+	public DisjointSets()
+	{
+		parentMap = new HashMap<E, E>();
+	}
+
+	public DisjointSets(Collection<E> identifiers)
+	{
+		parentMap = new HashMap<E, E>();
+		for(E identifier : identifiers)
+		{
+			make(identifier);
+		}
+	}
+
+	public void make(E identifier) throws IllegalArgumentException
+	{
+		if(!parentMap.containsKey(identifier))
+		{
+			parentMap.put(identifier, null);
+		}
+		else
+		{
+			throw new IllegalArgumentException("Identifier already exists in a set");
+		}
+	}
+
+	public E find(E element) throws IllegalArgumentException
+	{
+		if(parentMap.containsKey(element))
+		{
+			E parent = parentMap.get(element);
+			if(parent == null)
+			{
+				return element;
+			}
+			else
+			{
+				return find(parent);
+			}
+		}
+		else
+		{
+			throw new IllegalArgumentException("Element not found in any disjoint set");
+		}
+	}
+
+	public E union(E elem1, E elem2)
+	{
+		E iden1 = find(elem1);
+		E iden2 = find(elem2);
+		E union_iden;
+		if(iden1 == iden2)
+		{
+			union_iden = iden1;
+		}
+		else
+		{
+			try //if E extends comparable, the lesser element will always be new identifier
+			{
+				if (((Comparable) iden1).compareTo((Comparable) iden2) <= 0)
+				{
+					parentMap.put(iden2, iden1);
+					union_iden = iden1;
+				}
+				else
+				{
+					parentMap.put(iden1, iden2);
+					union_iden = iden2;
+				}
+			}
+			catch(Exception e)
+			{
+				parentMap.put(iden2, iden1);
+				union_iden = iden1;
+			}
+		}
+		return union_iden;
+	}
+
+	public HashMap<E, HashSet<E>> getSets()
+	{
+		HashMap<E, HashSet<E>> sets = new HashMap<E, HashSet<E>>();
+		for(E element : parentMap.keySet())
+		{
+			E identifier = find(element);
+			if(!sets.containsKey(identifier))
+			{
+				HashSet<E> set = new HashSet<E>();
+				set.add(element);
+				sets.put(identifier, set);
+			}
+			else
+			{
+				sets.get(identifier).add(element);
+			}
+		}
+		return sets;
+	}
+
+	public String toString()
+	{
+		return getSets().toString();
+	}
+
+
+
+}

IncrementalMinimization/src/Main.java

@@ -0,0 +1,207 @@
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Set;
+
+import org.apache.commons.lang3.NotImplementedException;
+import org.sat4j.specs.TimeoutException;
+
+import theory.BooleanAlgebra;
+import theory.intervals.IntPred;
+import theory.intervals.IntegerSolver;
+import automata.sfa.SFA;
+import automata.sfa.SFAInputMove;
+import automata.sfa.SFAMove;
+
+public class Main
+{
+	private static class EquivTest<P,S>
+	{
+		private SFA<P,S> aut;
+		private HashSet<Integer[]> equiv;
+		private HashSet<Integer[]> path;
+
+		public EquivTest(SFA<P,S> aut, HashSet<Integer[]> equiv, HashSet<Integer[]> path)
+		{
+			this.aut = aut;
+			this.equiv = equiv;
+			this.path = path;
+		}
+
+		public boolean isEquiv(Integer p, Integer q) throws NotImplementedException
+		{
+			//TODO
+			throw new NotImplementedException("Incremental Equivalence Not Implemented Yet");
+		}
+
+		public HashSet<Integer[]> getEquiv()
+		{
+			return equiv;
+		}
+
+		public HashSet<Integer[]> getPath()
+		{
+			return path;
+		}
+	}
+
+	private static Integer[] normalize(Integer p, Integer q)
+	{
+		Integer[] pair;
+		if(p<q)
+		{
+			pair = new Integer[]{p,q};
+		}
+		else
+		{
+			pair = new Integer[]{q,p};
+		}
+		return pair;
+	}
+
+	public static <P, S> SFA<P, S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<P,S>  ba) throws TimeoutException
+	{
+		if(aut.isEmpty())
+		{
+			return SFA.getEmptySFA(ba);
+		}
+		aut = aut.determinize(ba).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<Integer[]> neq = new HashSet<Integer[]>(num_pairs, 1); //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())
+			{
+				if(q <= p)
+				{
+					continue;
+				}
+				Integer[] pair = new Integer[]{p,q};
+				if(neq.contains(pair))
+				{
+					//Already know p,q not equivalent
+					continue;
+				}
+				else if(equivClasses.find(p) == equivClasses.find(q))
+				{
+					//Already found p,q equivalent
+					continue;
+				}
+
+				//TODO: look into efficiency of HashSet operations, ideally should be O(1) for searching, inserting, removing
+				HashSet<Integer[]> equiv = new HashSet<Integer[]>(num_pairs,1);
+				HashSet<Integer[]> path = new HashSet<Integer[]>(num_pairs,1);
+				EquivTest<P,S> pEquiv = new EquivTest<P,S>(aut, equiv, path);
+				if(pEquiv.isEquiv(p,q))
+				{
+					//p,q found equivalent. Other pairs may be found equivalent.
+					for(Integer[] equivPair : pEquiv.getEquiv())
+					{
+						equivClasses.union(equivPair[0], equivPair[1]);
+					}
+				}
+				else
+				{
+					//p,q found non-equivalent. Other pairs may be found non-equivalent.
+					for(Integer[] pathPair : pEquiv.getPath())
+					{
+						neq.add(pathPair);
+					}
+				}
+			}
+		}
+
+		//new SFA created with minimum states
+		//TODO verify that this merges transitions correctly.
+		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 : aut.getInputMovesFrom(classes.get(p)))
+			{
+				newTransitions.add(new SFAInputMove<P,S>(p, equivClasses.find(t.to), t.guard));
+			}
+			if(aut.isFinalState(p))
+			{
+				newFinalStates.add(p);
+			}
+		}
+		Integer newInitialState = equivClasses.find(aut.getInitialState());
+		return SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba);
+	}
+
+	public static void main(String[] args) throws TimeoutException
+	{
+		//TODO: move tests to separate class
+
+		//our algebra is constructed
+		IntegerSolver ba = new IntegerSolver();
+		IntPred neg = new IntPred(null, new Integer(0));
+		IntPred less_neg_ten = new IntPred(null, new Integer(-10));
+		IntPred great_pos_ten = new IntPred(new Integer(10), null);
+		IntPred zero = new IntPred(new Integer(0));
+		IntPred one = new IntPred(1);
+		IntPred zero_five = new IntPred(new Integer(0), new Integer(5));
+		IntPred pos = new IntPred(new Integer(1), null);
+
+		//transitions are defined
+		Collection <SFAMove<IntPred,Integer>> transitions = new LinkedList<SFAMove<IntPred, Integer>>();
+		IntPred a_pred = ba.MkAnd(ba.MkNot(one), ba.MkNot(zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(0,0,a_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(0,1,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(0,2,one));
+		transitions.add(new SFAInputMove<IntPred, Integer>(1,0,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(1,1,a_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(1,2,one));
+		IntPred b_pred = ba.MkAnd(pos, ba.MkNot(zero_five));
+		transitions.add(new SFAInputMove<IntPred, Integer>(2,2,b_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(2,3,neg));
+		IntPred c_pred = ba.MkAnd(ba.MkNot(zero), zero_five);
+		transitions.add(new SFAInputMove<IntPred, Integer>(2,5,c_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(2,6,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(3,3,ba.True()));
+		transitions.add(new SFAInputMove<IntPred, Integer>(4,4,ba.True()));
+		transitions.add(new SFAInputMove<IntPred, Integer>(5,3, neg));
+		transitions.add(new SFAInputMove<IntPred, Integer>(5,3,c_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(5,6,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(5,7,b_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(6,4,neg));
+		transitions.add(new SFAInputMove<IntPred, Integer>(6,4,c_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(6,5,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(6,7,b_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(7,1,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(7,4,ba.MkNot(c_pred)));
+		transitions.add(new SFAInputMove<IntPred, Integer>(7,8,c_pred));
+		transitions.add(new SFAInputMove<IntPred, Integer>(8,0,zero));
+		transitions.add(new SFAInputMove<IntPred, Integer>(8,3,ba.MkNot(c_pred)));
+		transitions.add(new SFAInputMove<IntPred, Integer>(8,7,c_pred));
+
+		//SFA is defined
+		SFA<IntPred, Integer> aut = SFA.MkSFA(transitions, 0, Arrays.asList(7,8), ba);
+
+		//SFA is tested
+		assert(aut.accepts(Arrays.asList(1,7,10),ba));
+		assert(aut.isDeterministic(ba));
+		assert(aut.isTotal());
+
+
+		SFA<IntPred, Integer> minAut = incrementalMinimize(aut, ba);
+	}
+}

symbolicautomata/SVPAlib/src/theory/intervals/IntPred.java

@@ -114,7 +114,7 @@ public static ImmutableList<ImmutablePair<Integer, Integer>> invertIntervals(
 				end_point = interval.right + 1;
 			}
 			if (i == intervals.size() - 1 && interval.right != null) { 
-				ret.add(ImmutablePair.of(interval.right + 1,  null));
+				ret.add(ImmutablePair.of(interval.right + 1,  (Integer)null));
 			}
 		}
 		return ImmutableList.copyOf(ret);