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

42 files changed, 1987 insertions, 0 deletions

diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/ActionFactory.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/ActionFactory.java
new file mode 100644
index 00000000..48a508b4
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/ActionFactory.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.function.Consumer;
+
+public interface ActionFactory {
+        Consumer<Tuple> prepare(Model model);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationAdapter.java
new file mode 100644
index 00000000..f15c16e0
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationAdapter.java
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.dse.modification.internal.ModificationBuilderImpl;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
+
+public interface ModificationAdapter extends ModelAdapter {
+
+        int getModelSize();
+
+        Tuple1 createObject();
+
+        Tuple deleteObject(Tuple tuple);
+
+        static ModificationBuilder builder() {
+                return new ModificationBuilderImpl();
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationBuilder.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationBuilder.java
new file mode 100644
index 00000000..48c22bdf
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationBuilder.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+
+public interface ModificationBuilder extends ModelAdapterBuilder {
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationStoreAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationStoreAdapter.java
new file mode 100644
index 00000000..144c4d05
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/ModificationStoreAdapter.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+
+public interface ModificationStoreAdapter extends ModelStoreAdapter {
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationAdapterImpl.java
new file mode 100644
index 00000000..b2a80d71
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationAdapterImpl.java
@@ -0,0 +1,62 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification.internal;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.dse.modification.ModificationAdapter;
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
+
+public class ModificationAdapterImpl implements ModificationAdapter {
+        static final Symbol<Integer> NEXT_ID = Symbol.of("NEXT_ID", 0, Integer.class, 0);
+
+        final ModelStoreAdapter storeAdapter;
+        final Model model;
+        Interpretation<Integer> nodeCountInterpretation;
+
+        ModificationAdapterImpl(ModelStoreAdapter storeAdapter, Model model) {
+                this.storeAdapter = storeAdapter;
+                this.model = model;
+                this.nodeCountInterpretation = model.getInterpretation(NEXT_ID);
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public ModelStoreAdapter getStoreAdapter() {
+                return storeAdapter;
+        }
+
+        @Override
+        public int getModelSize() {
+                return nodeCountInterpretation.get(Tuple.of());
+        }
+
+        @Override
+        public Tuple1 createObject() {
+                var newNodeId = getModelSize();
+                nodeCountInterpretation.put(Tuple.of(), newNodeId + 1);
+                return Tuple.of(newNodeId);
+        }
+
+        @Override
+        public Tuple deleteObject(Tuple tuple) {
+                if (tuple.getSize() != 1) {
+                        throw new IllegalArgumentException("Tuple size must be 1");
+                }
+//              TODO: implement more efficient deletion
+                if (tuple.get(0) == getModelSize() - 1) {
+                        nodeCountInterpretation.put(Tuple.of(), getModelSize() - 1);
+                }
+                return tuple;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationBuilderImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationBuilderImpl.java
new file mode 100644
index 00000000..c4d38d22
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationBuilderImpl.java
@@ -0,0 +1,29 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification.internal;
+
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.dse.modification.ModificationBuilder;
+import tools.refinery.store.dse.modification.ModificationStoreAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.statecoding.StateCoderBuilder;
+
+public class ModificationBuilderImpl extends AbstractModelAdapterBuilder<ModificationStoreAdapter> implements ModificationBuilder {
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                storeBuilder.symbols(ModificationAdapterImpl.NEXT_ID);
+                storeBuilder.tryGetAdapter(StateCoderBuilder.class).ifPresent(
+                                coderBuilder -> coderBuilder.exclude(ModificationAdapterImpl.NEXT_ID));
+                super.doConfigure(storeBuilder);
+        }
+
+        @Override
+        protected ModificationStoreAdapter doBuild(ModelStore store) {
+                return new ModificationStoreAdapterImpl(store);
+        }
+}
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
new file mode 100644
index 00000000..913cb33f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/modification/internal/ModificationStoreAdapterImpl.java
@@ -0,0 +1,29 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.modification.internal;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.dse.modification.ModificationStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+
+public class ModificationStoreAdapterImpl implements ModificationStoreAdapter {
+        ModelStore store;
+
+        ModificationStoreAdapterImpl(ModelStore store) {
+                this.store = store;
+        }
+
+        @Override
+        public ModelStore getStore() {
+                return store;
+        }
+
+        @Override
+        public ModelAdapter createModelAdapter(Model model) {
+                return null;
+        }
+}
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
new file mode 100644
index 00000000..72bbbc55
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
@@ -0,0 +1,164 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+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;
+
+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;
+                this.random = new Random(id);
+        }
+
+        private boolean interrupted = false;
+        public void interrupt() {
+                this.interrupted = true;
+        }
+
+        private boolean shouldRun() {
+                return !interrupted && !hasEnoughSolution();
+        }
+
+        public void explore() {
+                VersionWithObjectiveValue lastVisited = submit().newVersion();
+
+                mainLoop: while (shouldRun()) {
+
+                        if (lastVisited == null) {
+                                var restored = this.restoreToBest();
+                                if(restored != null) {
+                                        lastVisited = restored;
+                                } else {
+                                        return;
+                                }
+                        }
+
+                        boolean tryActivation = true;
+                        while(tryActivation && shouldRun()) {
+                                RandomVisitResult randomVisitResult = this.visitRandomUnvisited(random);
+
+                                tryActivation &= randomVisitResult.shouldRetry();
+                                var newSubmit = randomVisitResult.submitResult();
+                                if(newSubmit != null) {
+                                        if(!newSubmit.include()) {
+                                                restoreToLast();
+                                        } else {
+                                                var newVisit = newSubmit.newVersion();
+                                                int compareResult = compare(lastVisited,newVisit);
+                                                if(compareResult >= 0) {
+                                                        lastVisited = newVisit;
+                                                        continue mainLoop;
+                                                }
+                                        }
+                                }
+                        }
+
+                //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();
+                                                } else {
+                                                        // Equally good fitness, moving on
+                                                        currentTrajectoryWithFitness = nextTrajectoryWithFitness;
+                                                        continue mainLoop;
+                                                }
+                                        } else {
+                                                //"Worse fitness
+                                                currentTrajectoryWithFitness = null;
+                                                continue mainLoop;
+                                        }
+                                }
+                        }
+
+                        // 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
new file mode 100644
index 00000000..693b0903
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
@@ -0,0 +1,72 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.strategy;
+
+import tools.refinery.store.dse.transition.DesignSpaceExplorationStoreAdapter;
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.ActivationStore;
+import tools.refinery.store.dse.transition.statespace.EquivalenceClassStore;
+import tools.refinery.store.dse.transition.statespace.ObjectivePriorityQueue;
+import tools.refinery.store.dse.transition.statespace.SolutionStore;
+import tools.refinery.store.dse.transition.statespace.internal.ActivationStoreImpl;
+import tools.refinery.store.dse.transition.statespace.internal.FastEquivalenceClassStore;
+import tools.refinery.store.dse.transition.statespace.internal.ObjectivePriorityQueueImpl;
+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.StateCoderStoreAdapter;
+
+import java.util.function.Consumer;
+
+public class BestFirstStoreManager {
+        ModelStore modelStore;
+        ObjectivePriorityQueue objectiveStore;
+        ActivationStore activationStore;
+        SolutionStore solutionStore;
+        EquivalenceClassStore equivalenceClassStore;
+
+        public BestFirstStoreManager(ModelStore modelStore) {
+                this.modelStore = modelStore;
+                DesignSpaceExplorationStoreAdapter storeAdapter =
+                                modelStore.getAdapter(DesignSpaceExplorationStoreAdapter.class);
+
+                objectiveStore = new ObjectivePriorityQueueImpl(storeAdapter.getObjectives());
+                Consumer<VersionWithObjectiveValue> whenAllActivationsVisited = x -> objectiveStore.remove(x);
+                activationStore = new ActivationStoreImpl(storeAdapter.getTransformations().size(), whenAllActivationsVisited);
+                solutionStore = new SolutionStoreImpl(1);
+                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);
+                                }
+                        }
+                };
+        }
+
+        ObjectivePriorityQueue getObjectiveStore() {
+                return objectiveStore;
+        }
+
+        ActivationStore getActivationStore() {
+                return activationStore;
+        }
+
+        SolutionStore getSolutionStore() {
+                return solutionStore;
+        }
+
+        EquivalenceClassStore getEquivalenceClassStore() {
+                return equivalenceClassStore;
+        }
+
+        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
new file mode 100644
index 00000000..ea7fe43f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
@@ -0,0 +1,113 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.strategy;
+
+import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
+import tools.refinery.store.dse.transition.ObjectiveValue;
+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.statecoding.StateCoderAdapter;
+
+
+import java.util.Random;
+
+public class BestFirstWorker {
+        final BestFirstStoreManager storeManager;
+        final Model model;
+        final ActivationStoreWorker activationStoreWorker;
+        final StateCoderAdapter stateCoderAdapter;
+        final DesignSpaceExplorationAdapter explorationAdapter;
+
+        public BestFirstWorker(BestFirstStoreManager storeManager, Model model) {
+                this.storeManager = storeManager;
+                this.model = model;
+
+                explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class);
+                stateCoderAdapter = model.getAdapter(StateCoderAdapter.class);
+                activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(),
+                                explorationAdapter.getTransformations());
+        }
+
+        private VersionWithObjectiveValue last = null;
+
+        //public boolean isIncluded
+
+        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);
+
+                last = new VersionWithObjectiveValue(version, objectiveValue);
+                return new SubmitResult(isNew, accepted, objectiveValue, last);
+        }
+
+        public void restoreToLast() {
+                if (explorationAdapter.getModel().hasUncommittedChanges()) {
+                        explorationAdapter.getModel().restore(last.version());
+                }
+        }
+
+        public VersionWithObjectiveValue restoreToBest() {
+                var bestVersion = storeManager.getObjectiveStore().getBest();
+                if (bestVersion != null) {
+                        this.model.restore(bestVersion.version());
+                }
+                return bestVersion;
+        }
+
+        public VersionWithObjectiveValue restoreToRandom(Random random) {
+                var randomVersion = storeManager.getObjectiveStore().getRandom(random);
+                last = randomVersion;
+                if (randomVersion != null) {
+                        this.model.restore(randomVersion.version());
+                }
+                return randomVersion;
+        }
+
+        public int compare(VersionWithObjectiveValue s1, VersionWithObjectiveValue s2) {
+                return storeManager.getObjectiveStore().getComparator().compare(s1, s2);
+        }
+
+        public boolean stateHasUnvisited() {
+                if (!model.hasUncommittedChanges()) {
+                        return storeManager.getActivationStore().hasUnmarkedActivation(last);
+                } else {
+                        throw new IllegalStateException("The model has uncommitted changes!");
+                }
+        }
+
+        record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) {
+        }
+
+        public RandomVisitResult visitRandomUnvisited(Random random) {
+                if (!model.hasUncommittedChanges()) {
+                        var visitResult = activationStoreWorker.fireRandomActivation(this.last, random);
+                        if (visitResult.successfulVisit()) {
+                                return new RandomVisitResult(submit(), visitResult.mayHaveMore());
+                        } else {
+                                return new RandomVisitResult(null, visitResult.mayHaveMore());
+                        }
+                } else {
+                        throw new IllegalStateException("The model has uncommitted changes!");
+                }
+        }
+
+        public boolean hasEnoughSolution() {
+                return storeManager.solutionStore.hasEnoughSolution();
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/SubmitResult.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/SubmitResult.java
new file mode 100644
index 00000000..37d548d7
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/SubmitResult.java
@@ -0,0 +1,14 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.strategy;
+
+import tools.refinery.store.dse.transition.ObjectiveValue;
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.map.Version;
+
+public record SubmitResult(boolean include, boolean accepted, ObjectiveValue objective, VersionWithObjectiveValue newVersion) {
+
+        }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java
new file mode 100644
index 00000000..37448309
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationAdapter.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.dse.transition.internal.DesignSpaceExplorationBuilderImpl;
+import tools.refinery.store.map.Version;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
+
+import java.util.Collection;
+import java.util.List;
+
+public interface DesignSpaceExplorationAdapter extends ModelAdapter {
+
+
+
+        @Override
+        DesignSpaceExplorationStoreAdapter getStoreAdapter();
+
+        static DesignSpaceExplorationBuilder builder() {
+                return new DesignSpaceExplorationBuilderImpl();
+        }
+        List<Transformation> getTransformations();
+        boolean checkAccept();
+        boolean checkExclude();
+        ObjectiveValue getObjectiveValue();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationBuilder.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationBuilder.java
new file mode 100644
index 00000000..3855a20a
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationBuilder.java
@@ -0,0 +1,59 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.dse.transition.objectives.Criterion;
+import tools.refinery.store.dse.transition.objectives.Objective;
+
+import java.util.Collection;
+import java.util.List;
+
+public interface DesignSpaceExplorationBuilder extends ModelAdapterBuilder {
+
+        DesignSpaceExplorationBuilder transformation(TransformationRule transformationRuleDefinition);
+        default DesignSpaceExplorationBuilder transformations(TransformationRule... transformationRuleDefinitions) {
+                return transformations(List.of(transformationRuleDefinitions));
+        }
+
+        default DesignSpaceExplorationBuilder transformations(Collection<? extends TransformationRule> transformationRules) {
+                transformationRules.forEach(this::transformation);
+                return this;
+        }
+
+        DesignSpaceExplorationBuilder accept(Criterion criteria);
+
+        default DesignSpaceExplorationBuilder accept(Criterion... criteria) {
+                return accept(List.of(criteria));
+        }
+
+        default DesignSpaceExplorationBuilder accept(Collection<Criterion> criteria) {
+                criteria.forEach(this::accept);
+                return this;
+        }
+
+        DesignSpaceExplorationBuilder exclude(Criterion criteria);
+
+        default DesignSpaceExplorationBuilder exclude(Criterion... criteria) {
+                return exclude(List.of(criteria));
+        }
+
+        default DesignSpaceExplorationBuilder exclude(Collection<Criterion> criteria) {
+                criteria.forEach(this::exclude);
+                return this;
+        }
+
+        DesignSpaceExplorationBuilder objective(Objective objective);
+
+        default DesignSpaceExplorationBuilder objectives(Objective... objectives) {
+                return objectives(List.of(objectives));
+        }
+
+        default DesignSpaceExplorationBuilder objectives(Collection<? extends Objective> objectives) {
+                objectives.forEach(this::objective);
+                return this;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationStoreAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationStoreAdapter.java
new file mode 100644
index 00000000..5c8c7a4d
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/DesignSpaceExplorationStoreAdapter.java
@@ -0,0 +1,27 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.dse.transition.objectives.Criterion;
+import tools.refinery.store.dse.transition.objectives.Objective;
+import tools.refinery.store.model.Model;
+
+import java.util.List;
+
+public interface DesignSpaceExplorationStoreAdapter extends ModelStoreAdapter
+{
+        @Override
+        DesignSpaceExplorationAdapter createModelAdapter(Model model);
+
+        List<TransformationRule> getTransformations();
+
+        List<Criterion> getAccepts();
+
+        List<Criterion> getExcludes();
+
+        List<Objective> getObjectives();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValue.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValue.java
new file mode 100644
index 00000000..89ee61c8
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValue.java
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+public interface ObjectiveValue {
+        double get(int index);
+        int getSize();
+
+        static ObjectiveValue of(double v1) {
+                return new ObjectiveValues.ObjectiveValue1(v1);
+        }
+
+        static ObjectiveValue of(double v1, double v2) {
+                return new ObjectiveValues.ObjectiveValue2(v1,v2);
+        }
+
+        static ObjectiveValue of(double[] v) {
+                return new ObjectiveValues.ObjectiveValueN(v);
+        }
+
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValues.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValues.java
new file mode 100644
index 00000000..60913ff3
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/ObjectiveValues.java
@@ -0,0 +1,69 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import java.util.Arrays;
+
+public interface ObjectiveValues {
+        public record ObjectiveValue1(double value0) implements ObjectiveValue {
+                @Override
+                public double get(int index) {
+                        if(index == 0) return value0;
+                        else throw new IllegalArgumentException("No value at " + index);
+                }
+
+                @Override
+                public int getSize() {
+                        return 1;
+                }
+        }
+        public record ObjectiveValue2(double value0, double value1) implements ObjectiveValue {
+                @Override
+                public double get(int index) {
+                        if(index == 0) return value0;
+                        else if(index == 1) return value1;
+                        else throw new IllegalArgumentException("No value at " + index);
+                }
+
+                @Override
+                public int getSize() {
+                        return 2;
+                }
+        }
+        public record ObjectiveValueN(double[] values) implements ObjectiveValue {
+                @Override
+                public double get(int index) {
+                        return values[index];
+                }
+
+                @Override
+                public int getSize() {
+                        return values().length;
+                }
+
+                @Override
+                public boolean equals(Object o) {
+                        if (this == o) return true;
+                        if (o == null || getClass() != o.getClass()) return false;
+
+                        ObjectiveValueN that = (ObjectiveValueN) o;
+
+                        return Arrays.equals(values, that.values);
+                }
+
+                @Override
+                public int hashCode() {
+                        return Arrays.hashCode(values);
+                }
+
+                @Override
+                public String toString() {
+                        return "ObjectiveValueN{" +
+                                        "values=" + Arrays.toString(values) +
+                                        '}';
+                }
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/Transformation.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/Transformation.java
new file mode 100644
index 00000000..ab9fda3e
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/Transformation.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.query.resultset.OrderedResultSet;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.function.Consumer;
+
+public class Transformation {
+        private final TransformationRule definition;
+
+        private final OrderedResultSet<Boolean> activations;
+
+        private final Consumer<Tuple> action;
+
+        public Transformation(TransformationRule definition, OrderedResultSet<Boolean> activations, Consumer<Tuple> action) {
+                this.definition = definition;
+                this.activations = activations;
+                this.action = action;
+        }
+
+        public TransformationRule getDefinition() {
+                return definition;
+        }
+
+        public ResultSet<Boolean> getAllActivationsAsResultSet() {
+                return activations;
+        }
+
+        public Tuple getActivation(int index) {
+                return activations.getKey(index);
+        }
+
+        public boolean fireActivation(Tuple activation) {
+                action.accept(activation);
+                //queryEngine.flushChanges();
+                return true;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/TransformationRule.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/TransformationRule.java
new file mode 100644
index 00000000..d64a3db1
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/TransformationRule.java
@@ -0,0 +1,63 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.dse.ActionFactory;
+import tools.refinery.store.query.resultset.OrderedResultSet;
+import tools.refinery.store.query.resultset.ResultSet;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.*;
+
+public class TransformationRule {
+
+        private final String name;
+        private final RelationalQuery precondition;
+        private final ActionFactory actionFactory;
+
+        private Random random;
+        private ModelQueryAdapter queryEngine;
+
+        public TransformationRule(String name, RelationalQuery precondition, ActionFactory actionFactory) {
+                this(name, precondition, actionFactory, new Random());
+        }
+
+        public TransformationRule(String name, RelationalQuery precondition, ActionFactory actionFactory, long seed) {
+                this(name, precondition, actionFactory, new Random(seed));
+        }
+
+        public TransformationRule(String name, RelationalQuery precondition, ActionFactory actionFactory, Random random) {
+                this.name = name;
+                this.precondition = precondition;
+                this.actionFactory = actionFactory;
+                this.random = random;
+        }
+        public void doConfigure(ModelStoreBuilder storeBuilder) {
+                var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
+                queryBuilder.query(this.precondition);
+        }
+
+        public Transformation prepare(Model model) {
+                var queryEngine = model.getAdapter(ModelQueryAdapter.class);
+                var activations = new OrderedResultSet<>(queryEngine.getResultSet(precondition));
+                var action = actionFactory.prepare(model);
+                return new Transformation(this,activations,action);
+        }
+
+        public String getName() {
+                return name;
+        }
+
+        public RelationalQuery getPrecondition() {
+                return precondition;
+        }
+
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/VersionWithObjectiveValue.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/VersionWithObjectiveValue.java
new file mode 100644
index 00000000..ca28e27f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/VersionWithObjectiveValue.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition;
+
+import tools.refinery.store.map.Version;
+
+public record VersionWithObjectiveValue(Version version, ObjectiveValue objectiveValue) {
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationAdapterImpl.java
new file mode 100644
index 00000000..e1a29d40
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationAdapterImpl.java
@@ -0,0 +1,90 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.internal;
+
+import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
+import tools.refinery.store.dse.transition.DesignSpaceExplorationStoreAdapter;
+import tools.refinery.store.dse.transition.ObjectiveValue;
+import tools.refinery.store.dse.transition.Transformation;
+import tools.refinery.store.dse.transition.objectives.CriterionCalculator;
+import tools.refinery.store.dse.transition.objectives.ObjectiveCalculator;
+import tools.refinery.store.model.Model;
+
+import java.util.List;
+
+public class DesignSpaceExplorationAdapterImpl implements DesignSpaceExplorationAdapter {
+        final Model model;
+        final DesignSpaceExplorationStoreAdapter designSpaceExplorationStoreAdapter;
+
+        final List<Transformation> transformations;
+        final List<CriterionCalculator> accepts;
+        final List<CriterionCalculator> excludes;
+        final List<ObjectiveCalculator> objectives;
+
+        public DesignSpaceExplorationAdapterImpl(Model model,
+                                                                                         DesignSpaceExplorationStoreAdapter designSpaceExplorationStoreAdapter,
+                                                                                         List<Transformation> transformations,
+                                                                                         List<CriterionCalculator> accepts,
+                                                                                         List<CriterionCalculator> excludes,
+                                                                                         List<ObjectiveCalculator> objectives) {
+                this.model = model;
+                this.designSpaceExplorationStoreAdapter = designSpaceExplorationStoreAdapter;
+
+                this.transformations = transformations;
+                this.accepts = accepts;
+                this.excludes = excludes;
+                this.objectives = objectives;
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public DesignSpaceExplorationStoreAdapter getStoreAdapter() {
+                return designSpaceExplorationStoreAdapter;
+        }
+
+        public List<Transformation> getTransformations() {
+                return transformations;
+        }
+
+        @Override
+        public boolean checkAccept() {
+                for (var accept : this.accepts) {
+                        if (!accept.isSatisfied()) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public boolean checkExclude() {
+                for (var exclude : this.excludes) {
+                        if (exclude.isSatisfied()) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        @Override
+        public ObjectiveValue getObjectiveValue() {
+                if (objectives.size() == 1) {
+                        return ObjectiveValue.of(objectives.get(0).getValue());
+                } else if (objectives.size() == 2) {
+                        return ObjectiveValue.of(objectives.get(0).getValue(), objectives.get(1).getValue());
+                } else {
+                        double[] res = new double[objectives.size()];
+                        for (int i = 0; i < objectives.size(); i++) {
+                                res[i] = objectives.get(i).getValue();
+                        }
+                        return ObjectiveValue.of(res);
+                }
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationBuilderImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationBuilderImpl.java
new file mode 100644
index 00000000..4371cc03
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationBuilderImpl.java
@@ -0,0 +1,75 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.internal;
+
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
+import tools.refinery.store.dse.transition.TransformationRule;
+import tools.refinery.store.dse.transition.objectives.Criterion;
+import tools.refinery.store.dse.transition.objectives.Objective;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+import java.util.ArrayList;
+import java.util.LinkedHashSet;
+import java.util.List;
+
+public class DesignSpaceExplorationBuilderImpl
+                extends AbstractModelAdapterBuilder<DesignSpaceExplorationStoreAdapterImpl>
+                implements DesignSpaceExplorationBuilder {
+
+        LinkedHashSet<TransformationRule> transformationRuleDefinitions = new LinkedHashSet<>();
+        LinkedHashSet<Criterion> accepts = new LinkedHashSet<>();
+        LinkedHashSet<Criterion> excludes = new LinkedHashSet<>();
+        LinkedHashSet<Objective> objectives = new LinkedHashSet<>();
+
+        @Override
+        public DesignSpaceExplorationBuilder transformation(TransformationRule transformationRuleDefinition) {
+                transformationRuleDefinitions.add(transformationRuleDefinition);
+                return this;
+        }
+
+        @Override
+        public DesignSpaceExplorationBuilder accept(Criterion criteria) {
+                accepts.add(criteria);
+                return this;
+        }
+
+        @Override
+        public DesignSpaceExplorationBuilder exclude(Criterion criteria) {
+                excludes.add(criteria);
+                return this;
+        }
+
+
+        @Override
+        public DesignSpaceExplorationBuilder objective(Objective objective) {
+                objectives.add(objective);
+                return this;
+        }
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                transformationRuleDefinitions.forEach(x -> x.doConfigure(storeBuilder));
+                accepts.forEach(x -> x.doConfigure(storeBuilder));
+                excludes.forEach(x -> x.doConfigure(storeBuilder));
+                objectives.forEach(x -> x.doConfigure(storeBuilder));
+
+                super.doConfigure(storeBuilder);
+        }
+
+        @Override
+        protected DesignSpaceExplorationStoreAdapterImpl doBuild(ModelStore store) {
+                List<TransformationRule> transformationRuleDefinitiions1 = new ArrayList<>(transformationRuleDefinitions);
+                List<Criterion> accepts1 = new ArrayList<>(accepts);
+                List<Criterion> excludes1 = new ArrayList<>(excludes);
+                List<Objective> objectives1 = new ArrayList<>(objectives);
+
+                return new DesignSpaceExplorationStoreAdapterImpl(store,
+                                transformationRuleDefinitiions1, accepts1,
+                                excludes1, objectives1);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationStoreAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationStoreAdapterImpl.java
new file mode 100644
index 00000000..3319e148
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/internal/DesignSpaceExplorationStoreAdapterImpl.java
@@ -0,0 +1,70 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.internal;
+
+import tools.refinery.store.dse.transition.DesignSpaceExplorationStoreAdapter;
+import tools.refinery.store.dse.transition.Transformation;
+import tools.refinery.store.dse.transition.TransformationRule;
+import tools.refinery.store.dse.transition.objectives.Criterion;
+import tools.refinery.store.dse.transition.objectives.CriterionCalculator;
+import tools.refinery.store.dse.transition.objectives.Objective;
+import tools.refinery.store.dse.transition.objectives.ObjectiveCalculator;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+
+import java.util.List;
+
+public class DesignSpaceExplorationStoreAdapterImpl implements DesignSpaceExplorationStoreAdapter {
+        protected final ModelStore store;
+
+        protected final List<TransformationRule> transformationRuleDefinitions;
+        protected final List<Criterion> accepts;
+        protected final List<Criterion> excludes;
+        protected final List<Objective> objectives;
+
+        public DesignSpaceExplorationStoreAdapterImpl(ModelStore store,
+                                                                                                  List<TransformationRule> transformationRuleDefinitions,
+                                                                                                  List<Criterion> accepts, List<Criterion> excludes,
+                                                                                                  List<Objective> objectives) {
+                this.store = store;
+
+                this.transformationRuleDefinitions = transformationRuleDefinitions;
+                this.accepts = accepts;
+                this.excludes = excludes;
+                this.objectives = objectives;
+        }
+
+        @Override
+        public ModelStore getStore() {
+                return store;
+        }
+
+        @Override
+        public DesignSpaceExplorationAdapterImpl createModelAdapter(Model model) {
+                final List<Transformation> t = this.transformationRuleDefinitions.stream().map(x->x.prepare(model)).toList();
+                final List<CriterionCalculator> a = this.accepts.stream().map(x->x.createCalculator(model)).toList();
+                final List<CriterionCalculator> e = this.excludes.stream().map(x->x.createCalculator(model)).toList();
+                final List<ObjectiveCalculator> o = this.objectives.stream().map(x->x.createCalculator(model)).toList();
+
+                return new DesignSpaceExplorationAdapterImpl(model, this, t, a, e, o);
+        }
+        @Override
+        public List<TransformationRule> getTransformations() {
+                return transformationRuleDefinitions;
+        }
+        @Override
+        public List<Criterion> getAccepts() {
+                return accepts;
+        }
+        @Override
+        public List<Criterion> getExcludes() {
+                return excludes;
+        }
+        @Override
+        public List<Objective> getObjectives() {
+                return objectives;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java
new file mode 100644
index 00000000..66ca6f5e
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Criterion.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+public interface Criterion {
+        default void doConfigure(ModelStoreBuilder storeBuilder) {
+        }
+        CriterionCalculator createCalculator(Model model);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CriterionCalculator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CriterionCalculator.java
new file mode 100644
index 00000000..944ffed6
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/CriterionCalculator.java
@@ -0,0 +1,10 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+public interface CriterionCalculator {
+        boolean isSatisfied();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java
new file mode 100644
index 00000000..b5924455
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/Objective.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+public interface Objective {
+        default void doConfigure(ModelStoreBuilder storeBuilder) {
+        }
+        ObjectiveCalculator createCalculator(Model model);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/ObjectiveCalculator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/ObjectiveCalculator.java
new file mode 100644
index 00000000..f01b8de9
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/ObjectiveCalculator.java
@@ -0,0 +1,10 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+public interface ObjectiveCalculator {
+        double getValue();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriteria.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriteria.java
new file mode 100644
index 00000000..e2260cca
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryCriteria.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.AnyQuery;
+
+public class QueryCriteria implements Criterion {
+        protected final boolean acceptIfHasMatch;
+        protected final AnyQuery query;
+
+        /**
+         * Criteria based on the existence of matches evaluated on the model.
+         * @param query The query evaluated on the model.
+         * @param acceptIfHasMatch If true, the criteria satisfied if the query has any match on the model. Otherwise,
+         *                            the criteria satisfied if the query has no match on the model.
+         */
+        public QueryCriteria(AnyQuery query, boolean acceptIfHasMatch) {
+                this.query = query;
+                this.acceptIfHasMatch = acceptIfHasMatch;
+        }
+
+        @Override
+        public CriterionCalculator createCalculator(Model model) {
+                var resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(query);
+                if(acceptIfHasMatch) {
+                        return () -> resultSet.size() > 0;
+                } else {
+                        return () -> resultSet.size() == 0;
+                }
+        }
+
+        @Override
+        public void doConfigure(ModelStoreBuilder storeBuilder) {
+                Criterion.super.doConfigure(storeBuilder);
+                storeBuilder.getAdapter(ModelQueryBuilder.class).query(query);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java
new file mode 100644
index 00000000..dfddccfc
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.objectives;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.dnf.FunctionalQuery;
+
+public class QueryObjective implements Objective {
+        protected final FunctionalQuery<? extends Number> objectiveFunction;
+
+        public QueryObjective(FunctionalQuery<? extends Number> objectiveFunction) {
+                this.objectiveFunction = objectiveFunction;
+        }
+
+        @Override
+        public ObjectiveCalculator createCalculator(Model model) {
+                var resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(objectiveFunction);
+                return () -> {
+                        var cursor = resultSet.getAll();
+                        boolean hasElement = cursor.move();
+                        if(hasElement) {
+                                double result = cursor.getValue().doubleValue();
+                                if(cursor.move()) {
+                                        throw new IllegalStateException("Query providing the objective function has multiple values!");
+                                }
+                                return result;
+                        } else {
+                                throw new IllegalStateException("Query providing the objective function has no values!");
+                        }
+                };
+        }
+
+        @Override
+        public void doConfigure(ModelStoreBuilder storeBuilder) {
+                Objective.super.doConfigure(storeBuilder);
+                storeBuilder.getAdapter(ModelQueryBuilder.class).query(objectiveFunction);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ActivationStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ActivationStore.java
new file mode 100644
index 00000000..52e0611d
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ActivationStore.java
@@ -0,0 +1,18 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.map.Version;
+
+import java.util.Random;
+
+public interface ActivationStore {
+        record VisitResult(boolean successfulVisit, boolean mayHaveMore, int transformation, int activation) { }
+        VisitResult markNewAsVisited(VersionWithObjectiveValue to, int[] emptyEntrySizes);
+        boolean hasUnmarkedActivation(VersionWithObjectiveValue version);
+        VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random);
+}
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
new file mode 100644
index 00000000..bbe26fe5
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/EquivalenceClassStore.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.statecoding.StateCoderResult;
+
+public interface EquivalenceClassStore {
+        boolean submit(VersionWithObjectiveValue version, StateCoderResult stateCoderResult, int[] emptyActivations, boolean accept);
+        boolean hasUnresolvedSymmetry();
+        void resolveOneSymmetry();
+        int getNumberOfUnresolvedSymmetries();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ObjectivePriorityQueue.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ObjectivePriorityQueue.java
new file mode 100644
index 00000000..df72c343
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/ObjectivePriorityQueue.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.map.Version;
+
+import java.util.Comparator;
+import java.util.Random;
+
+public interface ObjectivePriorityQueue {
+        Comparator<VersionWithObjectiveValue> getComparator();
+        void submit(VersionWithObjectiveValue versionWithObjectiveValue);
+        void remove(VersionWithObjectiveValue versionWithObjectiveValue);
+        int getSize();
+        VersionWithObjectiveValue getBest();
+        VersionWithObjectiveValue getRandom(Random random);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/SolutionStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/SolutionStore.java
new file mode 100644
index 00000000..d1bfaa79
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/SolutionStore.java
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+
+import java.util.List;
+import java.util.concurrent.Future;
+
+public interface SolutionStore {
+        boolean submit(VersionWithObjectiveValue version);
+        List<VersionWithObjectiveValue> getSolutions();
+        boolean hasEnoughSolution();
+}
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
new file mode 100644
index 00000000..8466a0f3
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/AbstractEquivalenceClassStore.java
@@ -0,0 +1,47 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.EquivalenceClassStore;
+import tools.refinery.store.statecoding.StateCoderResult;
+import tools.refinery.store.statecoding.StateCoderStoreAdapter;
+
+public abstract class AbstractEquivalenceClassStore implements EquivalenceClassStore {
+        protected final StateCoderStoreAdapter stateCoderStoreAdapter;
+        AbstractEquivalenceClassStore(StateCoderStoreAdapter stateCoderStoreAdapter) {
+                this.stateCoderStoreAdapter = stateCoderStoreAdapter;
+        }
+
+        protected int numberOfUnresolvedSymmetries = 0;
+
+        protected abstract void delegate(VersionWithObjectiveValue version, int[] emptyActivations, boolean accept);
+        protected abstract boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion,
+                                                           int[] emptyActivations, boolean accept);
+
+        @Override
+        public synchronized boolean submit(VersionWithObjectiveValue version, StateCoderResult stateCoderResult,
+                                                                           int[] emptyActivations, boolean accept) {
+                boolean hasNewVersion = tryToAdd(stateCoderResult, version, emptyActivations, accept);
+                if (hasNewVersion) {
+                        delegate(version, emptyActivations, accept);
+                        return true;
+                } else {
+                        numberOfUnresolvedSymmetries++;
+                        return false;
+                }
+        }
+
+        @Override
+        public boolean hasUnresolvedSymmetry() {
+                return numberOfUnresolvedSymmetries > 0;
+        }
+
+        @Override
+        public int getNumberOfUnresolvedSymmetries() {
+                return numberOfUnresolvedSymmetries;
+        }
+}
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
new file mode 100644
index 00000000..ba243d7d
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreBitVectorEntry.java
@@ -0,0 +1,46 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+public class ActivationStoreBitVectorEntry extends ActivationStoreEntry {
+        final int[] selected;
+
+        ActivationStoreBitVectorEntry(int numberOfActivations) {
+                super(numberOfActivations);
+                this.selected = new int[(numberOfActivations / Integer.SIZE) + 1];
+        }
+
+        @Override
+        public int getNumberOfUnvisitedActivations() {
+                int visited = 0;
+                for (int i : selected) {
+                        visited += Integer.bitCount(i);
+                }
+                return visited;
+        }
+
+        private static final int ELEMENT_POSITION = 5; // size of Integer.SIZE
+        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 = position & ELEMENT_BITMASK;
+                        if((selected[selectedElement] & selectedBit) == 0) {
+                                selected[selectedElement] |= selectedBit;
+                                return position;
+                        } else {
+                                if(position < this.numberOfActivations) {
+                                        position++;
+                                } else {
+                                        position = 0;
+                                }
+                        }
+                } 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
new file mode 100644
index 00000000..f69b234c
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreEntry.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+public abstract class ActivationStoreEntry {
+        protected final int numberOfActivations;
+
+        ActivationStoreEntry(int numberOfActivations) {
+                this.numberOfActivations = numberOfActivations;
+        }
+
+        public int getNumberOfVisitedActivations() {
+                return numberOfActivations;
+        }
+
+        public abstract int getNumberOfUnvisitedActivations();
+        public abstract int getAndAddActivationAfter(int index);
+
+        //      public abstract boolean contains(int activation)
+        //      public abstract boolean add(int activation)
+
+        public static ActivationStoreEntry create(int size) {
+                if(size <= Integer.SIZE*6) {
+                        return new ActivationStoreBitVectorEntry(size);
+                } else {
+                        return new ActivationStoreListEntry(size);
+                }
+        }
+}
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
new file mode 100644
index 00000000..3e59b21a
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
@@ -0,0 +1,131 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.ActivationStore;
+
+import java.util.*;
+import java.util.function.Consumer;
+
+public class ActivationStoreImpl implements ActivationStore {
+        final int numberOfTransformations;
+        final Consumer<VersionWithObjectiveValue> actionWhenAllActivationVisited;
+        final Map<VersionWithObjectiveValue, List<ActivationStoreEntry>> versionToActivations;
+
+        public ActivationStoreImpl(final int numberOfTransformations,
+                                                           Consumer<VersionWithObjectiveValue> actionWhenAllActivationVisited) {
+                this.numberOfTransformations = numberOfTransformations;
+                this.actionWhenAllActivationVisited = actionWhenAllActivationVisited;
+                versionToActivations = new HashMap<>();
+        }
+
+        public synchronized VisitResult markNewAsVisited(VersionWithObjectiveValue to, int[] emptyEntrySizes) {
+                boolean[] successful = new boolean[]{false};
+                var entries = versionToActivations.computeIfAbsent(to, x -> {
+                        successful[0] = true;
+                        List<ActivationStoreEntry> result = new ArrayList<>(emptyEntrySizes.length);
+                        for(int emptyEntrySize : emptyEntrySizes) {
+                                result.add(ActivationStoreListEntry.create(emptyEntrySize));
+                        }
+                        return result;
+                });
+                boolean hasMore = false;
+                for (var entry : entries) {
+                        if (entry.getNumberOfUnvisitedActivations() > 0) {
+                                hasMore = true;
+                                break;
+                        }
+                }
+                if(!hasMore) {
+                        actionWhenAllActivationVisited.accept(to);
+                }
+                return new VisitResult(successful[0], hasMore, -1, -1);
+        }
+
+        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();
+
+                final boolean successfulVisit = unvisited > 0;
+                final boolean hasMoreInActivation = unvisited > 1;
+                final boolean hasMore;
+                final int transformation;
+                final int activation;
+
+                if (successfulVisit) {
+                        transformation = transformationIndex;
+                        activation = entry.getAndAddActivationAfter(activationIndex);
+
+                } else {
+                        transformation = -1;
+                        activation = -1;
+                }
+
+                if(hasMoreInActivation) {
+                        boolean hasMoreInOtherTransformation = false;
+                        for (var e : entries) {
+                                if (e != entry && e.getNumberOfVisitedActivations() > 0) {
+                                        hasMoreInOtherTransformation = true;
+                                        break;
+                                }
+                        }
+                        hasMore = hasMoreInOtherTransformation;
+                } else {
+                        hasMore = true;
+                }
+
+                if(!hasMore) {
+                        actionWhenAllActivationVisited.accept(from);
+                }
+
+                return new VisitResult(false, hasMore, transformation, activation);
+        }
+
+        @Override
+        public synchronized boolean hasUnmarkedActivation(VersionWithObjectiveValue version) {
+                var entries = versionToActivations.get(version);
+                boolean hasMore = false;
+                for (var entry : entries) {
+                        if (entry.getNumberOfUnvisitedActivations() > 0) {
+                                hasMore = true;
+                                break;
+                        }
+                }
+                return hasMore;
+        }
+
+        @Override
+        public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) {
+                var entries = versionToActivations.get(version);
+
+                int sum1 = 0;
+                for (var entry : entries) {
+                        sum1 += entry.getNumberOfUnvisitedActivations();
+                }
+
+                int selected = random.nextInt(sum1);
+                int sum2 = 0;
+                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;
+                                break;
+                        } else {
+                                sum2 += unvisited;
+                        }
+                }
+                if (activation == -1) {
+                        throw new IllegalArgumentException("no unvisited");
+                }
+
+                return this.visitActivation(version, transformation, 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
new file mode 100644
index 00000000..e560f8c5
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreListEntry.java
@@ -0,0 +1,95 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import org.eclipse.collections.api.factory.primitive.IntLists;
+import org.eclipse.collections.api.list.primitive.MutableIntList;
+
+public class ActivationStoreListEntry extends ActivationStoreEntry {
+        private final MutableIntList visitedActivations = IntLists.mutable.empty();
+
+        ActivationStoreListEntry(int numberOfActivations) {
+                super(numberOfActivations);
+        }
+
+        @Override
+        public int getNumberOfUnvisitedActivations() {
+                return this.numberOfActivations - visitedActivations.size();
+        }
+
+        @Override
+        public int getAndAddActivationAfter(int index) {
+                // If it is empty, just add it.
+                if(this.visitedActivations.isEmpty()) {
+                        this.visitedActivations.add(index);
+                        return index;
+                }
+
+                int position = getPosition(index);
+
+                // 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++;
+                        if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) {
+                                this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1);
+                        }
+                }
+
+                // Otherwise, try to add to the last space
+                int last = this.visitedActivations.get(this.visitedActivations.size()-1);
+                if(last<this.numberOfActivations) {
+                        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);
+                        return 0;
+                }
+
+                // Otherwise, get the next empty space between two elements
+                position = 0;
+                while(position + 2 < this.visitedActivations.size()) {
+                        position++;
+                        if(this.visitedActivations.get(position+1)-this.visitedActivations.get(position) > 1) {
+                                this.visitedActivations.addAtIndex(position+1, this.visitedActivations.get(position+1)+1);
+                        }
+                }
+
+                throw new IllegalArgumentException("There is are no unvisited activations!");
+        }
+
+        /**
+         * Returns the position of an index in the {@code visitedActivations}. If the collection contains the index, in
+         * returns its position, otherwise, it  returns the position where the index need to be put.
+         *
+         * @param index Index of an activation.
+         * @return The position of the index.
+         */
+        private int getPosition(int index) {
+                int left = 0;
+                int right = this.visitedActivations.size() - 1;
+                while (left <= right) {
+                        final int middle = (right - left) / 2 + left;
+                        final int middleElement = visitedActivations.get(middle);
+                        if(middleElement == index) {
+                                return middle;
+                        } else if(middleElement < index) {
+                                left = middle +1;
+                        } else{
+                                right = middle-1;
+                        }
+                }
+                return right+1;
+        }
+}
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
new file mode 100644
index 00000000..e05f5122
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
@@ -0,0 +1,56 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+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;
+
+public class ActivationStoreWorker {
+        final ActivationStore store;
+        final List<Transformation> transformations;
+
+        public ActivationStoreWorker(ActivationStore store, List<Transformation> transformations) {
+                this.store = store;
+                this.transformations = transformations;
+        }
+
+        public int[] calculateEmptyActivationSize() {
+                int[] result = new int[transformations.size()];
+                for (int i = 0; i < result.length; i++) {
+                        result[i] = transformations.get(i).getAllActivationsAsResultSet().size();
+                }
+                return result;
+        }
+
+
+        public ActivationStore.VisitResult fireRandomActivation(VersionWithObjectiveValue thisVersion, Random random) {
+                var result = store.getRandomAndMarkAsVisited(thisVersion, random);
+                if(result.successfulVisit()) {
+                        int selectedTransformation = result.transformation();
+                        int selectedActivation = result.activation();
+
+                        Transformation transformation = transformations.get(selectedTransformation);
+                        var tuple = transformation.getActivation(selectedActivation);
+
+                        boolean success = transformation.fireActivation(tuple);
+                        if(success) {
+                                return result;
+                        } else {
+                                return new ActivationStore.VisitResult(
+                                                false,
+                                                result.mayHaveMore(),
+                                                selectedActivation,
+                                                selectedActivation);
+                        }
+                }
+                return result;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/CompleteEquivalenceClassStore.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/CompleteEquivalenceClassStore.java
new file mode 100644
index 00000000..20a026b6
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/CompleteEquivalenceClassStore.java
@@ -0,0 +1,104 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.EquivalenceClassStore;
+import tools.refinery.store.statecoding.StateCoderResult;
+import tools.refinery.store.statecoding.StateCoderStoreAdapter;
+import tools.refinery.store.statecoding.StateEquivalenceChecker;
+
+import java.util.ArrayList;
+
+public abstract class CompleteEquivalenceClassStore extends AbstractEquivalenceClassStore implements EquivalenceClassStore {
+
+        static class SymmetryStoreArray extends ArrayList<VersionWithObjectiveValue> {
+                final int[] activationSizes;
+                final boolean accept;
+
+                SymmetryStoreArray(int[] activationSizes, boolean accept) {
+                        super();
+                        this.activationSizes = activationSizes;
+                        this.accept = accept;
+                }
+        }
+
+        private final MutableIntObjectMap<Object> modelCode2Versions = IntObjectMaps.mutable.empty();
+
+        protected CompleteEquivalenceClassStore(StateCoderStoreAdapter stateCoderStoreAdapter) {
+                super(stateCoderStoreAdapter);
+        }
+
+        @Override
+        protected boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion,
+                                           int[] emptyActivations, boolean accept) {
+                int modelCode = stateCoderResult.modelCode();
+                Object old = modelCode2Versions.updateValue(
+                                modelCode,
+                                () -> newVersion,
+                                x -> {
+                                        if (x instanceof SymmetryStoreArray array) {
+                                                if(array.accept != accept || array.activationSizes != emptyActivations) {
+                                                        this.delegate(newVersion,emptyActivations,accept);
+                                                        return x;
+                                                }
+                                                array.add(newVersion);
+                                                return array;
+                                        } else {
+                                                SymmetryStoreArray result = new SymmetryStoreArray(emptyActivations, accept);
+                                                result.add((VersionWithObjectiveValue) x);
+                                                result.add(newVersion);
+                                                return result;
+                                        }
+                                });
+                return old == null;
+        }
+
+        @Override
+        public void resolveOneSymmetry() {
+                var unresolvedSimilarity = getOneUnresolvedSymmetry();
+                if (unresolvedSimilarity == null) {
+                        return;
+                }
+                var outcome = this.stateCoderStoreAdapter.checkEquivalence(unresolvedSimilarity.get(0).version(),
+                                unresolvedSimilarity.get(1).version());
+                if (outcome != StateEquivalenceChecker.EquivalenceResult.ISOMORPHIC) {
+                        delegate(unresolvedSimilarity.get(1), unresolvedSimilarity.activationSizes, unresolvedSimilarity.accept);
+                }
+        }
+
+        //record  UnresolvedSymmetryResult
+
+        private synchronized SymmetryStoreArray getOneUnresolvedSymmetry() {
+                if (numberOfUnresolvedSymmetries <= 0) {
+                        return null;
+                }
+
+                for (var entry : modelCode2Versions.keyValuesView()) {
+                        int hash = entry.getOne();
+                        var value = entry.getTwo();
+                        if (value instanceof SymmetryStoreArray array) {
+                                int size = array.size();
+                                var representative = array.get(0);
+                                var similar = array.get(size - 1);
+                                array.remove(size - 1);
+
+                                if (size <= 2) {
+                                        modelCode2Versions.put(hash, representative);
+                                }
+
+                                var result = new SymmetryStoreArray(array.activationSizes, array.accept);
+                                result.add(representative);
+                                result.add(similar);
+                                return result;
+                        }
+                }
+
+                return null;
+        }
+}
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
new file mode 100644
index 00000000..6ee8e196
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/FastEquivalenceClassStore.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import org.eclipse.collections.api.factory.primitive.IntSets;
+import org.eclipse.collections.api.set.primitive.MutableIntSet;
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.EquivalenceClassStore;
+import tools.refinery.store.statecoding.StateCoderResult;
+import tools.refinery.store.statecoding.StateCoderStoreAdapter;
+
+public abstract class FastEquivalenceClassStore extends AbstractEquivalenceClassStore implements EquivalenceClassStore {
+
+        private final MutableIntSet codes = IntSets.mutable.empty();
+
+        public FastEquivalenceClassStore(StateCoderStoreAdapter stateCoderStoreAdapter) {
+                super(stateCoderStoreAdapter);
+        }
+
+        @Override
+        protected boolean tryToAdd(StateCoderResult stateCoderResult, VersionWithObjectiveValue newVersion, int[] emptyActivations, boolean accept) {
+                return this.codes.add(stateCoderResult.modelCode());
+        }
+
+        @Override
+        public void resolveOneSymmetry() {
+                throw new IllegalArgumentException("This equivalence storage is not prepared to resolve symmetries!");
+        }
+}
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
new file mode 100644
index 00000000..249b22da
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ObjectivePriorityQueueImpl.java
@@ -0,0 +1,74 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+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;
+import java.util.PriorityQueue;
+import java.util.Random;
+
+public class ObjectivePriorityQueueImpl implements ObjectivePriorityQueue {
+        public static final Comparator<VersionWithObjectiveValue> c1 = (o1, o2) -> Double.compare(
+                        ((ObjectiveValues.ObjectiveValue1) o1.objectiveValue()).value0(),
+                        ((ObjectiveValues.ObjectiveValue1) o2.objectiveValue()).value0());
+        // TODO: support multi objective!
+        final PriorityQueue<VersionWithObjectiveValue> priorityQueue;
+
+        public ObjectivePriorityQueueImpl(List<Objective> objectives) {
+
+                if(objectives.size() == 1) {
+                        this.priorityQueue = new PriorityQueue<>(c1);
+                } else {
+                        throw new UnsupportedOperationException("Only single objective comparator is implemented currently!");
+                }
+        }
+        @Override
+        public Comparator<VersionWithObjectiveValue> getComparator() {
+                return c1;
+        }
+
+        @Override
+        public void submit(VersionWithObjectiveValue versionWithObjectiveValue) {
+                priorityQueue.add(versionWithObjectiveValue);
+        }
+
+        @Override
+        public void remove(VersionWithObjectiveValue versionWithObjectiveValue) {
+                priorityQueue.remove(versionWithObjectiveValue);
+        }
+
+        @Override
+        public 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!");
+                }
+        }
+
+        @Override
+        public VersionWithObjectiveValue getRandom(Random random) {
+                int randomPosition = random.nextInt(getSize());
+                for (VersionWithObjectiveValue entry : this.priorityQueue) {
+                        if (randomPosition-- == 0) {
+                                return entry;
+                        }
+                }
+                throw new IllegalStateException("The priority queue is inconsistent!");
+        }
+}
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
new file mode 100644
index 00000000..cc48864f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/SolutionStoreImpl.java
@@ -0,0 +1,53 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.transition.statespace.internal;
+
+import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
+import tools.refinery.store.dse.transition.statespace.SolutionStore;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.SortedSet;
+import java.util.TreeSet;
+
+public class SolutionStoreImpl implements SolutionStore {
+        final int maxNumberSolutions;
+        public static final int UNLIMITED = -1;
+        final SortedSet<VersionWithObjectiveValue> solutions;
+
+        public SolutionStoreImpl(int maxNumberSolutions) {
+                this.maxNumberSolutions = maxNumberSolutions;
+                solutions = new TreeSet<>(ObjectivePriorityQueueImpl.c1);
+        }
+
+
+        @Override
+        public synchronized boolean submit(VersionWithObjectiveValue version) {
+                boolean removeLast = hasEnoughSolution();
+                solutions.add(version);
+                if(removeLast) {
+                        var last = solutions.last();
+                        solutions.remove(last);
+                        return last != version;
+                } else {
+                        return true;
+                }
+        }
+
+        @Override
+        public List<VersionWithObjectiveValue> getSolutions() {
+                return new ArrayList<>(solutions);
+        }
+
+        @Override
+        public boolean hasEnoughSolution() {
+                if (maxNumberSolutions == UNLIMITED) {
+                        return false;
+                } else {
+                        return solutions.size() >= maxNumberSolutions;
+                }
+        }
+}