From eddf21f4b583fecb982c2c2f4ee733ee156371d7 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 3 Nov 2023 02:03:56 +0100 Subject: feat: model generator facade --- .../tools/refinery/generator/ModelGenerator.java | 104 +++++++++++++ .../refinery/generator/ModelGeneratorBuilder.java | 167 +++++++++++++++++++++ .../tools/refinery/generator/ProblemTrace.java | 25 +++ .../generator/StandaloneInjectorHolder.java | 27 ++++ .../generator/UnsatisfiableProblemException.java | 12 ++ .../generator/ValidationErrorsException.java | 64 ++++++++ .../refinery/generator/impl/ProblemTraceImpl.java | 84 +++++++++++ 7 files changed, 483 insertions(+) create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/StandaloneInjectorHolder.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/UnsatisfiableProblemException.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ValidationErrorsException.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java (limited to 'subprojects/generator/src/main/java/tools') 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 + * + * 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 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 PartialInterpretation getCandidateInterpretation(PartialSymbol partialSymbol) { + return reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialSymbol); + } + + public PartialInterpretation getCandidateInterpretation(Relation relation) { + return getCandidateInterpretation(problemTrace.getPartialRelation(relation)); + } + + public PartialInterpretation getCandidateInterpretation(QualifiedName qualifiedName) { + return getCandidateInterpretation(problemTrace.getPartialRelation(qualifiedName)); + } + + public PartialInterpretation 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 + * + * 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 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 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 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 + * + * 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 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 + * + * 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 + * + * 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 + * + * 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 errors; + + private final List errorStrings; + + public ValidationErrorsException(URI resourceUri, List 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 getErrors() { + return errors; + } + + public List 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 + * + * 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 relationTrace; + + public void setInitializer(ModelInitializer initializer) { + problem = initializer.getProblem(); + relationTrace = Collections.unmodifiableMap(initializer.getRelationTrace()); + } + + public Problem getProblem() { + return problem; + } + + public Map 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); + } +} -- cgit v1.2.3-54-g00ecf