diff --git a/IncrementalMinimization/lib/symbolicautomata.jar b/IncrementalMinimization/lib/symbolicautomata.jar index b8811025..67796227 100644 Binary files a/IncrementalMinimization/lib/symbolicautomata.jar and b/IncrementalMinimization/lib/symbolicautomata.jar differ diff --git a/IncrementalMinimization/src/Main.java b/IncrementalMinimization/src/IncrementalMinimization.java similarity index 67% rename from IncrementalMinimization/src/Main.java rename to IncrementalMinimization/src/IncrementalMinimization.java index 1d409a6d..9388cdd5 100644 --- a/IncrementalMinimization/src/Main.java +++ b/IncrementalMinimization/src/IncrementalMinimization.java @@ -7,7 +7,6 @@ import java.util.List; import java.util.Set; -import org.apache.commons.lang3.NotImplementedException; import org.sat4j.specs.TimeoutException; import theory.BooleanAlgebra; @@ -17,7 +16,7 @@ import automata.sfa.SFAInputMove; import automata.sfa.SFAMove; -public class Main +public class IncrementalMinimization { private static class EquivTest { @@ -220,63 +219,4 @@ else if(equivClasses.find(p) == equivClasses.find(q)) return SFA.MkSFA(newTransitions, newInitialState, newFinalStates, ba); } - public static void main(String[] args) throws TimeoutException - { - //TODO: move tests to separate class - - //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 > transitions = new LinkedList>(); - IntPred a_pred = ba.MkAnd(ba.MkNot(one), ba.MkNot(zero)); - transitions.add(new SFAInputMove(0,0,a_pred)); - transitions.add(new SFAInputMove(0,1,zero)); - transitions.add(new SFAInputMove(0,2,one)); - transitions.add(new SFAInputMove(1,0,zero)); - transitions.add(new SFAInputMove(1,1,a_pred)); - transitions.add(new SFAInputMove(1,2,one)); - IntPred b_pred = ba.MkAnd(pos, ba.MkNot(zero_five)); - transitions.add(new SFAInputMove(2,2,b_pred)); - transitions.add(new SFAInputMove(2,3,neg)); - IntPred c_pred = ba.MkAnd(ba.MkNot(zero), zero_five); - transitions.add(new SFAInputMove(2,5,c_pred)); - transitions.add(new SFAInputMove(2,6,zero)); - transitions.add(new SFAInputMove(3,3,ba.True())); - transitions.add(new SFAInputMove(4,4,ba.True())); - transitions.add(new SFAInputMove(5,3, neg)); - transitions.add(new SFAInputMove(5,3,c_pred)); - transitions.add(new SFAInputMove(5,6,zero)); - transitions.add(new SFAInputMove(5,7,b_pred)); - transitions.add(new SFAInputMove(6,4,neg)); - transitions.add(new SFAInputMove(6,4,c_pred)); - transitions.add(new SFAInputMove(6,5,zero)); - transitions.add(new SFAInputMove(6,7,b_pred)); - transitions.add(new SFAInputMove(7,1,zero)); - transitions.add(new SFAInputMove(7,4,ba.MkNot(c_pred))); - transitions.add(new SFAInputMove(7,8,c_pred)); - transitions.add(new SFAInputMove(8,0,zero)); - transitions.add(new SFAInputMove(8,3,ba.MkNot(c_pred))); - transitions.add(new SFAInputMove(8,7,c_pred)); - - //SFA is defined - SFA aut = SFA.MkSFA(transitions, 0, Arrays.asList(7,8), ba); - - //SFA is tested - assert(aut.accepts(Arrays.asList(1,7,10),ba)); - assert(aut.isDeterministic(ba)); - assert(aut.isTotal()); - - - SFA minAut = incrementalMinimize(aut, ba); - System.out.println(minAut.getStates().size()); - System.out.println(aut.minimize(ba).getStates().size()); - } } diff --git a/IncrementalMinimization/src/TestDisjointSets.java b/IncrementalMinimization/src/TestDisjointSets.java new file mode 100644 index 00000000..4a01b073 --- /dev/null +++ b/IncrementalMinimization/src/TestDisjointSets.java @@ -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 sets; + + private void initialize() + { + sets = new DisjointSets(); + 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))); + } + +} diff --git a/IncrementalMinimization/src/TestIncrementalMinimization.java b/IncrementalMinimization/src/TestIncrementalMinimization.java new file mode 100644 index 00000000..01363d50 --- /dev/null +++ b/IncrementalMinimization/src/TestIncrementalMinimization.java @@ -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 > transitions = new LinkedList>(); + IntPred a_pred = ba.MkAnd(ba.MkNot(one), ba.MkNot(zero)); + transitions.add(new SFAInputMove(0,0,a_pred)); + transitions.add(new SFAInputMove(0,1,zero)); + transitions.add(new SFAInputMove(0,2,one)); + transitions.add(new SFAInputMove(1,0,zero)); + transitions.add(new SFAInputMove(1,1,a_pred)); + transitions.add(new SFAInputMove(1,2,one)); + IntPred b_pred = ba.MkAnd(pos, ba.MkNot(zero_five)); + transitions.add(new SFAInputMove(2,2,b_pred)); + transitions.add(new SFAInputMove(2,3,neg)); + IntPred c_pred = ba.MkAnd(ba.MkNot(zero), zero_five); + transitions.add(new SFAInputMove(2,5,c_pred)); + transitions.add(new SFAInputMove(2,6,zero)); + transitions.add(new SFAInputMove(3,3,ba.True())); + transitions.add(new SFAInputMove(4,4,ba.True())); + transitions.add(new SFAInputMove(5,3, neg)); + transitions.add(new SFAInputMove(5,3,c_pred)); + transitions.add(new SFAInputMove(5,6,zero)); + transitions.add(new SFAInputMove(5,7,b_pred)); + transitions.add(new SFAInputMove(6,4,neg)); + transitions.add(new SFAInputMove(6,4,c_pred)); + transitions.add(new SFAInputMove(6,5,zero)); + transitions.add(new SFAInputMove(6,7,b_pred)); + transitions.add(new SFAInputMove(7,1,zero)); + transitions.add(new SFAInputMove(7,4,ba.MkNot(c_pred))); + transitions.add(new SFAInputMove(7,8,c_pred)); + transitions.add(new SFAInputMove(8,0,zero)); + transitions.add(new SFAInputMove(8,3,ba.MkNot(c_pred))); + transitions.add(new SFAInputMove(8,7,c_pred)); + + //SFA is defined + SFA aut = SFA.MkSFA(transitions, 0, Arrays.asList(7,8), ba); + + SFA incrMinAut = IncrementalMinimization.incrementalMinimize(aut, ba); + SFA 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 + +}