Merge pull request #50 from kris7t/generator-roundtrip

Round-trip model serialization and command line application

45 files changed, 1774 insertions, 253 deletions

diff --git a/subprojects/frontend/config/graphvizUMDVitePlugin.ts b/subprojects/frontend/config/graphvizUMDVitePlugin.ts
index ab726e4f..0c3c9aa0 100644
--- a/subprojects/frontend/config/graphvizUMDVitePlugin.ts
+++ b/subprojects/frontend/config/graphvizUMDVitePlugin.ts
@@ -27,13 +27,15 @@ export default function graphvizUMDVitePlugin(): PluginOption {
     async buildStart() {
       const issuer =
         root === undefined ? issuerFileName : path.join(root, issuerFileName);
-      const resolvedPath = pnpapi.resolveRequest(
-        '@hpcc-js/wasm/graphviz',
-        issuer,
-      );
-      if (resolvedPath === null) {
+      // Since https://github.com/hpcc-systems/hpcc-js-wasm/commit/15e1ace5edae7f94714e547a3ac20e0e17cd6b0c,
+      // hpcc-js has both a `.cjs` and a `.umd.js` build. PnPAPI will find the former, but we need the latter.
+      const resolvedPath = pnpapi
+        .resolveRequest('@hpcc-js/wasm/graphviz', issuer)
+        ?.replace(/\.cjs$/, '.umd.js');
+      if (resolvedPath === undefined) {
         return;
       }
+      console.log(resolvedPath);
       if (command === 'serve') {
         url = `/@fs/${resolvedPath}`;
       } else {
diff --git a/subprojects/frontend/package.json b/subprojects/frontend/package.json
index f55093ce..9dec8b32 100644
--- a/subprojects/frontend/package.json
+++ b/subprojects/frontend/package.json
@@ -33,23 +33,23 @@
     "@codemirror/language": "^6.9.3",
     "@codemirror/lint": "^6.4.2",
     "@codemirror/search": "^6.5.5",
-    "@codemirror/state": "^6.3.2",
-    "@codemirror/view": "^6.22.1",
-    "@emotion/react": "^11.11.1",
+    "@codemirror/state": "^6.3.3",
+    "@codemirror/view": "^6.22.3",
+    "@emotion/react": "^11.11.3",
     "@emotion/styled": "^11.11.0",
-    "@fontsource-variable/jetbrains-mono": "^5.0.18",
-    "@fontsource-variable/open-sans": "^5.0.18",
-    "@hpcc-js/wasm": "^2.15.0",
-    "@lezer/common": "^1.1.1",
+    "@fontsource-variable/jetbrains-mono": "^5.0.19",
+    "@fontsource-variable/open-sans": "^5.0.21",
+    "@hpcc-js/wasm": "^2.15.3",
+    "@lezer/common": "^1.1.2",
     "@lezer/highlight": "^1.2.0",
     "@lezer/lr": "^1.3.14",
     "@material-icons/svg": "^1.0.33",
-    "@mui/icons-material": "5.14.19",
-    "@mui/material": "5.14.19",
-    "@mui/system": "^5.14.19",
-    "@mui/x-data-grid": "^6.18.2",
+    "@mui/icons-material": "^5.15.1",
+    "@mui/material": "^5.15.1",
+    "@mui/system": "^5.15.1",
+    "@mui/x-data-grid": "^6.18.6",
     "ansi-styles": "^6.2.1",
-    "csstype": "^3.1.2",
+    "csstype": "^3.1.3",
     "d3": "^7.8.5",
     "d3-graphviz": "patch:d3-graphviz@npm%3A5.2.0#~/.yarn/patches/d3-graphviz-npm-5.2.0-161b1fbad4.patch",
     "d3-selection": "^3.0.0",
@@ -65,7 +65,7 @@
     "notistack": "^3.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",
-    "react-resize-detector": "^9.1.0",
+    "react-resize-detector": "^9.1.1",
     "xstate": "^4.38.3",
     "zod": "^3.22.4"
   },
@@ -75,38 +75,38 @@
     "@types/d3-graphviz": "^2.6.10",
     "@types/d3-selection": "^3.0.10",
     "@types/d3-zoom": "^3.0.8",
-    "@types/eslint": "^8.44.8",
+    "@types/eslint": "^8.56.0",
     "@types/html-minifier-terser": "^7.0.2",
     "@types/lodash-es": "^4.17.12",
     "@types/micromatch": "^4.0.6",
     "@types/ms": "^0.7.34",
-    "@types/node": "^20.10.2",
+    "@types/node": "^20.10.5",
     "@types/pnpapi": "^0.0.5",
-    "@types/react": "^18.2.41",
-    "@types/react-dom": "^18.2.17",
-    "@typescript-eslint/eslint-plugin": "^6.13.1",
-    "@typescript-eslint/parser": "^6.13.1",
+    "@types/react": "^18.2.45",
+    "@types/react-dom": "^18.2.18",
+    "@typescript-eslint/eslint-plugin": "^6.15.0",
+    "@typescript-eslint/parser": "^6.15.0",
     "@vitejs/plugin-react-swc": "^3.5.0",
-    "@xstate/cli": "^0.5.11",
+    "@xstate/cli": "^0.5.15",
     "cross-env": "^7.0.3",
-    "eslint": "^8.55.0",
+    "eslint": "^8.56.0",
     "eslint-config-airbnb": "^19.0.4",
     "eslint-config-airbnb-typescript": "^17.1.0",
     "eslint-config-prettier": "^9.1.0",
     "eslint-import-resolver-typescript": "^3.6.1",
-    "eslint-plugin-import": "^2.29.0",
+    "eslint-plugin-import": "^2.29.1",
     "eslint-plugin-jsx-a11y": "^6.8.0",
     "eslint-plugin-mobx": "^0.0.9",
-    "eslint-plugin-prettier": "^5.0.1",
+    "eslint-plugin-prettier": "^5.1.1",
     "eslint-plugin-react": "^7.33.2",
     "eslint-plugin-react-hooks": "^4.6.0",
     "html-minifier-terser": "^7.2.0",
     "micromatch": "^4.0.5",
     "pnpapi": "^0.0.0",
-    "prettier": "^3.1.0",
-    "typescript": "5.3.2",
-    "vite": "^5.0.4",
-    "vite-plugin-pwa": "^0.17.2",
+    "prettier": "^3.1.1",
+    "typescript": "5.3.3",
+    "vite": "^5.0.10",
+    "vite-plugin-pwa": "^0.17.4",
     "workbox-window": "^7.0.0"
   }
 }
diff --git a/subprojects/generator-cli/build.gradle.kts b/subprojects/generator-cli/build.gradle.kts
new file mode 100644
index 00000000..6c681222
--- /dev/null
+++ b/subprojects/generator-cli/build.gradle.kts
@@ -0,0 +1,24 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+        id("tools.refinery.gradle.java-application")
+}
+
+dependencies {
+        implementation(project(":refinery-generator"))
+        implementation(libs.jcommander)
+        implementation(libs.slf4j.api)
+}
+
+application {
+        mainClass.set("tools.refinery.generator.cli.RefineryCli")
+}
+
+tasks.shadowJar {
+        // Silence Xtext warning.
+        append("plugin.properties")
+}
diff --git a/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/RefineryCli.java b/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/RefineryCli.java
new file mode 100644
index 00000000..5de579e6
--- /dev/null
+++ b/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/RefineryCli.java
@@ -0,0 +1,64 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator.cli;
+
+import com.beust.jcommander.JCommander;
+import com.beust.jcommander.ParameterException;
+import com.google.inject.Inject;
+import tools.refinery.generator.cli.commands.GenerateCommand;
+import tools.refinery.generator.standalone.StandaloneRefinery;
+
+import java.io.IOException;
+
+public class RefineryCli {
+        private static final String GENERATE_COMMAND = "generate";
+
+        @Inject
+        private GenerateCommand generateCommand;
+
+        private JCommander jCommander;
+
+        public String parseArguments(String... args) {
+                var jc = getJCommander();
+                jc.parse(args);
+                return jc.getParsedCommand();
+        }
+
+        public void run(String command) throws IOException {
+                switch (command) {
+                case GENERATE_COMMAND -> generateCommand.run();
+                case null, default -> showUsageAndExit();
+                }
+        }
+
+        public void showUsageAndExit() {
+                getJCommander().usage();
+                System.exit(1);
+        }
+
+        private JCommander getJCommander() {
+                if (jCommander == null) {
+                        jCommander = JCommander.newBuilder()
+                                        .programName("refinery")
+                                        .addObject(this)
+                                        .addCommand(GENERATE_COMMAND, generateCommand)
+                                        .build();
+                }
+                return jCommander;
+        }
+
+        public static void main(String[] args) throws IOException {
+                var cli = StandaloneRefinery.getInjector().getInstance(RefineryCli.class);
+                String command = null;
+                try {
+                        command = cli.parseArguments(args);
+                } catch (ParameterException e) {
+                        System.err.println(e.getMessage());
+                        cli.showUsageAndExit();
+                }
+                cli.run(command);
+        }
+}
diff --git a/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/commands/GenerateCommand.java b/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/commands/GenerateCommand.java
new file mode 100644
index 00000000..b33fce23
--- /dev/null
+++ b/subprojects/generator-cli/src/main/java/tools/refinery/generator/cli/commands/GenerateCommand.java
@@ -0,0 +1,87 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator.cli.commands;
+
+import com.beust.jcommander.Parameter;
+import com.beust.jcommander.Parameters;
+import com.google.inject.Inject;
+import org.eclipse.emf.ecore.resource.Resource;
+import tools.refinery.generator.ModelGeneratorFactory;
+import tools.refinery.generator.ProblemLoader;
+
+import java.io.FileOutputStream;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+@Parameters(commandDescription = "Generate a model from a partial model")
+public class GenerateCommand {
+        @Inject
+        private ProblemLoader loader;
+
+        @Inject
+        private ModelGeneratorFactory generatorFactory;
+
+        private String inputPath;
+        private String outputPath = "-";
+        private List<String> scopes = new ArrayList<>();
+        private List<String> overrideScopes = new ArrayList<>();
+        private long randomSeed = 1;
+
+        @Parameter(description = "input path", required = true)
+        public void setInputPath(String inputPath) {
+                this.inputPath = inputPath;
+        }
+
+        @Parameter(names = {"-output", "-o"}, description = "Output path")
+        public void setOutputPath(String outputPath) {
+                this.outputPath = outputPath;
+        }
+
+        @Parameter(names = {"-scope", "-s"}, description = "Extra scope constraints")
+        public void setScopes(List<String> scopes) {
+                this.scopes = scopes;
+        }
+
+        @Parameter(names = {"-scope-override", "-S"}, description = "Override scope constraints")
+        public void setOverrideScopes(List<String> overrideScopes) {
+                this.overrideScopes = overrideScopes;
+        }
+
+        @Parameter(names = {"-random-seed", "-r"}, description = "Random seed")
+        public void setRandomSeed(long randomSeed) {
+                this.randomSeed = randomSeed;
+        }
+
+        public void run() throws IOException {
+                var problem = isStandardStream(inputPath) ? loader.loadStream(System.in) : loader.loadFile(inputPath);
+                problem = loader.loadScopeConstraints(problem, scopes, overrideScopes);
+                var generator = generatorFactory.createGenerator(problem);
+                generator.setRandomSeed(randomSeed);
+                generator.generate();
+                var solution = generator.serializeSolution();
+                var solutionResource = solution.eResource();
+                var saveOptions = Map.of();
+                if (isStandardStream(outputPath)) {
+                        printSolution(solutionResource, saveOptions);
+                } else {
+                        try (var outputStream = new FileOutputStream(outputPath)) {
+                                solutionResource.save(outputStream, saveOptions);
+                        }
+                }
+        }
+
+        private boolean isStandardStream(String path) {
+                return path == null || path.equals("-");
+        }
+
+        // We deliberately write to the standard output if no output path is specified.
+        @SuppressWarnings("squid:S106")
+        private void printSolution(Resource solutionResource, Map<?, ?> saveOptions) throws IOException {
+                solutionResource.save(System.out, saveOptions);
+        }
+}
diff --git a/subprojects/generator/build.gradle.kts b/subprojects/generator/build.gradle.kts
index d87ce6de..f78fee4d 100644
--- a/subprojects/generator/build.gradle.kts
+++ b/subprojects/generator/build.gradle.kts
@@ -12,4 +12,5 @@ dependencies {
         api(project(":refinery-language-semantics"))
         api(libs.eclipseCollections.api)
         implementation(project(":refinery-store-query-interpreter"))
+        testImplementation(testFixtures(project(":refinery-language")))
 }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
index 5b44c10a..1515dceb 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
@@ -5,7 +5,10 @@
  */
 package tools.refinery.generator;
 
+import com.google.inject.Provider;
+import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.semantics.ProblemTrace;
+import tools.refinery.language.semantics.SolutionSerializer;
 import tools.refinery.store.dse.strategy.BestFirstStoreManager;
 import tools.refinery.store.map.Version;
 import tools.refinery.store.model.ModelStore;
@@ -16,21 +19,22 @@ import tools.refinery.store.reasoning.seed.ModelSeed;
 
 public class ModelGenerator extends ModelFacade {
         private final Version initialVersion;
-
-        private int randomSeed = 0;
-
+        private final Provider<SolutionSerializer> solutionSerializerProvider;
+        private long randomSeed = 1;
         private boolean lastGenerationSuccessful;
 
-        public ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
+        ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed,
+                          Provider<SolutionSerializer> solutionSerializerProvider) {
                 super(problemTrace, store, modelSeed, Concreteness.CANDIDATE);
+                this.solutionSerializerProvider = solutionSerializerProvider;
                 initialVersion = getModel().commit();
         }
 
-        public int getRandomSeed() {
+        public long getRandomSeed() {
                 return randomSeed;
         }
 
-        public void setRandomSeed(int randomSeed) {
+        public void setRandomSeed(long randomSeed) {
                 this.randomSeed = randomSeed;
                 this.lastGenerationSuccessful = false;
         }
@@ -50,7 +54,7 @@ public class ModelGenerator extends ModelFacade {
                 if (solutions.isEmpty()) {
                         return false;
                 }
-                getModel().restore(solutions.get(0).version());
+                getModel().restore(solutions.getFirst().version());
                 lastGenerationSuccessful = true;
                 return true;
         }
@@ -63,9 +67,19 @@ public class ModelGenerator extends ModelFacade {
 
         @Override
         public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+                checkSuccessfulGeneration();
+                return super.getPartialInterpretation(partialSymbol);
+        }
+
+        public Problem serializeSolution() {
+                checkSuccessfulGeneration();
+                var serializer = solutionSerializerProvider.get();
+                return serializer.serializeSolution(getProblemTrace(), getModel());
+        }
+
+        private void checkSuccessfulGeneration() {
                 if (!lastGenerationSuccessful) {
                         throw new IllegalStateException("No generated model is available");
                 }
-                return super.getPartialInterpretation(partialSymbol);
         }
 }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java
index 6642d591..587601f2 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java
@@ -9,6 +9,7 @@ import com.google.inject.Inject;
 import com.google.inject.Provider;
 import tools.refinery.language.model.problem.Problem;
 import tools.refinery.language.semantics.ModelInitializer;
+import tools.refinery.language.semantics.SolutionSerializer;
 import tools.refinery.store.dse.propagation.PropagationAdapter;
 import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
 import tools.refinery.store.model.ModelStore;
@@ -25,6 +26,9 @@ public final class ModelGeneratorFactory {
         @Inject
         private Provider<ModelInitializer> initializerProvider;
 
+        @Inject
+        private Provider<SolutionSerializer> solutionSerializerProvider;
+
         private CancellationToken cancellationToken = CancellationToken.NONE;
 
         private boolean debugPartialInterpretations;
@@ -53,7 +57,8 @@ public final class ModelGeneratorFactory {
                                                 .requiredInterpretations(getRequiredInterpretations()));
                 initializer.configureStoreBuilder(storeBuilder);
                 var store = storeBuilder.build();
-                return new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed());
+                return new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed(),
+                solutionSerializerProvider);
         }
 
         private Collection<Concreteness> getRequiredInterpretations() {
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java
index bc02c887..7207a509 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java
@@ -11,7 +11,7 @@ import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 
 public class ModelSemantics extends ModelFacade {
-        public ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
+        ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
                 super(problemTrace, store, modelSeed, Concreteness.PARTIAL);
         }
 }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java
index 29f80714..20ea8132 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java
@@ -10,20 +10,30 @@ import com.google.inject.Provider;
 import org.eclipse.emf.common.util.URI;
 import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.xtext.diagnostics.Severity;
+import org.eclipse.xtext.resource.FileExtensionProvider;
 import org.eclipse.xtext.resource.IResourceFactory;
 import org.eclipse.xtext.resource.XtextResourceSet;
 import org.eclipse.xtext.util.LazyStringInputStream;
 import org.eclipse.xtext.validation.CheckMode;
 import org.eclipse.xtext.validation.IResourceValidator;
 import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.Relation;
+import tools.refinery.language.model.problem.ScopeDeclaration;
 import tools.refinery.store.util.CancellationToken;
 
+import java.io.ByteArrayOutputStream;
 import java.io.File;
 import java.io.IOException;
 import java.io.InputStream;
+import java.nio.charset.StandardCharsets;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
 import java.util.Map;
 
 public class ProblemLoader {
+        private String fileExtension;
+
         @Inject
         private Provider<XtextResourceSet> resourceSetProvider;
 
@@ -35,25 +45,39 @@ public class ProblemLoader {
 
         private CancellationToken cancellationToken = CancellationToken.NONE;
 
+        @Inject
+        public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) {
+                this.fileExtension = fileExtensionProvider.getPrimaryFileExtension();
+        }
+
         public ProblemLoader cancellationToken(CancellationToken cancellationToken) {
                 this.cancellationToken = cancellationToken;
                 return this;
         }
 
-        public Problem loadString(String problemString) throws IOException {
+        public Problem loadString(String problemString, URI uri) throws IOException {
                 try (var stream = new LazyStringInputStream(problemString)) {
-                        return loadStream(stream);
+                        return loadStream(stream, uri);
                 }
         }
 
-        public Problem loadStream(InputStream inputStream) throws IOException {
+        public Problem loadString(String problemString) throws IOException {
+                return loadString(problemString, null);
+        }
+
+        public Problem loadStream(InputStream inputStream, URI uri) throws IOException {
                 var resourceSet = resourceSetProvider.get();
-                var resource = resourceFactory.createResource(URI.createFileURI("__synthetic.problem"));
+                var resourceUri = uri == null ? URI.createFileURI("__synthetic." + fileExtension) : uri;
+                var resource = resourceFactory.createResource(resourceUri);
                 resourceSet.getResources().add(resource);
                 resource.load(inputStream, Map.of());
                 return loadResource(resource);
         }
 
+        public Problem loadStream(InputStream inputStream) throws IOException {
+                return loadStream(inputStream, null);
+        }
+
         public Problem loadFile(File file) throws IOException {
                 return loadFile(file.getAbsolutePath());
         }
@@ -82,9 +106,63 @@ public class ProblemLoader {
                 if (!errors.isEmpty()) {
                         throw new ValidationErrorsException(resource.getURI(), errors);
                 }
-                if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) {
+                if (resource.getContents().isEmpty() || !(resource.getContents().getFirst() instanceof Problem problem)) {
                         throw new IllegalArgumentException("Model generation problem not found in resource " + resource.getURI());
                 }
                 return problem;
         }
+
+        public Problem loadScopeConstraints(Problem problem, List<String> extraScopes,
+                                                                                List<String> overrideScopes) throws IOException {
+                var allScopes = new ArrayList<>(extraScopes);
+                allScopes.addAll(overrideScopes);
+                if (allScopes.isEmpty()) {
+                        return problem;
+                }
+                int originalStatementCount = problem.getStatements().size();
+                var builder = new StringBuilder();
+                var problemResource = problem.eResource();
+                try (var outputStream = new ByteArrayOutputStream()) {
+                        problemResource.save(outputStream, Map.of());
+                        builder.append(outputStream.toString(StandardCharsets.UTF_8));
+                }
+                builder.append('\n');
+                for (var scope : allScopes) {
+                        builder.append("scope ").append(scope).append(".\n");
+                }
+                var modifiedProblem = loadString(builder.toString(), problemResource.getURI());
+                var modifiedStatements = modifiedProblem.getStatements();
+                int modifiedStatementCount = modifiedStatements.size();
+                if (modifiedStatementCount != originalStatementCount + allScopes.size()) {
+                        throw new IllegalArgumentException("Failed to parse scope constraints");
+                }
+                // Override scopes remove any scope constraint from the original problem with the same target type.
+                var overriddenScopes = new HashSet<Relation>();
+                for (int i = modifiedStatementCount - overrideScopes.size(); i < modifiedStatementCount; i++) {
+                        var statement = modifiedStatements.get(i);
+                        if (!(statement instanceof ScopeDeclaration scopeDeclaration)) {
+                                throw new IllegalStateException("Invalid scope constraint: " + statement);
+                        }
+                        for (var typeScope : scopeDeclaration.getTypeScopes()) {
+                                overriddenScopes.add(typeScope.getTargetType());
+                        }
+                }
+                int statementIndex = 0;
+                var iterator = modifiedStatements.iterator();
+                // Scope overrides only affect type scopes from the original problem and leave type scopes added on the
+                // command line intact.
+                while (statementIndex < originalStatementCount && iterator.hasNext()) {
+                        var statement = iterator.next();
+                        if (statement instanceof ScopeDeclaration scopeDeclaration) {
+                                var typeScopes = scopeDeclaration.getTypeScopes();
+                                typeScopes.removeIf(typeScope -> overriddenScopes.contains(typeScope.getTargetType()));
+                                // Scope declarations with no type scopes are invalid, so we have to remove them.
+                                if (typeScopes.isEmpty()) {
+                                        iterator.remove();
+                                }
+                        }
+                        statementIndex++;
+                }
+                return modifiedProblem;
+        }
 }
diff --git a/subprojects/generator/src/test/java/tools/refinery/generator/ProblemLoaderTest.java b/subprojects/generator/src/test/java/tools/refinery/generator/ProblemLoaderTest.java
new file mode 100644
index 00000000..0c0db105
--- /dev/null
+++ b/subprojects/generator/src/test/java/tools/refinery/generator/ProblemLoaderTest.java
@@ -0,0 +1,129 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.extension.ExtendWith;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.nio.charset.StandardCharsets;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemLoaderTest {
+        private static final String PREFIX = """
+                        class Foo.
+                        class Bar.
+                        """;
+
+        @Inject
+        private ProblemLoader loader;
+
+        @ParameterizedTest
+        @MethodSource
+        void loadScopeConstraintsTest(String originalScopes, List<String> scopes, List<String> overrideScopes,
+                                                                  String expectedScopes) throws IOException {
+                var problem = loader.loadString(PREFIX + originalScopes);
+                var modifiedProblem = loader.loadScopeConstraints(problem, scopes, overrideScopes);
+                String serializedProblem;
+                try (var outputStream = new ByteArrayOutputStream()) {
+                        modifiedProblem.eResource().save(outputStream, Map.of());
+                        serializedProblem = outputStream.toString(StandardCharsets.UTF_8);
+                }
+                assertThat(serializedProblem, is(PREFIX + expectedScopes));
+        }
+
+        static Stream<Arguments> loadScopeConstraintsTest() {
+                return Stream.of(Arguments.of("",
+                                List.of(),
+                                List.of(),
+                                ""), Arguments.of("",
+                                List.of("node=5..10"),
+                                List.of(), """
+
+                                                scope node=5..10.
+                                                """), Arguments.of("",
+                                List.of("Foo=2", "Bar=3"),
+                                List.of(), """
+
+                                                scope Foo=2.
+                                                scope Bar=3.
+                                                """), Arguments.of("""
+                                                scope Foo = 1, Bar = 1.
+                                                """,
+                                List.of("node=5..10"),
+                                List.of(), """
+                                                scope Foo = 1, Bar = 1.
+
+                                                scope node=5..10.
+                                                """), Arguments.of("""
+                                                scope Foo = 0..10, Bar = 1.
+                                                """,
+                                List.of("Foo = 5"),
+                                List.of(), """
+                                                scope Foo = 0..10, Bar = 1.
+
+                                                scope Foo = 5.
+                                                """), Arguments.of("""
+                                                scope Foo = 1, Bar = 1.
+                                                """,
+                                List.of(),
+                                List.of("node=5..10"), """
+                                                scope Foo = 1, Bar = 1.
+
+                                                scope node=5..10.
+                                                """), Arguments.of("""
+                                                scope Foo = 1, Bar = 1.
+                                                """,
+                                List.of(),
+                                List.of("Foo=3..4"), """
+                                                scope Bar = 1.
+
+                                                scope Foo=3..4.
+                                                """), Arguments.of("""
+                                                scope Foo = 1, Bar = 1.
+                                                """,
+                                List.of("Foo=2"),
+                                List.of("Foo=3..4"), """
+                                                scope Bar = 1.
+
+                                                scope Foo=2.
+                                                scope Foo=3..4.
+                                                """), Arguments.of("""
+                                                scope Foo = 1.
+                                                scope Bar = 1.
+                                                """,
+                                List.of(),
+                                List.of("Bar=3..4"), """
+                                                scope Foo = 1.
+
+
+                                                scope Bar=3..4.
+                                                """), Arguments.of("""
+                                                scope Foo = 1, Bar = 1.
+                                                """,
+                                List.of(),
+                                List.of("Foo=3..4", "Bar=4..5"), """
+
+                                                scope Foo=3..4.
+                                                scope Bar=4..5.
+                                                """));
+        }
+}
diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore
index 204f922c..74229a89 100644
--- a/subprojects/language-model/src/main/resources/model/problem.ecore
+++ b/subprojects/language-model/src/main/resources/model/problem.ecore
@@ -23,7 +23,7 @@
     <eStructuralFeatures xsi:type="ecore:EAttribute" name="kind" eType="#//ReferenceKind"/>
     <eStructuralFeatures xsi:type="ecore:EReference" name="referenceType" eType="#//Relation"/>
     <eStructuralFeatures xsi:type="ecore:EReference" name="invalidMultiplicity" eType="#//Relation"
-        containment="true"/>
+        transient="true" containment="true"/>
   </eClassifiers>
   <eClassifiers xsi:type="ecore:EClass" name="NamedElement" abstract="true">
     <eStructuralFeatures xsi:type="ecore:EAttribute" name="name" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts
index 689f621e..777ef993 100644
--- a/subprojects/language-semantics/build.gradle.kts
+++ b/subprojects/language-semantics/build.gradle.kts
@@ -16,6 +16,7 @@ dependencies {
         api(project(":refinery-store-reasoning"))
         implementation(project(":refinery-store-reasoning-scope"))
         runtimeOnly(libs.eclipseCollections)
+        testImplementation(project(":refinery-generator"))
         testImplementation(project(":refinery-store-dse-visualization"))
         testImplementation(project(":refinery-store-query-interpreter"))
         testImplementation(testFixtures(project(":refinery-language")))
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
index ecaa7e0d..38bf5a61 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java
@@ -27,9 +27,7 @@ import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.seed.Seed;
 import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
-import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
-import tools.refinery.store.reasoning.translator.metamodel.MetamodelBuilder;
-import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
+import tools.refinery.store.reasoning.translator.metamodel.*;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
 import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
@@ -73,6 +71,10 @@ public class ModelInitializer {
 
         private ScopePropagator scopePropagator;
 
+        private int nodeCount;
+
+        private ModelSeed.Builder modelSeedBuilder;
+
         private ModelSeed modelSeed;
 
         public void readProblem(Problem problem) {
@@ -101,13 +103,17 @@ public class ModelInitializer {
                                                         TruthValue.FALSE));
                         collectNodes();
                         collectPartialSymbols();
+                        nodeCount = problemTrace.getNodeTrace().size();
+                        modelSeedBuilder = ModelSeed.builder(nodeCount);
+                        collectAssertions();
                         collectMetamodel();
                         metamodel = metamodelBuilder.build();
                         problemTrace.setMetamodel(metamodel);
-                        collectAssertions();
-                        int nodeCount = problemTrace.getNodeTrace().size();
-                        var modelSeedBuilder = ModelSeed.builder(nodeCount);
+                        fixClassDeclarationAssertions();
                         for (var entry : relationInfoMap.entrySet()) {
+                                if (entry.getKey() instanceof ReferenceDeclaration) {
+                                        continue;
+                                }
                                 var info = entry.getValue();
                                 var partialRelation = info.partialRelation();
                                 modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount));
@@ -296,7 +302,20 @@ public class ModelInitializer {
                 }
                 var multiplicity = getMultiplicityConstraint(referenceDeclaration);
                 try {
-                        metamodelBuilder.reference(relation, source, containment, multiplicity, target, oppositeRelation);
+                        var seed = relationInfoMap.get(referenceDeclaration).toSeed(nodeCount);
+                        var defaultValue = seed.majorityValue();
+                        if (defaultValue.must()) {
+                                defaultValue = TruthValue.FALSE;
+                        }
+                        modelSeedBuilder.seed(relation, seed);
+                        metamodelBuilder.reference(relation, ReferenceInfo.builder()
+                                        .containment(containment)
+                                        .source(source)
+                                        .multiplicity(multiplicity)
+                                        .target(target)
+                                        .opposite(oppositeRelation)
+                                        .defaultValue(defaultValue)
+                                        .build());
                 } catch (RuntimeException e) {
                         throw TracedException.addTrace(classDeclaration, e);
                 }
@@ -355,10 +374,6 @@ public class ModelInitializer {
                 collectCardinalityAssertions(newNodeId, TruthValue.UNKNOWN);
                 var tuple = Tuple.of(newNodeId);
                 mergeValue(classDeclaration, tuple, TruthValue.TRUE);
-                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
-                for (var subType : typeInfo.getDirectSubtypes()) {
-                        partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
-                }
         }
 
         private void collectEnumAssertions(EnumDeclaration enumDeclaration) {
@@ -399,6 +414,27 @@ public class ModelInitializer {
                 }
         }
 
+        private void fixClassDeclarationAssertions() {
+                for (var statement : problem.getStatements()) {
+                        if (statement instanceof ClassDeclaration classDeclaration) {
+                                fixClassDeclarationAssertions(classDeclaration);
+                        }
+                }
+        }
+
+        private void fixClassDeclarationAssertions(ClassDeclaration classDeclaration) {
+                var newNode = classDeclaration.getNewNode();
+                if (newNode == null) {
+                        return;
+                }
+                var newNodeId = getNodeId(newNode);
+                var tuple = Tuple.of(newNodeId);
+                var typeInfo = metamodel.typeHierarchy().getAnalysisResult(getPartialRelation(classDeclaration));
+                for (var subType : typeInfo.getDirectSubtypes()) {
+                        partialRelationInfoMap.get(subType).assertions().mergeValue(tuple, TruthValue.FALSE);
+                }
+        }
+
         private void mergeValue(Relation relation, Tuple key, TruthValue value) {
                 getRelationInfo(relation).assertions().mergeValue(key, value);
         }
@@ -482,7 +518,7 @@ public class ModelInitializer {
                         defaultValue = TruthValue.FALSE;
                 } else {
                         var seed = modelSeed.getSeed(partialRelation);
-                        defaultValue = seed.reducedValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
+                        defaultValue = seed.majorityValue() == TruthValue.FALSE ? TruthValue.FALSE : TruthValue.UNKNOWN;
                         var cursor = seed.getCursor(defaultValue, problemTrace.getNodeTrace().size());
                         // The symbol should be mutable if there is at least one non-default entry in the seed.
                         mutable = mutable || cursor.move();
@@ -495,7 +531,7 @@ public class ModelInitializer {
                 var problemParameters = predicateDefinition.getParameters();
                 int arity = problemParameters.size();
                 var parameters = new NodeVariable[arity];
-                var parameterMap = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(arity);
+                var parameterMap = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(arity);
                 var commonLiterals = new ArrayList<Literal>();
                 for (int i = 0; i < arity; i++) {
                         var problemParameter = problemParameters.get(i);
@@ -532,7 +568,7 @@ public class ModelInitializer {
                         return existing;
                 }
                 int localScopeSize = existing.size() + newVariables.size();
-                var localScope = new HashMap<tools.refinery.language.model.problem.Variable, Variable>(localScopeSize);
+                var localScope = HashMap.<tools.refinery.language.model.problem.Variable, Variable>newHashMap(localScopeSize);
                 localScope.putAll(existing);
                 for (var newVariable : newVariables) {
                         localScope.put(newVariable, Variable.of(newVariable.getName()));
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java
index cc634949..f686e980 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ProblemTraceImpl.java
@@ -9,7 +9,6 @@ import com.google.inject.Inject;
 import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
 import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
 import org.eclipse.collections.api.map.primitive.ObjectIntMap;
-import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.QualifiedName;
 import org.eclipse.xtext.scoping.IScope;
@@ -28,7 +27,7 @@ import java.util.HashMap;
 import java.util.LinkedHashMap;
 import java.util.Map;
 
-public class ProblemTraceImpl implements ProblemTrace {
+class ProblemTraceImpl implements ProblemTrace {
         @Inject
         private IQualifiedNameConverter qualifiedNameConverter;
 
@@ -164,24 +163,6 @@ public class ProblemTraceImpl implements ProblemTrace {
         }
 
         private <T> T getElement(IScope scope, QualifiedName qualifiedName, Class<T> type) {
-                var iterator = scope.getElements(qualifiedName).iterator();
-                if (!iterator.hasNext()) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("No such %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                var eObjectDescription = iterator.next();
-                if (iterator.hasNext()) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("Ambiguous %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), getProblem());
-                if (!type.isInstance(eObject)) {
-                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
-                        throw new IllegalArgumentException("Not a %s: %s"
-                                        .formatted(type.getName(), qualifiedNameString));
-                }
-                return type.cast(eObject);
+                return semanticsUtils.getElement(problem, scope, qualifiedName, type);
         }
 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
index b195a8e7..b72ba697 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SemanticsUtils.java
@@ -8,8 +8,14 @@ package tools.refinery.language.semantics;
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
 import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.scoping.IScope;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.language.model.problem.Problem;
 
 import java.util.Optional;
 
@@ -28,4 +34,39 @@ public class SemanticsUtils {
                 }
                 return Optional.of(qualifiedNameConverter.toString(qualifiedName));
         }
+
+        @Nullable
+        public <T> T maybeGetElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) {
+                if (qualifiedName == null) {
+                        throw new IllegalArgumentException("Element name must not be null");
+                }
+                var iterator = scope.getElements(qualifiedName).iterator();
+                if (!iterator.hasNext()) {
+                        return null;
+                }
+                var eObjectDescription = iterator.next();
+                if (iterator.hasNext()) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Ambiguous %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), problem);
+                if (!type.isInstance(eObject)) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Not a %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                return type.cast(eObject);
+        }
+
+        @NotNull
+        public <T> T getElement(Problem problem, IScope scope, QualifiedName qualifiedName, Class<T> type) {
+                var element = maybeGetElement(problem, scope, qualifiedName, type);
+                if (element == null) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("No such %s: %s"
+                                        .formatted(type.getName(), qualifiedNameString));
+                }
+                return element;
+        }
 }
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
new file mode 100644
index 00000000..57af599e
--- /dev/null
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java
@@ -0,0 +1,335 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import org.eclipse.collections.api.factory.primitive.IntObjectMaps;
+import org.eclipse.collections.api.factory.primitive.ObjectIntMaps;
+import org.eclipse.collections.api.map.primitive.MutableIntObjectMap;
+import org.eclipse.collections.api.map.primitive.MutableObjectIntMap;
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
+import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.resource.FileExtensionProvider;
+import org.eclipse.xtext.resource.IResourceFactory;
+import org.eclipse.xtext.resource.XtextResource;
+import org.eclipse.xtext.resource.XtextResourceSet;
+import org.eclipse.xtext.scoping.IScopeProvider;
+import tools.refinery.language.model.problem.*;
+import tools.refinery.language.utils.ProblemDesugarer;
+import tools.refinery.language.utils.ProblemUtil;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.typehierarchy.InferredType;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Locale;
+import java.util.Map;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class SolutionSerializer {
+        private String fileExtension;
+
+        @Inject
+        private Provider<XtextResourceSet> resourceSetProvider;
+
+        @Inject
+        private IResourceFactory resourceFactory;
+
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        @Inject
+        private SemanticsUtils semanticsUtils;
+
+        @Inject
+        private IScopeProvider scopeProvider;
+
+        @Inject
+        private ProblemDesugarer desugarer;
+
+        private ProblemTrace trace;
+        private Model model;
+        private ReasoningAdapter reasoningAdapter;
+        private PartialInterpretation<TruthValue, Boolean> existsInterpretation;
+        private Problem problem;
+        private final MutableIntObjectMap<Node> nodes = IntObjectMaps.mutable.empty();
+
+        @Inject
+        public void setFileExtensionProvider(FileExtensionProvider fileExtensionProvider) {
+                this.fileExtension = fileExtensionProvider.getPrimaryFileExtension();
+        }
+
+        public Problem serializeSolution(ProblemTrace trace, Model model) {
+                var uri = URI.createFileURI("__synthetic" + fileExtension);
+                return serializeSolution(trace, model, uri);
+        }
+
+        public Problem serializeSolution(ProblemTrace trace, Model model, URI uri) {
+                this.trace = trace;
+                this.model = model;
+                reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                existsInterpretation = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE,
+                                ReasoningAdapter.EXISTS_SYMBOL);
+                var originalProblem = trace.getProblem();
+                problem = copyProblem(originalProblem, uri);
+                problem.getStatements().removeIf(SolutionSerializer::shouldRemoveStatement);
+                problem.getNodes().removeIf(this::shouldRemoveNode);
+                addExistsAssertions();
+                addClassAssertions();
+                addReferenceAssertions();
+                return problem;
+        }
+
+        private static boolean shouldRemoveStatement(Statement statement) {
+                return statement instanceof Assertion || statement instanceof ScopeDeclaration;
+        }
+
+        private boolean shouldRemoveNode(Node newNode) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(newNode);
+                var scope = scopeProvider.getScope(trace.getProblem(), ProblemPackage.Literals.ASSERTION__RELATION);
+                var originalNode = semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class);
+                if (originalNode == null) {
+                        return false;
+                }
+                int nodeId = trace.getNodeId(originalNode);
+                return !isExistingNode(nodeId);
+        }
+
+        private boolean isExistingNode(int nodeId) {
+                var exists = existsInterpretation.get(Tuple.of(nodeId));
+                if (!exists.isConcrete()) {
+                        throw new IllegalStateException("Invalid EXISTS %s for node %d".formatted(exists, nodeId));
+                }
+                return exists.may();
+        }
+
+        private Problem copyProblem(Problem originalProblem, URI uri) {
+                var newResourceSet = resourceSetProvider.get();
+                if (!fileExtension.equals(uri.fileExtension())) {
+                        uri = uri.appendFileExtension(fileExtension);
+                }
+                var newResource = resourceFactory.createResource(uri);
+                newResourceSet.getResources().add(newResource);
+                var originalResource = originalProblem.eResource();
+                if (originalResource instanceof XtextResource) {
+                        byte[] bytes;
+                        try {
+                                try (var outputStream = new ByteArrayOutputStream()) {
+                                        originalResource.save(outputStream, Map.of());
+                                        bytes = outputStream.toByteArray();
+                                }
+                                try (var inputStream = new ByteArrayInputStream(bytes)) {
+                                        newResource.load(inputStream, Map.of());
+                                }
+                        } catch (IOException e) {
+                                throw new IllegalStateException("Failed to copy problem", e);
+                        }
+                        var contents = newResource.getContents();
+                        if (!contents.isEmpty() && contents.getFirst() instanceof Problem newProblem) {
+                                return newProblem;
+                        }
+                        throw new IllegalStateException("Invalid contents of copied problem");
+                } else {
+                        var newProblem = EcoreUtil.copy(originalProblem);
+                        newResource.getContents().add(newProblem);
+                        return newProblem;
+                }
+        }
+
+        private Relation findRelation(Relation originalRelation) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalRelation);
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
+                return semanticsUtils.getElement(problem, scope, qualifiedName, Relation.class);
+        }
+
+        private Relation findPartialRelation(PartialRelation partialRelation) {
+                return findRelation(trace.getRelation(partialRelation));
+        }
+
+        private Node findNode(Node originalNode) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(originalNode);
+                return findNode(qualifiedName);
+        }
+
+        private Node findNode(String name) {
+                var qualifiedName = qualifiedNameConverter.toQualifiedName(name);
+                return findNode(qualifiedName);
+        }
+
+        private Node findNode(QualifiedName qualifiedName) {
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
+                return semanticsUtils.maybeGetElement(problem, scope, qualifiedName, Node.class);
+        }
+
+        private void addAssertion(Relation relation, LogicValue value, Node... arguments) {
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setRelation(relation);
+                for (var node : arguments) {
+                        var argument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                        argument.setNode(node);
+                        assertion.getArguments().add(argument);
+                }
+                var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant();
+                logicConstant.setLogicValue(value);
+                assertion.setValue(logicConstant);
+                problem.getStatements().add(assertion);
+        }
+
+        private void addExistsAssertions() {
+                var builtinSymbols = desugarer.getBuiltinSymbols(problem)
+                                .orElseThrow(() -> new IllegalStateException("No builtin library in copied problem"));
+                // Make sure to output exists assertions in a deterministic order.
+                var sortedNewNodes = new TreeMap<Integer, Node>();
+                for (var pair : trace.getNodeTrace().keyValuesView()) {
+                        var originalNode = pair.getOne();
+                        int nodeId = pair.getTwo();
+                        var newNode = findNode(originalNode);
+                        // Since all implicit nodes that do not exist has already been remove in serializeSolution,
+                        // we only need to add !exists assertions to ::new nodes (nodes marked as an individual must always exist).
+                        if (ProblemUtil.isNewNode(originalNode)) {
+                                sortedNewNodes.put(nodeId, newNode);
+                        } else {
+                                nodes.put(nodeId, newNode);
+                        }
+                }
+                for (var newNode : sortedNewNodes.values()) {
+                        // If a node is a new node of the class, we should replace it with a normal node.
+                        addAssertion(builtinSymbols.exists(), LogicValue.FALSE, newNode);
+                }
+        }
+
+        private void addClassAssertions() {
+                var types = trace.getMetamodel().typeHierarchy().getPreservedTypes().keySet().stream()
+                                .collect(Collectors.toMap(Function.identity(), this::findPartialRelation));
+                var indexMap = ObjectIntMaps.mutable.empty();
+                var cursor = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL).getAll();
+                while (cursor.move()) {
+                        var key = cursor.getKey();
+                        var nodeId = key.get(0);
+                        if (isExistingNode(nodeId)) {
+                                createNodeAndAssertType(nodeId, cursor.getValue(), types, indexMap);
+                        }
+                }
+        }
+
+        private void createNodeAndAssertType(int nodeId, InferredType inferredType, Map<PartialRelation, Relation> types,
+                                                                                 MutableObjectIntMap<Object> indexMap) {
+                var candidateTypeSymbol = inferredType.candidateType();
+                var candidateRelation = types.get(candidateTypeSymbol);
+                if (candidateRelation instanceof EnumDeclaration) {
+                        // Type assertions for enum literals are added implicitly.
+                        return;
+                }
+                Node node = nodes.get(nodeId);
+                if (node == null) {
+                        String typeName = candidateRelation.getName();
+                        if (typeName == null || typeName.isEmpty()) {
+                                typeName = "node";
+                        } else {
+                                typeName = typeName.substring(0, 1).toLowerCase(Locale.ROOT) + typeName.substring(1);
+                        }
+                        int index = indexMap.getIfAbsent(typeName, 0);
+                        String nodeName;
+                        do {
+                                index++;
+                                nodeName = typeName + index;
+                        } while (findNode(nodeName) != null);
+                        node = ProblemFactory.eINSTANCE.createNode();
+                        node.setName(nodeName);
+                        problem.getNodes().add(node);
+                        nodes.put(nodeId, node);
+                }
+                addAssertion(candidateRelation, LogicValue.TRUE, node);
+                var typeAnalysisResult = trace.getMetamodel().typeHierarchy().getPreservedTypes().get(candidateTypeSymbol);
+                for (var subtype : typeAnalysisResult.getDirectSubtypes()) {
+                        var subtypeRelation = types.get(subtype);
+                        addAssertion(subtypeRelation, LogicValue.FALSE, node);
+                }
+        }
+
+        private void addReferenceAssertions() {
+                var metamodel = trace.getMetamodel();
+                for (var partialRelation : metamodel.containmentHierarchy().keySet()) {
+                        // No need to add a default value, because in a concrete model, each contained node has only a single
+                        // container.
+                        addAssertions(partialRelation);
+                }
+                for (var partialRelation : metamodel.directedCrossReferences().keySet()) {
+                        addDefaultAssertion(partialRelation);
+                        addAssertions(partialRelation);
+                }
+                // No need to add directed opposite references, because their default value is {@code unknown} and their
+                // actual value will always be computed from the value of the directed forward reference.
+                // However, undirected cross-references have to be serialized in both directions due to the default value of
+                // {@code false}.
+                for (var partialRelation : metamodel.undirectedCrossReferences().keySet()) {
+                        addDefaultAssertion(partialRelation);
+                        addAssertions(partialRelation);
+                }
+        }
+
+        private void addAssertions(PartialRelation partialRelation) {
+                var relation = findPartialRelation(partialRelation);
+                var cursor = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialRelation).getAll();
+                // Make sure to output assertions in a deterministic order.
+                var sortedTuples = new TreeSet<Tuple>();
+                while (cursor.move()) {
+                        var tuple = cursor.getKey();
+                        var from = nodes.get(tuple.get(0));
+                        var to = nodes.get(tuple.get(1));
+                        if (from == null || to == null) {
+                                // One of the endpoints does not exist in the candidate model.
+                                continue;
+                        }
+                        var value = cursor.getValue();
+                        if (!value.isConcrete()) {
+                                throw new IllegalStateException("Invalid %s %s for tuple %s".formatted(partialRelation, value, tuple));
+                        }
+                        if (value.may()) {
+                                sortedTuples.add(tuple);
+                        }
+                }
+                for (var tuple : sortedTuples) {
+                        var from = nodes.get(tuple.get(0));
+                        var to = nodes.get(tuple.get(1));
+                        addAssertion(relation, LogicValue.TRUE, from, to);
+                }
+        }
+
+        private void addDefaultAssertion(PartialRelation partialRelation) {
+                var relation = findPartialRelation(partialRelation);
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setDefault(true);
+                assertion.setRelation(relation);
+                int arity = ProblemUtil.getArity(relation);
+                for (int i = 0; i < arity; i++) {
+                        var argument = ProblemFactory.eINSTANCE.createWildcardAssertionArgument();
+                        assertion.getArguments().add(argument);
+                }
+                var logicConstant = ProblemFactory.eINSTANCE.createLogicConstant();
+                logicConstant.setLogicValue(LogicValue.FALSE);
+                assertion.setValue(logicConstant);
+                problem.getStatements().add(assertion);
+        }
+}
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
index c732f784..5d25f148 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTree.java
@@ -40,8 +40,8 @@ class DecisionTree implements MutableSeed<TruthValue> {
         }
 
         @Override
-        public TruthValue reducedValue() {
-                return root.getOtherwiseReducedValue().getTruthValue();
+        public TruthValue majorityValue() {
+                return root.getMajorityValue().getTruthValueOrElse(TruthValue.FALSE);
         }
 
         @Override
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
index ebca2634..31d6fc78 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/DecisionTreeNode.java
@@ -100,6 +100,8 @@ abstract class DecisionTreeNode {
 
         protected abstract LazyIntIterable getChildKeys();
 
+        public abstract DecisionTreeValue getMajorityValue();
+
         protected abstract boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex,
                                                                                           int[] sortedChildren);
 
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
index 0e2f5d18..2ad216ce 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/IntermediateNode.java
@@ -130,6 +130,11 @@ final class IntermediateNode extends DecisionTreeNode {
                 return children.keysView();
         }
 
+        @Override
+        public DecisionTreeValue getMajorityValue() {
+                return otherwise.getMajorityValue();
+        }
+
         protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
                 for (int i = startIndex; i < sortedChildren.length; i++) {
                         var key = sortedChildren[i];
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
index 7a72c656..f100c5a6 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/NullaryMutableSeed.java
@@ -29,14 +29,14 @@ class NullaryMutableSeed implements MutableSeed<TruthValue> {
         }
 
         @Override
-        public TruthValue reducedValue() {
+        public TruthValue majorityValue() {
                 return value.getTruthValue();
         }
 
         @Override
         public TruthValue get(Tuple key) {
                 validateKey(key);
-                return reducedValue();
+                return majorityValue();
         }
 
         private static void validateKey(Tuple key) {
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
index d3dd757c..dc501479 100644
--- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
+++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/internal/TerminalNode.java
@@ -115,7 +115,7 @@ class TerminalNode extends DecisionTreeNode {
 
         @Override
         protected DecisionTreeValue getOtherwiseReducedValue() {
-                return otherwise;
+                return getMajorityValue();
         }
 
         @Override
@@ -124,6 +124,11 @@ class TerminalNode extends DecisionTreeNode {
         }
 
         @Override
+        public DecisionTreeValue getMajorityValue() {
+                return otherwise;
+        }
+
+        @Override
         protected boolean moveNextSparse(int level, DecisionTreeCursor cursor, int startIndex, int[] sortedChildren) {
                 if (startIndex >= sortedChildren.length) {
                         return false;
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java
new file mode 100644
index 00000000..2d759c86
--- /dev/null
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/SolutionSerializerTest.java
@@ -0,0 +1,164 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.semantics;
+
+import com.google.inject.Inject;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.junit.jupiter.api.extension.ExtendWith;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.generator.ModelGeneratorFactory;
+import tools.refinery.generator.ProblemLoader;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.util.Map;
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class SolutionSerializerTest {
+        @Inject
+        ProblemLoader loader;
+
+        @Inject
+        ModelGeneratorFactory generatorFactory;
+
+        @Inject
+        SolutionSerializer serializer;
+
+        @ParameterizedTest
+        @MethodSource
+        void solutionSerializerTest(String prefix, String input, String expectedOutput) throws IOException {
+                var problem = loader.loadString(prefix + "\n" + input);
+                var generator = generatorFactory.createGenerator(problem);
+                generator.generate();
+                var solution = serializer.serializeSolution(generator.getProblemTrace(), generator.getModel());
+                String actualOutput;
+                try (var outputStream = new ByteArrayOutputStream()) {
+                        solution.eResource().save(outputStream, Map.of());
+                        actualOutput = outputStream.toString();
+                }
+                assertThat(actualOutput, is(prefix + "\n" + expectedOutput));
+        }
+
+        static Stream<Arguments> solutionSerializerTest() {
+                return Stream.of(Arguments.of("""
+                                class Foo.
+                                """, """
+                                scope Foo = 3.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(foo1).
+                                Foo(foo2).
+                                Foo(foo3).
+                                """), Arguments.of("""
+                                class Foo {
+                                        contains Bar[2] bars
+                                }
+
+                                class Bar.
+                                """, """
+                                scope Foo = 1.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                Bar(bar1).
+                                Bar(bar2).
+                                bars(foo1, bar1).
+                                bars(foo1, bar2).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Bar[2] bars opposite foo
+                                }
+
+                                class Bar {
+                                        Foo[1] foo opposite bars
+                                }
+                                """, """
+                                scope Foo = 1, Bar = 2.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                Bar(bar1).
+                                Bar(bar2).
+                                default !bars(*, *).
+                                bars(foo1, bar1).
+                                bars(foo1, bar2).
+                                """), Arguments.of("""
+                                class Person {
+                                        Person[2] friend opposite friend
+                                }
+                                """, """
+                                friend(a, b).
+                                friend(a, c).
+                                friend(b, c).
+
+                                scope Person += 0.
+                                """, """
+                                !exists(Person::new).
+                                Person(a).
+                                Person(b).
+                                Person(c).
+                                default !friend(*, *).
+                                friend(a, b).
+                                friend(a, c).
+                                friend(b, a).
+                                friend(b, c).
+                                friend(c, a).
+                                friend(c, b).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Bar bar
+                                }
+
+                                enum Bar {
+                                        BAR_A,
+                                        BAR_B
+                                }
+                                """, """
+                                bar(foo, BAR_A).
+
+                                scope Foo += 0.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(foo).
+                                default !bar(*, *).
+                                bar(foo, BAR_A).
+                                """), Arguments.of("""
+                                class Foo.
+                                class Bar extends Foo.
+                                """, """
+                                scope Foo = 1, Bar = 0.
+                                """, """
+                                !exists(Foo::new).
+                                !exists(Bar::new).
+                                Foo(foo1).
+                                !Bar(foo1).
+                                """), Arguments.of("""
+                                class Foo {
+                                        Foo[] ref
+                                }
+                                """, """
+                                ref(a, b).
+                                !exists(b).
+
+                                scope Foo += 0.
+                                """, """
+                                !exists(Foo::new).
+                                Foo(a).
+                                default !ref(*, *).
+                                """));
+        }
+}
diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
index 2320de2c..61ce850f 100644
--- a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
+++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/internal/DecisionTreeTests.java
@@ -276,6 +276,16 @@ class DecisionTreeTests {
                 assertThat(sut.getReducedValue(), is(TruthValue.TRUE));
         }
 
+        @Test
+        void overwriteWildcardAllTest() {
+                var first = new DecisionTree(2, TruthValue.UNKNOWN);
+                first.mergeValue(Tuple.of(-1, -1), TruthValue.FALSE);
+                var second = new DecisionTree(2, null);
+                second.mergeValue(Tuple.of(1, -1), TruthValue.TRUE);
+                first.overwriteValues(second);
+                assertThat(first.majorityValue(), is(TruthValue.FALSE));
+        }
+
         private Map<Tuple, TruthValue> iterateAll(DecisionTree sut, TruthValue defaultValue, int nodeCount) {
                 var cursor = sut.getCursor(defaultValue, nodeCount);
                 var map = new LinkedHashMap<Tuple, TruthValue>();
diff --git a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
index 0a5cb3c2..00dd3de3 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
@@ -20,6 +20,7 @@ import org.eclipse.xtext.scoping.IGlobalScopeProvider;
 import org.eclipse.xtext.scoping.IScopeProvider;
 import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider;
 import org.eclipse.xtext.serializer.sequencer.ISemanticSequencer;
+import org.eclipse.xtext.serializer.tokens.ICrossReferenceSerializer;
 import org.eclipse.xtext.validation.IDiagnosticConverter;
 import org.eclipse.xtext.validation.IResourceValidator;
 import org.eclipse.xtext.xbase.annotations.validation.DerivedStateAwareResourceValidator;
@@ -34,12 +35,15 @@ import tools.refinery.language.resource.ProblemResourceDescriptionStrategy;
 import tools.refinery.language.scoping.ProblemGlobalScopeProvider;
 import tools.refinery.language.scoping.ProblemLocalScopeProvider;
 import tools.refinery.language.serializer.PreferShortAssertionsProblemSemanticSequencer;
+import tools.refinery.language.serializer.ProblemCrossReferenceSerializer;
 import tools.refinery.language.validation.ProblemDiagnosticConverter;
 
 /**
  * Use this class to register components to be used at runtime / without the
  * Equinox extension registry.
  */
+// Unused methods in this class are called by reflection to configure the Xtext Injector.
+@SuppressWarnings("unused")
 public class ProblemRuntimeModule extends AbstractProblemRuntimeModule {
         @Override
         public Class<? extends IParser> bindIParser() {
@@ -104,6 +108,10 @@ public class ProblemRuntimeModule extends AbstractProblemRuntimeModule {
                 return PreferShortAssertionsProblemSemanticSequencer.class;
         }
 
+        public Class<? extends ICrossReferenceSerializer> bindICrossReferenceSerializer() {
+                return ProblemCrossReferenceSerializer.class;
+        }
+
         public Class<? extends IDiagnosticConverter> bindIDiagnosticConverter() {
                 return ProblemDiagnosticConverter.class;
         }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
index 55a5ac20..0f3bd3ee 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
@@ -69,12 +69,24 @@ public class ProblemFormatter extends AbstractJavaFormatter {
                 doc.prepend(region.keyword("{"), this::oneSpace);
                 doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2));
                 doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2));
+                doc.interior(region.keyword("{"), region.keyword("}"), IHiddenRegionFormatter::indent);
                 doc.prepend(region.keyword("."), this::noSpace);
                 for (var featureDeclaration : classDeclaration.getFeatureDeclarations()) {
                         doc.format(featureDeclaration);
                 }
         }
 
+        protected void format(EnumDeclaration enumDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, enumDeclaration, this::twoNewLines);
+                var region = regionFor(enumDeclaration);
+                doc.append(region.keyword("enum"), this::oneSpace);
+                doc.prepend(region.keyword("{"), this::oneSpace);
+                doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2));
+                doc.interior(region.keyword("{"), region.keyword("}"), IHiddenRegionFormatter::indent);
+                doc.prepend(region.keyword("."), this::noSpace);
+        }
+
         protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) {
                 surroundNewLines(doc, predicateDefinition, this::twoNewLines);
                 var region = regionFor(predicateDefinition);
@@ -151,14 +163,14 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         }
 
         protected void surroundNewLines(IFormattableDocument doc, EObject eObject,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                        Procedure1<? super IHiddenRegionFormatter> init) {
                 var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject);
                 preprendNewLines(doc, region, init);
                 appendNewLines(doc, region, init);
         }
 
         protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                        Procedure1<? super IHiddenRegionFormatter> init) {
                 if (region == null) {
                         return;
                 }
@@ -174,7 +186,7 @@ public class ProblemFormatter extends AbstractJavaFormatter {
         }
 
         protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region,
-                        Procedure1<? super IHiddenRegionFormatter> init) {
+                                                                  Procedure1<? super IHiddenRegionFormatter> init) {
                 if (region == null) {
                         return;
                 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
index b9cafbc2..3432b2d8 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/serializer/PreferShortAssertionsProblemSemanticSequencer.java
@@ -21,8 +21,7 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant
 
         @Override
         protected void sequence_Assertion(ISerializationContext context, Assertion semanticObject) {
-                if (semanticObject.isDefault() ||
-                                !(semanticObject.getValue() instanceof LogicConstant logicConstant) ||
+                if (!(semanticObject.getValue() instanceof LogicConstant logicConstant) ||
                                 logicConstant.getLogicValue() == LogicValue.ERROR) {
                         super.sequence_Assertion(context, semanticObject);
                         return;
@@ -39,6 +38,9 @@ public class PreferShortAssertionsProblemSemanticSequencer extends ProblemSemant
                 }
                 var feeder = createSequencerFeeder(context, semanticObject);
                 var access = grammarAccess.getAssertionAccess();
+                if (semanticObject.isDefault()) {
+                        feeder.accept(access.getDefaultDefaultKeyword_0_0());
+                }
                 feeder.accept(access.getValueShortLogicConstantParserRuleCall_1_1_0_0(), logicConstant);
                 feeder.accept(access.getRelationRelationQualifiedNameParserRuleCall_1_1_1_0_1(), semanticObject.getRelation());
                 var iterator = semanticObject.getArguments().iterator();
diff --git a/subprojects/language/src/main/java/tools/refinery/language/serializer/ProblemCrossReferenceSerializer.java b/subprojects/language/src/main/java/tools/refinery/language/serializer/ProblemCrossReferenceSerializer.java
new file mode 100644
index 00000000..42950e61
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/serializer/ProblemCrossReferenceSerializer.java
@@ -0,0 +1,167 @@
+/*******************************************************************************
+ * Copyright (c) 2008, 2018 itemis AG (http://www.itemis.eu) and others.
+ * Copyright (c) 2023 The Refinery Authors <https://refinery.tools/>
+ * This program and the accompanying materials are made available under the
+ * terms of the Eclipse Public License 2.0 which is available at
+ * http://www.eclipse.org/legal/epl-2.0.
+ * SPDX-License-Identifier: EPL-2.0
+ *******************************************************************************/
+package tools.refinery.language.serializer;
+
+import com.google.common.collect.Lists;
+import com.google.inject.Inject;
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+import org.eclipse.xtext.CrossReference;
+import org.eclipse.xtext.EcoreUtil2;
+import org.eclipse.xtext.GrammarUtil;
+import org.eclipse.xtext.IGrammarAccess;
+import org.eclipse.xtext.conversion.IValueConverterService;
+import org.eclipse.xtext.conversion.ValueConverterException;
+import org.eclipse.xtext.linking.impl.LinkingHelper;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
+import org.eclipse.xtext.naming.QualifiedName;
+import org.eclipse.xtext.nodemodel.INode;
+import org.eclipse.xtext.scoping.IScope;
+import org.eclipse.xtext.scoping.IScopeProvider;
+import org.eclipse.xtext.serializer.diagnostic.ISerializationDiagnostic;
+import org.eclipse.xtext.serializer.diagnostic.SerializationDiagnostic;
+import org.eclipse.xtext.serializer.tokens.CrossReferenceSerializer;
+import org.eclipse.xtext.serializer.tokens.SerializerScopeProviderBinding;
+import org.eclipse.xtext.util.EmfFormatter;
+
+import java.util.List;
+
+public class ProblemCrossReferenceSerializer extends CrossReferenceSerializer {
+        public static final String AMBIGUOUS_REFERENCE_DIAGNOSTIC = "tools.refinery.language.serializer" +
+                        ".ProblemCrossReferenceSerializer.AMBIGUOUS_REFERENCE";
+
+        @Inject
+        private LinkingHelper linkingHelper;
+
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        @Inject
+        @SerializerScopeProviderBinding
+        private IScopeProvider scopeProvider;
+
+        @Inject
+        private IValueConverterService valueConverter;
+
+        @Inject
+        private IGrammarAccess grammarAccess;
+
+        @Override
+        public String serializeCrossRef(EObject semanticObject, CrossReference crossref, EObject target, INode node,
+                                                                        ISerializationDiagnostic.Acceptor errors) {
+                if ((target == null || target.eIsProxy()) && node != null) {
+                        return tokenUtil.serializeNode(node);
+                }
+
+                final EReference ref = GrammarUtil.getReference(crossref, semanticObject.eClass());
+                final IScope scope = scopeProvider.getScope(semanticObject, ref);
+                if (scope == null) {
+                        if (errors != null) {
+                                errors.accept(diagnostics.getNoScopeFoundDiagnostic(semanticObject, crossref, target));
+                        }
+                        return null;
+                }
+
+                if (target != null && target.eIsProxy()) {
+                        target = handleProxy(target, semanticObject, ref);
+                }
+
+                if (target != null && node != null) {
+                        String text = linkingHelper.getCrossRefNodeAsString(node, true);
+                        QualifiedName qualifiedName = qualifiedNameConverter.toQualifiedName(text);
+                        URI targetUri = EcoreUtil2.getPlatformResourceOrNormalizedURI(target);
+                        if (isUniqueInScope(scope, qualifiedName, targetUri)) {
+                                return tokenUtil.serializeNode(node);
+                        }
+                }
+
+                return getCrossReferenceNameFromScope(semanticObject, crossref, target, scope, errors);
+        }
+
+        private boolean isUniqueInScope(IScope scope, QualifiedName qualifiedName, URI targetUri) {
+                var iterator = scope.getElements(qualifiedName).iterator();
+                if (!iterator.hasNext()) {
+                        return false;
+                }
+                var description = iterator.next();
+                return targetUri.equals(description.getEObjectURI()) && !iterator.hasNext();
+        }
+
+        @Override
+        protected String getCrossReferenceNameFromScope(EObject semanticObject, CrossReference crossref, EObject target,
+                                                                                                        IScope scope, ISerializationDiagnostic.Acceptor errors) {
+                var ruleName = linkingHelper.getRuleNameFrom(crossref);
+                var targetUri = EcoreUtil2.getPlatformResourceOrNormalizedURI(target);
+                FoundName foundName = FoundName.NONE;
+                int shortestNameLength = Integer.MAX_VALUE;
+                String shortestName = null;
+                List<ISerializationDiagnostic> recordedErrors = null;
+                for (var description : scope.getElements(target)) {
+                        var qualifiedName = description.getName();
+                        var segmentCount = qualifiedName.getSegmentCount();
+                        if (shortestName != null && segmentCount >= shortestNameLength) {
+                                continue;
+                        }
+                        if (isUniqueInScope(scope, qualifiedName, targetUri)) {
+                                var unconverted = qualifiedNameConverter.toString(qualifiedName);
+                                try {
+                                        shortestName = valueConverter.toString(unconverted, ruleName);
+                                        shortestNameLength = segmentCount;
+                                        foundName = FoundName.VALID;
+                                } catch (ValueConverterException e) {
+                                        if (recordedErrors == null) {
+                                                recordedErrors = Lists.newArrayList();
+                                        }
+                                        recordedErrors.add(diagnostics.getValueConversionExceptionDiagnostic(semanticObject, crossref,
+                                                        unconverted, e));
+                                }
+                        } else if (foundName == FoundName.NONE) {
+                                foundName = FoundName.AMBIGUOUS;
+                        }
+                }
+                handleErrors(semanticObject, crossref, target, scope, errors, recordedErrors, foundName);
+                return shortestName;
+        }
+
+        private void handleErrors(
+                        EObject semanticObject, CrossReference crossref, EObject target, IScope scope,
+                        ISerializationDiagnostic.Acceptor errors, List<ISerializationDiagnostic> recordedErrors,
+                        FoundName foundName) {
+                if (errors == null) {
+                        return;
+                }
+                if (recordedErrors != null) {
+                        recordedErrors.forEach(errors::accept);
+                }
+                if (foundName == FoundName.NONE) {
+                        errors.accept(diagnostics.getNoEObjectDescriptionFoundDiagnostic(semanticObject, crossref, target,
+                                        scope));
+                } else if (foundName == FoundName.AMBIGUOUS) {
+                        // Computation of reference name copied from
+                        // {@link org.eclipse.xtext.serializer.diagnostic.TokenDiagnosticProvider#getFullReferenceName}.
+                        var ref = GrammarUtil.getReference(crossref);
+                        var clazz = semanticObject.eClass().getName();
+                        if (ref.getEContainingClass() != semanticObject.eClass()) {
+                clazz = ref.getEContainingClass().getName() + "(" + clazz + ")";
+            }
+                        var message = "No unambiguous name could be found in scope %s.%s for %s"
+                                        .formatted(clazz, ref.getName(), EmfFormatter.objPath(target));
+                        var diagnostic = new SerializationDiagnostic(AMBIGUOUS_REFERENCE_DIAGNOSTIC, semanticObject, crossref,
+                                        grammarAccess.getGrammar(), message);
+                        errors.accept(diagnostic);
+                }
+        }
+
+        private enum FoundName {
+                NONE,
+                AMBIGUOUS,
+                VALID
+        }
+}
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
index 9f4f2bbf..65675b6b 100644
--- a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
+++ b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
@@ -74,8 +74,8 @@ class ProblemSerializerTest {
         }
 
         @ParameterizedTest
-        @MethodSource
-        void defaultAssertionTest(LogicValue value, String valueAsString) {
+        @MethodSource("assertionTest")
+        void defaultAssertionTest(LogicValue value, String serializedAssertion) {
                 var pred = createPred();
                 var node = ProblemFactory.eINSTANCE.createNode();
                 node.setName("a");
@@ -88,12 +88,7 @@ class ProblemSerializerTest {
                                 pred foo(node p).
 
                                 indiv a.
-                                default foo(a):\040""" + valueAsString + ".\n");
-        }
-
-        static Stream<Arguments> defaultAssertionTest() {
-                return Stream.of(Arguments.of(LogicValue.TRUE, "true"), Arguments.of(LogicValue.FALSE, "false"),
-                                Arguments.of(LogicValue.UNKNOWN, "unknown"), Arguments.of(LogicValue.ERROR, "error"));
+                                default\040""" + serializedAssertion + "\n");
         }
 
         @Test
@@ -161,6 +156,7 @@ class ProblemSerializerTest {
                 problem.getStatements().add(assertion);
         }
 
+
         @Test
         void implicitVariableTest() {
                 var pred = ProblemFactory.eINSTANCE.createPredicateDefinition();
@@ -232,20 +228,77 @@ class ProblemSerializerTest {
                                 """);
         }
 
+        @Test
+        void unambiguousNameTest() {
+                createClassAndAssertion("Foo", "foo");
+
+                assertSerializedResult("""
+                                class Foo {
+                                        Foo ref
+                                }
+
+                                ref(foo, foo).
+                                """);
+        }
+
+        @Test
+        void ambiguousNameTest() {
+                createClassAndAssertion("Foo", "foo");
+                createClassAndAssertion("Bar", "bar");
+
+                assertSerializedResult("""
+                                class Foo {
+                                        Foo ref
+                                }
+
+                                Foo::ref(foo, foo).
+
+                                class Bar {
+                                        Bar ref
+                                }
+
+                                Bar::ref(bar, bar).
+                                """);
+        }
+
+        private void createClassAndAssertion(String className, String nodeName) {
+                var classDeclaration = ProblemFactory.eINSTANCE.createClassDeclaration();
+                classDeclaration.setName(className);
+                var referenceDeclaration = ProblemFactory.eINSTANCE.createReferenceDeclaration();
+                referenceDeclaration.setReferenceType(classDeclaration);
+                referenceDeclaration.setName("ref");
+                classDeclaration.getFeatureDeclarations().add(referenceDeclaration);
+                problem.getStatements().add(classDeclaration);
+                var node = ProblemFactory.eINSTANCE.createNode();
+                node.setName(nodeName);
+                problem.getNodes().add(node);
+                createBinaryAssertion(referenceDeclaration, node, node);
+        }
+
+        private void createBinaryAssertion(Relation relation, Node from, Node to) {
+                var assertion = ProblemFactory.eINSTANCE.createAssertion();
+                assertion.setRelation(relation);
+                var fromArgument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                fromArgument.setNode(from);
+                assertion.getArguments().add(fromArgument);
+                var toArgument = ProblemFactory.eINSTANCE.createNodeAssertionArgument();
+                toArgument.setNode(to);
+                assertion.getArguments().add(toArgument);
+                var value = ProblemFactory.eINSTANCE.createLogicConstant();
+                value.setLogicValue(LogicValue.TRUE);
+                assertion.setValue(value);
+                problem.getStatements().add(assertion);
+        }
+
         private void assertSerializedResult(String expected) {
-                var outputStream = new ByteArrayOutputStream();
-                try {
+                String problemString;
+                try (var outputStream = new ByteArrayOutputStream()) {
                         resource.save(outputStream, Map.of());
+                        problemString = outputStream.toString();
                 } catch (IOException e) {
                         throw new AssertionError("Failed to serialize problem", e);
-                } finally {
-                        try {
-                                outputStream.close();
-                        } catch (IOException e) {
-                                // Nothing to handle in a test.
-                        }
                 }
-                var problemString = outputStream.toString();
+                // Nothing to handle in a test.
 
                 assertThat(problemString.replace("\r\n", "\n"), equalTo(expected.replace("\r\n", "\n")));
         }
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 ce3efb21..22f38ca9 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
@@ -10,10 +10,10 @@ import tools.refinery.store.model.Model;
 import java.util.Random;
 
 public class BestFirstExplorer extends BestFirstWorker {
-        final int id;
+        final long id;
         Random random;
 
-        public BestFirstExplorer(BestFirstStoreManager storeManager, Model model, int id) {
+        public BestFirstExplorer(BestFirstStoreManager storeManager, Model model, long id) {
                 super(storeManager, model);
                 this.id = id;
                 // The use of a non-cryptographic random generator is safe here, because we only use it to direct the state
diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
index 3d32f84c..c20ab9a0 100644
--- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
+++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstStoreManager.java
@@ -79,7 +79,7 @@ public class BestFirstStoreManager {
                 startExploration(initial, 1);
         }
 
-        public void startExploration(Version initial, int randomSeed) {
+        public void startExploration(Version initial, long randomSeed) {
                 BestFirstExplorer bestFirstExplorer = new BestFirstExplorer(this, modelStore.createModelForState(initial),
                                 randomSeed);
                 bestFirstExplorer.explore();
diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
index a2c56a6b..5ee97ce1 100644
--- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
+++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/PredicateScopeTest.java
@@ -27,7 +27,6 @@ import tools.refinery.store.reasoning.translator.containment.ContainmentHierarch
 import tools.refinery.store.reasoning.translator.metamodel.Metamodel;
 import tools.refinery.store.reasoning.translator.metamodel.MetamodelTranslator;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
-import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.representation.cardinality.CardinalityIntervals;
 import tools.refinery.store.statecoding.StateCoderAdapter;
@@ -109,10 +108,16 @@ class PredicateScopeTest {
         private ModelStore createStore() {
                 var metamodel = Metamodel.builder()
                                 .type(index)
-                                .reference(next, index, false,
-                                                ConstrainedMultiplicity.of(CardinalityIntervals.LONE, nextInvalidMultiplicity), index, prev)
-                                .reference(prev, index, false,
-                                                ConstrainedMultiplicity.of(CardinalityIntervals.LONE, prevInvalidMultiplicity), index, next)
+                                .reference(next, builder -> builder
+                                                .source(index)
+                                                .target(index)
+                                                .multiplicity(CardinalityIntervals.LONE, nextInvalidMultiplicity)
+                                                .opposite(prev))
+                                .reference(prev, builder -> builder
+                                                .source(index)
+                                                .target(index)
+                                                .multiplicity(CardinalityIntervals.LONE, prevInvalidMultiplicity)
+                                                .opposite(next))
                                 .build();
                 return ModelStore.builder()
                                 .with(QueryInterpreterAdapter.builder())
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
index 8b1c3bb3..3b78db02 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/MapBasedSeed.java
@@ -12,19 +12,19 @@ import tools.refinery.store.tuple.Tuple;
 import java.util.Map;
 import java.util.Objects;
 
-record MapBasedSeed<T>(int arity, Class<T> valueType, T reducedValue, Map<Tuple, T> map) implements Seed<T> {
+record MapBasedSeed<T>(int arity, Class<T> valueType, T majorityValue, Map<Tuple, T> map) implements Seed<T> {
         @Override
         public T get(Tuple key) {
                 var value = map.get(key);
-                return value == null ? reducedValue : value;
+                return value == null ? majorityValue : value;
         }
 
         @Override
         public Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount) {
-                if (Objects.equals(defaultValue, reducedValue)) {
+                if (Objects.equals(defaultValue, majorityValue)) {
                         return Cursors.of(map);
                 }
-                return new CartesianProductCursor<>(arity, nodeCount, reducedValue, defaultValue, map);
+                return new CartesianProductCursor<>(arity, nodeCount, majorityValue, defaultValue, map);
         }
 
         private static class CartesianProductCursor<T> implements Cursor<Tuple, T> {
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
index 732efbcc..d9bad866 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/seed/Seed.java
@@ -19,7 +19,7 @@ public interface Seed<T> {
 
         Class<T> valueType();
 
-        T reducedValue();
+        T majorityValue();
 
         T get(Tuple key);
 
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java
index d8c6a5ea..7241b032 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java
@@ -7,9 +7,11 @@ package tools.refinery.store.reasoning.translator.crossreference;
 
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.representation.TruthValue;
 
 public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity,
-                                                                                 PartialRelation targetType, Multiplicity targetMultiplicity) {
+                                                                                 PartialRelation targetType, Multiplicity targetMultiplicity,
+                                                                                 TruthValue defaultValue) {
         public boolean isConstrained() {
                 return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained();
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java
new file mode 100644
index 00000000..9347e91e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInitializer.java
@@ -0,0 +1,52 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+class DirectedCrossReferenceInitializer implements PartialModelInitializer {
+        private final PartialRelation linkType;
+        private final PartialRelation sourceType;
+        private final PartialRelation targetType;
+        private final Symbol<TruthValue> symbol;
+
+        public DirectedCrossReferenceInitializer(PartialRelation linkType, PartialRelation sourceType,
+                                                                                         PartialRelation targetType, Symbol<TruthValue> symbol) {
+                this.linkType = linkType;
+                this.sourceType = sourceType;
+                this.targetType = targetType;
+                this.symbol = symbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                var sourceRefiner = reasoningAdapter.getRefiner(sourceType);
+                var targetRefiner = reasoningAdapter.getRefiner(targetType);
+                var interpretation = model.getInterpretation(symbol);
+                var cursor = modelSeed.getCursor(linkType, symbol.defaultValue());
+                while (cursor.move()) {
+                        var key = cursor.getKey();
+                        var value = cursor.getValue();
+                        interpretation.put(key, value);
+                        if (value.must()) {
+                                boolean merged = sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
+                                                targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                                if (!merged) {
+                                        throw new IllegalArgumentException("Failed to merge end types of reference %s for key %s"
+                                                        .formatted(linkType, key));
+                                }
+                        }
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
index 9028337c..fc7477f1 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.translator.crossreference;
 
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
@@ -14,9 +15,9 @@ import tools.refinery.store.query.view.ForbiddenView;
 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.RefinementBasedInitializer;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
 import tools.refinery.store.representation.Symbol;
@@ -24,6 +25,7 @@ import tools.refinery.store.representation.TruthValue;
 
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
+import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
 import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
 import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
 
@@ -35,7 +37,7 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
         public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) {
                 this.linkType = linkType;
                 this.info = info;
-                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN);
+                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, info.defaultValue());
         }
 
         @Override
@@ -45,41 +47,77 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration
                 var targetType = info.targetType();
                 var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false);
                 var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true);
-                var forbiddenView = new ForbiddenView(symbol);
                 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
 
-                storeBuilder.with(PartialRelationTranslator.of(linkType)
-                                .symbol(symbol)
-                                .may(Query.of(mayName, (builder, source, target) -> {
+                var defaultValue = info.defaultValue();
+                if (defaultValue.must()) {
+                        throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s"
+                                        .formatted(defaultValue, linkType));
+                }
+
+                var translator = PartialRelationTranslator.of(linkType);
+                translator.symbol(symbol);
+                if (defaultValue.may()) {
+                        var forbiddenView = new ForbiddenView(symbol);
+                        translator.may(Query.of(mayName, (builder, source, target) -> {
+                                builder.clause(
+                                                mayNewSource.call(source),
+                                                mayNewTarget.call(target),
+                                                not(forbiddenView.call(source, target))
+                                );
+                                if (info.isConstrained()) {
+                                        // Violation of monotonicity:
+                                        // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                        // corresponding error pattern will already mark the node as invalid.
+                                        builder.clause(
+                                                        must(linkType.call(source, target)),
+                                                        not(forbiddenView.call(source, target)),
+                                                        may(sourceType.call(source)),
+                                                        may(targetType.call(target))
+                                        );
+                                }
+                        }));
+                } else {
+                        var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
+                        propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(may(sourceType.call(p1)))
+                                );
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(may(targetType.call(p2)))
+                                );
+                                if (info.isConstrained()) {
+                                        builder.clause(
+                                                        may(linkType.call(p1, p2)),
+                                                        not(must(linkType.call(p1, p2))),
+                                                        not(mayNewSource.call(p1))
+                                        );
                                         builder.clause(
-                                                        mayNewSource.call(source),
-                                                        mayNewTarget.call(target),
-                                                        not(forbiddenView.call(source, target))
+                                                        may(linkType.call(p1, p2)),
+                                                        not(must(linkType.call(p1, p2))),
+                                                        not(mayNewTarget.call(p2))
                                         );
-                                        if (info.isConstrained()) {
-                                                // Violation of monotonicity:
-                                                // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
-                                                // corresponding error pattern will already mark the node as invalid.
-                                                builder.clause(
-                                                                must(linkType.call(source, target)),
-                                                                not(forbiddenView.call(source, target)),
-                                                                may(sourceType.call(source)),
-                                                                may(targetType.call(target))
-                                                );
-                                        }
-                                }))
-                                .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType))
-                                .initializer(new RefinementBasedInitializer<>(linkType))
-                                .decision(Rule.of(linkType.name(), (builder, source, target) -> builder
-                                                .clause(
-                                                                may(linkType.call(source, target)),
-                                                                not(candidateMust(linkType.call(source, target))),
-                                                                not(MULTI_VIEW.call(source)),
-                                                                not(MULTI_VIEW.call(target))
-                                                )
-                                                .action(
-                                                                add(linkType, source, target)
-                                                ))));
+                                }
+                                builder.action(
+                                                merge(linkType, TruthValue.FALSE, p1, p2)
+                                );
+                        }));
+                }
+                translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType));
+                translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol));
+                translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder
+                                .clause(
+                                                may(linkType.call(source, target)),
+                                                not(candidateMust(linkType.call(source, target))),
+                                                not(MULTI_VIEW.call(source)),
+                                                not(MULTI_VIEW.call(target))
+                                )
+                                .action(
+                                                add(linkType, source, target)
+                                )));
+                storeBuilder.with(translator);
 
                 storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false,
                                 info.sourceMultiplicity()));
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java
index fe99bc54..34e9032a 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java
@@ -7,8 +7,9 @@ package tools.refinery.store.reasoning.translator.crossreference;
 
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.representation.TruthValue;
 
-public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity) {
+public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue) {
         public boolean isConstrained() {
                 return multiplicity.isConstrained();
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java
new file mode 100644
index 00000000..77339aa0
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInitializer.java
@@ -0,0 +1,84 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.reasoning.translator.TranslationException;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.LinkedHashMap;
+
+class UndirectedCrossReferenceInitializer implements PartialModelInitializer {
+        private final PartialRelation linkType;
+        private final PartialRelation sourceType;
+        private final Symbol<TruthValue> symbol;
+
+        UndirectedCrossReferenceInitializer(PartialRelation linkType, PartialRelation sourceType,
+                                                                                Symbol<TruthValue> symbol) {
+                this.linkType = linkType;
+                this.sourceType = sourceType;
+                this.symbol = symbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                var mergedMap = getMergedMap(modelSeed);
+                var sourceRefiner = reasoningAdapter.getRefiner(sourceType);
+                var interpretation = model.getInterpretation(symbol);
+                for (var entry : mergedMap.entrySet()) {
+                        var key = entry.getKey();
+                        var value = entry.getValue();
+                        interpretation.put(key, value);
+                        if (value.must()) {
+                                boolean merged = sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
+                                                sourceRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                                if (!merged) {
+                                        throw new IllegalArgumentException("Failed to merge end types of reference %s for key %s"
+                                                        .formatted(linkType, key));
+                                }
+                        }
+                }
+        }
+
+        @NotNull
+        private LinkedHashMap<Tuple, TruthValue> getMergedMap(ModelSeed modelSeed) {
+                var defaultValue = symbol.defaultValue();
+                var originalMap = new LinkedHashMap<Tuple, TruthValue>();
+                var cursor = modelSeed.getCursor(linkType, defaultValue);
+                while (cursor.move()) {
+                        if (originalMap.put(cursor.getKey(), cursor.getValue()) != null) {
+                                throw new TranslationException(linkType, "Duplicate value for key " + cursor.getKey());
+                        }
+                }
+                var mergedMap = LinkedHashMap.<Tuple, TruthValue>newLinkedHashMap(originalMap.size());
+                for (var entry : originalMap.entrySet()) {
+                        var key = entry.getKey();
+                        var value = entry.getValue();
+                        int first = key.get(0);
+                        int second = key.get(1);
+                        var oppositeKey = Tuple.of(second, first);
+                        var oppositeValue = originalMap.get(oppositeKey);
+                        if (oppositeValue != null && second < first) {
+                                // Already processed entry.
+                                continue;
+                        }
+                        var mergedValue = value.merge(oppositeValue == null ? defaultValue : oppositeValue);
+                        mergedMap.put(key, mergedValue);
+                        if (first != second) {
+                                mergedMap.put(oppositeKey, mergedValue);
+                        }
+                }
+                return mergedMap;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
index c554e2a4..b76838b3 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
@@ -5,6 +5,7 @@
  */
 package tools.refinery.store.reasoning.translator.crossreference;
 
+import tools.refinery.store.dse.propagation.PropagationBuilder;
 import tools.refinery.store.dse.transition.Rule;
 import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.model.ModelStoreConfiguration;
@@ -13,15 +14,16 @@ import tools.refinery.store.query.view.ForbiddenView;
 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.RefinementBasedInitializer;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.TranslationException;
 import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
 import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.representation.TruthValue;
 
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add;
+import static tools.refinery.store.reasoning.actions.PartialActionLiterals.merge;
 import static tools.refinery.store.reasoning.literal.PartialLiterals.*;
 import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW;
 
@@ -33,50 +35,77 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati
         public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) {
                 this.linkType = linkType;
                 this.info = info;
-                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN);
+                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, info.defaultValue());
         }
 
         @Override
         public void apply(ModelStoreBuilder storeBuilder) {
                 var name = linkType.name();
                 var type = info.type();
-                var forbiddenView = new ForbiddenView(symbol);
                 var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
 
+                var defaultValue = info.defaultValue();
+                if (defaultValue.must()) {
+                        throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s"
+                                        .formatted(defaultValue, linkType));
+                }
+
                 var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false);
 
-                storeBuilder.with(PartialRelationTranslator.of(linkType)
-                                .symbol(symbol)
-                                .may(Query.of(mayName, (builder, source, target) -> {
+                var translator = PartialRelationTranslator.of(linkType);
+                translator.symbol(symbol);
+                if (defaultValue.may()) {
+                        var forbiddenView = new ForbiddenView(symbol);
+                        translator.may(Query.of(mayName, (builder, source, target) -> {
+                                builder.clause(
+                                                mayNewSource.call(source),
+                                                mayNewSource.call(target),
+                                                not(forbiddenView.call(source, target))
+                                );
+                                if (info.isConstrained()) {
+                                        // Violation of monotonicity:
+                                        // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                        // corresponding error pattern will already mark the node as invalid.
+                                        builder.clause(
+                                                        must(linkType.call(source, target)),
+                                                        not(forbiddenView.call(source, target)),
+                                                        may(type.call(source)),
+                                                        may(type.call(target))
+                                        );
+                                }
+                        }));
+                } else {
+                        var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class);
+                        propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> {
+                                builder.clause(
+                                                may(linkType.call(p1, p2)),
+                                                not(may(type.call(p1)))
+                                );
+                                if (info.isConstrained()) {
                                         builder.clause(
-                                                        mayNewSource.call(source),
-                                                        mayNewSource.call(target),
-                                                        not(forbiddenView.call(source, target))
+                                                        may(linkType.call(p1, p2)),
+                                                        not(must(linkType.call(p1, p2))),
+                                                        not(mayNewSource.call(p1))
                                         );
-                                        if (info.isConstrained()) {
-                                                // Violation of monotonicity:
-                                                // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
-                                                // corresponding error pattern will already mark the node as invalid.
-                                                builder.clause(
-                                                                must(linkType.call(source, target)),
-                                                                not(forbiddenView.call(source, target)),
-                                                                may(type.call(source)),
-                                                                may(type.call(target))
-                                                );
-                                        }
-                                }))
-                                .refiner(UndirectedCrossReferenceRefiner.of(symbol, type))
-                                .initializer(new RefinementBasedInitializer<>(linkType))
-                                .decision(Rule.of(linkType.name(), (builder, source, target) -> builder
-                                                .clause(
-                                                                may(linkType.call(source, target)),
-                                                                not(candidateMust(linkType.call(source, target))),
-                                                                not(MULTI_VIEW.call(source)),
-                                                                not(MULTI_VIEW.call(target))
-                                                )
-                                                .action(
-                                                                add(linkType, source, target)
-                                                ))));
+                                }
+                                builder.action(
+                                                merge(linkType, TruthValue.FALSE, p1, p2)
+                                );
+                        }));
+                }
+                translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type));
+                translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol));
+                translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder
+                                .clause(
+                                                may(linkType.call(source, target)),
+                                                not(candidateMust(linkType.call(source, target))),
+                                                not(MULTI_VIEW.call(source)),
+                                                not(MULTI_VIEW.call(target))
+                                )
+                                .action(
+                                                add(linkType, source, target)
+                                )));
+                storeBuilder.with(translator);
 
                 storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity()));
         }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java
index 74022fc6..a5047768 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java
@@ -16,6 +16,7 @@ import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMulti
 import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo;
 
 import java.util.*;
+import java.util.function.Consumer;
 
 public class MetamodelBuilder {
         private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder();
@@ -68,6 +69,12 @@ public class MetamodelBuilder {
                 return this;
         }
 
+        public MetamodelBuilder reference(PartialRelation linkType, Consumer<ReferenceInfoBuilder> callback) {
+                var builder = ReferenceInfo.builder();
+                callback.accept(builder);
+                return reference(linkType, builder.build());
+        }
+
         public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) {
                 if (linkType.arity() != 2) {
                         throw new TranslationException(linkType,
@@ -81,47 +88,6 @@ public class MetamodelBuilder {
                 return this;
         }
 
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
-                                                                          Multiplicity multiplicity, PartialRelation targetType,
-                                                                          PartialRelation opposite) {
-                return reference(linkType, new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite));
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
-                                                                          PartialRelation targetType, PartialRelation opposite) {
-                return reference(linkType, sourceType, false, multiplicity, targetType, opposite);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
-                                                                          boolean containment, PartialRelation targetType, PartialRelation opposite) {
-                return reference(linkType, sourceType, containment, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, PartialRelation targetType,
-                                                                          PartialRelation opposite) {
-                return reference(linkType, sourceType, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
-                                                                          Multiplicity multiplicity, PartialRelation targetType) {
-                return reference(linkType, sourceType, containment, multiplicity, targetType, null);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
-                                                                          PartialRelation targetType) {
-                return reference(linkType, sourceType, multiplicity, targetType, null);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
-                                                                          PartialRelation targetType) {
-                return reference(linkType, sourceType, containment, targetType, null);
-        }
-
-        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
-                                                                          PartialRelation targetType) {
-                return reference(linkType, sourceType, targetType, null);
-        }
-
         public MetamodelBuilder references(Collection<Map.Entry<PartialRelation, ReferenceInfo>> entries) {
                 for (var entry : entries) {
                         reference(entry.getKey(), entry.getValue());
@@ -160,10 +126,12 @@ public class MetamodelBuilder {
                 var targetType = info.targetType();
                 var opposite = info.opposite();
                 Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE;
+                var defaultValue = info.defaultValue();
                 if (opposite != null) {
                         var oppositeInfo = referenceInfoMap.get(opposite);
                         validateOpposite(linkType, info, opposite, oppositeInfo);
                         targetMultiplicity = oppositeInfo.multiplicity();
+                        defaultValue = defaultValue.merge(oppositeInfo.defaultValue());
                         if (oppositeInfo.containment()) {
                                 // Skip processing this reference and process it once we encounter its containment opposite.
                                 return;
@@ -175,7 +143,7 @@ public class MetamodelBuilder {
                                                                         targetType, linkType, sourceType));
                                 }
                                 undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType,
-                                                info.multiplicity()));
+                                                info.multiplicity(), defaultValue));
                                 return;
                         }
                         oppositeReferences.put(opposite, linkType);
@@ -185,7 +153,7 @@ public class MetamodelBuilder {
                         return;
                 }
                 directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(),
-                                targetType, targetMultiplicity));
+                                targetType, targetMultiplicity, defaultValue));
         }
 
         private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info,
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java
index 9a6b4012..9d7fc9c3 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java
@@ -7,7 +7,11 @@ package tools.refinery.store.reasoning.translator.metamodel;
 
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.representation.TruthValue;
 
 public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity,
-                                                        PartialRelation targetType, PartialRelation opposite) {
+                                                        PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue) {
+        public static ReferenceInfoBuilder builder() {
+                return new ReferenceInfoBuilder();
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java
new file mode 100644
index 00000000..43d01503
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java
@@ -0,0 +1,84 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+public final class ReferenceInfoBuilder {
+        private boolean containment;
+        private PartialRelation sourceType;
+        private Multiplicity multiplicity = UnconstrainedMultiplicity.INSTANCE;
+        private PartialRelation targetType;
+        private PartialRelation opposite;
+        private TruthValue defaultValue = TruthValue.UNKNOWN;
+
+        ReferenceInfoBuilder() {
+        }
+
+        public ReferenceInfoBuilder source(@NotNull PartialRelation sourceType) {
+                if (sourceType.arity() != 1) {
+                        throw new IllegalArgumentException("Source type %s must be of arity 1".formatted(sourceType));
+                }
+                this.sourceType = sourceType;
+                return this;
+        }
+
+        public ReferenceInfoBuilder target(@NotNull PartialRelation targetType) {
+                if (targetType.arity() != 1) {
+                        throw new IllegalArgumentException("Target type %s must be of arity 1".formatted(targetType));
+                }
+                this.targetType = targetType;
+                return this;
+        }
+
+        public ReferenceInfoBuilder containment(boolean containment) {
+                this.containment = containment;
+                return this;
+        }
+
+        public ReferenceInfoBuilder multiplicity(@NotNull Multiplicity multiplicity) {
+                this.multiplicity = multiplicity;
+                return this;
+        }
+
+        public ReferenceInfoBuilder multiplicity(@NotNull CardinalityInterval multiplicityInterval,
+                                                                                         @NotNull PartialRelation errorSymbol) {
+                return multiplicity(ConstrainedMultiplicity.of(multiplicityInterval, errorSymbol));
+        }
+
+        public ReferenceInfoBuilder opposite(@Nullable PartialRelation opposite) {
+                if (opposite != null && opposite.arity() != 2) {
+                        throw new IllegalArgumentException("Opposite %s must be of arity 2".formatted(targetType));
+                }
+                this.opposite = opposite;
+                return this;
+        }
+
+        public ReferenceInfoBuilder defaultValue(@NotNull TruthValue defaultValue) {
+                if (defaultValue.must()) {
+                        throw new IllegalArgumentException("Unsupported default value");
+                }
+                this.defaultValue = defaultValue;
+                return this;
+        }
+
+        public ReferenceInfo build() {
+                if (sourceType == null) {
+                        throw new IllegalStateException("Source type is required");
+                }
+                if (targetType == null) {
+                        throw new IllegalStateException("Target type is required");
+                }
+                return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue);
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
index 0f1a1006..ba6ba6da 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilderTest.java
@@ -8,7 +8,6 @@ package tools.refinery.store.reasoning.translator.metamodel;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.TranslationException;
-import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.representation.cardinality.CardinalityIntervals;
 
 import static org.junit.jupiter.api.Assertions.assertThrows;
@@ -24,8 +23,13 @@ class MetamodelBuilderTest {
                 var builder = Metamodel.builder()
                                 .type(university)
                                 .type(course)
-                                .reference(courses, university, course, location)
-                                .reference(location, course, university);
+                                .reference(courses, referenceBuilder -> referenceBuilder
+                                                .source(university)
+                                                .target(course)
+                                                .opposite(location))
+                                .reference(location, referenceBuilder -> referenceBuilder
+                                                .source(course)
+                                                .target(university));
 
                 assertThrows(TranslationException.class, builder::build);
         }
@@ -35,8 +39,14 @@ class MetamodelBuilderTest {
                 var builder = Metamodel.builder()
                                 .type(university)
                                 .type(course)
-                                .reference(courses, university, course, location)
-                                .reference(location, course, course, courses);
+                                .reference(courses, referenceBuilder -> referenceBuilder
+                                                .source(university)
+                                                .target(course)
+                                                .opposite(location))
+                                .reference(location, referenceBuilder -> referenceBuilder
+                                                .source(course)
+                                                .target(course)
+                                                .opposite(courses));
 
                 assertThrows(TranslationException.class, builder::build);
         }
@@ -48,10 +58,16 @@ class MetamodelBuilderTest {
                 var builder = Metamodel.builder()
                                 .type(university)
                                 .type(course)
-                                .reference(courses, university, true, course, location)
-                                .reference(location, course,
-                                                ConstrainedMultiplicity.of(CardinalityIntervals.atLeast(2), invalidMultiplicity),
-                                                university,     courses);
+                                .reference(courses, referenceBuilder -> referenceBuilder
+                                                .containment(true)
+                                                .source(university)
+                                                .target(course)
+                                                .opposite(location))
+                                .reference(location, referenceBuilder -> referenceBuilder
+                                                .source(course)
+                                                .multiplicity(CardinalityIntervals.atLeast(2), invalidMultiplicity)
+                                                .target(university)
+                                                .opposite(courses));
 
                 assertThrows(TranslationException.class, builder::build);
         }
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
index 6c2f55af..88e6a4d7 100644
--- a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTest.java
@@ -16,7 +16,6 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.seed.ModelSeed;
 import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
-import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.representation.cardinality.CardinalityIntervals;
 import tools.refinery.store.tuple.Tuple;
@@ -45,12 +44,23 @@ class MetamodelTest {
                                 .type(teacher, person)
                                 .type(university)
                                 .type(course)
-                                .reference(courses, university, true, course, location)
-                                .reference(location, course, university, courses)
-                                .reference(lecturer, course,
-                                                ConstrainedMultiplicity.of(CardinalityIntervals.ONE, invalidLecturerCount), teacher)
-                                .reference(enrolledStudents, course,
-                                                ConstrainedMultiplicity.of(CardinalityIntervals.SOME, invalidStudentCount), student)
+                                .reference(courses, builder -> builder
+                                                .containment(true)
+                                                .source(university)
+                                                .target(course)
+                                                .opposite(location))
+                                .reference(location, builder -> builder
+                                                .source(course)
+                                                .target(university)
+                                                .opposite(courses))
+                                .reference(lecturer, builder -> builder
+                                                .source(course)
+                                                .multiplicity(CardinalityIntervals.ONE, invalidLecturerCount)
+                                                .target(teacher))
+                                .reference(enrolledStudents, builder -> builder
+                                                .source(course)
+                                                .multiplicity(CardinalityIntervals.SOME, invalidStudentCount)
+                                                .target(student))
                                 .build();
 
                 var seed = ModelSeed.builder(5)
@@ -105,10 +115,12 @@ class MetamodelTest {
                 var metamodel = Metamodel.builder()
                                 .type(university)
                                 .type(course)
-                                .reference(courses, university, true, course)
+                                .reference(courses, builder -> builder
+                                                .containment(true)
+                                                .source(university)
+                                                .target(course))
                                 .build();
 
-
                 var seed = ModelSeed.builder(4)
                                 .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder
                                                 .reducedValue(CardinalityIntervals.ONE)