Fix numerous issues with DSE

5 files changed, 16 insertions, 18 deletions

diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
index 03a7fca3..f82d7c06 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
@@ -58,6 +58,10 @@ public class BestFirstExplorer extends BestFirstWorker {
                                                 }
                                         }
                                 }
+                                else {
+                                        lastVisited = null;
+                                        break;
+                                }
                         }
 
                 //final ObjectiveComparatorHelper objectiveComparatorHelper = dseAdapter.getObjectiveComparatorHelper();
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
index 4240fdf9..b8662d8d 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
@@ -45,12 +45,12 @@ public class BestFirstWorker {
 
                 Version version = model.commit();
                 ObjectiveValue objectiveValue = explorationAdapter.getObjectiveValue();
-                var res = new VersionWithObjectiveValue(version, objectiveValue);
+                last = new VersionWithObjectiveValue(version, objectiveValue);
                 var code = stateCoderAdapter.calculateStateCode();
                 var accepted = explorationAdapter.checkAccept();
-                boolean isNew = storeManager.getEquivalenceClassStore().submit(res, code,
+                boolean isNew = storeManager.getEquivalenceClassStore().submit(last, code,
                                 activationStoreWorker.calculateEmptyActivationSize(), accepted);
-                return new SubmitResult(isNew, accepted, objectiveValue, isNew ? res : null);
+                return new SubmitResult(isNew, accepted, objectiveValue, isNew ? last : null);
         }
 
         public void restoreToLast() {
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
index 1229ec15..559c715a 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
@@ -66,7 +66,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         activation = -1;
                 }
 
-                if(hasMoreInActivation) {
+                if(!hasMoreInActivation) {
                         boolean hasMoreInOtherTransformation = false;
                         for (var e : entries) {
                                 if (e != entry && e.getNumberOfVisitedActivations() > 0) {
@@ -83,7 +83,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         actionWhenAllActivationVisited.accept(from);
                 }
 
-                return new VisitResult(false, hasMore, transformation, activation);
+                return new VisitResult(successfulVisit, hasMore, transformation, activation);
         }
 
         @Override
@@ -116,7 +116,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         var entry = entries.get(transformation);
                         int unvisited = entry.getNumberOfUnvisitedActivations();
                         if (selected < sum2 + unvisited) {
-                                activation = sum2 + unvisited - selected;
+                                activation = sum2 + unvisited - selected - 1;
                                 break;
                         } else {
                                 sum2 += unvisited;
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ObjectivePriorityQueueImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ObjectivePriorityQueueImpl.java
index 249b22da..c88a411f 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ObjectivePriorityQueueImpl.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ObjectivePriorityQueueImpl.java
@@ -53,12 +53,7 @@ public class ObjectivePriorityQueueImpl implements ObjectivePriorityQueue {
 
         @Override
         public VersionWithObjectiveValue getBest() {
-                var best = priorityQueue.peek();
-                if (best != null) {
-                        return best;
-                } else {
-                        throw new IllegalArgumentException("The objective store is empty!");
-                }
+                return priorityQueue.peek();
         }
 
         @Override
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/SolutionStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/SolutionStoreImpl.java
index cc48864f..43548eaa 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/SolutionStoreImpl.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/SolutionStoreImpl.java
@@ -10,17 +10,17 @@ import tools.refinery.store.dse.transition.statespace.SolutionStore;
 
 import java.util.ArrayList;
 import java.util.List;
-import java.util.SortedSet;
-import java.util.TreeSet;
+import java.util.PriorityQueue;
+
 
 public class SolutionStoreImpl implements SolutionStore {
         final int maxNumberSolutions;
         public static final int UNLIMITED = -1;
-        final SortedSet<VersionWithObjectiveValue> solutions;
+        final PriorityQueue<VersionWithObjectiveValue> solutions;
 
         public SolutionStoreImpl(int maxNumberSolutions) {
                 this.maxNumberSolutions = maxNumberSolutions;
-                solutions = new TreeSet<>(ObjectivePriorityQueueImpl.c1);
+                solutions = new PriorityQueue<>(ObjectivePriorityQueueImpl.c1.reversed());
         }
 
 
@@ -29,8 +29,7 @@ public class SolutionStoreImpl implements SolutionStore {
                 boolean removeLast = hasEnoughSolution();
                 solutions.add(version);
                 if(removeLast) {
-                        var last = solutions.last();
-                        solutions.remove(last);
+                        var last = solutions.poll();
                         return last != version;
                 } else {
                         return true;