feat: model semantics facade

6 files changed, 277 insertions, 156 deletions

diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java
new file mode 100644
index 00000000..81bf712a
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+
+public class AbstractRefinery {
+        protected final ProblemTrace problemTrace;
+        protected final ModelStore store;
+        protected final Model model;
+        protected final ReasoningAdapter reasoningAdapter;
+
+        public AbstractRefinery(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
+                this.problemTrace = problemTrace;
+                this.store = store;
+                model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
+                reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+        }
+
+        public ProblemTrace getProblemTrace() {
+                return problemTrace;
+        }
+
+        public ModelStore getModelStore() {
+                return store;
+        }
+
+        public Model getModel() {
+                return model;
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java
new file mode 100644
index 00000000..b60a3890
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java
@@ -0,0 +1,152 @@
+/*
+ * 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 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.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.generator.impl.ProblemTraceImpl;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.semantics.model.ModelInitializer;
+import tools.refinery.store.query.ModelQueryBuilder;
+import tools.refinery.store.query.interpreter.QueryInterpreterAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.util.CancellationToken;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStream;
+import java.util.Collection;
+import java.util.Map;
+
+public abstract class AbstractRefineryBuilder<T> {
+        @Inject
+        private Provider<XtextResourceSet> resourceSetProvider;
+
+        @Inject
+        private IResourceFactory resourceFactory;
+
+        @Inject
+        private IResourceValidator resourceValidator;
+
+        @Inject
+        protected ModelInitializer initializer;
+
+        @Inject
+        private ProblemTraceImpl problemTrace;
+
+        protected CancellationToken cancellationToken = CancellationToken.NONE;
+        private boolean problemLoaded;
+        private ModelQueryBuilder queryEngineBuilder;
+        protected Collection<Concreteness> requiredInterpretations;
+
+        protected AbstractRefineryBuilder(Collection<Concreteness> defaultRequiredInterpretations) {
+                requiredInterpretations = defaultRequiredInterpretations;
+        }
+
+        protected abstract T self();
+
+        public T cancellationToken(CancellationToken cancellationToken) {
+                this.cancellationToken = cancellationToken;
+                return self();
+        }
+
+        public T fromString(String problemString) throws IOException {
+                try (var stream = new LazyStringInputStream(problemString)) {
+                        return fromStream(stream);
+                }
+        }
+
+        public T fromStream(InputStream inputStream) throws IOException {
+                var resourceSet = resourceSetProvider.get();
+                var resource = resourceFactory.createResource(URI.createFileURI("__synthetic.problem"));
+                resourceSet.getResources().add(resource);
+                resource.load(inputStream, Map.of());
+                return fromResource(resource);
+        }
+
+        public T fromFile(File file) throws IOException {
+                return fromFile(file.getAbsolutePath());
+        }
+
+        public T fromFile(String filePath) throws IOException {
+                return fromUri(URI.createFileURI(filePath));
+        }
+
+        public T fromUri(URI uri) throws IOException {
+                var resourceSet = resourceSetProvider.get();
+                var resource = resourceFactory.createResource(uri);
+                resourceSet.getResources().add(resource);
+                resource.load(Map.of());
+                return fromResource(resource);
+        }
+
+        public T fromResource(Resource resource) {
+                var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> {
+                        cancellationToken.checkCancelled();
+                        return Thread.interrupted();
+                });
+                cancellationToken.checkCancelled();
+                var errors = issues.stream()
+                                .filter(issue -> issue.getSeverity() == Severity.ERROR)
+                                .toList();
+                if (!errors.isEmpty()) {
+                        throw new ValidationErrorsException(resource.getURI(), errors);
+                }
+                if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) {
+                        throw new IllegalArgumentException("Model generation problem not found in resource " + resource.getURI());
+                }
+                return problem(problem);
+        }
+
+        public T problem(Problem problem) {
+                if (problemLoaded) {
+                        throw new IllegalStateException("Problem was already set");
+                }
+                initializer.readProblem(problem);
+                problemTrace.setInitializer(initializer);
+                problemLoaded = true;
+                return self();
+        }
+
+        public ProblemTrace getProblemTrace() {
+                checkProblem();
+                return problemTrace;
+        }
+
+        public T queryEngine(ModelQueryBuilder queryEngineBuilder) {
+                if (this.queryEngineBuilder != null) {
+                        throw new IllegalStateException("Query engine was already set");
+                }
+                this.queryEngineBuilder = queryEngineBuilder;
+                return self();
+        }
+
+        public T requiredInterpretations(Collection<Concreteness> requiredInterpretations) {
+                this.requiredInterpretations = requiredInterpretations;
+                return self();
+        }
+
+        protected void checkProblem() {
+                if (!problemLoaded) {
+                        throw new IllegalStateException("Problem was not loaded");
+                }
+        }
+
+        protected ModelQueryBuilder getQueryEngineBuilder() {
+                if (queryEngineBuilder == null) {
+                        return QueryInterpreterAdapter.builder();
+                }
+                return queryEngineBuilder;
+        }
+}
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 4c3e52f3..e5115352 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
@@ -10,10 +10,7 @@ import tools.refinery.language.model.problem.Relation;
 import tools.refinery.store.dse.strategy.BestFirstStoreManager;
 import tools.refinery.store.dse.transition.VersionWithObjectiveValue;
 import tools.refinery.store.map.Version;
-import tools.refinery.store.model.Model;
 import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.reasoning.ReasoningAdapter;
-import tools.refinery.store.reasoning.ReasoningStoreAdapter;
 import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.representation.PartialSymbol;
@@ -22,35 +19,16 @@ import tools.refinery.store.representation.TruthValue;
 
 import java.util.Collection;
 
-public class ModelGenerator {
-        private final ProblemTrace problemTrace;
-        private final ModelStore store;
-        private final Model model;
-        private final ReasoningAdapter reasoningAdapter;
+public class ModelGenerator extends AbstractRefinery {
         private final Version initialVersion;
 
         private int randomSeed = 1;
 
         public ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
-                this.problemTrace = problemTrace;
-                this.store = store;
-                model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed);
-                reasoningAdapter = model.getAdapter(ReasoningAdapter.class);
+                super(problemTrace, store, modelSeed);
                 initialVersion = model.commit();
         }
 
-        public ProblemTrace getProblemTrace() {
-                return problemTrace;
-        }
-
-        public ModelStore getModelStore() {
-                return store;
-        }
-
-        public Model getModel() {
-                return model;
-        }
-
         public int getRandomSeed() {
                 return randomSeed;
         }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java
index 98b6653d..d14cbe3a 100644
--- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java
@@ -5,135 +5,22 @@
  */
 package tools.refinery.generator;
 
-import com.google.inject.Inject;
-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.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.generator.impl.ProblemTraceImpl;
-import tools.refinery.language.model.problem.Problem;
-import tools.refinery.language.semantics.model.ModelInitializer;
 import tools.refinery.store.dse.propagation.PropagationAdapter;
 import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter;
 import tools.refinery.store.model.ModelStore;
-import tools.refinery.store.query.ModelQueryBuilder;
-import tools.refinery.store.query.interpreter.QueryInterpreterAdapter;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.statecoding.StateCoderAdapter;
-import tools.refinery.store.util.CancellationToken;
 
-import java.io.File;
-import java.io.IOException;
-import java.io.InputStream;
-import java.util.Collection;
-import java.util.Map;
 import java.util.Set;
 
-public abstract class ModelGeneratorBuilder {
-        @Inject
-        private Provider<XtextResourceSet> resourceSetProvider;
-
-        @Inject
-        private IResourceFactory resourceFactory;
-
-        @Inject
-        private IResourceValidator resourceValidator;
-
-        @Inject
-        private ModelInitializer initializer;
-
-        @Inject
-        private ProblemTraceImpl problemTrace;
-
-        private CancellationToken cancellationToken = CancellationToken.NONE;
-        private boolean problemLoaded;
-        private ModelQueryBuilder queryEngineBuilder;
-        private Collection<Concreteness> requiredInterpretations = Set.of(Concreteness.CANDIDATE);
-
-        public ModelGeneratorBuilder cancellationToken(CancellationToken cancellationToken) {
-                this.cancellationToken = cancellationToken;
-                return this;
-        }
-
-        public ModelGeneratorBuilder fromString(String problemString) throws IOException {
-                try (var stream = new LazyStringInputStream(problemString)) {
-                        return fromStream(stream);
-                }
-        }
-
-        public ModelGeneratorBuilder fromStream(InputStream inputStream) throws IOException {
-                var resourceSet = resourceSetProvider.get();
-                var resource = resourceFactory.createResource(URI.createFileURI("__synthetic.problem"));
-                resourceSet.getResources().add(resource);
-                resource.load(inputStream, Map.of());
-                return fromResource(resource);
-        }
-
-        public ModelGeneratorBuilder fromFile(File file) throws IOException {
-                return fromFile(file.getAbsolutePath());
-        }
-
-        public ModelGeneratorBuilder fromFile(String filePath) throws IOException {
-                return fromUri(URI.createFileURI(filePath));
-        }
-
-        public ModelGeneratorBuilder fromUri(URI uri) throws IOException {
-                var resourceSet = resourceSetProvider.get();
-                var resource = resourceFactory.createResource(uri);
-                resourceSet.getResources().add(resource);
-                resource.load(Map.of());
-                return fromResource(resource);
-        }
-
-        public ModelGeneratorBuilder fromResource(Resource resource) {
-                var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> {
-                        cancellationToken.checkCancelled();
-                        return Thread.interrupted();
-                });
-                cancellationToken.checkCancelled();
-                var errors = issues.stream()
-                                .filter(issue -> issue.getSeverity() == Severity.ERROR)
-                                .toList();
-                if (!errors.isEmpty()) {
-                        throw new ValidationErrorsException(resource.getURI(), errors);
-                }
-                if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) {
-                        throw new IllegalArgumentException("Model generation problem not found in resource " + resource.getURI());
-                }
-                return problem(problem);
-        }
-
-        public ModelGeneratorBuilder problem(Problem problem) {
-                if (problemLoaded) {
-                        throw new IllegalStateException("Problem was already set");
-                }
-                initializer.readProblem(problem);
-                problemTrace.setInitializer(initializer);
-                problemLoaded = true;
-                return this;
-        }
-
-        public ProblemTrace getProblemTrace() {
-                checkProblem();
-                return problemTrace;
-        }
-
-        public ModelGeneratorBuilder queryEngine(ModelQueryBuilder queryEngineBuilder) {
-                if (this.queryEngineBuilder != null) {
-                        throw new IllegalStateException("Query engine was already set");
-                }
-                this.queryEngineBuilder = queryEngineBuilder;
-                return this;
+public final class ModelGeneratorBuilder extends AbstractRefineryBuilder<ModelGeneratorBuilder> {
+        public ModelGeneratorBuilder() {
+                super(Set.of(Concreteness.CANDIDATE));
         }
 
-        public ModelGeneratorBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) {
-                this.requiredInterpretations = requiredInterpretations;
+        @Override
+        protected ModelGeneratorBuilder self() {
                 return this;
         }
 
@@ -149,19 +36,6 @@ public abstract class ModelGeneratorBuilder {
                                                 .requiredInterpretations(requiredInterpretations));
                 initializer.configureStoreBuilder(storeBuilder);
                 var store = storeBuilder.build();
-                return new ModelGenerator(problemTrace, store, initializer.getModelSeed());
-        }
-
-        private void checkProblem() {
-                if (!problemLoaded) {
-                        throw new IllegalStateException("Problem was not loaded");
-                }
-        }
-
-        private ModelQueryBuilder getQueryEngineBuilder() {
-                if (queryEngineBuilder == null) {
-                        return QueryInterpreterAdapter.builder();
-                }
-                return queryEngineBuilder;
+                return new ModelGenerator(getProblemTrace(), store, initializer.getModelSeed());
         }
 }
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java
new file mode 100644
index 00000000..8bac1910
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java
@@ -0,0 +1,42 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+import org.eclipse.xtext.naming.QualifiedName;
+import tools.refinery.language.model.problem.Relation;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+import tools.refinery.store.representation.TruthValue;
+
+public class ModelSemantics extends AbstractRefinery {
+        public ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) {
+                super(problemTrace, store, modelSeed);
+        }
+
+        public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+                return reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol);
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(Relation relation) {
+                return getPartialInterpretation(problemTrace.getPartialRelation(relation));
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(QualifiedName qualifiedName) {
+                return getPartialInterpretation(problemTrace.getPartialRelation(qualifiedName));
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(String qualifiedName) {
+                return getPartialInterpretation(problemTrace.getPartialRelation(qualifiedName));
+        }
+
+        public static ModelSemanticsBuilder standaloneBuilder() {
+                var injector = StandaloneInjectorHolder.getInjector();
+                return injector.getInstance(ModelSemanticsBuilder.class);
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java
new file mode 100644
index 00000000..a560ebe4
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java
@@ -0,0 +1,37 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+import tools.refinery.store.dse.propagation.PropagationAdapter;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+
+import java.util.Set;
+
+public final class ModelSemanticsBuilder extends AbstractRefineryBuilder<ModelSemanticsBuilder> {
+        public ModelSemanticsBuilder() {
+                super(Set.of(Concreteness.PARTIAL));
+        }
+
+        @Override
+        protected ModelSemanticsBuilder self() {
+                return this;
+        }
+
+        public ModelSemantics build() {
+                checkProblem();
+                var storeBuilder = ModelStore.builder()
+                                .cancellationToken(cancellationToken)
+                                .with(getQueryEngineBuilder())
+                                .with(PropagationAdapter.builder())
+                                .with(ReasoningAdapter.builder()
+                                                .requiredInterpretations(requiredInterpretations));
+                initializer.configureStoreBuilder(storeBuilder);
+                var store = storeBuilder.build();
+                return new ModelSemantics(getProblemTrace(), store, initializer.getModelSeed());
+        }
+}