Skip to content

Commit

Permalink
Incremental Minimization fully implemented but not yet fully tested
Browse files Browse the repository at this point in the history
  • Loading branch information
@jah12014
jah12014 committed Nov 27, 2017
1 parent 5190e62 commit b8f5b27
Showing 1 changed file with 98 additions and 23 deletions.
121 changes: 98 additions & 23 deletions IncrementalMinimization/src/Main.java
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
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.Set;

import org.apache.commons.lang3.NotImplementedException;
Expand All @@ -19,44 +21,116 @@ public class Main
{
private static class EquivTest<P,S>
{
private SFA<P,S> aut;
private HashSet<Integer[]> equiv;
private HashSet<Integer[]> path;
private final SFA<P,S> aut;
private final BooleanAlgebra<P, S> ba;
private final DisjointSets<Integer> equivClasses;

public EquivTest(SFA<P,S> aut, HashSet<Integer[]> equiv, HashSet<Integer[]> path)
private HashSet<List<Integer>> neq;
private HashSet<List<Integer>> equiv;
private HashSet<List<Integer>> path;

public EquivTest(SFA<P,S> aut, BooleanAlgebra<P,S> ba, DisjointSets<Integer> equivClasses,
HashSet<List<Integer>> neq, HashSet<List<Integer>> equiv, HashSet<List<Integer>> path)
{
this.aut = aut;
this.ba = ba;
this.equivClasses = equivClasses;
this.neq = neq;
this.equiv = equiv;
this.path = path;
}

public boolean isEquiv(Integer p, Integer q) throws NotImplementedException
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
SFAInputMove<P,S> pMove = outp.iterator().next();
P pGuard = pMove.guard;
for(SFAInputMove<P,S> qMove : outq)
{
P qGuard = qMove.guard;
P pqAnd = ba.MkAnd(pGuard, qGuard);
if(ba.IsSatisfiable(pqAnd))
{
return Arrays.asList(pMove,qMove);
}
}
return null;
}

public boolean isEquiv(Integer p, Integer q) throws TimeoutException
{
//TODO
throw new NotImplementedException("Incremental Equivalence Not Implemented Yet");
List<Integer> pair = Arrays.asList(p, q); //Should already be normalized
if (neq.contains(pair))
{
return false;
}
if (path.contains(pair))
{
return true;
}
path.add(pair);
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())
{
List<SFAInputMove<P,S>> nonDisjointGuards = findNonDisjointMoves(outp,outq);
SFAInputMove<P,S> pMove = nonDisjointGuards.get(0);
SFAInputMove<P,S> 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<Integer> nextPair = normalize(pNextClass, qNextClass);
if ( !pNextClass.equals(qNextClass) && !equiv.contains(nextPair))
{
equiv.add(nextPair);
if(!isEquiv(pNextClass, qNextClass))
{
return false;
}
else
{
path.remove(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(pair);
return true;
}

public HashSet<Integer[]> getEquiv()
public HashSet<List<Integer>> getEquiv()
{
return equiv;
}

public HashSet<Integer[]> getPath()
public HashSet<List<Integer>> getPath()
{
return path;
}
}

private static Integer[] normalize(Integer p, Integer q)
private static List<Integer> normalize(Integer p, Integer q)
{
Integer[] pair;
List<Integer> pair;
if(p<q)
{
pair = new Integer[]{p,q};
pair = Arrays.asList(p,q);
}
else
{
pair = new Integer[]{q,p};
pair = Arrays.asList(q,p);
}
return pair;
}
Expand All @@ -67,14 +141,14 @@ public static <P, S> SFA<P, S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<
{
return SFA.getEmptySFA(ba);
}
aut = aut.determinize(ba).mkTotal(ba);
aut = aut.determinize(ba).mkTotal(ba); //TODO: normalizes?
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
HashSet<List<Integer>> neq = new HashSet<List<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())
Expand All @@ -91,10 +165,9 @@ public static <P, S> SFA<P, S> incrementalMinimize(SFA<P,S> aut, BooleanAlgebra<
{
continue;
}
Integer[] pair = new Integer[]{p,q};
List<Integer> pair = Arrays.asList(p,q);
if(neq.contains(pair))
{
//Already know p,q not equivalent
continue;
}
else if(equivClasses.find(p) == equivClasses.find(q))
Expand All @@ -104,21 +177,21 @@ else if(equivClasses.find(p) == equivClasses.find(q))
}

//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);
HashSet<List<Integer>> equiv = new HashSet<List<Integer>>(num_pairs,1);
HashSet<List<Integer>> path = new HashSet<List<Integer>>(num_pairs,1);
EquivTest<P,S> pEquiv = new EquivTest<P,S>(aut, ba, equivClasses, neq, equiv, path);
if(pEquiv.isEquiv(p,q))
{
//p,q found equivalent. Other pairs may be found equivalent.
for(Integer[] equivPair : pEquiv.getEquiv())
for(List<Integer> equivPair : pEquiv.getEquiv())
{
equivClasses.union(equivPair[0], equivPair[1]);
equivClasses.union(equivPair.get(0), equivPair.get(1));
}
}
else
{
//p,q found non-equivalent. Other pairs may be found non-equivalent.
for(Integer[] pathPair : pEquiv.getPath())
for(List<Integer> pathPair : pEquiv.getPath())
{
neq.add(pathPair);
}
Expand Down Expand Up @@ -203,5 +276,7 @@ public static void main(String[] args) throws TimeoutException


SFA<IntPred, Integer> minAut = incrementalMinimize(aut, ba);
System.out.println(minAut.getStates().size());
System.out.println(aut.minimize(ba).getStates().size());
}
}

0 comments on commit b8f5b27

Please sign in to comment.