feat: model generator facade

8 files changed, 498 insertions, 0 deletions

diff --git a/subprojects/generator/build.gradle.kts b/subprojects/generator/build.gradle.kts
new file mode 100644
index 00000000..f1a4ed54
--- /dev/null
+++ b/subprojects/generator/build.gradle.kts
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+        id("tools.refinery.gradle.java-library")
+}
+
+dependencies {
+        api(project(":refinery-language-semantics"))
+        implementation(project(":refinery-store-query-interpreter"))
+        implementation(project(":refinery-store-reasoning-scope"))
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
new file mode 100644
index 00000000..4c3e52f3
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java
@@ -0,0 +1,104 @@
+/*
+ * 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.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;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+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;
+        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);
+                initialVersion = model.commit();
+        }
+
+        public ProblemTrace getProblemTrace() {
+                return problemTrace;
+        }
+
+        public ModelStore getModelStore() {
+                return store;
+        }
+
+        public Model getModel() {
+                return model;
+        }
+
+        public int getRandomSeed() {
+                return randomSeed;
+        }
+
+        public void setRandomSeed(int randomSeed) {
+                this.randomSeed = randomSeed;
+        }
+
+        public Collection<Version> run(int maxNumberOfSolutions) {
+                var bestFirst = new BestFirstStoreManager(store, maxNumberOfSolutions);
+                int currentRandomSeed = randomSeed;
+                // Increment random seed even if generation is unsuccessful.
+                randomSeed++;
+                bestFirst.startExploration(initialVersion, currentRandomSeed);
+                return bestFirst.getSolutionStore()
+                                .getSolutions()
+                                .stream()
+                                .map(VersionWithObjectiveValue::version)
+                                .toList();
+        }
+
+        public boolean tryRun() {
+                var iterator = run(1).iterator();
+                if (!iterator.hasNext()) {
+                        return false;
+                }
+                model.restore(iterator.next());
+                return true;
+        }
+
+        public <A, C> PartialInterpretation<A, C> getCandidateInterpretation(PartialSymbol<A, C> partialSymbol) {
+                return reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialSymbol);
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getCandidateInterpretation(Relation relation) {
+                return getCandidateInterpretation(problemTrace.getPartialRelation(relation));
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getCandidateInterpretation(QualifiedName qualifiedName) {
+                return getCandidateInterpretation(problemTrace.getPartialRelation(qualifiedName));
+        }
+
+        public PartialInterpretation<TruthValue, Boolean> getCandidateInterpretation(String qualifiedName) {
+                return getCandidateInterpretation(problemTrace.getPartialRelation(qualifiedName));
+        }
+
+        public static ModelGeneratorBuilder standaloneBuilder() {
+                var injector = StandaloneInjectorHolder.getInjector();
+                return injector.getInstance(ModelGeneratorBuilder.class);
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java
new file mode 100644
index 00000000..98b6653d
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java
@@ -0,0 +1,167 @@
+/*
+ * 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.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 ModelGeneratorBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) {
+                this.requiredInterpretations = requiredInterpretations;
+                return this;
+        }
+
+        public ModelGenerator build() {
+                checkProblem();
+                var storeBuilder = ModelStore.builder()
+                                .cancellationToken(cancellationToken)
+                                .with(getQueryEngineBuilder())
+                                .with(PropagationAdapter.builder())
+                                .with(StateCoderAdapter.builder())
+                                .with(DesignSpaceExplorationAdapter.builder())
+                                .with(ReasoningAdapter.builder()
+                                                .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;
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java
new file mode 100644
index 00000000..7be2dc00
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java
@@ -0,0 +1,25 @@
+/*
+ * 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.Problem;
+import tools.refinery.language.model.problem.Relation;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Map;
+
+public interface ProblemTrace {
+        Problem getProblem();
+
+        Map<Relation, PartialRelation> getRelationTrace();
+
+        PartialRelation getPartialRelation(Relation relation);
+
+        PartialRelation getPartialRelation(QualifiedName qualifiedName);
+
+        PartialRelation getPartialRelation(String qualifiedName);
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/StandaloneInjectorHolder.java b/subprojects/generator/src/main/java/tools/refinery/generator/StandaloneInjectorHolder.java
new file mode 100644
index 00000000..7db96163
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/StandaloneInjectorHolder.java
@@ -0,0 +1,27 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+import com.google.inject.Injector;
+import tools.refinery.language.ProblemStandaloneSetup;
+
+public final class StandaloneInjectorHolder {
+        private StandaloneInjectorHolder() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static Injector getInjector() {
+                return LazyHolder.INJECTOR;
+        }
+
+        private static final class LazyHolder {
+                private static final Injector INJECTOR = createInjector();
+
+                private static Injector createInjector() {
+                        return new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration();
+                }
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/UnsatisfiableProblemException.java b/subprojects/generator/src/main/java/tools/refinery/generator/UnsatisfiableProblemException.java
new file mode 100644
index 00000000..4fb18b90
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/UnsatisfiableProblemException.java
@@ -0,0 +1,12 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+public class UnsatisfiableProblemException extends RuntimeException {
+        public UnsatisfiableProblemException() {
+                super("Model generation problem was unsatisfiable");
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ValidationErrorsException.java b/subprojects/generator/src/main/java/tools/refinery/generator/ValidationErrorsException.java
new file mode 100644
index 00000000..d668e51d
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/ValidationErrorsException.java
@@ -0,0 +1,64 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator;
+
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.xtext.validation.Issue;
+
+import java.util.List;
+
+public class ValidationErrorsException extends IllegalArgumentException {
+        private final transient URI resourceUri;
+
+        private final String resourceUriString;
+
+        private final transient List<Issue> errors;
+
+        private final List<String> errorStrings;
+
+        public ValidationErrorsException(URI resourceUri, List<Issue> errors) {
+                this.resourceUri = resourceUri;
+                resourceUriString = resourceUri.toString();
+                this.errors = errors;
+                errorStrings = errors.stream()
+                                .map(Issue::toString)
+                                .toList();
+        }
+
+        public URI getResourceUri() {
+                return resourceUri;
+        }
+
+        public String getResourceUriString() {
+                return resourceUriString;
+        }
+
+        public List<Issue> getErrors() {
+                return errors;
+        }
+
+        public List<String> getErrorStrings() {
+                return errorStrings;
+        }
+
+        @Override
+        public String getMessage() {
+                var builder = new StringBuilder();
+                builder.append("Validation errors in resource ");
+                builder.append(resourceUriString);
+                builder.append(": ");
+                var iterator = errorStrings.iterator();
+                if (!iterator.hasNext()) {
+                        return builder.toString();
+                }
+                builder.append(iterator.next());
+                while (iterator.hasNext()) {
+                        builder.append(",\n");
+                        builder.append(iterator.next());
+                }
+                return builder.toString();
+        }
+}
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java b/subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java
new file mode 100644
index 00000000..109e34af
--- /dev/null
+++ b/subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java
@@ -0,0 +1,84 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.generator.impl;
+
+import com.google.inject.Inject;
+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.IScopeProvider;
+import tools.refinery.generator.ProblemTrace;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.ProblemPackage;
+import tools.refinery.language.model.problem.Relation;
+import tools.refinery.language.semantics.model.ModelInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Collections;
+import java.util.Map;
+
+public final class ProblemTraceImpl implements ProblemTrace {
+        @Inject
+        private IQualifiedNameConverter qualifiedNameConverter;
+
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IScopeProvider scopeProvider;
+
+        private Problem problem;
+        private Map<Relation, PartialRelation> relationTrace;
+
+        public void setInitializer(ModelInitializer initializer) {
+                problem = initializer.getProblem();
+                relationTrace = Collections.unmodifiableMap(initializer.getRelationTrace());
+        }
+
+        public Problem getProblem() {
+                return problem;
+        }
+
+        public Map<Relation, PartialRelation> getRelationTrace() {
+                return relationTrace;
+        }
+
+        public PartialRelation getPartialRelation(Relation relation) {
+                var partialRelation = relationTrace.get(relation);
+                if (partialRelation == null) {
+                        var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(relation);
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("No partial relation for relation " + qualifiedNameString);
+                }
+                return partialRelation;
+        }
+
+        public PartialRelation getPartialRelation(QualifiedName qualifiedName) {
+                var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION);
+                var iterator = scope.getElements(qualifiedName).iterator();
+                if (!iterator.hasNext()) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("No such relation: " + qualifiedNameString);
+                }
+                var eObjectDescription = iterator.next();
+                if (iterator.hasNext()) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Ambiguous relation: " + qualifiedNameString);
+                }
+                var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), problem);
+                if (!(eObject instanceof Relation relation)) {
+                        var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName);
+                        throw new IllegalArgumentException("Not a relation: " + qualifiedNameString);
+                }
+                return getPartialRelation(relation);
+        }
+
+        public PartialRelation getPartialRelation(String qualifiedName) {
+                var convertedName = qualifiedNameConverter.toQualifiedName(qualifiedName);
+                return getPartialRelation(convertedName);
+        }
+}