fixed numerous issues with activation coder

4 files changed, 110 insertions, 41 deletions

diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java
index ba243d7d..24145d03 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java
@@ -14,7 +14,7 @@ public class ActivationStoreBitVectorEntry extends ActivationStoreEntry {
         }
 
         @Override
-        public int getNumberOfUnvisitedActivations() {
+        public int getNumberOfVisitedActivations() {
                 int visited = 0;
                 for (int i : selected) {
                         visited += Integer.bitCount(i);
@@ -29,12 +29,13 @@ public class ActivationStoreBitVectorEntry extends ActivationStoreEntry {
                 int position = index;
                 do {
                         final int selectedElement = position >> ELEMENT_POSITION;
-                        final int selectedBit = position & ELEMENT_BITMASK;
+                        final int selectedBit = 1<<(position & ELEMENT_BITMASK);
+
                         if((selected[selectedElement] & selectedBit) == 0) {
                                 selected[selectedElement] |= selectedBit;
                                 return position;
                         } else {
-                                if(position < this.numberOfActivations) {
+                                if(position < this.numberOfActivations-1) {
                                         position++;
                                 } else {
                                         position = 0;
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java
index f69b234c..d7339805 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java
@@ -12,11 +12,11 @@ public abstract class ActivationStoreEntry {
                 this.numberOfActivations = numberOfActivations;
         }
 
-        public int getNumberOfVisitedActivations() {
-                return numberOfActivations;
-        }
+        public abstract int getNumberOfVisitedActivations();
 
-        public abstract int getNumberOfUnvisitedActivations();
+        public int getNumberOfUnvisitedActivations() {
+                return numberOfActivations - getNumberOfVisitedActivations();
+        }
         public abstract int getAndAddActivationAfter(int index);
 
         //      public abstract boolean contains(int activation)
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java
index 9e25301f..3d4cbfdc 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java
@@ -16,8 +16,8 @@ public class ActivationStoreListEntry extends ActivationStoreEntry {
         }
 
         @Override
-        public int getNumberOfUnvisitedActivations() {
-                return this.numberOfActivations - visitedActivations.size();
+        public int getNumberOfVisitedActivations() {
+                return visitedActivations.size();
         }
 
         @Override
@@ -27,43 +27,52 @@ public class ActivationStoreListEntry extends ActivationStoreEntry {
                         this.visitedActivations.add(index);
                         return index;
                 }
+                final int positionInSearch = getPosition(index);
+                int position = positionInSearch;
 
-                int position = getPosition(index);
+                // if the position is after the last, we can insert it at the end of the list
+                if(position == this.visitedActivations.size()) {
+                        this.visitedActivations.add(index);
+                        return index;
+                } else if(this.visitedActivations.get(position) != index) {
+                        // If the index is not in the position, one can insert it
 
-                // If the index is not in the position, one can insert it
-                if(this.visitedActivations.get(position) != index) {
                         this.visitedActivations.addAtIndex(position,index);
                         return index;
                 }
 
                 // Otherwise, get the next empty space between two elements
-                while(position + 2 < this.visitedActivations.size()) {
-                        position++;
+                while(position + 1 < this.visitedActivations.size()) {
                         if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) {
-                                this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1);
+                                int newElement = this.visitedActivations.get(position)+1;
+                                this.visitedActivations.addAtIndex(position+1, newElement);
+                                return newElement;
                         }
+                        position++;
                 }
 
                 // Otherwise, try to add to the last space
                 int last = this.visitedActivations.get(this.visitedActivations.size()-1);
-                if(last<this.numberOfActivations) {
+                if(last<this.numberOfActivations-1) {
                         this.visitedActivations.add(last+1);
                         return last+1;
                 }
 
                 // Otherwise, try to put to the beginning
                 if(this.visitedActivations.get(0) > 0) {
-                        this.visitedActivations.add(0);
+                        this.visitedActivations.addAtIndex(0,0);
                         return 0;
                 }
 
                 // Otherwise, get the next empty space between two elements
                 position = 0;
-                while(position + 2 < this.visitedActivations.size()) {
-                        position++;
+                while(position < positionInSearch) {
                         if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) {
-                                this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1);
+                                int newElement = this.visitedActivations.get(position)+1;
+                                this.visitedActivations.addAtIndex(position+1, newElement);
+                                return newElement;
                         }
+                        position++;
                 }
 
                 throw new IllegalArgumentException("There is are no unvisited activations!");
diff --git a/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java b/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java
index e7960a06..3a672b18 100644
--- a/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java
+++ b/subprojects/store-dse/src/test/java/tools/refinery/store/dse/transition/statespace/internal/ActivationUnitTest.java
@@ -9,6 +9,11 @@ import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.MethodSource;
 
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+import java.util.Random;
+import java.util.function.Supplier;
 import java.util.stream.Stream;
 
 class ActivationUnitTest {
@@ -17,56 +22,110 @@ class ActivationUnitTest {
         private static Stream<ActivationStoreEntry> entries() {
                 return Stream.of(
                                 new ActivationStoreBitVectorEntry(SMALL_SIZE),
-                                new ActivationStoreListEntry(SMALL_SIZE));
+                                new ActivationStoreListEntry(SMALL_SIZE)
+                );
         }
 
         void addTest(ActivationStoreEntry entry, int elementsAdded) {
-                Assertions.assertEquals(elementsAdded,entry.getNumberOfVisitedActivations());
-                Assertions.assertEquals(SMALL_SIZE-elementsAdded,entry.getNumberOfUnvisitedActivations());
+                Assertions.assertEquals(elementsAdded, entry.getNumberOfVisitedActivations());
+                Assertions.assertEquals(SMALL_SIZE - elementsAdded, entry.getNumberOfUnvisitedActivations());
         }
 
         @ParameterizedTest
         @MethodSource("entries")
         void testDifferent(ActivationStoreEntry entry) {
                 int elementsAdded = 0;
-                addTest(entry,elementsAdded);
+                addTest(entry, elementsAdded);
                 Assertions.assertEquals(2, entry.getAndAddActivationAfter(2));
-                addTest(entry,++elementsAdded);
-                Assertions.assertEquals(3,entry.getAndAddActivationAfter(3));
-                addTest(entry,++elementsAdded);
-                Assertions.assertEquals(1,entry.getAndAddActivationAfter(1));
-                addTest(entry,++elementsAdded);
-                Assertions.assertEquals(4,entry.getAndAddActivationAfter(4));
-                addTest(entry,++elementsAdded);
-                Assertions.assertEquals(0,entry.getAndAddActivationAfter(0));
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
+                Assertions.assertEquals(3, entry.getAndAddActivationAfter(3));
+                addTest(entry, ++elementsAdded);
+                Assertions.assertEquals(1, entry.getAndAddActivationAfter(1));
+                addTest(entry, ++elementsAdded);
+                Assertions.assertEquals(4, entry.getAndAddActivationAfter(4));
+                addTest(entry, ++elementsAdded);
+                Assertions.assertEquals(0, entry.getAndAddActivationAfter(0));
+                addTest(entry, ++elementsAdded);
         }
 
+
         @ParameterizedTest
         @MethodSource("entries")
         void testSame(ActivationStoreEntry entry) {
                 int elementsAdded = 0;
-                addTest(entry,elementsAdded);
+                addTest(entry, 0);
                 entry.getAndAddActivationAfter(2);
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
                 entry.getAndAddActivationAfter(2);
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
                 entry.getAndAddActivationAfter(2);
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
                 entry.getAndAddActivationAfter(2);
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
                 entry.getAndAddActivationAfter(2);
-                addTest(entry,++elementsAdded);
+                addTest(entry, ++elementsAdded);
         }
 
         @ParameterizedTest
         @MethodSource("entries")
         void testFilling(ActivationStoreEntry entry) {
                 int elementsAdded = 0;
-                while(elementsAdded < SMALL_SIZE) {
+                while (elementsAdded < SMALL_SIZE) {
                         entry.getAndAddActivationAfter(2);
                         elementsAdded++;
                 }
-                Assertions.assertThrows(IllegalArgumentException.class,()-> entry.getAndAddActivationAfter(2));
+                Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2));
+        }
+
+        void randomDifferentTestCase(ActivationStoreEntry entry, int seed) {
+                List<Integer> elements = new ArrayList<>(SMALL_SIZE);
+                for (int i = 0; i < SMALL_SIZE; i++) {
+                        elements.add(i);
+                }
+                @SuppressWarnings("squid:S2245")
+                var random = new Random(seed);
+                Collections.shuffle(elements, random);
+
+                for (int element : elements) {
+                        entry.getAndAddActivationAfter(element);
+                }
+                Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2));
+        }
+
+        private static final int fuzzNumber = 20;
+
+        @ParameterizedTest
+        @MethodSource("entryFactories")
+        void randomDifferentTest(Supplier<ActivationStoreEntry> entry) {
+                for (int i = 0; i < fuzzNumber; i++) {
+                        randomDifferentTestCase(entry.get(), i);
+                }
+        }
+
+        void randomSameTestCase(ActivationStoreEntry entry, int seed) {
+
+                @SuppressWarnings("squid:S2245")
+                var random = new Random(seed);
+
+                for (int i = 0; i < SMALL_SIZE; i++) {
+                        entry.getAndAddActivationAfter(random.nextInt(SMALL_SIZE));
+                }
+
+                Assertions.assertThrows(IllegalArgumentException.class, () -> entry.getAndAddActivationAfter(2));
+        }
+
+        @ParameterizedTest
+        @MethodSource("entryFactories")
+        void randomSameTest(Supplier<ActivationStoreEntry> entry) {
+                for (int i = 0; i < fuzzNumber; i++) {
+                        randomSameTestCase(entry.get(), i);
+                }
+        }
+
+        private static Stream<Supplier<ActivationStoreEntry>> entryFactories() {
+                return Stream.of(
+                                () -> new ActivationStoreBitVectorEntry(SMALL_SIZE),
+                                () -> new ActivationStoreListEntry(SMALL_SIZE)
+                );
         }
 }