Skip to content

Commit

Permalink
Many changes, mostly related to testing
Browse files Browse the repository at this point in the history
Added test to compare runtimes of standard incremental and incremental with neq initialized to only contain final/non-final pairs of states and started refactoring tests to perform multiple trials.
  • Loading branch information
jah12014 committed Apr 19, 2018
1 parent 23a17e9 commit 5680d5c
Show file tree
Hide file tree
Showing 8 changed files with 540 additions and 505 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ public static <P,S> SFA<P,S> mooreMinimize(SFA<P,S> aut, BooleanAlgebra<P,S> ba)
private SFA<P,S> aut;
private BooleanAlgebra<P,S> ba;

private MooreMinimization(SFA<P,S> aut, BooleanAlgebra<P,S> ba)
public MooreMinimization(SFA<P,S> aut, BooleanAlgebra<P,S> ba)
{
this.aut = aut;
this.ba = ba;
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
package minimization.incremental;

import java.util.Comparator;
import java.util.LinkedHashMap;
import java.util.List;

import org.sat4j.specs.TimeoutException;

import theory.BooleanAlgebra;
import automata.sfa.SFA;

/*
* CLASS FOR TESTING PURPOSES ONLY
*
* This class uses a naive non-equivalence check that initially only checks
* whether or not the given pair contains one final and one non-final state.
*/

public class IncrSimpleNEQ<P,S> extends IncrementalMinimization<P,S>
{
protected class StateComparatorSimple extends StateComparator
{
@Override
public int compare(Integer a, Integer b)
{
return a-b;
}
}

public IncrSimpleNEQ(SFA<P, S> aut, BooleanAlgebra<P, S> ba) throws TimeoutException
{
super(aut, ba);
this.stateComp = new StateComparatorSimple();
for(Integer p : aut.getFinalStates())
{
for(Integer q : aut.getNonFinalStates())
{
neq.add(normalize(p,q));
}
}
}

@Override
protected LinkedHashMap<Integer, Integer> generateDistanceToFinalMap()
{
return null;
}

@Override
protected Integer getStateDistanceToFinal(Integer state)
{
return 0;
}

@Override
protected boolean isKnownNotEqual(Integer p, Integer q)
{
List<Integer> normalizedPair = normalize(p,q);
return neq.contains(normalizedPair);
}
}
Original file line number Diff line number Diff line change
@@ -1,19 +1,14 @@
package minimization.incremental;

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.Queue;
import java.util.Stack;

import minimization.incremental.IncrementalMinimization.EquivTest;

import org.sat4j.specs.TimeoutException;

import structures.DependencyGraph;
import structures.DisjointSets;
import theory.BooleanAlgebra;
import automata.sfa.SFA;
Expand All @@ -25,196 +20,13 @@ public class IncrWithDependencyChecks<P,S> extends IncrementalMinimization<P,S>
protected class EquivTestDependency extends EquivTest //tests for equality of two given states in the automata
{

protected class Dependencies //tracks the pairs of states that an equivalence result depends on within our algorithm.
{
protected class StatePair
{
public final List<Integer> pair;
private boolean isTested;
private LinkedList<StatePair> deps;

public StatePair(List<Integer> pair, boolean isTested)
{
this.pair = pair;
this.isTested = isTested;
this.deps = new LinkedList<StatePair>();
}

public StatePair(List<Integer> pair)
{
this(pair, true);
}

public void addDependency(StatePair dep)
{
assert(dep != null);
deps.add(dep);
}

public LinkedList<StatePair> getDependencies()
{
return deps;
}

public boolean isTested()
{
return isTested;
}

public void setTested(boolean b)
{
isTested = b;
}

@Override
public boolean equals(Object other)
{
if(other == null || (other.getClass() != getClass()))
{
return false;
}
StatePair otherPair = (StatePair) other;
if(pair.equals((otherPair.pair)))
{
assert(deps.equals(otherPair.getDependencies()));
return true;
}
else
{
return false;
}
}

@Override
public int hashCode()
{
return pair.hashCode();
}

@Override
public String toString()
{
return String.format("%s | %s ", pair.toString(), Boolean.toString(isTested));
}

public String toStringLong()
{
return String.format("%s | %s | %s", pair.toString(), Boolean.toString(isTested), deps.toString());
}
}


private HashMap<List<Integer>,StatePair> pairLookup;

public Dependencies()
{
this.pairLookup = new HashMap<List<Integer>,StatePair>(num_pairs);
}

public void addDependency(List<Integer> pair, List<Integer> dependency)
{
if(pair.equals(dependency))
{
return;
}
StatePair pairEntry;
if(pairLookup.containsKey(pair))
{
pairEntry = pairLookup.get(pair);
pairEntry.setTested(true);
}
else
{
pairEntry = new StatePair(pair, true);
pairLookup.put(pair, pairEntry);
}
StatePair depEntry;
if(pairLookup.containsKey(dependency))
{
depEntry = pairLookup.get(dependency);
}
else
{
depEntry = new StatePair(dependency, false);
pairLookup.put(dependency, depEntry);
}
assert(depEntry != null);
pairEntry.addDependency(depEntry);
}

public void addAllDependencies(List<Integer> pair, ArrayList<List<Integer>> dpairs)
{
for(List<Integer> dpair : dpairs)
{
addDependency(pair, dpair);
}
}

private void mergePair(StatePair pairEntry, HashSet<List<Integer>> badPath) throws TimeoutException
{

Queue<StatePair> depQueue = new LinkedList<StatePair>();
depQueue.addAll(pairEntry.getDependencies());
//HashSet<List<Integer>> debugTest = new HashSet<List<Integer>>();
HashSet<StatePair> seenPairs = new HashSet<StatePair>();
while(!depQueue.isEmpty())
{
StatePair dep = depQueue.remove();
assert(! (dep == null));
if(seenPairs.contains(dep))
{
continue;
}
seenPairs.add(dep);
if(!dep.isTested())
{
return;
}
if(badPath.contains(dep.pair))
{
return;
}
assert(pairLookup.values().contains(dep));
depQueue.addAll(dep.getDependencies());
}
System.out.println("SQUIBLLITY DOOP BOP"); //unique string for debug purposes
equivClasses.union(pairEntry.pair.get(0), pairEntry.pair.get(1));
}

public void mergeStates(HashSet<List<Integer>> badPath) throws TimeoutException
{
for(StatePair pairEntry : pairLookup.values())
{
if(!pairEntry.isTested)
{
continue;
}
else if(badPath.contains(pairEntry.pair))
{
continue;
}
else
{
mergePair(pairEntry,badPath);
}
}
}
}

private Dependencies deps;

public EquivTestDependency (DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv,
HashSet<List<Integer>> path, Dependencies deps)
{
super(equivClasses, equiv, path);
this.deps = deps;
}
private DependencyGraph deps;

public EquivTestDependency (DisjointSets<Integer> equivClasses, HashSet<List<Integer>> equiv,
HashSet<List<Integer>> path)
{
super(equivClasses, equiv, path);
this.deps = new Dependencies();
this.deps = new DependencyGraph();
}

@Override
Expand All @@ -234,19 +46,19 @@ public boolean isEquiv(Integer pStart, Integer qStart) throws TimeoutException
Integer q = curEquivTest.qState;
HashSet<List<Integer>> curPath = curEquivTest.curPath;
List<Integer> pair = normalize(p,q);
HashSet<List<Integer>> newPath = new HashSet<List<Integer>>(curPath);
newPath.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())
{
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) || path.contains(nextPair))
if(equiv.contains(nextPair) || curPath.contains(nextPair))
{
deps.addDependency(pair, nextPair);
}
Expand All @@ -259,15 +71,16 @@ else if(!pNextClass.equals(qNextClass))
{
neq.add(pathPair); //TODO: remove this call from outer minimize method
}
this.path = newPath;
deps.mergeStates(newPath);
deps.mergeStates(equivClasses, newPath);
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);
Expand Down
Loading

0 comments on commit 5680d5c

Please sign in to comment.