diff options
Diffstat (limited to 'subprojects')
11 files changed, 147 insertions, 127 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 index 81bf712a..56c7a23b 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java | |||
@@ -5,22 +5,31 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.generator; | 6 | package tools.refinery.generator; |
7 | 7 | ||
8 | import tools.refinery.generator.impl.ProblemTraceImpl; | ||
9 | import tools.refinery.language.semantics.metadata.NodeMetadata; | ||
8 | import tools.refinery.store.model.Model; | 10 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.model.ModelStore; | 11 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.reasoning.ReasoningAdapter; | 12 | import tools.refinery.store.reasoning.ReasoningAdapter; |
11 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | 13 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; |
12 | import tools.refinery.store.reasoning.seed.ModelSeed; | 14 | import tools.refinery.store.reasoning.seed.ModelSeed; |
15 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
13 | 16 | ||
14 | public class AbstractRefinery { | 17 | import java.util.List; |
18 | |||
19 | public abstract class AbstractRefinery { | ||
15 | protected final ProblemTrace problemTrace; | 20 | protected final ProblemTrace problemTrace; |
16 | protected final ModelStore store; | 21 | protected final ModelStore store; |
17 | protected final Model model; | 22 | protected final Model model; |
18 | protected final ReasoningAdapter reasoningAdapter; | 23 | protected final ReasoningAdapter reasoningAdapter; |
19 | 24 | ||
20 | public AbstractRefinery(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | 25 | protected AbstractRefinery(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { |
21 | this.problemTrace = problemTrace; | 26 | this.problemTrace = problemTrace; |
22 | this.store = store; | 27 | this.store = store; |
23 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | 28 | try { |
29 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
30 | } catch (TranslationException e) { | ||
31 | throw ProblemTraceImpl.wrapException(problemTrace, e); | ||
32 | } | ||
24 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | 33 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); |
25 | } | 34 | } |
26 | 35 | ||
@@ -35,4 +44,11 @@ public class AbstractRefinery { | |||
35 | public Model getModel() { | 44 | public Model getModel() { |
36 | return model; | 45 | return model; |
37 | } | 46 | } |
47 | |||
48 | public List<NodeMetadata> getNodesMetadata() { | ||
49 | int nodeCount = reasoningAdapter.getNodeCount(); | ||
50 | return problemTrace.getNodesMetadata(nodeCount, isPreserveNewNodes()); | ||
51 | } | ||
52 | |||
53 | protected abstract boolean isPreserveNewNodes(); | ||
38 | } | 54 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java index b60a3890..d4649051 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java | |||
@@ -21,6 +21,7 @@ import tools.refinery.language.semantics.model.ModelInitializer; | |||
21 | import tools.refinery.store.query.ModelQueryBuilder; | 21 | import tools.refinery.store.query.ModelQueryBuilder; |
22 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | 22 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; |
23 | import tools.refinery.store.reasoning.literal.Concreteness; | 23 | import tools.refinery.store.reasoning.literal.Concreteness; |
24 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
24 | import tools.refinery.store.util.CancellationToken; | 25 | import tools.refinery.store.util.CancellationToken; |
25 | 26 | ||
26 | import java.io.File; | 27 | import java.io.File; |
@@ -29,6 +30,8 @@ import java.io.InputStream; | |||
29 | import java.util.Collection; | 30 | import java.util.Collection; |
30 | import java.util.Map; | 31 | import java.util.Map; |
31 | 32 | ||
33 | // This class is used as a fluent builder. | ||
34 | @SuppressWarnings("UnusedReturnValue") | ||
32 | public abstract class AbstractRefineryBuilder<T> { | 35 | public abstract class AbstractRefineryBuilder<T> { |
33 | @Inject | 36 | @Inject |
34 | private Provider<XtextResourceSet> resourceSetProvider; | 37 | private Provider<XtextResourceSet> resourceSetProvider; |
@@ -113,8 +116,12 @@ public abstract class AbstractRefineryBuilder<T> { | |||
113 | if (problemLoaded) { | 116 | if (problemLoaded) { |
114 | throw new IllegalStateException("Problem was already set"); | 117 | throw new IllegalStateException("Problem was already set"); |
115 | } | 118 | } |
116 | initializer.readProblem(problem); | ||
117 | problemTrace.setInitializer(initializer); | 119 | problemTrace.setInitializer(initializer); |
120 | try { | ||
121 | initializer.readProblem(problem); | ||
122 | } catch (TranslationException e) { | ||
123 | throw ProblemTraceImpl.wrapException(problemTrace, e); | ||
124 | } | ||
118 | problemLoaded = true; | 125 | problemLoaded = true; |
119 | return self(); | 126 | return self(); |
120 | } | 127 | } |
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 e5115352..78c807d1 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java | |||
@@ -29,6 +29,11 @@ public class ModelGenerator extends AbstractRefinery { | |||
29 | initialVersion = model.commit(); | 29 | initialVersion = model.commit(); |
30 | } | 30 | } |
31 | 31 | ||
32 | @Override | ||
33 | protected boolean isPreserveNewNodes() { | ||
34 | return false; | ||
35 | } | ||
36 | |||
32 | public int getRandomSeed() { | 37 | public int getRandomSeed() { |
33 | return randomSeed; | 38 | return randomSeed; |
34 | } | 39 | } |
@@ -50,6 +55,8 @@ public class ModelGenerator extends AbstractRefinery { | |||
50 | .toList(); | 55 | .toList(); |
51 | } | 56 | } |
52 | 57 | ||
58 | // This method only makes sense if it returns {@code true} on success. | ||
59 | @SuppressWarnings("BooleanMethodIsAlwaysInverted") | ||
53 | public boolean tryRun() { | 60 | public boolean tryRun() { |
54 | var iterator = run(1).iterator(); | 61 | var iterator = run(1).iterator(); |
55 | if (!iterator.hasNext()) { | 62 | if (!iterator.hasNext()) { |
@@ -59,6 +66,12 @@ public class ModelGenerator extends AbstractRefinery { | |||
59 | return true; | 66 | return true; |
60 | } | 67 | } |
61 | 68 | ||
69 | public void run() { | ||
70 | if (!tryRun()) { | ||
71 | throw new UnsatisfiableProblemException(); | ||
72 | } | ||
73 | } | ||
74 | |||
62 | public <A, C> PartialInterpretation<A, C> getCandidateInterpretation(PartialSymbol<A, C> partialSymbol) { | 75 | public <A, C> PartialInterpretation<A, C> getCandidateInterpretation(PartialSymbol<A, C> partialSymbol) { |
63 | return reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialSymbol); | 76 | return reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialSymbol); |
64 | } | 77 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java index 8bac1910..661bc97c 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java | |||
@@ -19,6 +19,11 @@ public class ModelSemantics extends AbstractRefinery { | |||
19 | super(problemTrace, store, modelSeed); | 19 | super(problemTrace, store, modelSeed); |
20 | } | 20 | } |
21 | 21 | ||
22 | @Override | ||
23 | protected boolean isPreserveNewNodes() { | ||
24 | return true; | ||
25 | } | ||
26 | |||
22 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | 27 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { |
23 | return reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol); | 28 | return reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol); |
24 | } | 29 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java index 7be2dc00..f7963c58 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemTrace.java | |||
@@ -8,8 +8,12 @@ package tools.refinery.generator; | |||
8 | import org.eclipse.xtext.naming.QualifiedName; | 8 | import org.eclipse.xtext.naming.QualifiedName; |
9 | import tools.refinery.language.model.problem.Problem; | 9 | import tools.refinery.language.model.problem.Problem; |
10 | import tools.refinery.language.model.problem.Relation; | 10 | import tools.refinery.language.model.problem.Relation; |
11 | import tools.refinery.language.semantics.metadata.NodeMetadata; | ||
12 | import tools.refinery.language.semantics.metadata.RelationMetadata; | ||
13 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
11 | import tools.refinery.store.reasoning.representation.PartialRelation; | 14 | import tools.refinery.store.reasoning.representation.PartialRelation; |
12 | 15 | ||
16 | import java.util.List; | ||
13 | import java.util.Map; | 17 | import java.util.Map; |
14 | 18 | ||
15 | public interface ProblemTrace { | 19 | public interface ProblemTrace { |
@@ -17,9 +21,15 @@ public interface ProblemTrace { | |||
17 | 21 | ||
18 | Map<Relation, PartialRelation> getRelationTrace(); | 22 | Map<Relation, PartialRelation> getRelationTrace(); |
19 | 23 | ||
24 | Relation getInverseTrace(AnyPartialSymbol partialSymbol); | ||
25 | |||
20 | PartialRelation getPartialRelation(Relation relation); | 26 | PartialRelation getPartialRelation(Relation relation); |
21 | 27 | ||
22 | PartialRelation getPartialRelation(QualifiedName qualifiedName); | 28 | PartialRelation getPartialRelation(QualifiedName qualifiedName); |
23 | 29 | ||
24 | PartialRelation getPartialRelation(String qualifiedName); | 30 | PartialRelation getPartialRelation(String qualifiedName); |
31 | |||
32 | List<RelationMetadata> getRelationsMetadata(); | ||
33 | |||
34 | List<NodeMetadata> getNodesMetadata(int nodeCount, boolean preserveNewNodes); | ||
25 | } | 35 | } |
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 index 109e34af..5671d3f8 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/impl/ProblemTraceImpl.java | |||
@@ -6,6 +6,7 @@ | |||
6 | package tools.refinery.generator.impl; | 6 | package tools.refinery.generator.impl; |
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import com.google.inject.Provider; | ||
9 | import org.eclipse.emf.ecore.util.EcoreUtil; | 10 | import org.eclipse.emf.ecore.util.EcoreUtil; |
10 | import org.eclipse.xtext.naming.IQualifiedNameConverter; | 11 | import org.eclipse.xtext.naming.IQualifiedNameConverter; |
11 | import org.eclipse.xtext.naming.IQualifiedNameProvider; | 12 | import org.eclipse.xtext.naming.IQualifiedNameProvider; |
@@ -15,10 +16,17 @@ import tools.refinery.generator.ProblemTrace; | |||
15 | import tools.refinery.language.model.problem.Problem; | 16 | import tools.refinery.language.model.problem.Problem; |
16 | import tools.refinery.language.model.problem.ProblemPackage; | 17 | import tools.refinery.language.model.problem.ProblemPackage; |
17 | import tools.refinery.language.model.problem.Relation; | 18 | import tools.refinery.language.model.problem.Relation; |
19 | import tools.refinery.language.semantics.metadata.MetadataCreator; | ||
20 | import tools.refinery.language.semantics.metadata.NodeMetadata; | ||
21 | import tools.refinery.language.semantics.metadata.RelationMetadata; | ||
18 | import tools.refinery.language.semantics.model.ModelInitializer; | 22 | import tools.refinery.language.semantics.model.ModelInitializer; |
23 | import tools.refinery.language.semantics.model.TracedException; | ||
24 | import tools.refinery.store.reasoning.representation.AnyPartialSymbol; | ||
19 | import tools.refinery.store.reasoning.representation.PartialRelation; | 25 | import tools.refinery.store.reasoning.representation.PartialRelation; |
26 | import tools.refinery.store.reasoning.translator.TranslationException; | ||
20 | 27 | ||
21 | import java.util.Collections; | 28 | import java.util.Collections; |
29 | import java.util.List; | ||
22 | import java.util.Map; | 30 | import java.util.Map; |
23 | 31 | ||
24 | public final class ProblemTraceImpl implements ProblemTrace { | 32 | public final class ProblemTraceImpl implements ProblemTrace { |
@@ -31,22 +39,31 @@ public final class ProblemTraceImpl implements ProblemTrace { | |||
31 | @Inject | 39 | @Inject |
32 | private IScopeProvider scopeProvider; | 40 | private IScopeProvider scopeProvider; |
33 | 41 | ||
34 | private Problem problem; | 42 | @Inject |
43 | private Provider<MetadataCreator> metadataCreatorProvider; | ||
44 | |||
45 | private ModelInitializer initializer; | ||
35 | private Map<Relation, PartialRelation> relationTrace; | 46 | private Map<Relation, PartialRelation> relationTrace; |
47 | private MetadataCreator metadataCreator; | ||
36 | 48 | ||
37 | public void setInitializer(ModelInitializer initializer) { | 49 | public void setInitializer(ModelInitializer initializer) { |
38 | problem = initializer.getProblem(); | 50 | this.initializer = initializer; |
39 | relationTrace = Collections.unmodifiableMap(initializer.getRelationTrace()); | 51 | relationTrace = Collections.unmodifiableMap(initializer.getRelationTrace()); |
40 | } | 52 | } |
41 | 53 | ||
42 | public Problem getProblem() { | 54 | public Problem getProblem() { |
43 | return problem; | 55 | return initializer.getProblem(); |
44 | } | 56 | } |
45 | 57 | ||
46 | public Map<Relation, PartialRelation> getRelationTrace() { | 58 | public Map<Relation, PartialRelation> getRelationTrace() { |
47 | return relationTrace; | 59 | return relationTrace; |
48 | } | 60 | } |
49 | 61 | ||
62 | @Override | ||
63 | public Relation getInverseTrace(AnyPartialSymbol partialSymbol) { | ||
64 | return initializer.getInverseTrace(partialSymbol); | ||
65 | } | ||
66 | |||
50 | public PartialRelation getPartialRelation(Relation relation) { | 67 | public PartialRelation getPartialRelation(Relation relation) { |
51 | var partialRelation = relationTrace.get(relation); | 68 | var partialRelation = relationTrace.get(relation); |
52 | if (partialRelation == null) { | 69 | if (partialRelation == null) { |
@@ -58,7 +75,7 @@ public final class ProblemTraceImpl implements ProblemTrace { | |||
58 | } | 75 | } |
59 | 76 | ||
60 | public PartialRelation getPartialRelation(QualifiedName qualifiedName) { | 77 | public PartialRelation getPartialRelation(QualifiedName qualifiedName) { |
61 | var scope = scopeProvider.getScope(problem, ProblemPackage.Literals.ASSERTION__RELATION); | 78 | var scope = scopeProvider.getScope(getProblem(), ProblemPackage.Literals.ASSERTION__RELATION); |
62 | var iterator = scope.getElements(qualifiedName).iterator(); | 79 | var iterator = scope.getElements(qualifiedName).iterator(); |
63 | if (!iterator.hasNext()) { | 80 | if (!iterator.hasNext()) { |
64 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | 81 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); |
@@ -69,7 +86,7 @@ public final class ProblemTraceImpl implements ProblemTrace { | |||
69 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | 86 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); |
70 | throw new IllegalArgumentException("Ambiguous relation: " + qualifiedNameString); | 87 | throw new IllegalArgumentException("Ambiguous relation: " + qualifiedNameString); |
71 | } | 88 | } |
72 | var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), problem); | 89 | var eObject = EcoreUtil.resolve(eObjectDescription.getEObjectOrProxy(), getProblem()); |
73 | if (!(eObject instanceof Relation relation)) { | 90 | if (!(eObject instanceof Relation relation)) { |
74 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); | 91 | var qualifiedNameString = qualifiedNameConverter.toString(qualifiedName); |
75 | throw new IllegalArgumentException("Not a relation: " + qualifiedNameString); | 92 | throw new IllegalArgumentException("Not a relation: " + qualifiedNameString); |
@@ -81,4 +98,30 @@ public final class ProblemTraceImpl implements ProblemTrace { | |||
81 | var convertedName = qualifiedNameConverter.toQualifiedName(qualifiedName); | 98 | var convertedName = qualifiedNameConverter.toQualifiedName(qualifiedName); |
82 | return getPartialRelation(convertedName); | 99 | return getPartialRelation(convertedName); |
83 | } | 100 | } |
101 | |||
102 | @Override | ||
103 | public List<RelationMetadata> getRelationsMetadata() { | ||
104 | return getMetadataCreator().getRelationsMetadata(); | ||
105 | } | ||
106 | |||
107 | @Override | ||
108 | public List<NodeMetadata> getNodesMetadata(int nodeCount, boolean preserveNewNodes) { | ||
109 | return getMetadataCreator().getNodesMetadata(nodeCount, preserveNewNodes); | ||
110 | } | ||
111 | |||
112 | private MetadataCreator getMetadataCreator() { | ||
113 | if (metadataCreator == null) { | ||
114 | metadataCreator = metadataCreatorProvider.get(); | ||
115 | metadataCreator.setInitializer(initializer); | ||
116 | } | ||
117 | return metadataCreator; | ||
118 | } | ||
119 | |||
120 | public static RuntimeException wrapException(ProblemTrace trace, TranslationException translationException) { | ||
121 | var source = trace.getInverseTrace(translationException.getPartialSymbol()); | ||
122 | if (source == null) { | ||
123 | return translationException; | ||
124 | } | ||
125 | return new TracedException(source, translationException); | ||
126 | } | ||
84 | } | 127 | } |
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java index a0081041..a05e647d 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java | |||
@@ -68,7 +68,7 @@ public class ModelInitializer { | |||
68 | 68 | ||
69 | private final Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>(); | 69 | private final Map<AnyPartialSymbol, Relation> inverseTrace = new HashMap<>(); |
70 | 70 | ||
71 | private Map<Relation, PartialRelation> relationTrace; | 71 | private final Map<Relation, PartialRelation> relationTrace = new LinkedHashMap<>(); |
72 | 72 | ||
73 | private final MetamodelBuilder metamodelBuilder = Metamodel.builder(); | 73 | private final MetamodelBuilder metamodelBuilder = Metamodel.builder(); |
74 | 74 | ||
@@ -128,7 +128,6 @@ public class ModelInitializer { | |||
128 | collectMetamodel(); | 128 | collectMetamodel(); |
129 | metamodel = metamodelBuilder.build(); | 129 | metamodel = metamodelBuilder.build(); |
130 | collectAssertions(); | 130 | collectAssertions(); |
131 | relationTrace = new LinkedHashMap<>(relationInfoMap.size()); | ||
132 | int nodeCount = getNodeCount(); | 131 | int nodeCount = getNodeCount(); |
133 | var modelSeedBuilder = ModelSeed.builder(nodeCount); | 132 | var modelSeedBuilder = ModelSeed.builder(nodeCount); |
134 | for (var entry : relationInfoMap.entrySet()) { | 133 | for (var entry : relationInfoMap.entrySet()) { |
diff --git a/subprojects/language-web/build.gradle.kts b/subprojects/language-web/build.gradle.kts index 2370794d..c3a0b7e9 100644 --- a/subprojects/language-web/build.gradle.kts +++ b/subprojects/language-web/build.gradle.kts | |||
@@ -15,11 +15,9 @@ val webapp: Configuration by configurations.creating { | |||
15 | } | 15 | } |
16 | 16 | ||
17 | dependencies { | 17 | dependencies { |
18 | implementation(project(":refinery-generator")) | ||
18 | implementation(project(":refinery-language")) | 19 | implementation(project(":refinery-language")) |
19 | implementation(project(":refinery-language-ide")) | 20 | implementation(project(":refinery-language-ide")) |
20 | implementation(project(":refinery-language-semantics")) | ||
21 | implementation(project(":refinery-store-query-interpreter")) | ||
22 | implementation(project(":refinery-store-reasoning-scope")) | ||
23 | implementation(libs.gson) | 21 | implementation(libs.gson) |
24 | implementation(libs.jetty.server) | 22 | implementation(libs.jetty.server) |
25 | implementation(libs.jetty.servlet) | 23 | implementation(libs.jetty.servlet) |
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) { |