fix(dse): best-first strategy

The query engine must be flushed after firing a tranformation activation.

6 files changed, 69 insertions, 161 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 a2b6268f..8f7e3bdc 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
@@ -5,7 +5,6 @@
  */
 package tools.refinery.store.dse.strategy;
 
-import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.model.Model;
 
 import java.util.Random;
@@ -13,6 +12,7 @@ import java.util.Random;
 public class BestFirstExplorer extends BestFirstWorker {
         final int id;
         Random random;
+
         public BestFirstExplorer(BestFirstStoreManager storeManager, Model model, int id) {
                 super(storeManager, model);
                 this.id = id;
@@ -20,6 +20,7 @@ public class BestFirstExplorer extends BestFirstWorker {
         }
 
         private boolean interrupted = false;
+
         public void interrupt() {
                 this.interrupted = true;
         }
@@ -29,138 +30,37 @@ public class BestFirstExplorer extends BestFirstWorker {
         }
 
         public void explore() {
-                VersionWithObjectiveValue lastVisited = submit().newVersion();
-
+                var lastBest = submit().newVersion();
                 while (shouldRun()) {
-
-                        if (lastVisited == null) {
-                                lastVisited = this.restoreToBest();
-                                if(lastVisited == null) {
+                        if (lastBest == null) {
+                                lastBest = restoreToBest();
+                                if (lastBest == null) {
                                         return;
                                 }
                         }
-
                         boolean tryActivation = true;
-                        while(tryActivation && shouldRun()) {
-                                RandomVisitResult randomVisitResult = this.visitRandomUnvisited(random);
-
+                        while (tryActivation && shouldRun()) {
+                                var randomVisitResult = this.visitRandomUnvisited(random);
                                 tryActivation = randomVisitResult.shouldRetry();
                                 var newSubmit = randomVisitResult.submitResult();
-                                if(newSubmit != null) {
-                                        if(!newSubmit.include()) {
+                                if (newSubmit != null) {
+                                        if (!newSubmit.include()) {
                                                 restoreToLast();
                                         } else {
                                                 var newVisit = newSubmit.newVersion();
-                                                int compareResult = compare(lastVisited,newVisit);
-                                                if(compareResult >= 0) {
-                                                        lastVisited = newVisit;
-                                                        break;
-                                                }
-                                        }
-                                }
-                                else {
-                                        lastVisited = null;
-                                        break;
-                                }
-                        }
-
-                //final ObjectiveComparatorHelper objectiveComparatorHelper = dseAdapter.getObjectiveComparatorHelper();
-
-                /*boolean globalConstraintsAreSatisfied = dseAdapter.checkGlobalConstraints();
-                if (!globalConstraintsAreSatisfied) {
-                        // Global constraint is not satisfied in the first state. Terminate.
-                        return;
-                }
-
-                final Fitness firstFitness = dseAdapter.getFitness();
-                if (firstFitness.isSatisfiesHardObjectives()) {
-                        dseAdapter.newSolution();
-                        // First state is a solution. Terminate.
-                        if (backTrackIfSolution) {
-                                return;
-                        }
-                }
-
-                if (maxDepth == 0) {
-                        return;
-                }*/
-
-                /*
-                var firstTrajectoryWithFitness = new TrajectoryWithFitness(dseAdapter.getTrajectory(), firstFitness);
-                trajectoriesToExplore.add(firstTrajectoryWithFitness);
-                TrajectoryWithFitness currentTrajectoryWithFitness = null;
-                */
-/*
-                        Collection<Activation> activations = dseAdapter.getUntraversedActivations();
-                        Iterator<Activation> iterator = activations.iterator();
-
-                        while (iterator.hasNext()) {
-                                final Activation nextActivation = iterator.next();
-                                if (!iterator.hasNext()) {
-                                        // Last untraversed activation of the state.
-                                        trajectoriesToExplore.remove(currentTrajectoryWithFitness);
-                                }
-
-                                // Executing new activation
-                                dseAdapter.fireActivation(nextActivation);
-                                if (dseAdapter.isCurrentStateAlreadyTraversed()) {
-                                        // The new state is already visited.
-                                        dseAdapter.backtrack();
-                                } else if (!dseAdapter.checkGlobalConstraints()) {
-                                        // Global constraint is not satisfied.
-                                        dseAdapter.backtrack();
-                                } else {
-                                        final Fitness nextFitness = dseAdapter.getFitness();
-                                        if (nextFitness.isSatisfiesHardObjectives()) {
-                                                dseAdapter.newSolution();
-                                                var solutions = dseAdapter.getSolutions().size();
-                                                if (solutions >= maxSolutions) {
-                                                        return;
-                                                }
-                                                // Found a solution.
-                                                if (backTrackIfSolution) {
-                                                        dseAdapter.backtrack();
-                                                        continue;
-                                                }
-                                        }
-                                        if (dseAdapter.getDepth() >= maxDepth) {
-                                                // Reached max depth.
-                                                dseAdapter.backtrack();
-                                                continue;
-                                        }
-
-                                        TrajectoryWithFitness nextTrajectoryWithFitness = new TrajectoryWithFitness(
-                                                        dseAdapter.getTrajectory(), nextFitness);
-                                        trajectoriesToExplore.add(nextTrajectoryWithFitness);
-
-                                        int compare = objectiveComparatorHelper.compare(currentTrajectoryWithFitness.fitness,
-                                                        nextTrajectoryWithFitness.fitness);
-                                        if (compare < 0) {
-                                                // Better fitness, moving on
-                                                currentTrajectoryWithFitness = nextTrajectoryWithFitness;
-                                                continue mainLoop;
-                                        } else if (compare == 0) {
-                                                if (onlyBetterFirst) {
-                                                        // Equally good fitness, backtrack
-                                                        dseAdapter.backtrack();
+                                                int compareResult = compare(lastBest, newVisit);
+                                                if (compareResult >= 0) {
+                                                        lastBest = newVisit;
                                                 } else {
-                                                        // Equally good fitness, moving on
-                                                        currentTrajectoryWithFitness = nextTrajectoryWithFitness;
-                                                        continue mainLoop;
+                                                        lastBest = null;
                                                 }
-                                        } else {
-                                                //"Worse fitness
-                                                currentTrajectoryWithFitness = null;
-                                                continue mainLoop;
+                                                break;
                                         }
+                                } else {
+                                        lastBest = null;
+                                        break;
                                 }
                         }
-
-                        // State is fully traversed.
-                        currentTrajectoryWithFitness = null;
-*/
                 }
-                // Interrupted.
-
         }
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
index 4ccba6f7..02634a02 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
@@ -17,9 +17,7 @@ import tools.refinery.store.dse.transition.statespace.internal.ObjectivePriority
 import tools.refinery.store.dse.transition.statespace.internal.SolutionStoreImpl;
 import tools.refinery.store.map.Version;
 import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.statecoding.StateCoderResult;
 import tools.refinery.store.statecoding.StateCoderStoreAdapter;
-import tools.refinery.visualization.ModelVisualizerStoreAdapter;
 import tools.refinery.visualization.statespace.VisualizationStore;
 import tools.refinery.visualization.statespace.internal.VisualizationStoreImpl;
 
@@ -34,7 +32,7 @@ public class BestFirstStoreManager {
         EquivalenceClassStore equivalenceClassStore;
         VisualizationStore visualizationStore;
 
-        public BestFirstStoreManager(ModelStore modelStore) {
+        public BestFirstStoreManager(ModelStore modelStore, int maxNumberOfSolutions) {
                 this.modelStore = modelStore;
                 DesignSpaceExplorationStoreAdapter storeAdapter =
                                 modelStore.getAdapter(DesignSpaceExplorationStoreAdapter.class);
@@ -42,7 +40,7 @@ public class BestFirstStoreManager {
                 objectiveStore = new ObjectivePriorityQueueImpl(storeAdapter.getObjectives());
                 Consumer<VersionWithObjectiveValue> whenAllActivationsVisited = x -> objectiveStore.remove(x);
                 activationStore = new ActivationStoreImpl(storeAdapter.getTransformations().size(), whenAllActivationsVisited);
-                solutionStore = new SolutionStoreImpl(50);
+                solutionStore = new SolutionStoreImpl(maxNumberOfSolutions);
                 equivalenceClassStore = new FastEquivalenceClassStore(modelStore.getAdapter(StateCoderStoreAdapter.class)) {
                         @Override
                         protected void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept) {
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 f1bec14f..5d738297 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
@@ -40,11 +40,13 @@ public class BestFirstWorker {
                 isVisualizationEnabled = visualizationStore != null;
         }
 
-        private VersionWithObjectiveValue last = null;
-
-        //public boolean isIncluded
+        protected VersionWithObjectiveValue last = null;
 
         public SubmitResult submit() {
+                checkSynchronized();
+                if (queryAdapter.hasPendingChanges()) {
+                        throw new AssertionError("Pending changes detected before model submission");
+                }
                 if (explorationAdapter.checkExclude()) {
                         return new SubmitResult(false, false, null, null);
                 }
@@ -86,14 +88,11 @@ public class BestFirstWorker {
 
         public VersionWithObjectiveValue restoreToBest() {
                 var bestVersion = storeManager.getObjectiveStore().getBest();
+                last = bestVersion;
                 if (bestVersion != null) {
-                        var oldVersion = model.getState();
                         this.model.restore(bestVersion.version());
-                        if (isVisualizationEnabled) {
-                                visualizationStore.addTransition(oldVersion, last.version(), "");
-                        }
                 }
-                return bestVersion;
+                return last;
         }
 
         public VersionWithObjectiveValue restoreToRandom(Random random) {
@@ -102,7 +101,7 @@ public class BestFirstWorker {
                 if (randomVersion != null) {
                         this.model.restore(randomVersion.version());
                 }
-                return randomVersion;
+                return last;
         }
 
         public int compare(VersionWithObjectiveValue s1, VersionWithObjectiveValue s2) {
@@ -121,9 +120,10 @@ public class BestFirstWorker {
         }
 
         public RandomVisitResult visitRandomUnvisited(Random random) {
+                checkSynchronized();
                 if (!model.hasUncommittedChanges()) {
-                        queryAdapter.flushChanges();
                         var visitResult = activationStoreWorker.fireRandomActivation(this.last, random);
+                        queryAdapter.flushChanges();
 
                         if (visitResult.successfulVisit()) {
                                 Version oldVersion = null;
@@ -133,7 +133,8 @@ public class BestFirstWorker {
                                 var submitResult = submit();
                                 if (isVisualizationEnabled && submitResult.newVersion() != null) {
                                         var newVersion = submitResult.newVersion().version();
-                                        visualizationStore.addTransition(oldVersion, newVersion, "");
+                                        visualizationStore.addTransition(oldVersion, newVersion,
+                                                        "fire: " + visitResult.transformation() + ", " + visitResult.activation());
                                 }
                                 return new RandomVisitResult(submitResult, visitResult.mayHaveMore());
                         } else {
@@ -147,4 +148,10 @@ public class BestFirstWorker {
         public boolean hasEnoughSolution() {
                 return storeManager.solutionStore.hasEnoughSolution();
         }
+
+        private void checkSynchronized() {
+                if (last != null && !last.version().equals(model.getState())) {
+                        throw new AssertionError("Worker is not synchronized with model state");
+                }
+        }
 }
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 24145d03..c204ae35 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
@@ -16,32 +16,35 @@ public class ActivationStoreBitVectorEntry extends ActivationStoreEntry {
         @Override
         public int getNumberOfVisitedActivations() {
                 int visited = 0;
-                for (int i : selected) {
-                        visited += Integer.bitCount(i);
+                // Use indexed for loop to avoid allocating an iterator.
+                //noinspection ForLoopReplaceableByForEach
+                for (int i = 0; i < selected.length; i++) {
+                        visited += Integer.bitCount(selected[i]);
                 }
                 return visited;
         }
 
         private static final int ELEMENT_POSITION = 5; // size of Integer.SIZE
-        private static final int ELEMENT_BITMASK = (1<<ELEMENT_POSITION)-1;
+        private static final int ELEMENT_BITMASK = (1 << ELEMENT_POSITION) - 1;
+
         @Override
         public int getAndAddActivationAfter(int index) {
                 int position = index;
                 do {
                         final int selectedElement = position >> ELEMENT_POSITION;
-                        final int selectedBit = 1<<(position & ELEMENT_BITMASK);
+                        final int selectedBit = 1 << (position & ELEMENT_BITMASK);
 
-                        if((selected[selectedElement] & selectedBit) == 0) {
+                        if ((selected[selectedElement] & selectedBit) == 0) {
                                 selected[selectedElement] |= selectedBit;
                                 return position;
                         } else {
-                                if(position < this.numberOfActivations-1) {
+                                if (position < this.numberOfActivations - 1) {
                                         position++;
                                 } else {
                                         position = 0;
                                 }
                         }
-                } while(position != index);
-                throw  new IllegalArgumentException("There is are no unvisited activations!");
+                } while (position != index);
+                throw new IllegalArgumentException("There is are no unvisited activations!");
         }
 }
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 d7339805..7249751c 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
@@ -17,6 +17,11 @@ public abstract class ActivationStoreEntry {
         public int getNumberOfUnvisitedActivations() {
                 return numberOfActivations - getNumberOfVisitedActivations();
         }
+
+        public int getNumberOfActivations() {
+                return numberOfActivations;
+        }
+
         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/ActivationStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
index 4d775b5a..d9e29eca 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
@@ -28,7 +28,7 @@ public class ActivationStoreImpl implements ActivationStore {
                 var entries = versionToActivations.computeIfAbsent(to, x -> {
                         successful[0] = true;
                         List<ActivationStoreEntry> result = new ArrayList<>(emptyEntrySizes.length);
-                        for(int emptyEntrySize : emptyEntrySizes) {
+                        for (int emptyEntrySize : emptyEntrySizes) {
                                 result.add(ActivationStoreEntry.create(emptyEntrySize));
                         }
                         return result;
@@ -40,13 +40,14 @@ public class ActivationStoreImpl implements ActivationStore {
                                 break;
                         }
                 }
-                if(!hasMore) {
+                if (!hasMore) {
                         actionWhenAllActivationVisited.accept(to);
                 }
                 return new VisitResult(successful[0], hasMore, -1, -1);
         }
 
-        public synchronized VisitResult visitActivation(VersionWithObjectiveValue from, int transformationIndex, int activationIndex) {
+        public synchronized VisitResult visitActivation(VersionWithObjectiveValue from, int transformationIndex,
+                                                                                                        int activationIndex) {
                 var entries = versionToActivations.get(from);
                 var entry = entries.get(transformationIndex);
                 final int unvisited = entry.getNumberOfUnvisitedActivations();
@@ -66,7 +67,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         activation = -1;
                 }
 
-                if(!hasMoreInActivation) {
+                if (!hasMoreInActivation) {
                         boolean hasMoreInOtherTransformation = false;
                         for (var e : entries) {
                                 if (e != entry && e.getNumberOfUnvisitedActivations() > 0) {
@@ -79,7 +80,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         hasMore = true;
                 }
 
-                if(!hasMore) {
+                if (!hasMore) {
                         actionWhenAllActivationVisited.accept(from);
                 }
 
@@ -103,34 +104,28 @@ public class ActivationStoreImpl implements ActivationStore {
         public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) {
                 var entries = versionToActivations.get(version);
 
-                int sum1 = 0;
+                int numberOfAllUnvisitedActivations = 0;
                 for (var entry : entries) {
-                        sum1 += entry.getNumberOfUnvisitedActivations();
+                        numberOfAllUnvisitedActivations += entry.getNumberOfUnvisitedActivations();
                 }
 
-                if(sum1 == 0) {
+                if (numberOfAllUnvisitedActivations == 0) {
                         this.actionWhenAllActivationVisited.accept(version);
                         return new VisitResult(false, false, -1, -1);
                 }
 
-                int selected = random.nextInt(sum1);
-                int sum2 = 0;
+                int offset = random.nextInt(numberOfAllUnvisitedActivations);
                 int transformation = 0;
-                int activation = -1;
                 for (; transformation < entries.size(); transformation++) {
                         var entry = entries.get(transformation);
                         int unvisited = entry.getNumberOfUnvisitedActivations();
-                        if (selected < sum2 + unvisited) {
-                                activation = sum2 + unvisited - selected - 1;
-                                break;
-                        } else {
-                                sum2 += unvisited;
+                        if (unvisited > 0 && offset < unvisited) {
+                                int activation = random.nextInt(entry.getNumberOfActivations());
+                                return this.visitActivation(version, transformation, activation);
                         }
-                }
-                if (activation == -1) {
-                        throw new IllegalArgumentException("no unvisited");
+                        offset -= unvisited;
                 }
 
-                return this.visitActivation(version, transformation, activation);
+                throw new AssertionError("Unvisited activation %d not found".formatted(offset));
         }
 }