diff options
Diffstat (limited to 'subprojects/language-web/src')
3 files changed, 42 insertions, 113 deletions
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java index 1fce10a4..7b4f957c 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/generator/ModelGenerationWorker.java | |||
@@ -6,36 +6,18 @@ | |||
6 | package tools.refinery.language.web.generator; | 6 | package tools.refinery.language.web.generator; |
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Provider; | ||
10 | import org.eclipse.emf.common.util.URI; | ||
11 | import org.eclipse.xtext.diagnostics.Severity; | ||
12 | import org.eclipse.xtext.resource.IResourceFactory; | ||
13 | import org.eclipse.xtext.resource.XtextResourceSet; | ||
14 | import org.eclipse.xtext.service.OperationCanceledManager; | 9 | import org.eclipse.xtext.service.OperationCanceledManager; |
15 | import org.eclipse.xtext.util.LazyStringInputStream; | ||
16 | import org.eclipse.xtext.validation.CheckMode; | ||
17 | import org.eclipse.xtext.validation.IResourceValidator; | ||
18 | import org.slf4j.Logger; | 10 | import org.slf4j.Logger; |
19 | import org.slf4j.LoggerFactory; | 11 | import org.slf4j.LoggerFactory; |
20 | import tools.refinery.language.model.problem.Problem; | 12 | import tools.refinery.generator.ModelGeneratorBuilder; |
21 | import tools.refinery.language.semantics.metadata.MetadataCreator; | 13 | import tools.refinery.generator.ValidationErrorsException; |
22 | import tools.refinery.language.semantics.model.ModelInitializer; | ||
23 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; | 14 | import tools.refinery.language.web.semantics.PartialInterpretation2Json; |
24 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; | 15 | import tools.refinery.language.web.xtext.server.ThreadPoolExecutorServiceProvider; |
25 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; | 16 | import tools.refinery.language.web.xtext.server.push.PushWebDocument; |
26 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
27 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | ||
28 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | ||
29 | import tools.refinery.store.model.ModelStore; | ||
30 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | ||
31 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
32 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
33 | import tools.refinery.store.reasoning.literal.Concreteness; | 17 | import tools.refinery.store.reasoning.literal.Concreteness; |
34 | import tools.refinery.store.statecoding.StateCoderAdapter; | ||
35 | import tools.refinery.store.util.CancellationToken; | 18 | import tools.refinery.store.util.CancellationToken; |
36 | 19 | ||
37 | import java.io.IOException; | 20 | import java.io.IOException; |
38 | import java.util.Map; | ||
39 | import java.util.UUID; | 21 | import java.util.UUID; |
40 | import java.util.concurrent.*; | 22 | import java.util.concurrent.*; |
41 | 23 | ||
@@ -56,19 +38,7 @@ public class ModelGenerationWorker implements Runnable { | |||
56 | private OperationCanceledManager operationCanceledManager; | 38 | private OperationCanceledManager operationCanceledManager; |
57 | 39 | ||
58 | @Inject | 40 | @Inject |
59 | private Provider<XtextResourceSet> resourceSetProvider; | 41 | private ModelGeneratorBuilder generatorBuilder; |
60 | |||
61 | @Inject | ||
62 | private IResourceFactory resourceFactory; | ||
63 | |||
64 | @Inject | ||
65 | private IResourceValidator resourceValidator; | ||
66 | |||
67 | @Inject | ||
68 | private ModelInitializer initializer; | ||
69 | |||
70 | @Inject | ||
71 | private MetadataCreator metadataCreator; | ||
72 | 42 | ||
73 | @Inject | 43 | @Inject |
74 | private PartialInterpretation2Json partialInterpretation2Json; | 44 | private PartialInterpretation2Json partialInterpretation2Json; |
@@ -157,56 +127,29 @@ public class ModelGenerationWorker implements Runnable { | |||
157 | 127 | ||
158 | public ModelGenerationResult doRun() throws IOException { | 128 | public ModelGenerationResult doRun() throws IOException { |
159 | cancellationToken.checkCancelled(); | 129 | cancellationToken.checkCancelled(); |
160 | var resourceSet = resourceSetProvider.get(); | 130 | try { |
161 | var uri = URI.createURI("__synthetic_" + uuid + ".problem"); | 131 | generatorBuilder.cancellationToken(cancellationToken); |
162 | var resource = resourceFactory.createResource(uri); | 132 | generatorBuilder.fromString(text); |
163 | resourceSet.getResources().add(resource); | 133 | } catch (ValidationErrorsException e) { |
164 | var inputStream = new LazyStringInputStream(text); | 134 | var errors = e.getErrors(); |
165 | resource.load(inputStream, Map.of()); | 135 | if (errors != null && !errors.isEmpty()) { |
166 | cancellationToken.checkCancelled(); | 136 | return new ModelGenerationErrorResult(uuid, "Validation error: " + errors.get(0).getMessage()); |
167 | var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> cancelled || Thread.interrupted()); | ||
168 | cancellationToken.checkCancelled(); | ||
169 | for (var issue : issues) { | ||
170 | if (issue.getSeverity() == Severity.ERROR) { | ||
171 | return new ModelGenerationErrorResult(uuid, "Validation error: " + issue.getMessage()); | ||
172 | } | 137 | } |
138 | throw e; | ||
173 | } | 139 | } |
174 | if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) { | 140 | var generator = generatorBuilder.build(); |
175 | return new ModelGenerationErrorResult(uuid, "Model generation problem not found"); | ||
176 | } | ||
177 | cancellationToken.checkCancelled(); | ||
178 | var storeBuilder = ModelStore.builder() | ||
179 | .cancellationToken(cancellationToken) | ||
180 | .with(QueryInterpreterAdapter.builder()) | ||
181 | .with(PropagationAdapter.builder()) | ||
182 | .with(StateCoderAdapter.builder()) | ||
183 | .with(DesignSpaceExplorationAdapter.builder()) | ||
184 | .with(ReasoningAdapter.builder() | ||
185 | .requiredInterpretations(Concreteness.CANDIDATE)); | ||
186 | var modelSeed = initializer.createModel(problem, storeBuilder); | ||
187 | var store = storeBuilder.build(); | ||
188 | cancellationToken.checkCancelled(); | ||
189 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
190 | var initialVersion = model.commit(); | ||
191 | cancellationToken.checkCancelled(); | ||
192 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); | 141 | notifyResult(new ModelGenerationStatusResult(uuid, "Generating model")); |
193 | var bestFirst = new BestFirstStoreManager(store, 1); | 142 | generator.setRandomSeed(randomSeed); |
194 | bestFirst.startExploration(initialVersion, randomSeed); | 143 | if (!generator.tryRun()) { |
195 | cancellationToken.checkCancelled(); | ||
196 | var solutionStore = bestFirst.getSolutionStore(); | ||
197 | if (solutionStore.getSolutions().isEmpty()) { | ||
198 | return new ModelGenerationErrorResult(uuid, "Problem is unsatisfiable"); | 144 | return new ModelGenerationErrorResult(uuid, "Problem is unsatisfiable"); |
199 | } | 145 | } |
200 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); | 146 | notifyResult(new ModelGenerationStatusResult(uuid, "Saving generated model")); |
201 | model.restore(solutionStore.getSolutions().get(0).version()); | ||
202 | cancellationToken.checkCancelled(); | 147 | cancellationToken.checkCancelled(); |
203 | metadataCreator.setInitializer(initializer); | 148 | var nodesMetadata = generator.getNodesMetadata(); |
204 | var nodesMetadata = metadataCreator.getNodesMetadata(model.getAdapter(ReasoningAdapter.class).getNodeCount(), | ||
205 | false); | ||
206 | cancellationToken.checkCancelled(); | 149 | cancellationToken.checkCancelled(); |
207 | var relationsMetadata = metadataCreator.getRelationsMetadata(); | 150 | var relationsMetadata = generator.getProblemTrace().getRelationsMetadata(); |
208 | cancellationToken.checkCancelled(); | 151 | cancellationToken.checkCancelled(); |
209 | var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(initializer, model, | 152 | var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(generator, |
210 | Concreteness.CANDIDATE, cancellationToken); | 153 | Concreteness.CANDIDATE, cancellationToken); |
211 | return new ModelGenerationSuccessResult(uuid, nodesMetadata, relationsMetadata, partialInterpretation); | 154 | return new ModelGenerationSuccessResult(uuid, nodesMetadata, relationsMetadata, partialInterpretation); |
212 | } | 155 | } |
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java index 5d5da8fe..7afed5c0 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/PartialInterpretation2Json.java | |||
@@ -9,7 +9,7 @@ import com.google.gson.JsonArray; | |||
9 | import com.google.gson.JsonObject; | 9 | import com.google.gson.JsonObject; |
10 | import com.google.inject.Inject; | 10 | import com.google.inject.Inject; |
11 | import com.google.inject.Singleton; | 11 | import com.google.inject.Singleton; |
12 | import tools.refinery.language.semantics.model.ModelInitializer; | 12 | import tools.refinery.generator.AbstractRefinery; |
13 | import tools.refinery.language.semantics.model.SemanticsUtils; | 13 | import tools.refinery.language.semantics.model.SemanticsUtils; |
14 | import tools.refinery.store.map.Cursor; | 14 | import tools.refinery.store.map.Cursor; |
15 | import tools.refinery.store.model.Model; | 15 | import tools.refinery.store.model.Model; |
@@ -27,11 +27,12 @@ public class PartialInterpretation2Json { | |||
27 | @Inject | 27 | @Inject |
28 | private SemanticsUtils semanticsUtils; | 28 | private SemanticsUtils semanticsUtils; |
29 | 29 | ||
30 | public JsonObject getPartialInterpretation(ModelInitializer initializer, Model model, Concreteness concreteness, | 30 | public JsonObject getPartialInterpretation(AbstractRefinery refinery, Concreteness concreteness, |
31 | CancellationToken cancellationToken) { | 31 | CancellationToken cancellationToken) { |
32 | var model = refinery.getModel(); | ||
32 | var adapter = model.getAdapter(ReasoningAdapter.class); | 33 | var adapter = model.getAdapter(ReasoningAdapter.class); |
33 | var json = new JsonObject(); | 34 | var json = new JsonObject(); |
34 | for (var entry : initializer.getRelationTrace().entrySet()) { | 35 | for (var entry : refinery.getProblemTrace().getRelationTrace().entrySet()) { |
35 | var relation = entry.getKey(); | 36 | var relation = entry.getKey(); |
36 | var partialSymbol = entry.getValue(); | 37 | var partialSymbol = entry.getValue(); |
37 | var tuples = getTuplesJson(adapter, concreteness, partialSymbol); | 38 | var tuples = getTuplesJson(adapter, concreteness, partialSymbol); |
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java index fb89bea6..a8f16c84 100644 --- a/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java +++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/semantics/SemanticsWorker.java | |||
@@ -15,15 +15,10 @@ import org.eclipse.xtext.validation.FeatureBasedDiagnostic; | |||
15 | import org.eclipse.xtext.validation.IDiagnosticConverter; | 15 | import org.eclipse.xtext.validation.IDiagnosticConverter; |
16 | import org.eclipse.xtext.validation.Issue; | 16 | import org.eclipse.xtext.validation.Issue; |
17 | import org.eclipse.xtext.web.server.validation.ValidationResult; | 17 | import org.eclipse.xtext.web.server.validation.ValidationResult; |
18 | import tools.refinery.generator.ModelSemantics; | ||
19 | import tools.refinery.generator.ModelSemanticsBuilder; | ||
18 | import tools.refinery.language.model.problem.Problem; | 20 | import tools.refinery.language.model.problem.Problem; |
19 | import tools.refinery.language.semantics.metadata.MetadataCreator; | ||
20 | import tools.refinery.language.semantics.model.ModelInitializer; | ||
21 | import tools.refinery.language.semantics.model.TracedException; | 21 | import tools.refinery.language.semantics.model.TracedException; |
22 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
23 | import tools.refinery.store.model.ModelStore; | ||
24 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | ||
25 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
26 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
27 | import tools.refinery.store.reasoning.literal.Concreteness; | 22 | import tools.refinery.store.reasoning.literal.Concreteness; |
28 | import tools.refinery.store.reasoning.translator.TranslationException; | 23 | import tools.refinery.store.reasoning.translator.TranslationException; |
29 | import tools.refinery.store.util.CancellationToken; | 24 | import tools.refinery.store.util.CancellationToken; |
@@ -44,10 +39,7 @@ class SemanticsWorker implements Callable<SemanticsResult> { | |||
44 | private IDiagnosticConverter diagnosticConverter; | 39 | private IDiagnosticConverter diagnosticConverter; |
45 | 40 | ||
46 | @Inject | 41 | @Inject |
47 | private ModelInitializer initializer; | 42 | private ModelSemanticsBuilder semanticsBuilder; |
48 | |||
49 | @Inject | ||
50 | private MetadataCreator metadataCreator; | ||
51 | 43 | ||
52 | private Problem problem; | 44 | private Problem problem; |
53 | 45 | ||
@@ -64,36 +56,29 @@ class SemanticsWorker implements Callable<SemanticsResult> { | |||
64 | 56 | ||
65 | @Override | 57 | @Override |
66 | public SemanticsResult call() { | 58 | public SemanticsResult call() { |
67 | var builder = ModelStore.builder() | 59 | semanticsBuilder.cancellationToken(cancellationToken); |
68 | .cancellationToken(cancellationToken) | ||
69 | .with(QueryInterpreterAdapter.builder()) | ||
70 | .with(PropagationAdapter.builder()) | ||
71 | .with(ReasoningAdapter.builder() | ||
72 | .requiredInterpretations(Concreteness.PARTIAL)); | ||
73 | cancellationToken.checkCancelled(); | 60 | cancellationToken.checkCancelled(); |
61 | ModelSemantics semantics; | ||
74 | try { | 62 | try { |
75 | var modelSeed = initializer.createModel(problem, builder); | 63 | semanticsBuilder.problem(problem); |
76 | cancellationToken.checkCancelled(); | ||
77 | metadataCreator.setInitializer(initializer); | ||
78 | cancellationToken.checkCancelled(); | ||
79 | var nodesMetadata = metadataCreator.getNodesMetadata(); | ||
80 | cancellationToken.checkCancelled(); | ||
81 | var relationsMetadata = metadataCreator.getRelationsMetadata(); | ||
82 | cancellationToken.checkCancelled(); | ||
83 | var store = builder.build(); | ||
84 | cancellationToken.checkCancelled(); | ||
85 | var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
86 | cancellationToken.checkCancelled(); | 64 | cancellationToken.checkCancelled(); |
87 | var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(initializer, model, | 65 | semantics = semanticsBuilder.build(); |
88 | Concreteness.PARTIAL, cancellationToken); | ||
89 | |||
90 | return new SemanticsSuccessResult(nodesMetadata, relationsMetadata, partialInterpretation); | ||
91 | } catch (TracedException e) { | ||
92 | return getTracedErrorResult(e.getSourceElement(), e.getMessage()); | ||
93 | } catch (TranslationException e) { | 66 | } catch (TranslationException e) { |
94 | var sourceElement = initializer.getInverseTrace(e.getPartialSymbol()); | 67 | return new SemanticsInternalErrorResult(e.getMessage()); |
95 | return getTracedErrorResult(sourceElement, e.getMessage()); | 68 | } catch (TracedException e) { |
69 | var cause = e.getCause(); | ||
70 | // Suppress the type of the cause exception. | ||
71 | var message = cause == null ? e.getMessage() : cause.getMessage(); | ||
72 | return getTracedErrorResult(e.getSourceElement(), message); | ||
96 | } | 73 | } |
74 | cancellationToken.checkCancelled(); | ||
75 | var nodesMetadata = semantics.getNodesMetadata(); | ||
76 | cancellationToken.checkCancelled(); | ||
77 | var relationsMetadata = semantics.getProblemTrace().getRelationsMetadata(); | ||
78 | cancellationToken.checkCancelled(); | ||
79 | var partialInterpretation = partialInterpretation2Json.getPartialInterpretation(semantics, | ||
80 | Concreteness.PARTIAL, cancellationToken); | ||
81 | return new SemanticsSuccessResult(nodesMetadata, relationsMetadata, partialInterpretation); | ||
97 | } | 82 | } |
98 | 83 | ||
99 | private SemanticsResult getTracedErrorResult(EObject sourceElement, String message) { | 84 | private SemanticsResult getTracedErrorResult(EObject sourceElement, String message) { |