Skip to content

Commit

Permalink
Recursive algorithm now merges classes based on dependencies
Browse files Browse the repository at this point in the history 
Still need to optimize and possibly move to non-recursive algorithm if it improves performance
  • Loading branch information
@jah12014
jah12014 committed Mar 26, 2018
1 parent da2b801 commit 4f3e99b
Showing 1 changed file with 105 additions and 37 deletions.
142 changes: 105 additions & 37 deletions IncrementalMinimization/src/IncrementalMinimization.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,66 +184,126 @@ private class EquivTestRecursive extends EquivTest
private class ResultDependencies
{
private boolean result;
private List<List<Integer>> dependencies; //List of pairs of states that must be equivalent for current result to hold.
private boolean isindependent;
private HashMap<List<Integer>, Boolean> dependencyTest; //List of pairs of states that must be equivalent for current result to hold.
private HashSet<List<Integer>> dependencies;

public ResultDependencies(boolean result, ArrayList<List<Integer>> dependencies)
public ResultDependencies(boolean result)
{
this.result = result;
this.dependencies = dependencies;
this.isindependent = true;
this.dependencyTest = new HashMap<List<Integer>, Boolean>();
this.dependencies = new HashSet<List<Integer>>();
}

public ResultDependencies(boolean result) //TODO: make sure correct constructor is called
public ResultDependencies(boolean result, List<Integer> dependency)
{
this(result, new ArrayList<List<Integer>>());
this(result);
addDependency(dependency);
this.isindependent = false;
}

public boolean resultIsIndependent()
{
return (dependencies == null) || dependencies.isEmpty();
return isindependent;
}

public void addDependency(List<Integer> dependent)
public void addDependency(List<Integer> pair)
{
if (isEquiv())
{
dependencies.add(dependent);
dependencyTest.put(pair, false);
dependencies.add(pair);
isindependent = false;
}
else
{
throw new IllegalStateException("False result has no dependencies");
}
}

public void removeDependency(List<Integer> pair)
{
dependencyTest.put(pair, true);
dependencies.remove(pair);
if (dependencies.isEmpty())
{
isindependent = true;
}
}

public boolean isDependency(List<Integer> pair)
{
return dependencies.contains(pair);
}

public void combineWithResult(ResultDependencies other)
{
System.out.println("here");
assert(result == other.isEquiv());
dependencies.addAll(other.getDependencies());
System.out.println(path);
System.out.println(getDependencies());
System.out.println("stop");
result = result && other.isEquiv();
if(!result)
{
dependencies.clear();
}
else
{
HashMap<List<Integer>, Boolean> otherDepends = other.getDependencyTests();
for (List<Integer> 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 List<List<Integer>> getDependencies()
public HashMap<List<Integer>, Boolean> getDependencyTests()
{
return dependencies;
return dependencyTest;
}
public void setResultFalse()

public void updateDepenencies()
{
result = false;
List<List<Integer>> checked = new LinkedList<List<Integer>>();
for (List<Integer> pair : dependencies)
{
if(!path.contains(pair))
{
dependencyTest.put(pair, true);
checked.add(pair);
}
}
dependencies.removeAll(checked);
}
}

private HashMap<List<Integer>, ResultDependencies> equivDepends;

public EquivTestRecursive(DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv,
HashSet<List<Integer>> path)
{
super(equivClasses, equiv, path);
this.equivDepends = new HashMap<List<Integer>, ResultDependencies>();
}

public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutException
Expand All @@ -263,10 +323,8 @@ public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutE
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));
ResultDependencies thisResult = new ResultDependencies(true);
assert(thisResult.isEquiv());
while (!outp.isEmpty() && !outq.isEmpty())
{
assert(thisResult.isEquiv());
List<SFAInputMove<P,S>> nonDisjointGuards = findNonDisjointMoves(outp,outq);
SFAInputMove<P,S> pMove = nonDisjointGuards.get(0);
SFAInputMove<P,S> qMove = nonDisjointGuards.get(1);
Expand All @@ -277,24 +335,37 @@ public ResultDependencies isEquivRecursive(Integer p, Integer q) throws TimeoutE
if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair))
{
equiv.add(nextPair);
ResultDependencies nextResult = isEquivRecursive(pNextClass, qNextClass);
if(!nextResult.isEquiv())
equivDepends.put(nextPair, null);
if(path.contains(nextPair))
{
return nextResult;
thisResult.addDependency(nextPair);
}
else
{
path.remove(nextPair);
assert(nextResult.isEquiv());
thisResult.combineWithResult(nextResult);
assert(thisResult.isEquiv());
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))
{
assert(thisResult.isEquiv());
thisResult.addDependency(nextPair);
assert(thisResult.isEquiv());
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);
Expand All @@ -309,13 +380,16 @@ else if (equiv.contains(nextPair))
outq.add(new SFAInputMove<P, S>(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;
}
Expand All @@ -324,12 +398,6 @@ else if (equiv.contains(nextPair))
public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
{
ResultDependencies finalResult = isEquivRecursive(pStart, qStart);
/*if(!finalResult.resultIsIndependent())
{
System.out.println(finalResult.getDependencies());
System.out.println(finalResult.isEquiv());
}
assert(finalResult.resultIsIndependent());*/
return finalResult.isEquiv();
}
}
Expand Down

0 comments on commit 4f3e99b

Please sign in to comment.