fixed numerous issues with activation coder

3 files changed, 30 insertions, 20 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!");