feat: integrate DSE with partial interpretation

46 files changed, 1138 insertions, 295 deletions

diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts
index 4374f78c..338ae345 100644
--- a/subprojects/language-semantics/build.gradle.kts
+++ b/subprojects/language-semantics/build.gradle.kts
@@ -16,4 +16,7 @@ dependencies {
         api(project(":refinery-store-reasoning"))
         implementation(project(":refinery-store-reasoning-scope"))
         runtimeOnly(libs.eclipseCollections)
+        testImplementation(project(":refinery-store-dse-visualization"))
+        testImplementation(project(":refinery-store-query-viatra"))
+        testImplementation(testFixtures(project(":refinery-language")))
 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
index 89c41a8e..a14b40d0 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java
@@ -13,6 +13,7 @@ import tools.refinery.language.semantics.model.internal.MutableSeed;
 import tools.refinery.language.utils.BuiltinSymbols;
 import tools.refinery.language.utils.ProblemDesugarer;
 import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.dnf.InvalidClauseException;
@@ -24,7 +25,7 @@ import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
+import tools.refinery.store.reasoning.scope.ScopePropagator;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
@@ -73,7 +74,9 @@ public class ModelInitializer {
 
         private Metamodel metamodel;
 
-        private Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
+        private final Map<Tuple, CardinalityInterval> countSeed = new LinkedHashMap<>();
+
+        private ScopePropagator scopePropagator;
 
         private ModelSeed modelSeed;
 
@@ -139,6 +142,12 @@ public class ModelInitializer {
                         modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
                 }
                 collectScopes();
+                if (scopePropagator != null) {
+                        if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) {
+                                throw new TracedException(problem, "Type scopes require a PropagationBuilder");
+                        }
+                        storeBuilder.with(scopePropagator);
+                }
                 modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
                                 .reducedValue(CardinalityIntervals.SET)
                                 .putAll(countSeed));
@@ -534,8 +543,7 @@ public class ModelInitializer {
                 }
         }
 
-        private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable,
-                        Variable> localScope,
+        private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope,
                                                         List<Literal> literals) {
                 if (expr instanceof LogicConstant logicConstant) {
                         switch (logicConstant.getLogicValue()) {
@@ -645,14 +653,15 @@ public class ModelInitializer {
         }
 
         private void collectTypeScope(TypeScope typeScope) {
-                var scopePropagatorBuilder = storeBuilder.tryGetAdapter(ScopePropagatorBuilder.class).orElseThrow(
-                                () -> new TracedException(typeScope, "Type scopes require a ScopePropagatorBuilder"));
                 var type = relationTrace.get(typeScope.getTargetType());
                 if (type == null) {
                         throw new TracedException(typeScope, "Unknown target type");
                 }
                 var interval = getCardinalityInterval(typeScope.getMultiplicity());
-                scopePropagatorBuilder.scope(type, interval);
+                if (scopePropagator == null) {
+                        scopePropagator = new ScopePropagator();
+                }
+                scopePropagator.scope(type, interval);
         }
 
         private record RelationInfo(PartialRelation partialRelation, MutableSeed<TruthValue> assertions,
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java
new file mode 100644
index 00000000..a383d043
--- /dev/null
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java
@@ -0,0 +1,82 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.scope.ScopePropagator;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.tuple.Tuple;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class CountPropagationTest {
+        @Test
+        void countPropagationTest() {
+                var a1 = new PartialRelation("A1", 1);
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+
+                var typeHierarchy = TypeHierarchy.builder()
+                                .type(a1, true)
+                                .type(c1, a1)
+                                .type(c2, a1)
+                                .build();
+
+                var store = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(PropagationAdapter.builder())
+                                .with(DesignSpaceExplorationAdapter.builder())
+                                .with(ReasoningAdapter.builder())
+                                .with(new MultiObjectTranslator())
+                                .with(new TypeHierarchyTranslator(typeHierarchy))
+                                .with(new ScopePropagator()
+                                                .scope(a1, CardinalityIntervals.between(1000, 1100))
+                                                .scope(c1, CardinalityIntervals.between(100, 150)))
+                                .build();
+
+                var modelSeed = ModelSeed.builder(4)
+                                .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
+                                                .reducedValue(CardinalityIntervals.ONE)
+                                                .put(Tuple.of(0), CardinalityIntervals.SET)
+                                                .put(Tuple.of(1), CardinalityIntervals.SET))
+                                .seed(a1, builder -> builder.reducedValue(TruthValue.UNKNOWN))
+                                .seed(c1, builder -> builder
+                                                .reducedValue(TruthValue.FALSE)
+                                                .put(Tuple.of(0), TruthValue.TRUE)
+                                                .put(Tuple.of(2), TruthValue.TRUE))
+                                .seed(c2, builder -> builder
+                                                .reducedValue(TruthValue.FALSE)
+                                                .put(Tuple.of(1), TruthValue.TRUE)
+                                                .put(Tuple.of(3), TruthValue.TRUE))
+                                .build();
+
+                var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                var propagationAdapter = model.getAdapter(PropagationAdapter.class);
+                model.commit();
+
+                reasoningAdapter.split(0);
+                assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED));
+                model.commit();
+
+                reasoningAdapter.split(0);
+                assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED));
+        }
+}
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java
new file mode 100644
index 00000000..779e18ab
--- /dev/null
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java
@@ -0,0 +1,272 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics.model;
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.Disabled;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+import tools.refinery.language.ProblemStandaloneSetup;
+import tools.refinery.language.model.tests.utils.ProblemParseHelper;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.strategy.BestFirstStoreManager;
+import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+import tools.refinery.store.statecoding.StateCoderAdapter;
+import tools.refinery.visualization.ModelVisualizerAdapter;
+import tools.refinery.visualization.internal.FileFormat;
+
+import java.util.LinkedHashMap;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.empty;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+@Disabled("For debugging purposes only")
+class ModelGenerationTest {
+        @Inject
+        private ProblemParseHelper parseHelper;
+
+        @Inject
+        private ModelInitializer modelInitializer;
+
+        @Test
+        void socialNetworkTest() {
+                var parsedProblem = parseHelper.parse("""
+                                % Metamodel
+                                class Person {
+                                    contains Post posts opposite author
+                                    Person friend opposite friend
+                                }
+
+                                class Post {
+                                    container Person[0..1] author opposite posts
+                                    Post replyTo
+                                }
+
+                                % Constraints
+                                error replyToNotFriend(Post x, Post y) <->
+                                    replyTo(x, y),
+                                    author(x, xAuthor),
+                                    author(y, yAuthor),
+                                    xAuthor != yAuthor,
+                                    !friend(xAuthor, yAuthor).
+
+                                error replyToCycle(Post x) <-> replyTo+(x, x).
+
+                                % Instance model
+                                !friend(a, b).
+                                author(p1, a).
+                                author(p2, b).
+
+                                !author(Post::new, a).
+
+                                % Scope
+                                scope Post = 5, Person = 5.
+                                """);
+                assertThat(parsedProblem.errors(), empty());
+                var problem = parsedProblem.problem();
+
+                var storeBuilder = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder())
+                                .with(ModelVisualizerAdapter.builder()
+                                                .withOutputPath("test_output")
+                                                .withFormat(FileFormat.DOT)
+                                                .withFormat(FileFormat.SVG)
+//                                              .saveStates()
+                                                .saveDesignSpace())
+                                .with(PropagationAdapter.builder())
+                                .with(StateCoderAdapter.builder())
+                                .with(DesignSpaceExplorationAdapter.builder())
+                                .with(ReasoningAdapter.builder());
+
+                var modelSeed = modelInitializer.createModel(problem, storeBuilder);
+
+                var store = storeBuilder.build();
+
+                var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+
+                var initialVersion = initialModel.commit();
+
+                var bestFirst = new BestFirstStoreManager(store, 1);
+                bestFirst.startExploration(initialVersion);
+                var resultStore = bestFirst.getSolutionStore();
+                System.out.println("states size: " + resultStore.getSolutions().size());
+//              initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore());
+        }
+
+        @Test
+        void statechartTest() {
+                var parsedProblem = parseHelper.parse("""
+                                // Metamodel
+                                abstract class CompositeElement {
+                                    contains Region[] regions
+                                }
+
+                                class Region {
+                                    contains Vertex[] vertices opposite region
+                                }
+
+                                abstract class Vertex {
+                                    container Region[0..1] region opposite vertices
+                                    Transition[] outgoingTransition opposite source
+                                    Transition[] incomingTransition opposite target
+                                }
+
+                                class Transition {
+                                    Vertex source opposite outgoingTransition
+                                    Vertex target opposite incomingTransition
+                                }
+
+                                abstract class Pseudostate extends Vertex {}
+
+                                abstract class RegularState extends Vertex {}
+
+                                class Entry extends Pseudostate {}
+
+                                class Exit extends Pseudostate {}
+
+                                class Choice extends Pseudostate {}
+
+                                class FinalState extends RegularState {}
+
+                                class State extends RegularState, CompositeElement {}
+
+                                class Statechart extends CompositeElement {}
+
+                                // Constraints
+
+                                /////////
+                                // Entry
+                                /////////
+
+                                pred entryInRegion(Region r, Entry e) <->
+                                        vertices(r, e).
+
+                                error noEntryInRegion(Region r) <->
+                                    !entryInRegion(r, _).
+
+                                error multipleEntryInRegion(Region r) <->
+                                    entryInRegion(r, e1),
+                                    entryInRegion(r, e2),
+                                    e1 != e2.
+
+                                error incomingToEntry(Transition t, Entry e) <->
+                                    target(t, e).
+
+                                error noOutgoingTransitionFromEntry(Entry e) <->
+                                    !source(_, e).
+
+                                error multipleTransitionFromEntry(Entry e, Transition t1, Transition t2) <->
+                                    outgoingTransition(e, t1),
+                                    outgoingTransition(e, t2),
+                                    t1 != t2.
+
+                                /////////
+                                // Exit
+                                /////////
+
+                                error outgoingFromExit(Transition t, Exit e) <->
+                                    source(t, e).
+
+                                /////////
+                                // Final
+                                /////////
+
+                                error outgoingFromFinal(Transition t, FinalState e) <->
+                                    source(t, e).
+
+                                /////////
+                                // State vs Region
+                                /////////
+
+                                pred stateInRegion(Region r, State s) <->
+                                    vertices(r, s).
+
+                                error noStateInRegion(Region r) <->
+                                    !stateInRegion(r, _).
+
+                                /////////
+                                // Choice
+                                /////////
+
+                                error choiceHasNoOutgoing(Choice c) <->
+                                    !source(_, c).
+
+                                error choiceHasNoIncoming(Choice c) <->
+                                    !target(_, c).
+
+                                scope node = 50..60, Statechart = 1.
+                                """);
+                assertThat(parsedProblem.errors(), empty());
+                var problem = parsedProblem.problem();
+
+                var storeBuilder = ModelStore.builder()
+                                .with(ViatraModelQueryAdapter.builder())
+//                              .with(ModelVisualizerAdapter.builder()
+//                                              .withOutputPath("test_output")
+//                                              .withFormat(FileFormat.DOT)
+//                                              .withFormat(FileFormat.SVG)
+//                                              .saveStates()
+//                                              .saveDesignSpace())
+                                .with(PropagationAdapter.builder())
+                                .with(StateCoderAdapter.builder())
+                                .with(DesignSpaceExplorationAdapter.builder())
+                                .with(ReasoningAdapter.builder());
+
+                var modelSeed = modelInitializer.createModel(problem, storeBuilder);
+
+                var store = storeBuilder.build();
+
+                var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+
+                var initialVersion = initialModel.commit();
+
+                var bestFirst = new BestFirstStoreManager(store, 1);
+                bestFirst.startExploration(initialVersion);
+                var resultStore = bestFirst.getSolutionStore();
+                System.out.println("states size: " + resultStore.getSolutions().size());
+
+                var model = store.createModelForState(resultStore.getSolutions().get(0).version());
+                var interpretation = model.getAdapter(ReasoningAdapter.class)
+                                .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL);
+                var cursor = interpretation.getAll();
+                int max = -1;
+                var types = new LinkedHashMap<PartialRelation, Integer>();
+                var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL);
+                while (cursor.move()) {
+                        max = Math.max(max, cursor.getKey().get(0));
+                        var type = typeInterpretation.get(cursor.getKey());
+                        if (type != null) {
+                                types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1);
+                        }
+                }
+                System.out.println("Model size: " + (max + 1));
+                System.out.println(types);
+//              initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore());
+        }
+
+        public static void main(String[] args) {
+                ProblemStandaloneSetup.doSetup();
+                var injector = new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration();
+                var test = injector.getInstance(ModelGenerationTest.class);
+                try {
+                        test.statechartTest();
+                } catch (AssertionError e) {
+                        e.printStackTrace();
+                }
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java
new file mode 100644
index 00000000..5ad61463
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.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.propagation;
+
+@FunctionalInterface
+public interface BoundPropagator {
+        PropagationResult propagateOne();
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java
new file mode 100644
index 00000000..3ea5a75f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java
@@ -0,0 +1,20 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.propagation;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.dse.propagation.impl.PropagationBuilderImpl;
+
+public interface PropagationAdapter extends ModelAdapter {
+        @Override
+        PropagationStoreAdapter getStoreAdapter();
+
+        PropagationResult propagate();
+
+        static PropagationBuilder builder() {
+                return new PropagationBuilderImpl();
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java
new file mode 100644
index 00000000..f8a89b30
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.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.propagation;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.model.ModelStore;
+
+import java.util.Collection;
+import java.util.List;
+
+@SuppressWarnings("UnusedReturnValue")
+public interface PropagationBuilder extends ModelAdapterBuilder {
+        PropagationBuilder rule(Rule propagationRule);
+
+        default PropagationBuilder rules(Rule... propagationRules) {
+                return rules(List.of(propagationRules));
+        }
+
+        default PropagationBuilder rules(Collection<Rule> propagationRules) {
+                propagationRules.forEach(this::rule);
+                return this;
+        }
+
+        PropagationBuilder propagator(Propagator propagator);
+
+        @Override
+        PropagationStoreAdapter build(ModelStore store);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java
index 1bc537d1..ea56653a 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java
@@ -3,17 +3,17 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.refinement;
+package tools.refinery.store.dse.propagation;
 
-public enum RefinementResult {
+public enum PropagationResult {
         UNCHANGED,
-        REFINED,
+        PROPAGATED,
         REJECTED;
 
-        public RefinementResult andThen(RefinementResult next) {
+        public PropagationResult andThen(PropagationResult next) {
                 return switch (this) {
                         case UNCHANGED -> next;
-                        case REFINED -> next == REJECTED ? REJECTED : REFINED;
+                        case PROPAGATED -> next == REJECTED ? REJECTED : PROPAGATED;
                         case REJECTED -> REJECTED;
                 };
         }
@@ -21,4 +21,8 @@ public enum RefinementResult {
         public boolean isRejected() {
                 return this == REJECTED;
         }
+
+        public boolean isChanged() {
+                return this == PROPAGATED;
+        }
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java
new file mode 100644
index 00000000..82cba909
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.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.propagation;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.model.Model;
+
+public interface PropagationStoreAdapter extends ModelStoreAdapter {
+        @Override
+        PropagationAdapter createModelAdapter(Model model);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java
new file mode 100644
index 00000000..c6b4e1c9
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.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.propagation;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+@FunctionalInterface
+public interface Propagator {
+        default void configure(ModelStoreBuilder storeBuilder) {
+        }
+
+        BoundPropagator bindToModel(Model model);
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java
new file mode 100644
index 00000000..586a8d7a
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.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.propagation.impl;
+
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.dse.propagation.PropagationStoreAdapter;
+import tools.refinery.store.model.Model;
+
+class PropagationAdapterImpl implements PropagationAdapter {
+        private final Model model;
+        private final PropagationStoreAdapterImpl storeAdapter;
+        private final BoundPropagator[] boundPropagators;
+
+        public PropagationAdapterImpl(Model model, PropagationStoreAdapterImpl storeAdapter) {
+                this.model = model;
+                this.storeAdapter = storeAdapter;
+                var propagators = storeAdapter.getPropagators();
+                boundPropagators = new BoundPropagator[propagators.size()];
+                for (int i = 0; i < boundPropagators.length; i++) {
+                        boundPropagators[i] = propagators.get(i).bindToModel(model);
+                }
+        }
+
+        @Override
+        public PropagationResult propagate() {
+                PropagationResult result = PropagationResult.UNCHANGED;
+                PropagationResult lastResult;
+                do {
+                        lastResult = propagateOne();
+                        result = result.andThen(lastResult);
+                } while (lastResult.isChanged());
+                return result;
+        }
+
+        private PropagationResult propagateOne() {
+                PropagationResult result = PropagationResult.UNCHANGED;
+                for (int i = 0; i < boundPropagators.length; i++) {
+                        var lastResult = propagateUntilFixedPoint(i);
+                        result = result.andThen(lastResult);
+                        if (result.isRejected()) {
+                                break;
+                        }
+                }
+                return result;
+        }
+
+        private PropagationResult propagateUntilFixedPoint(int propagatorIndex) {
+                var propagator = boundPropagators[propagatorIndex];
+                PropagationResult result = PropagationResult.UNCHANGED;
+                PropagationResult lastResult;
+                do {
+                        lastResult = propagator.propagateOne();
+                        result = result.andThen(lastResult);
+                } while (lastResult.isChanged());
+                return result;
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public PropagationStoreAdapter getStoreAdapter() {
+                return storeAdapter;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java
new file mode 100644
index 00000000..c844a89f
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.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.propagation.impl;
+
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.dse.propagation.PropagationStoreAdapter;
+import tools.refinery.store.dse.propagation.Propagator;
+import tools.refinery.store.dse.propagation.impl.rule.RuleBasedPropagator;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+
+import java.util.*;
+
+public class PropagationBuilderImpl extends AbstractModelAdapterBuilder<PropagationStoreAdapter>
+                implements PropagationBuilder {
+        private final Set<Rule> propagationRules = new LinkedHashSet<>();
+        private final Deque<Propagator> propagators = new ArrayDeque<>();
+
+        @Override
+        public PropagationBuilder rule(Rule propagationRule) {
+                checkNotConfigured();
+                propagationRules.add(propagationRule);
+                return this;
+        }
+
+        @Override
+        public PropagationBuilder propagator(Propagator propagator) {
+                checkNotConfigured();
+                propagators.addFirst(propagator);
+                return this;
+        }
+
+        @Override
+        protected void doConfigure(ModelStoreBuilder storeBuilder) {
+                super.doConfigure(storeBuilder);
+                if (!propagationRules.isEmpty()) {
+                        propagators.addFirst(new RuleBasedPropagator(List.copyOf(propagationRules)));
+                }
+                for (var propagator : propagators) {
+                        propagator.configure(storeBuilder);
+                }
+        }
+
+        @Override
+        protected PropagationStoreAdapter doBuild(ModelStore store) {
+                return new PropagationStoreAdapterImpl(store, List.copyOf(propagators));
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java
new file mode 100644
index 00000000..a223caed
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.propagation.impl;
+
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.propagation.PropagationStoreAdapter;
+import tools.refinery.store.dse.propagation.Propagator;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+
+import java.util.List;
+
+class PropagationStoreAdapterImpl implements PropagationStoreAdapter {
+        private final ModelStore store;
+        private final List<Propagator> propagators;
+
+        PropagationStoreAdapterImpl(ModelStore store, List<Propagator> propagators) {
+                this.store = store;
+                this.propagators = propagators;
+        }
+
+        @Override
+        public ModelStore getStore() {
+                return store;
+        }
+
+        @Override
+        public PropagationAdapter createModelAdapter(Model model) {
+                return new PropagationAdapterImpl(model, this);
+        }
+
+        List<Propagator> getPropagators() {
+                return propagators;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java
new file mode 100644
index 00000000..6e6a78d2
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java
@@ -0,0 +1,37 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.propagation.impl.rule;
+
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.dse.transition.actions.BoundAction;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.ModelQueryAdapter;
+import tools.refinery.store.query.resultset.ResultSet;
+
+class BoundPropagationRule {
+        private final ResultSet<Boolean> resultSet;
+        private final BoundAction action;
+
+        public BoundPropagationRule(Model model, Rule rule) {
+                resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(rule.getPrecondition());
+                action = rule.createAction(model);
+        }
+
+        public PropagationResult fireAll() {
+                if (resultSet.size() == 0) {
+                        return PropagationResult.UNCHANGED;
+                }
+                var cursor = resultSet.getAll();
+                while (cursor.move()) {
+                        var result = action.fire(cursor.getKey());
+                        if (!result) {
+                                return PropagationResult.REJECTED;
+                        }
+                }
+                return PropagationResult.PROPAGATED;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java
new file mode 100644
index 00000000..bd03f923
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java
@@ -0,0 +1,43 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.propagation.impl.rule;
+
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationResult;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.ModelQueryAdapter;
+
+import java.util.List;
+
+public class BoundRuleBasedPropagator implements BoundPropagator {
+        private final ModelQueryAdapter queryEngine;
+        private final BoundPropagationRule[] boundRules;
+
+        public BoundRuleBasedPropagator(Model model, List<Rule> propagationRules) {
+                queryEngine = model.getAdapter(ModelQueryAdapter.class);
+                boundRules = new BoundPropagationRule[propagationRules.size()];
+                for (int i = 0; i < boundRules.length; i++) {
+                        boundRules[i] = new BoundPropagationRule(model, propagationRules.get(i));
+                }
+        }
+
+        @Override
+        public PropagationResult propagateOne() {
+                queryEngine.flushChanges();
+                PropagationResult result = PropagationResult.UNCHANGED;
+                // Use a classic for loop to avoid allocating an iterator.
+                //noinspection ForLoopReplaceableByForEach
+                for (int i = 0; i < boundRules.length; i++) {
+                        var lastResult = boundRules[i].fireAll();
+                        result = result.andThen(lastResult);
+                        if (result.isRejected()) {
+                                break;
+                        }
+                }
+                return result;
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java
new file mode 100644
index 00000000..709b2416
--- /dev/null
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.dse.propagation.impl.rule;
+
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.Propagator;
+import tools.refinery.store.dse.transition.Rule;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.query.ModelQueryBuilder;
+
+import java.util.List;
+
+public class RuleBasedPropagator implements Propagator {
+        private final List<Rule> propagationRules;
+
+        public RuleBasedPropagator(List<Rule> propagationRules) {
+                this.propagationRules = propagationRules;
+        }
+
+        @Override
+        public void configure(ModelStoreBuilder storeBuilder) {
+                var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class);
+                for (var propagationRule : propagationRules) {
+                        queryBuilder.query(propagationRule.getPrecondition());
+                }
+        }
+
+        @Override
+        public BoundPropagator bindToModel(Model model) {
+                return new BoundRuleBasedPropagator(model, propagationRules);
+        }
+}
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
index 8f7e3bdc..4a75a3a6 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java
@@ -33,7 +33,11 @@ public class BestFirstExplorer extends BestFirstWorker {
                 var lastBest = submit().newVersion();
                 while (shouldRun()) {
                         if (lastBest == null) {
-                                lastBest = restoreToBest();
+                                if (random.nextInt(10) == 0) {
+                                        lastBest = restoreToRandom(random);
+                                } else {
+                                        lastBest = restoreToBest();
+                                }
                                 if (lastBest == null) {
                                         return;
                                 }
@@ -49,7 +53,7 @@ public class BestFirstExplorer extends BestFirstWorker {
                                         } else {
                                                 var newVisit = newSubmit.newVersion();
                                                 int compareResult = compare(lastBest, newVisit);
-                                                if (compareResult >= 0) {
+                                                if (compareResult >= 0)  {
                                                         lastBest = newVisit;
                                                 } else {
                                                         lastBest = null;
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
index 5d738297..aca800a3 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java
@@ -5,6 +5,8 @@
  */
 package tools.refinery.store.dse.strategy;
 
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
 import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
 import tools.refinery.store.dse.transition.ObjectiveValue;
 import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
@@ -24,6 +26,7 @@ public class BestFirstWorker {
         final StateCoderAdapter stateCoderAdapter;
         final DesignSpaceExplorationAdapter explorationAdapter;
         final ModelQueryAdapter queryAdapter;
+        final @Nullable PropagationAdapter propagationAdapter;
         final VisualizationStore visualizationStore;
         final boolean isVisualizationEnabled;
 
@@ -34,6 +37,7 @@ public class BestFirstWorker {
                 explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class);
                 stateCoderAdapter = model.getAdapter(StateCoderAdapter.class);
                 queryAdapter = model.getAdapter(ModelQueryAdapter.class);
+                propagationAdapter = model.tryGetAdapter(PropagationAdapter.class).orElse(null);
                 activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(),
                                 explorationAdapter.getTransformations());
                 visualizationStore = storeManager.getVisualizationStore();
@@ -96,7 +100,11 @@ public class BestFirstWorker {
         }
 
         public VersionWithObjectiveValue restoreToRandom(Random random) {
-                var randomVersion = storeManager.getObjectiveStore().getRandom(random);
+                var objectiveStore = storeManager.getObjectiveStore();
+                if (objectiveStore.getSize() == 0) {
+                        return null;
+                }
+                var randomVersion = objectiveStore.getRandom(random);
                 last = randomVersion;
                 if (randomVersion != null) {
                         this.model.restore(randomVersion.version());
@@ -108,41 +116,40 @@ public class BestFirstWorker {
                 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!");
-                }
-        }
-
         public record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) {
         }
 
         public RandomVisitResult visitRandomUnvisited(Random random) {
                 checkSynchronized();
-                if (!model.hasUncommittedChanges()) {
-                        var visitResult = activationStoreWorker.fireRandomActivation(this.last, random);
-                        queryAdapter.flushChanges();
-
-                        if (visitResult.successfulVisit()) {
-                                Version oldVersion = null;
-                                if (isVisualizationEnabled) {
-                                        oldVersion = last.version();
-                                }
-                                var submitResult = submit();
-                                if (isVisualizationEnabled && submitResult.newVersion() != null) {
-                                        var newVersion = submitResult.newVersion().version();
-                                        visualizationStore.addTransition(oldVersion, newVersion,
-                                                        "fire: " + visitResult.transformation() + ", " + visitResult.activation());
-                                }
-                                return new RandomVisitResult(submitResult, visitResult.mayHaveMore());
-                        } else {
+                if (model.hasUncommittedChanges()) {
+                        throw new IllegalStateException("The model has uncommitted changes!");
+                }
+
+                var visitResult = activationStoreWorker.fireRandomActivation(this.last, random);
+
+                if (!visitResult.successfulVisit()) {
+                        return new RandomVisitResult(null, visitResult.mayHaveMore());
+                }
+
+                if (propagationAdapter != null) {
+                        var propagationResult = propagationAdapter.propagate();
+                        if (propagationResult.isRejected()) {
                                 return new RandomVisitResult(null, visitResult.mayHaveMore());
                         }
-                } else {
-                        throw new IllegalStateException("The model has uncommitted changes!");
                 }
+                queryAdapter.flushChanges();
+
+                Version oldVersion = null;
+                if (isVisualizationEnabled) {
+                        oldVersion = last.version();
+                }
+                var submitResult = submit();
+                if (isVisualizationEnabled && submitResult.newVersion() != null) {
+                        var newVersion = submitResult.newVersion().version();
+                        visualizationStore.addTransition(oldVersion, newVersion,
+                                        "fire: " + visitResult.transformation() + ", " + visitResult.activation());
+                }
+                return new RandomVisitResult(submitResult, visitResult.mayHaveMore());
         }
 
         public boolean hasEnoughSolution() {
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java
index 55f43735..ed2ff33d 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java
@@ -11,18 +11,14 @@ import tools.refinery.store.tuple.Tuple;
 
 public class BoundAction {
         private final Action action;
-        private final BoundActionLiteral[] boundLiterals;
+        private final Model model;
+        private BoundActionLiteral @Nullable [] boundLiterals;
         private Tuple activation;
         private final int[] localVariables;
 
         BoundAction(Action action, Model model) {
                 this.action = action;
-                var actionLiterals = action.getActionLiterals();
-                int size = actionLiterals.size();
-                boundLiterals = new BoundActionLiteral[size];
-                for (int i = 0; i < size; i++) {
-                        boundLiterals[i] = actionLiterals.get(i).bindToModel(model);
-                }
+                this.model = model;
                 localVariables = new int[action.getLocalVariables().size()];
         }
 
@@ -31,6 +27,9 @@ public class BoundAction {
                         throw new IllegalStateException("Reentrant firing is not allowed");
                 }
                 this.activation = activation;
+                if (boundLiterals == null) {
+                        boundLiterals = bindLiterals();
+                }
                 try {
                         int size = boundLiterals.length;
                         for (int i = 0; i < size; i++) {
@@ -50,6 +49,16 @@ public class BoundAction {
                 return true;
         }
 
+        private BoundActionLiteral[] bindLiterals() {
+                var actionLiterals = action.getActionLiterals();
+                int size = actionLiterals.size();
+                var boundLiteralsArray = new BoundActionLiteral[size];
+                for (int i = 0; i < size; i++) {
+                        boundLiteralsArray[i] = actionLiterals.get(i).bindToModel(model);
+                }
+                return boundLiteralsArray;
+        }
+
         private Tuple getInputTuple(int @Nullable [] inputAllocation) {
                 if (inputAllocation == null) {
                         // Identity allocation.
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
index 9f4bb536..5a7ba8f4 100644
--- 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
@@ -28,9 +28,9 @@ public class QueryObjective implements Objective {
                 return () -> {
                         var cursor = resultSet.getAll();
                         if (!cursor.move()) {
-                                throw new IllegalStateException("Query providing the objective function has no values!");
+                                return 0;
                         }
-                        return cursor.getValue().doubleValue();
+                        return Math.max(cursor.getValue().doubleValue(), 0);
                 };
         }
 
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
index d9e29eca..82f89db7 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java
@@ -104,9 +104,16 @@ public class ActivationStoreImpl implements ActivationStore {
         public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) {
                 var entries = versionToActivations.get(version);
 
+                var weights = new double[entries.size()];
+                double totalWeight = 0;
                 int numberOfAllUnvisitedActivations = 0;
-                for (var entry : entries) {
-                        numberOfAllUnvisitedActivations += entry.getNumberOfUnvisitedActivations();
+                for (int i = 0; i < weights.length; i++) {
+                        var entry = entries.get(i);
+                        int unvisited = entry.getNumberOfUnvisitedActivations();
+                        double weight = unvisited == 0 ? 0 : unvisited; //(Math.log(unvisited) + 1.0);
+                        weights[i] = weight;
+                        totalWeight += weight;
+                        numberOfAllUnvisitedActivations += unvisited;
                 }
 
                 if (numberOfAllUnvisitedActivations == 0) {
@@ -114,18 +121,18 @@ public class ActivationStoreImpl implements ActivationStore {
                         return new VisitResult(false, false, -1, -1);
                 }
 
-                int offset = random.nextInt(numberOfAllUnvisitedActivations);
+                double offset = random.nextDouble(totalWeight);
                 int transformation = 0;
                 for (; transformation < entries.size(); transformation++) {
-                        var entry = entries.get(transformation);
-                        int unvisited = entry.getNumberOfUnvisitedActivations();
-                        if (unvisited > 0 && offset < unvisited) {
+                        double weight = weights[transformation];
+                        if (weight > 0 && offset < weight) {
+                                var entry = entries.get(transformation);
                                 int activation = random.nextInt(entry.getNumberOfActivations());
                                 return this.visitActivation(version, transformation, activation);
                         }
-                        offset -= unvisited;
+                        offset -= weight;
                 }
 
-                throw new AssertionError("Unvisited activation %d not found".formatted(offset));
+                throw new AssertionError("Unvisited activation %f not found".formatted(offset));
         }
 }
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
index 881b133c..1d7c5ce5 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java
@@ -32,7 +32,7 @@ public class ActivationStoreWorker {
 
         public ActivationStore.VisitResult fireRandomActivation(VersionWithObjectiveValue thisVersion, Random random) {
                 var result = store.getRandomAndMarkAsVisited(thisVersion, random);
-                if(result.successfulVisit()) {
+                if (result.successfulVisit()) {
                         int selectedTransformation = result.transformation();
                         int selectedActivation = result.activation();
 
@@ -40,13 +40,13 @@ public class ActivationStoreWorker {
                         var tuple = transformation.getActivation(selectedActivation);
 
                         boolean success = transformation.fireActivation(tuple);
-                        if(success) {
+                        if (success) {
                                 return result;
                         } else {
                                 return new ActivationStore.VisitResult(
                                                 false,
                                                 result.mayHaveMore(),
-                                                selectedActivation,
+                                                selectedTransformation,
                                                 selectedActivation);
                         }
                 }
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java
index 99c501ce..62aadb4a 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.linearsolver.MPConstraint;
 import com.google.ortools.linearsolver.MPObjective;
@@ -13,18 +13,15 @@ import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
 import org.eclipse.collections.api.factory.primitive.IntSets;
 import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
 import org.eclipse.collections.api.set.primitive.MutableIntSet;
+import tools.refinery.store.dse.propagation.BoundPropagator;
+import tools.refinery.store.dse.propagation.PropagationResult;
 import tools.refinery.store.model.Interpretation;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.query.ModelQueryAdapter;
-import tools.refinery.store.reasoning.refinement.RefinementResult;
-import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
 import tools.refinery.store.representation.cardinality.*;
 import tools.refinery.store.tuple.Tuple;
 
-class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
-        private final Model model;
-        private final ScopePropagatorStoreAdapterImpl storeAdapter;
+class BoundScopePropagator implements BoundPropagator {
         private final ModelQueryAdapter queryEngine;
         private final Interpretation<CardinalityInterval> countInterpretation;
         private final MPSolver solver;
@@ -34,30 +31,22 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
         private final TypeScopePropagator[] propagators;
         private boolean changed = true;
 
-        public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) {
-                this.model = model;
-                this.storeAdapter = storeAdapter;
+        public BoundScopePropagator(Model model, ScopePropagator storeAdapter) {
                 queryEngine = model.getAdapter(ModelQueryAdapter.class);
                 countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol());
                 solver = MPSolver.createSolver("GLOP");
                 objective = solver.objective();
                 initializeVariables();
                 countInterpretation.addListener(this::countChanged, true);
-                var propagatorFactories = storeAdapter.getPropagatorFactories();
+                var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories();
                 propagators = new TypeScopePropagator[propagatorFactories.size()];
                 for (int i = 0; i < propagators.length; i++) {
                         propagators[i] = propagatorFactories.get(i).createPropagator(this);
                 }
         }
 
-        @Override
-        public Model getModel() {
-                return model;
-        }
-
-        @Override
-        public ScopePropagatorStoreAdapter getStoreAdapter() {
-                return storeAdapter;
+        ModelQueryAdapter getQueryEngine() {
+                return queryEngine;
         }
 
         private void initializeVariables() {
@@ -149,29 +138,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
         }
 
         @Override
-        public RefinementResult propagate() {
-                var result = RefinementResult.UNCHANGED;
-                RefinementResult currentRoundResult;
-                do {
-                        currentRoundResult = propagateOne();
-                        result = result.andThen(currentRoundResult);
-                        if (result.isRejected()) {
-                                return result;
-                        }
-                } while (currentRoundResult != RefinementResult.UNCHANGED);
-                return result;
-        }
-
-        private RefinementResult propagateOne() {
+        public PropagationResult propagateOne() {
                 queryEngine.flushChanges();
                 if (!changed) {
-                        return RefinementResult.UNCHANGED;
+                        return PropagationResult.UNCHANGED;
                 }
                 changed = false;
                 for (var propagator : propagators) {
                         propagator.updateBounds();
                 }
-                var result = RefinementResult.UNCHANGED;
+                var result = PropagationResult.UNCHANGED;
                 if (activeVariables.isEmpty()) {
                         return checkEmptiness();
                 }
@@ -190,16 +166,16 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                 return result;
         }
 
-        private RefinementResult checkEmptiness() {
+        private PropagationResult checkEmptiness() {
                 var emptinessCheckingResult = solver.solve();
                 return switch (emptinessCheckingResult) {
-                        case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED;
-                        case INFEASIBLE -> RefinementResult.REJECTED;
+                        case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED;
+                        case INFEASIBLE -> PropagationResult.REJECTED;
                         default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult);
                 };
         }
 
-        private RefinementResult propagateNode(int nodeId, MPVariable variable) {
+        private PropagationResult propagateNode(int nodeId, MPVariable variable) {
                 objective.setCoefficient(variable, 1);
                 try {
                         objective.setMinimization();
@@ -209,7 +185,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                         case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value());
                         case UNBOUNDED -> lowerBound = 0;
                         case INFEASIBLE -> {
-                                return RefinementResult.REJECTED;
+                                return PropagationResult.REJECTED;
                         }
                         default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s"
                                         .formatted(variable, minimizationResult));
@@ -234,7 +210,7 @@ class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter {
                                 throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s"
                                                 .formatted(oldInterval, nodeId, newInterval));
                         }
-                        return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED;
+                        return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED;
                 } finally {
                         objective.setCoefficient(variable, 0);
                 }
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java
index 393c4b72..5d903f41 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder;
 import tools.refinery.store.dse.transition.objectives.Criteria;
@@ -28,7 +28,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT
 class LowerTypeScopePropagator extends TypeScopePropagator {
         private final int lowerBound;
 
-        private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery,
+        private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery,
                                                                          RelationalQuery multiQuery) {
                 super(adapter, allQuery, multiQuery);
                 this.lowerBound = lowerBound;
@@ -58,7 +58,7 @@ class LowerTypeScopePropagator extends TypeScopePropagator {
                 }
 
                 @Override
-                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
                         return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay);
                 }
 
@@ -72,10 +72,10 @@ class LowerTypeScopePropagator extends TypeScopePropagator {
                         super.configure(storeBuilder);
 
                         var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder
-                                        .clause(Integer.class, currentCount -> List.of(
-                                                        new CountCandidateLowerBoundLiteral(currentCount, type, List.of(Variable.of())),
-                                                        output.assign(sub(currentCount, constant(lowerBound))),
-                                                        check(greater(currentCount, constant(0)))
+                                        .clause(Integer.class, candidateLowerBound -> List.of(
+                                                        new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())),
+                                                        output.assign(sub(constant(lowerBound), candidateLowerBound)),
+                                                        check(greater(output, constant(0)))
                                         )));
 
                         storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects));
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java
index a6d663ea..986771a1 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 final class RoundingUtil {
         private static final double TOLERANCE = 0.01;
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java
index 531a7440..25b1966c 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java
@@ -3,15 +3,13 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.Loader;
-import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
-import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.representation.Symbol;
@@ -20,14 +18,16 @@ import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
 
 import java.util.*;
 
-public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<ScopePropagatorStoreAdapter>
-                implements ScopePropagatorBuilder {
-        private Symbol<CardinalityInterval> countSymbol = MultiObjectTranslator.COUNT_STORAGE;
+public class ScopePropagator implements ModelStoreConfiguration {
+        private final Symbol<CardinalityInterval> countSymbol;
         private final Map<PartialRelation, CardinalityInterval> scopes = new LinkedHashMap<>();
-        private List<TypeScopePropagator.Factory> typeScopePropagatorFactories;
+        private final List<TypeScopePropagator.Factory> typeScopePropagatorFactories = new ArrayList<>();
 
-        @Override
-        public ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol) {
+        public ScopePropagator() {
+                this(MultiObjectTranslator.COUNT_STORAGE);
+        }
+
+        public ScopePropagator(Symbol<CardinalityInterval> countSymbol) {
                 if (countSymbol.arity() != 1) {
                         throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead"
                                         .formatted(countSymbol, countSymbol.arity()));
@@ -39,11 +39,9 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                         throw new IllegalArgumentException("Count symbol must default value null");
                 }
                 this.countSymbol = countSymbol;
-                return this;
         }
 
-        @Override
-        public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) {
+        public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) {
                 if (type.arity() != 1) {
                         throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d"
                                         .formatted(type, type.arity()));
@@ -56,9 +54,29 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                 return this;
         }
 
+        public ScopePropagator scopes(Map<PartialRelation, CardinalityInterval> scopes) {
+                return scopes(scopes.entrySet());
+        }
+
+        public ScopePropagator scopes(Collection<Map.Entry<PartialRelation, CardinalityInterval>> scopes) {
+                for (var entry : scopes) {
+                        scope(entry.getKey(), entry.getValue());
+                }
+                return this;
+        }
+
         @Override
-        protected void doConfigure(ModelStoreBuilder storeBuilder) {
-                typeScopePropagatorFactories = new ArrayList<>(scopes.size());
+        public void apply(ModelStoreBuilder storeBuilder) {
+                createTypeScopePropagatorFactories();
+                Loader.loadNativeLibraries();
+                for (var factory : typeScopePropagatorFactories) {
+                        factory.configure(storeBuilder);
+                }
+                storeBuilder.getAdapter(PropagationBuilder.class)
+                                .propagator(model -> new BoundScopePropagator(model, this));
+        }
+
+        private void createTypeScopePropagatorFactories() {
                 for (var entry : scopes.entrySet()) {
                         var type = entry.getKey();
                         var bounds = entry.getValue();
@@ -72,15 +90,13 @@ public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder<Scop
                                 typeScopePropagatorFactories.add(upperFactory);
                         }
                 }
-                for (var factory : typeScopePropagatorFactories) {
-                        factory.configure(storeBuilder);
-                }
         }
 
-        @Override
-        protected ScopePropagatorStoreAdapter doBuild(ModelStore store) {
-                Loader.loadNativeLibraries();
-                return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes),
-                                Collections.unmodifiableList(typeScopePropagatorFactories));
+        Symbol<CardinalityInterval> getCountSymbol() {
+                return countSymbol;
+        }
+
+        List<TypeScopePropagator.Factory> getTypeScopePropagatorFactories() {
+                return typeScopePropagatorFactories;
         }
 }
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java
deleted file mode 100644
index c2d3f59e..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelAdapter;
-import tools.refinery.store.reasoning.refinement.RefinementResult;
-import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl;
-
-public interface ScopePropagatorAdapter extends ModelAdapter {
-        @Override
-        ScopePropagatorStoreAdapter getStoreAdapter();
-
-        RefinementResult propagate();
-
-        static ScopePropagatorBuilder builder() {
-                return new ScopePropagatorBuilderImpl();
-        }
-}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java
deleted file mode 100644
index a17e04a4..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelAdapterBuilder;
-import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-public interface ScopePropagatorBuilder extends ModelAdapterBuilder {
-        ScopePropagatorBuilder countSymbol(Symbol<CardinalityInterval> countSymbol);
-
-        ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval);
-
-        @Override
-        ScopePropagatorStoreAdapter build(ModelStore store);
-}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java
deleted file mode 100644
index 65d9c38d..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope;
-
-import tools.refinery.store.adapter.ModelStoreAdapter;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-import java.util.Map;
-
-public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter {
-        Map<PartialRelation, CardinalityInterval> getScopes();
-}
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java
index cfb95829..db80be7f 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java
@@ -3,11 +3,10 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import com.google.ortools.linearsolver.MPConstraint;
 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;
 import tools.refinery.store.query.dnf.RelationalQuery;
@@ -17,15 +16,15 @@ import tools.refinery.store.tuple.Tuple;
 import java.util.Collection;
 
 abstract class TypeScopePropagator {
-        private final ScopePropagatorAdapterImpl adapter;
+        private final BoundScopePropagator adapter;
         private final ResultSet<Boolean> allNodes;
         private final ResultSet<Boolean> multiNodes;
         protected final MPConstraint constraint;
 
-        protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery,
-                                                           RelationalQuery multiQuery) {
+        protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery,
+                                                                  RelationalQuery multiQuery) {
                 this.adapter = adapter;
-                var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class);
+                var queryEngine = adapter.getQueryEngine();
                 allNodes = queryEngine.getResultSet(allQuery);
                 multiNodes = queryEngine.getResultSet(multiQuery);
                 constraint = adapter.makeConstraint();
@@ -56,7 +55,7 @@ abstract class TypeScopePropagator {
         }
 
         public abstract static class Factory {
-                public abstract TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter);
+                public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter);
 
                 protected abstract Collection<AnyQuery> getQueries();
 
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java
index a0be0fb4..062f976c 100644
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java
+++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import tools.refinery.store.query.dnf.AnyQuery;
 import tools.refinery.store.query.dnf.Query;
@@ -19,7 +19,7 @@ import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectT
 class UpperTypeScopePropagator extends TypeScopePropagator {
         private final int upperBound;
 
-        private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery,
+        private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery,
                                                                          RelationalQuery multiQuery) {
                 super(adapter, allQuery, multiQuery);
                 this.upperBound = upperBound;
@@ -47,7 +47,7 @@ class UpperTypeScopePropagator extends TypeScopePropagator {
                 }
 
                 @Override
-                public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) {
+                public TypeScopePropagator createPropagator(BoundScopePropagator adapter) {
                         return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust);
                 }
 
diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java
deleted file mode 100644
index 282ffe6f..00000000
--- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java
+++ /dev/null
@@ -1,58 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.scope.internal;
-
-import tools.refinery.store.adapter.ModelAdapter;
-import tools.refinery.store.model.Model;
-import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.representation.PartialRelation;
-import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter;
-import tools.refinery.store.representation.Symbol;
-import tools.refinery.store.representation.cardinality.CardinalityInterval;
-
-import java.util.List;
-import java.util.Map;
-
-// Not a record, because we want to control getter visibility.
-@SuppressWarnings("ClassCanBeRecord")
-class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter {
-        private final ModelStore store;
-        private final Symbol<CardinalityInterval> countSymbol;
-        private final Map<PartialRelation, CardinalityInterval> scopes;
-        private final List<TypeScopePropagator.Factory> propagatorFactories;
-
-        public ScopePropagatorStoreAdapterImpl(
-                        ModelStore store, Symbol<CardinalityInterval> countSymbol,
-                        Map<PartialRelation, CardinalityInterval> scopes, List<TypeScopePropagator.Factory> propagatorFactories) {
-                this.store = store;
-                this.countSymbol = countSymbol;
-                this.scopes = scopes;
-                this.propagatorFactories = propagatorFactories;
-        }
-
-        @Override
-        public ModelStore getStore() {
-                return store;
-        }
-
-        Symbol<CardinalityInterval> getCountSymbol() {
-                return countSymbol;
-        }
-
-        @Override
-        public Map<PartialRelation, CardinalityInterval> getScopes() {
-                return scopes;
-        }
-
-        public List<TypeScopePropagator.Factory> getPropagatorFactories() {
-                return propagatorFactories;
-        }
-
-        @Override
-        public ModelAdapter createModelAdapter(Model model) {
-                return new ScopePropagatorAdapterImpl(model, this);
-        }
-}
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java
index 42ce2f56..5fc70ae1 100644
--- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java
@@ -7,13 +7,14 @@ package tools.refinery.store.reasoning.scope;
 
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.dse.propagation.PropagationResult;
 import tools.refinery.store.model.Interpretation;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningStoreAdapter;
-import tools.refinery.store.reasoning.refinement.RefinementResult;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
@@ -38,11 +39,12 @@ class MultiObjectTest {
         void beforeEach() {
                 store = ModelStore.builder()
                                 .with(ViatraModelQueryAdapter.builder())
+                                .with(PropagationAdapter.builder())
                                 .with(ReasoningAdapter.builder())
                                 .with(new MultiObjectTranslator())
                                 .with(PartialRelationTranslator.of(person)
                                                 .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE)))
-                                .with(ScopePropagatorAdapter.builder()
+                                .with(new ScopePropagator()
                                                 .scope(person, CardinalityIntervals.between(5, 15)))
                                 .build();
                 model = null;
@@ -57,7 +59,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12)));
         }
 
@@ -69,7 +71,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.between(5, 20)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12)));
         }
 
@@ -81,7 +83,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -90,7 +92,7 @@ class MultiObjectTest {
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+                assertThat(propagate(), is(PropagationResult.UNCHANGED));
         }
 
         @Test
@@ -99,7 +101,7 @@ class MultiObjectTest {
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -110,7 +112,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.atLeast(20)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -121,7 +123,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(0), CardinalityIntervals.atMost(1)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -133,7 +135,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12)));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12)));
         }
@@ -147,7 +149,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.atMost(11)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12)));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5)));
         }
@@ -161,7 +163,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.exactly(11)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -173,7 +175,7 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.atMost(2)))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REJECTED));
+                assertThat(propagate(), is(PropagationResult.REJECTED));
         }
 
         @Test
@@ -185,14 +187,14 @@ class MultiObjectTest {
                                                 .put(Tuple.of(1), CardinalityIntervals.SET))
                                 .seed(person, builder -> builder.reducedValue(TruthValue.TRUE))
                                 .build());
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12)));
                 countStorage.put(Tuple.of(0), CardinalityIntervals.ONE);
-                assertThat(propagate(), is(RefinementResult.REFINED));
+                assertThat(propagate(), is(PropagationResult.PROPAGATED));
                 assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11)));
                 countStorage.put(Tuple.of(1), CardinalityIntervals.ONE);
-                assertThat(propagate(), is(RefinementResult.UNCHANGED));
+                assertThat(propagate(), is(PropagationResult.UNCHANGED));
         }
 
         private void createModel(ModelSeed modelSeed) {
@@ -200,7 +202,7 @@ class MultiObjectTest {
                 countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE);
         }
 
-        private RefinementResult propagate() {
-                return model.getAdapter(ScopePropagatorAdapter.class).propagate();
+        private PropagationResult propagate() {
+                return model.getAdapter(PropagationAdapter.class).propagate();
         }
 }
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java
index 9daed660..e697298e 100644
--- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.reasoning.scope.internal;
+package tools.refinery.store.reasoning.scope;
 
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java
new file mode 100644
index 00000000..62c35cee
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java
@@ -0,0 +1,43 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.actions;
+
+import tools.refinery.store.dse.transition.actions.AbstractActionLiteral;
+import tools.refinery.store.dse.transition.actions.BoundActionLiteral;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+
+public class CleanupActionLiteral extends AbstractActionLiteral {
+        private final NodeVariable node;
+
+        public CleanupActionLiteral(NodeVariable node) {
+                this.node = node;
+        }
+
+        public NodeVariable getNode() {
+                return node;
+        }
+
+        @Override
+        public List<NodeVariable> getInputVariables() {
+                return List.of(node);
+        }
+
+        @Override
+        public List<NodeVariable> getOutputVariables() {
+                return List.of();
+        }
+
+        @Override
+        public BoundActionLiteral bindToModel(Model model) {
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                return tuple -> reasoningAdapter.cleanup(tuple.get(0)) ? Tuple.of() : null;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
index 990d11e5..f36fde44 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java
@@ -35,4 +35,8 @@ public final class PartialActionLiterals {
         public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) {
                 return new FocusActionLiteral(parent, child);
         }
+
+        public static CleanupActionLiteral cleanup(NodeVariable node) {
+                return new CleanupActionLiteral(node);
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
index d2cd2eb0..722458c8 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
@@ -18,18 +18,19 @@ import tools.refinery.store.query.dnf.Query;
 import tools.refinery.store.query.dnf.RelationalQuery;
 import tools.refinery.store.reasoning.ReasoningBuilder;
 import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
-import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
-import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
-import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.lifting.DnfLifter;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner;
 import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
 import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
 import tools.refinery.store.reasoning.refinement.StorageRefiner;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.representation.AnySymbol;
 import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.statecoding.StateCoderBuilder;
 
 import java.util.*;
 
@@ -109,6 +110,8 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder<ReasoningS
         @Override
         protected void doConfigure(ModelStoreBuilder storeBuilder) {
                 storeBuilder.symbols(ReasoningAdapterImpl.NODE_COUNT_SYMBOL);
+                storeBuilder.tryGetAdapter(StateCoderBuilder.class)
+                                .ifPresent(stateCoderBuilder -> stateCoderBuilder.exclude(ReasoningAdapterImpl.NODE_COUNT_SYMBOL));
                 for (var translator : translators.values()) {
                         translator.configure(storeBuilder);
                         if (translator instanceof PartialRelationTranslator relationConfiguration) {
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
index 8eb5a034..9ef6fb16 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.internal;
 
+import tools.refinery.store.dse.propagation.PropagationAdapter;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
 import tools.refinery.store.query.ModelQueryAdapter;
@@ -103,6 +104,11 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
                 for (var initializer : initializers) {
                         initializer.initialize(model, modelSeed);
                 }
+                model.tryGetAdapter(PropagationAdapter.class).ifPresent(propagationAdapter -> {
+                        if (propagationAdapter.propagate().isRejected()) {
+                                throw new IllegalArgumentException("Inconsistent initial mode: propagation failed");
+                        }
+                });
                 model.getAdapter(ModelQueryAdapter.class).flushChanges();
                 return model;
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
index 5c3298ac..61037be3 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
@@ -243,7 +243,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
                                                 MultiObjectTranslator.MULTI_VIEW.call(multi),
                                                 not(may(CONTAINED_SYMBOL.call(multi)))
                                 )
-                                .clause((container) -> List.of(
+                                .clause(container -> List.of(
                                                 MultiObjectTranslator.MULTI_VIEW.call(multi),
                                                 must(CONTAINS_SYMBOL.call(container, multi)),
                                                 not(MultiObjectTranslator.MULTI_VIEW.call(container))
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
index 90802864..8df23d9a 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
@@ -8,18 +8,23 @@ package tools.refinery.store.reasoning.translator.containment;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
 
+import java.util.Objects;
 import java.util.Set;
 
-record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
-                                                   Set<PartialRelation> forbiddenLinks) {
+final class InferredContainment {
         public static final InferredContainment UNKNOWN = new InferredContainment(
                         TruthValue.UNKNOWN, Set.of(), Set.of());
+        private final TruthValue contains;
+        private final Set<PartialRelation> mustLinks;
+        private final Set<PartialRelation> forbiddenLinks;
+        private final int hashCode;
 
         public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
                                                            Set<PartialRelation> forbiddenLinks) {
                 this.contains = adjustContains(contains, mustLinks, forbiddenLinks);
                 this.mustLinks = mustLinks;
                 this.forbiddenLinks = forbiddenLinks;
+                hashCode = Objects.hash(contains, mustLinks, forbiddenLinks);
         }
 
         private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks,
@@ -34,4 +39,39 @@ record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
                 }
                 return result;
         }
+
+        public TruthValue contains() {
+                return contains;
+        }
+
+        public Set<PartialRelation> mustLinks() {
+                return mustLinks;
+        }
+
+        public Set<PartialRelation> forbiddenLinks() {
+                return forbiddenLinks;
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (InferredContainment) obj;
+                return Objects.equals(this.contains, that.contains) &&
+                                Objects.equals(this.mustLinks, that.mustLinks) &&
+                                Objects.equals(this.forbiddenLinks, that.forbiddenLinks);
+        }
+
+        @Override
+        public int hashCode() {
+                return hashCode;
+        }
+
+        @Override
+        public String toString() {
+                return "InferredContainment[" +
+                                "contains=" + contains + ", " +
+                                "mustLinks=" + mustLinks + ", " +
+                                "forbiddenLinks=" + forbiddenLinks + ']';
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
index 05704096..bad96a66 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
@@ -5,17 +5,21 @@
  */
 package tools.refinery.store.reasoning.translator.multiobject;
 
+import tools.refinery.store.dse.propagation.PropagationBuilder;
+import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.dse.transition.objectives.Criteria;
 import tools.refinery.store.dse.transition.objectives.Objectives;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
 import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.literal.Literals;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.term.int_.IntTerms;
 import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
 import tools.refinery.store.query.view.AnySymbolView;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.actions.PartialActionLiterals;
 import tools.refinery.store.reasoning.representation.PartialFunction;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
 import tools.refinery.store.reasoning.translator.RoundingMode;
@@ -66,6 +70,11 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                                                                 LOWER_CARDINALITY_VIEW.call(p1, lower),
                                                                 check(greaterEq(lower, constant(1)))
                                                 ))))
+                                .candidate(Query.of("exists#candidate", (builder, p1) -> builder
+                                                .clause(
+                                                                LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)),
+                                                                Literals.not(MULTI_VIEW.call(p1))
+                                                )))
                                 .roundingMode(RoundingMode.PREFER_FALSE)
                                 .refiner(ExistsRefiner.of(COUNT_STORAGE))
                                 .exclude(null)
@@ -82,5 +91,17 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                 var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
                 reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE));
                 reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new);
+
+                storeBuilder.tryGetAdapter(PropagationBuilder.class)
+                                .ifPresent(propagationBuilder -> propagationBuilder.rule(
+                                                Rule.of("exists#cleanup", (builder, node) -> builder
+                                                                .clause(UpperCardinality.class, upper -> List.of(
+                                                                                UPPER_CARDINALITY_VIEW.call(node, upper),
+                                                                                check(UpperCardinalityTerms.less(upper,
+                                                                                                UpperCardinalityTerms.constant(UpperCardinalities.ONE)))
+                                                                ))
+                                                                .action(
+                                                                                PartialActionLiterals.cleanup(node)
+                                                                ))));
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
index 1ae94ae1..9a0c2b0f 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
@@ -8,17 +8,22 @@ package tools.refinery.store.reasoning.translator.typehierarchy;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 
 import java.util.Collections;
+import java.util.Objects;
 import java.util.Set;
 
-record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
-                                        PartialRelation candidateType) {
+public final class InferredType {
         public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null);
+        private final Set<PartialRelation> mustTypes;
+        private final Set<PartialRelation> mayConcreteTypes;
+        private final PartialRelation candidateType;
+        private final int hashCode;
 
         public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
                                                 PartialRelation candidateType) {
                 this.mustTypes = Collections.unmodifiableSet(mustTypes);
                 this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes);
                 this.candidateType = candidateType;
+                hashCode = Objects.hash(mustTypes, mayConcreteTypes, candidateType);
         }
 
         public boolean isConsistent() {
@@ -32,4 +37,40 @@ record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConc
         public boolean isMayConcrete(PartialRelation partialRelation) {
                 return mayConcreteTypes.contains(partialRelation);
         }
+
+
+        public Set<PartialRelation> mustTypes() {
+                return mustTypes;
+        }
+
+        public Set<PartialRelation> mayConcreteTypes() {
+                return mayConcreteTypes;
+        }
+
+        public PartialRelation candidateType() {
+                return candidateType;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                InferredType that = (InferredType) o;
+                return Objects.equals(mustTypes, that.mustTypes) &&
+                                Objects.equals(mayConcreteTypes, that.mayConcreteTypes) &&
+                                Objects.equals(candidateType, that.candidateType);
+        }
+
+        @Override
+        public int hashCode() {
+                return hashCode;
+        }
+
+        @Override
+        public String toString() {
+                return "InferredType[" +
+                                "mustTypes=" + mustTypes + ", " +
+                                "mayConcreteTypes=" + mayConcreteTypes + ", " +
+                                "candidateType=" + candidateType + ']';
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
index dc8a1d36..37ea1448 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
@@ -26,7 +26,8 @@ import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMu
 import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
 
 public class TypeHierarchyTranslator implements ModelStoreConfiguration {
-        private final Symbol<InferredType> typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED);
+        public static final Symbol<InferredType> TYPE_SYMBOL = Symbol.of("TYPE", 1, InferredType.class,
+                        InferredType.UNTYPED);
         private final TypeHierarchy typeHierarchy;
 
         public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) {
@@ -39,7 +40,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                         return;
                 }
 
-                storeBuilder.symbol(typeSymbol);
+                storeBuilder.symbol(TYPE_SYMBOL);
 
                 for (var entry : typeHierarchy.getPreservedTypes().entrySet()) {
                         storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue()));
@@ -50,13 +51,13 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                 }
 
                 var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class);
-                reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol));
+                reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, TYPE_SYMBOL));
         }
 
         private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) {
                 var may = Query.of(type.name() + "#partial#may", (builder, p1) -> {
                         if (!result.isAbstractType()) {
-                                builder.clause(new MayTypeView(typeSymbol, type).call(p1));
+                                builder.clause(new MayTypeView(TYPE_SYMBOL, type).call(p1));
                         }
                         for (var subtype : result.getDirectSubtypes()) {
                                 builder.clause(may(subtype.call(p1)));
@@ -64,12 +65,12 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                 });
 
                 var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause(
-                                new MustTypeView(typeSymbol, type).call(p1)
+                                new MustTypeView(TYPE_SYMBOL, type).call(p1)
                 ));
 
                 var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> {
                         if (!result.isAbstractType()) {
-                                builder.clause(new CandidateTypeView(typeSymbol, type).call(p1));
+                                builder.clause(new CandidateTypeView(TYPE_SYMBOL, type).call(p1));
                         }
                         for (var subtype : result.getDirectSubtypes()) {
                                 builder.clause(PartialLiterals.candidateMust(subtype.call(p1)));
@@ -80,7 +81,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                                 .may(may)
                                 .must(must)
                                 .candidate(candidate)
-                                .refiner(InferredTypeRefiner.of(typeSymbol, result));
+                                .refiner(InferredTypeRefiner.of(TYPE_SYMBOL, result));
 
                 if (!result.isAbstractType()) {
                         var decision = Rule.of(type.name(), (builder, instance) -> builder
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
index 088e3925..b63a8637 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java
@@ -67,4 +67,17 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi
                 }
                 throw new IllegalArgumentException("Unknown UpperCardinality: " + other);
         }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                FiniteUpperCardinality that = (FiniteUpperCardinality) o;
+                return finiteUpperBound == that.finiteUpperBound;
+        }
+
+        @Override
+        public int hashCode() {
+                return finiteUpperBound;
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
index bfaeea25..6bd66df7 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.representation.cardinality;
 
+import java.util.Objects;
 import java.util.function.BinaryOperator;
 import java.util.function.IntBinaryOperator;
 
@@ -89,4 +90,17 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper
                 }
                 return "[%d..%s]".formatted(lowerBound, upperBound);
         }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                NonEmptyCardinalityInterval that = (NonEmptyCardinalityInterval) o;
+                return lowerBound == that.lowerBound && Objects.equals(upperBound, that.upperBound);
+        }
+
+        @Override
+        public int hashCode() {
+                return lowerBound * 31 + upperBound.hashCode();
+        }
 }
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
index e3a334cd..03c701ae 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java
@@ -53,4 +53,14 @@ public final class UnboundedUpperCardinality implements UpperCardinality {
         public String toString() {
                 return "*";
         }
+
+        @Override
+        public boolean equals(Object obj) {
+                return this == obj || (obj != null && getClass() == obj.getClass());
+        }
+
+        @Override
+        public int hashCode() {
+                return -1;
+        }
 }