Merge remote-tracking branch 'nagilooh/datastructure' into partial-interpretation

11 files changed, 113 insertions, 54 deletions

diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationStoreAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationStoreAdapterImpl.java
index 913cb33f..62e4227b 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationStoreAdapterImpl.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationStoreAdapterImpl.java
@@ -24,6 +24,6 @@ public class ModificationStoreAdapterImpl implements ModificationStoreAdapter {
 
         @Override
         public ModelAdapter createModelAdapter(Model model) {
-                return null;
+                return new ModificationAdapterImpl(this, model);
         }
 }
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 72bbbc55..a2b6268f 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.ObjectiveValue;
 import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.model.Model;
 
@@ -32,13 +31,11 @@ public class BestFirstExplorer extends BestFirstWorker {
         public void explore() {
                 VersionWithObjectiveValue lastVisited = submit().newVersion();
 
-                mainLoop: while (shouldRun()) {
+                while (shouldRun()) {
 
                         if (lastVisited == null) {
-                                var restored = this.restoreToBest();
-                                if(restored != null) {
-                                        lastVisited = restored;
-                                } else {
+                                lastVisited = this.restoreToBest();
+                                if(lastVisited == null) {
                                         return;
                                 }
                         }
@@ -47,7 +44,7 @@ public class BestFirstExplorer extends BestFirstWorker {
                         while(tryActivation && shouldRun()) {
                                 RandomVisitResult randomVisitResult = this.visitRandomUnvisited(random);
 
-                                tryActivation &= randomVisitResult.shouldRetry();
+                                tryActivation = randomVisitResult.shouldRetry();
                                 var newSubmit = randomVisitResult.submitResult();
                                 if(newSubmit != null) {
                                         if(!newSubmit.include()) {
@@ -57,10 +54,14 @@ public class BestFirstExplorer extends BestFirstWorker {
                                                 int compareResult = compare(lastVisited,newVisit);
                                                 if(compareResult >= 0) {
                                                         lastVisited = newVisit;
-                                                        continue mainLoop;
+                                                        break;
                                                 }
                                         }
                                 }
+                                else {
+                                        lastVisited = null;
+                                        break;
+                                }
                         }
 
                 //final ObjectiveComparatorHelper objectiveComparatorHelper = dseAdapter.getObjectiveComparatorHelper();
@@ -160,5 +161,6 @@ public class BestFirstExplorer extends BestFirstWorker {
 */
                 }
                 // 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 693b0903..4ccba6f7 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,16 +17,22 @@ 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;
 
 import java.util.function.Consumer;
 
 public class BestFirstStoreManager {
+
         ModelStore modelStore;
         ObjectivePriorityQueue objectiveStore;
         ActivationStore activationStore;
         SolutionStore solutionStore;
         EquivalenceClassStore equivalenceClassStore;
+        VisualizationStore visualizationStore;
 
         public BestFirstStoreManager(ModelStore modelStore) {
                 this.modelStore = modelStore;
@@ -36,17 +42,17 @@ 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(1);
+                solutionStore = new SolutionStoreImpl(50);
                 equivalenceClassStore = new FastEquivalenceClassStore(modelStore.getAdapter(StateCoderStoreAdapter.class)) {
                         @Override
                         protected void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept) {
-                                objectiveStore.submit(version);
-                                activationStore.markNewAsVisited(version, emptyActivations);
-                                if(accept) {
-                                        solutionStore.submit(version);
-                                }
+                                throw new UnsupportedOperationException("This equivalence storage is not prepared to resolve symmetries!");
                         }
                 };
+                visualizationStore = new VisualizationStoreImpl();
+        }
+        public ModelStore getModelStore() {
+                return modelStore;
         }
 
         ObjectivePriorityQueue getObjectiveStore() {
@@ -57,7 +63,7 @@ public class BestFirstStoreManager {
                 return activationStore;
         }
 
-        SolutionStore getSolutionStore() {
+        public SolutionStore getSolutionStore() {
                 return solutionStore;
         }
 
@@ -65,6 +71,10 @@ public class BestFirstStoreManager {
                 return equivalenceClassStore;
         }
 
+        public VisualizationStore getVisualizationStore() {
+                return visualizationStore;
+        }
+
         public void startExploration(Version initial) {
                 BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial), 1);
                 bestFirstExplorer.explore();
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 ea7fe43f..f1bec14f 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
@@ -11,8 +11,9 @@ import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.dse.transition.statespace.internal.ActivationStoreWorker;
 import tools.refinery.store.map.Version;
 import tools.refinery.store.model.Model;
+import tools.refinery.store.query.ModelQueryAdapter;
 import tools.refinery.store.statecoding.StateCoderAdapter;
-
+import tools.refinery.visualization.statespace.VisualizationStore;
 
 import java.util.Random;
 
@@ -22,6 +23,9 @@ public class BestFirstWorker {
         final ActivationStoreWorker activationStoreWorker;
         final StateCoderAdapter stateCoderAdapter;
         final DesignSpaceExplorationAdapter explorationAdapter;
+        final ModelQueryAdapter queryAdapter;
+        final VisualizationStore visualizationStore;
+        final boolean isVisualizationEnabled;
 
         public BestFirstWorker(BestFirstStoreManager storeManager, Model model) {
                 this.storeManager = storeManager;
@@ -29,8 +33,11 @@ public class BestFirstWorker {
 
                 explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class);
                 stateCoderAdapter = model.getAdapter(StateCoderAdapter.class);
+                queryAdapter = model.getAdapter(ModelQueryAdapter.class);
                 activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(),
                                 explorationAdapter.getTransformations());
+                visualizationStore = storeManager.getVisualizationStore();
+                isVisualizationEnabled = visualizationStore != null;
         }
 
         private VersionWithObjectiveValue last = null;
@@ -39,21 +46,36 @@ public class BestFirstWorker {
 
         public SubmitResult submit() {
                 if (explorationAdapter.checkExclude()) {
-                        last = null;
                         return new SubmitResult(false, false, null, null);
                 }
 
-                Version version = model.commit();
-                ObjectiveValue objectiveValue = explorationAdapter.getObjectiveValue();
-                var res = new VersionWithObjectiveValue(version, objectiveValue);
                 var code = stateCoderAdapter.calculateStateCode();
-                var accepted = explorationAdapter.checkAccept();
 
-                boolean isNew = storeManager.getEquivalenceClassStore().submit(res, code,
-                                activationStoreWorker.calculateEmptyActivationSize(), accepted);
+                boolean isNew = storeManager.getEquivalenceClassStore().submit(code);
+                if (isNew) {
+                        Version version = model.commit();
+                        ObjectiveValue objectiveValue = explorationAdapter.getObjectiveValue();
+                        var versionWithObjectiveValue = new VersionWithObjectiveValue(version, objectiveValue);
+                        last = versionWithObjectiveValue;
+                        var accepted = explorationAdapter.checkAccept();
+
+                        storeManager.getObjectiveStore().submit(versionWithObjectiveValue);
+                        storeManager.getActivationStore().markNewAsVisited(versionWithObjectiveValue, activationStoreWorker.calculateEmptyActivationSize());
+                        if(accepted) {
+                                storeManager.solutionStore.submit(versionWithObjectiveValue);
+                        }
+
+                        if (isVisualizationEnabled) {
+                                visualizationStore.addState(last.version(), last.objectiveValue().toString());
+                                if (accepted) {
+                                        visualizationStore.addSolution(last.version());
+                                }
+                        }
+
+                        return new SubmitResult(true, accepted, objectiveValue, last);
+                }
 
-                last = new VersionWithObjectiveValue(version, objectiveValue);
-                return new SubmitResult(isNew, accepted, objectiveValue, last);
+                return new SubmitResult(false, false, null, null);
         }
 
         public void restoreToLast() {
@@ -65,7 +87,11 @@ public class BestFirstWorker {
         public VersionWithObjectiveValue restoreToBest() {
                 var bestVersion = storeManager.getObjectiveStore().getBest();
                 if (bestVersion != null) {
+                        var oldVersion = model.getState();
                         this.model.restore(bestVersion.version());
+                        if (isVisualizationEnabled) {
+                                visualizationStore.addTransition(oldVersion, last.version(), "");
+                        }
                 }
                 return bestVersion;
         }
@@ -91,14 +117,25 @@ public class BestFirstWorker {
                 }
         }
 
-        record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) {
+        public record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) {
         }
 
         public RandomVisitResult visitRandomUnvisited(Random random) {
                 if (!model.hasUncommittedChanges()) {
+                        queryAdapter.flushChanges();
                         var visitResult = activationStoreWorker.fireRandomActivation(this.last, random);
+
                         if (visitResult.successfulVisit()) {
-                                return new RandomVisitResult(submit(), visitResult.mayHaveMore());
+                                Version oldVersion = null;
+                                if (isVisualizationEnabled) {
+                                        oldVersion = last.version();
+                                }
+                                var submitResult = submit();
+                                if (isVisualizationEnabled && submitResult.newVersion() != null) {
+                                        var newVersion = submitResult.newVersion().version();
+                                        visualizationStore.addTransition(oldVersion, newVersion, "");
+                                }
+                                return new RandomVisitResult(submitResult, visitResult.mayHaveMore());
                         } else {
                                 return new RandomVisitResult(null, visitResult.mayHaveMore());
                         }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/EquivalenceClassStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/EquivalenceClassStore.java
index bbe26fe5..28d1488b 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/EquivalenceClassStore.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/EquivalenceClassStore.java
@@ -10,6 +10,7 @@ import tools.refinery.store.statecoding.StateCoderResult;
 
 public interface EquivalenceClassStore {
         boolean submit(VersionWithObjectiveValue version, StateCoderResult stateCoderResult, int[] emptyActivations, boolean accept);
+        boolean submit(StateCoderResult stateCoderResult);
         boolean hasUnresolvedSymmetry();
         void resolveOneSymmetry();
         int getNumberOfUnresolvedSymmetries();
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/AbstractEquivalenceClassStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/AbstractEquivalenceClassStore.java
index 8466a0f3..b5087e86 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/AbstractEquivalenceClassStore.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/AbstractEquivalenceClassStore.java
@@ -22,6 +22,13 @@ public abstract class AbstractEquivalenceClassStore implements EquivalenceClassS
         protected abstract boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion,
                                                            int[] emptyActivations, boolean accept);
 
+        public abstract boolean tryToAdd(StateCoderResult stateCoderResult);
+
+        @Override
+        public boolean submit(StateCoderResult stateCoderResult) {
+                return tryToAdd(stateCoderResult);
+        }
+
         @Override
         public synchronized boolean submit(VersionWithObjectiveValue version, StateCoderResult stateCoderResult,
                                                                            int[] emptyActivations, boolean accept) {
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 3e59b21a..4d775b5a 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
@@ -29,7 +29,7 @@ public class ActivationStoreImpl implements ActivationStore {
                         successful[0] = true;
                         List<ActivationStoreEntry> result = new ArrayList<>(emptyEntrySizes.length);
                         for(int emptyEntrySize : emptyEntrySizes) {
-                                result.add(ActivationStoreListEntry.create(emptyEntrySize));
+                                result.add(ActivationStoreEntry.create(emptyEntrySize));
                         }
                         return result;
                 });
@@ -66,10 +66,10 @@ public class ActivationStoreImpl implements ActivationStore {
                         activation = -1;
                 }
 
-                if(hasMoreInActivation) {
+                if(!hasMoreInActivation) {
                         boolean hasMoreInOtherTransformation = false;
                         for (var e : entries) {
-                                if (e != entry && e.getNumberOfVisitedActivations() > 0) {
+                                if (e != entry && e.getNumberOfUnvisitedActivations() > 0) {
                                         hasMoreInOtherTransformation = true;
                                         break;
                                 }
@@ -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
@@ -108,6 +108,11 @@ public class ActivationStoreImpl implements ActivationStore {
                         sum1 += entry.getNumberOfUnvisitedActivations();
                 }
 
+                if(sum1 == 0) {
+                        this.actionWhenAllActivationVisited.accept(version);
+                        return new VisitResult(false, false, -1, -1);
+                }
+
                 int selected = random.nextInt(sum1);
                 int sum2 = 0;
                 int transformation = 0;
@@ -116,7 +121,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/ActivationStoreWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
index e05f5122..881b133c 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
@@ -8,7 +8,6 @@ package tools.refinery.store.dse.transition.statespace.internal;
 import tools.refinery.store.dse.transition.Transformation;
 import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.dse.transition.statespace.ActivationStore;
-import tools.refinery.store.map.Version;
 
 import java.util.List;
 import java.util.Random;
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/FastEquivalenceClassStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/FastEquivalenceClassStore.java
index 6ee8e196..6d028124 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/FastEquivalenceClassStore.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/FastEquivalenceClassStore.java
@@ -16,12 +16,17 @@ public abstract class FastEquivalenceClassStore extends AbstractEquivalenceClass
 
         private final MutableIntSet codes = IntSets.mutable.empty();
 
-        public FastEquivalenceClassStore(StateCoderStoreAdapter stateCoderStoreAdapter) {
+        protected FastEquivalenceClassStore(StateCoderStoreAdapter stateCoderStoreAdapter) {
                 super(stateCoderStoreAdapter);
         }
 
         @Override
-        protected boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion, int[] emptyActivations, boolean accept) {
+        protected synchronized boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion,
+                                                                int[] emptyActivations, boolean accept) {
+                return this.codes.add(stateCoderResult.modelCode());
+        }
+
+        public synchronized boolean tryToAdd(StateCoderResult stateCoderResult) {
                 return this.codes.add(stateCoderResult.modelCode());
         }
 
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..2f3e142a 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
@@ -9,7 +9,6 @@ import tools.refinery.store.dse.transition.ObjectiveValues;
 import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.dse.transition.objectives.Objective;
 import tools.refinery.store.dse.transition.statespace.ObjectivePriorityQueue;
-import tools.refinery.store.map.Version;
 
 import java.util.Comparator;
 import java.util.List;
@@ -37,32 +36,27 @@ public class ObjectivePriorityQueueImpl implements ObjectivePriorityQueue {
         }
 
         @Override
-        public void submit(VersionWithObjectiveValue versionWithObjectiveValue) {
+        public synchronized void submit(VersionWithObjectiveValue versionWithObjectiveValue) {
                 priorityQueue.add(versionWithObjectiveValue);
         }
 
         @Override
-        public void remove(VersionWithObjectiveValue versionWithObjectiveValue) {
+        public synchronized void remove(VersionWithObjectiveValue versionWithObjectiveValue) {
                 priorityQueue.remove(versionWithObjectiveValue);
         }
 
         @Override
-        public int getSize() {
+        public synchronized int getSize() {
                 return priorityQueue.size();
         }
 
         @Override
-        public VersionWithObjectiveValue getBest() {
-                var best = priorityQueue.peek();
-                if (best != null) {
-                        return best;
-                } else {
-                        throw new IllegalArgumentException("The objective store is empty!");
-                }
+        public synchronized VersionWithObjectiveValue getBest() {
+                return priorityQueue.peek();
         }
 
         @Override
-        public VersionWithObjectiveValue getRandom(Random random) {
+        public synchronized VersionWithObjectiveValue getRandom(Random random) {
                 int randomPosition = random.nextInt(getSize());
                 for (VersionWithObjectiveValue entry : this.priorityQueue) {
                         if (randomPosition-- == 0) {
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;