From 66d6abd60f03390fb8aebd1584eeeeac0cbac3d9 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 3 Nov 2023 02:16:04 +0100 Subject: feat: model semantics facade --- .../tools/refinery/generator/AbstractRefinery.java | 38 ++++++ .../generator/AbstractRefineryBuilder.java | 152 +++++++++++++++++++++ .../tools/refinery/generator/ModelGenerator.java | 26 +--- .../refinery/generator/ModelGeneratorBuilder.java | 138 +------------------ .../tools/refinery/generator/ModelSemantics.java | 42 ++++++ .../refinery/generator/ModelSemanticsBuilder.java | 37 +++++ 6 files changed, 277 insertions(+), 156 deletions(-) create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java create mode 100644 subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java 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 + * + * 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 + * + * 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 { + @Inject + private Provider 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 requiredInterpretations; + + protected AbstractRefineryBuilder(Collection 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 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 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 final class ModelGeneratorBuilder extends AbstractRefineryBuilder { + public ModelGeneratorBuilder() { + super(Set.of(Concreteness.CANDIDATE)); } - public ModelGeneratorBuilder requiredInterpretations(Collection 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 + * + * 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 PartialInterpretation getPartialInterpretation(PartialSymbol partialSymbol) { + return reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol); + } + + public PartialInterpretation getPartialInterpretation(Relation relation) { + return getPartialInterpretation(problemTrace.getPartialRelation(relation)); + } + + public PartialInterpretation getPartialInterpretation(QualifiedName qualifiedName) { + return getPartialInterpretation(problemTrace.getPartialRelation(qualifiedName)); + } + + public PartialInterpretation 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 + * + * 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 { + 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()); + } +} -- cgit v1.2.3-54-g00ecf