IncrWithDependencyChecks.java

package minimization.incremental;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.Stack;

import org.sat4j.specs.TimeoutException;

import structures.DependencyGraph;
import structures.DisjointSets;
import theory.BooleanAlgebra;
import automata.sfa.SFA;
import automata.sfa.SFAInputMove;

public class IncrWithDependencyChecks<P,S> extends IncrementalMinimization<P,S>
{
	/*
	 * Non-recursive incremental minimization with dependency checking
	 * 
	 * Key idea: whenever a pair of states (p,q) is tested in an equivalence test, if it does not return false
	 * then for all successor pairs (p',q') either we already know p'=q' or we have (p',q') in equiv or 
	 * (p',q') in path. In the cases where p'=/=q', we have that the equivalence of (p,q) is "dependent" on
	 * the equivalence of (p',q'). By keeping track of this dependency relation in a directed graph, we may be
	 * able to identify when a pair of states has been found to be equivalent even if the initial pair of states
	 * tested are not equivalent.
	 * 
	 *   Currently not as efficient as non-recursive incremental minimization without dependency checking
	 *   (given in IncrementalMinimization.java) but there is a lot of room for improvement and optimization.
	 */

	protected class EquivTestDependency extends EquivTest
	{
		
		private DependencyGraph deps;
		
		public EquivTestDependency (DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv, 
				HashSet<List<Integer>> path)
		{
			super(equivClasses, equiv, path);
			this.deps = new DependencyGraph();
		}
		
		@Override
		public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
		{
			if (isKnownNotEqual(pStart,qStart))
			{
				return false;
			}
			EquivRecord start = new EquivRecord(pStart,qStart,path);
			Stack<EquivRecord> testStack = new Stack<EquivRecord>();
			testStack.add(start);
			while (!testStack.isEmpty())
			{
				EquivRecord curEquivTest = testStack.pop();
				Integer p = curEquivTest.pState;
				Integer q = curEquivTest.qState;
				HashSet<List<Integer>> curPath = curEquivTest.curPath;
				List<Integer> pair = normalize(p,q);
				Collection<SFAInputMove<P,S>> outp = new ArrayList<SFAInputMove<P,S>>(aut.getInputMovesFrom(p));
				Collection<SFAInputMove<P,S>> outq = new ArrayList<SFAInputMove<P,S>>(aut.getInputMovesFrom(q));
				while(!outp.isEmpty() && !outq.isEmpty())
				{	
					HashSet<List<Integer>> newPath = new HashSet<List<Integer>>(curPath);
					newPath.add(pair);
					List<SFAInputMove<P,S>> nonDisjointGuards = findNonDisjointMoves(outp, outq);
					SFAInputMove<P,S> pMove = nonDisjointGuards.get(0);
					SFAInputMove<P,S> qMove = nonDisjointGuards.get(1);
					Integer pNextClass = equivClasses.find(pMove.to);
					Integer qNextClass = equivClasses.find(qMove.to);
					List<Integer> nextPair = normalize(pNextClass, qNextClass);
					if(equiv.contains(nextPair) || curPath.contains(nextPair))
					{
						//Dependencies may be added to the dependency graph more often than is necessary to check for equivalence. 
						//TODO: look into
						deps.addDependency(pair, nextPair);
					}
					else if(!pNextClass.equals(qNextClass))
					{
						if(isKnownNotEqual(pNextClass,qNextClass))
						{
							newPath.add(nextPair);
							for(List<Integer> pathPair : path)
							{
								neq.add(pathPair); //TODO: remove this call from outer minimize method
							}
							int result = deps.mergeStates(equivClasses, newPath);
							if(result > 0)
							{
								//Debug print, indicates when dependency checking actually merges pairs that would not have been found otherwise
								System.out.println(String.format("Non-recursive dependency alg merged %d pairs", result));
							}
							this.path.clear();
							return false;
						}
						else
						{
							equiv.add(nextPair);
							EquivRecord nextTest = new EquivRecord(pNextClass, qNextClass, newPath);
							testStack.add(nextTest);
							deps.addDependency(pair, nextPair);
						}
					}
					outp.remove(pMove);
					outq.remove(qMove);
					P newPGuard = ba.MkAnd(pMove.guard, ba.MkNot(qMove.guard));
					if (ba.IsSatisfiable(newPGuard))
					{
						outp.add(new SFAInputMove<P,S>(pMove.from, pMove.to, newPGuard));
					}
					P newQGuard = ba.MkAnd(qMove.guard, ba.MkNot(pMove.guard));
					if (ba.IsSatisfiable(newQGuard))
					{
						outq.add(new SFAInputMove<P,S>(qMove.from, qMove.to, newQGuard));
					}
				}
			}
			equiv.add(normalize(pStart, qStart));
			return true;
		}
	}
	
	public IncrWithDependencyChecks(SFA<P,S> aut, BooleanAlgebra<P,S> ba) throws TimeoutException
	{
		super(aut,ba);
	}
	
	@Override
	protected EquivTest makeEquivTest(DisjointSets<Integer> equivClasses)
	{
		HashSet<List<Integer>> equiv = new HashSet<List<Integer>>(num_pairs,0.9f);
		HashSet<List<Integer>> path = new HashSet<List<Integer>>(num_pairs,0.9f);
		return new EquivTestDependency(equivClasses, equiv, path);
	}
}