-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Need to add more tests in later but this is a start
- Loading branch information
Showing
4 changed files
with
130 additions
and
61 deletions.
There are no files selected for viewing
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,44 @@ | ||
| import static org.junit.Assert.*; | ||
| import junit.framework.Assert; | ||
|
|
||
| import org.junit.Before; | ||
| import org.junit.Test; | ||
|
|
||
| public class TestDisjointSets { | ||
|
|
||
| DisjointSets<Integer> sets; | ||
|
|
||
| private void initialize() | ||
| { | ||
| sets = new DisjointSets<Integer>(); | ||
| for (Integer i = 0; i < 10; i++) | ||
| { | ||
| sets.make(i); | ||
| } | ||
| } | ||
|
|
||
| @Test | ||
| public void testFind() | ||
| { | ||
| initialize(); | ||
| for (Integer i = 0; i < 10; i++) | ||
| { | ||
| Assert.assertEquals(i, sets.find(i)); | ||
| } | ||
| } | ||
|
|
||
| @Test | ||
| public void testUnion() | ||
| { | ||
| initialize(); | ||
| sets.union(new Integer(1), new Integer(2)); | ||
| Assert.assertEquals(sets.find(1), sets.find(2)); | ||
| Assert.assertEquals(new Integer(1),sets.find(1)); | ||
| Assert.assertEquals(new Integer(1),sets.find(2)); | ||
| sets.union(3, 4); | ||
| sets.union(2, 3); | ||
| Assert.assertEquals(sets.find(1), sets.find(4)); | ||
| Assert.assertFalse(sets.find(1).equals(sets.find(5))); | ||
| } | ||
|
|
||
| } |
85 changes: 85 additions & 0 deletions
85
IncrementalMinimization/src/TestIncrementalMinimization.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| import static org.junit.Assert.*; | ||
|
|
||
| import java.util.Arrays; | ||
| import java.util.Collection; | ||
| import java.util.LinkedList; | ||
|
|
||
| import org.junit.Assert; | ||
| import org.junit.Before; | ||
| import org.junit.Test; | ||
| 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 TestIncrementalMinimization { | ||
|
|
||
| @Test | ||
| public void testMyAut() throws TimeoutException { | ||
| //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<IntPred, Integer> incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); | ||
| SFA<IntPred, Integer> stdMinAut = aut.minimize(ba); //auts are equivalent but incrMin is not determinstic! | ||
| Assert.assertTrue(incrMinAut.isDeterministic(ba)); | ||
| Assert.assertTrue(stdMinAut.isDeterministic(ba)); | ||
| Assert.assertTrue(incrMinAut.getStates().size() <= stdMinAut.getStates().size()); | ||
| Assert.assertTrue(SFA.areEquivalent(incrMinAut, aut, ba)); | ||
| Assert.assertTrue(SFA.areEquivalent(incrMinAut, stdMinAut, ba)); | ||
|
|
||
| //Note that because of how the symbolic automata library stores automata that it does not | ||
| //recognize as explicitly minimal, we may have a case where our minimum automata has | ||
| //less states than theirs (b/c the SFA does not store "sink states" AFAIK). So, to check that | ||
| //our SFA is minimal, we test if it is deterministic and has no more than the minimum | ||
| //SFA that the library computes | ||
| } | ||
|
|
||
| //TODO: add more tests both for correctness and for speed | ||
|
|
||
| } |