diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-12-24 17:28:11 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-12-24 17:41:29 +0100 |
commit | f7c9414c4bcc8a48cbc1c25879e9c8eafe772320 (patch) | |
tree | b3adee36064e0dcf1fefac89466b41cfc52e631b /subprojects/generator/src/main | |
parent | chore(deps): bump dependencies (diff) | |
download | refinery-f7c9414c4bcc8a48cbc1c25879e9c8eafe772320.tar.gz refinery-f7c9414c4bcc8a48cbc1c25879e9c8eafe772320.tar.zst refinery-f7c9414c4bcc8a48cbc1c25879e9c8eafe772320.zip |
feat: command line model generator
Diffstat (limited to 'subprojects/generator/src/main')
4 files changed, 42 insertions, 15 deletions
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 5b44c10a..1515dceb 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java | |||
@@ -5,7 +5,10 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.generator; | 6 | package tools.refinery.generator; |
7 | 7 | ||
8 | import com.google.inject.Provider; | ||
9 | import tools.refinery.language.model.problem.Problem; | ||
8 | import tools.refinery.language.semantics.ProblemTrace; | 10 | import tools.refinery.language.semantics.ProblemTrace; |
11 | import tools.refinery.language.semantics.SolutionSerializer; | ||
9 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | 12 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; |
10 | import tools.refinery.store.map.Version; | 13 | import tools.refinery.store.map.Version; |
11 | import tools.refinery.store.model.ModelStore; | 14 | import tools.refinery.store.model.ModelStore; |
@@ -16,21 +19,22 @@ import tools.refinery.store.reasoning.seed.ModelSeed; | |||
16 | 19 | ||
17 | public class ModelGenerator extends ModelFacade { | 20 | public class ModelGenerator extends ModelFacade { |
18 | private final Version initialVersion; | 21 | private final Version initialVersion; |
19 | 22 | private final Provider<SolutionSerializer> solutionSerializerProvider; | |
20 | private int randomSeed = 0; | 23 | private long randomSeed = 1; |
21 | |||
22 | private boolean lastGenerationSuccessful; | 24 | private boolean lastGenerationSuccessful; |
23 | 25 | ||
24 | public ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | 26 | ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed, |
27 | Provider<SolutionSerializer> solutionSerializerProvider) { | ||
25 | super(problemTrace, store, modelSeed, Concreteness.CANDIDATE); | 28 | super(problemTrace, store, modelSeed, Concreteness.CANDIDATE); |
29 | this.solutionSerializerProvider = solutionSerializerProvider; | ||
26 | initialVersion = getModel().commit(); | 30 | initialVersion = getModel().commit(); |
27 | } | 31 | } |
28 | 32 | ||
29 | public int getRandomSeed() { | 33 | public long getRandomSeed() { |
30 | return randomSeed; | 34 | return randomSeed; |
31 | } | 35 | } |
32 | 36 | ||
33 | public void setRandomSeed(int randomSeed) { | 37 | public void setRandomSeed(long randomSeed) { |
34 | this.randomSeed = randomSeed; | 38 | this.randomSeed = randomSeed; |
35 | this.lastGenerationSuccessful = false; | 39 | this.lastGenerationSuccessful = false; |
36 | } | 40 | } |
@@ -50,7 +54,7 @@ public class ModelGenerator extends ModelFacade { | |||
50 | if (solutions.isEmpty()) { | 54 | if (solutions.isEmpty()) { |
51 | return false; | 55 | return false; |
52 | } | 56 | } |
53 | getModel().restore(solutions.get(0).version()); | 57 | getModel().restore(solutions.getFirst().version()); |
54 | lastGenerationSuccessful = true; | 58 | lastGenerationSuccessful = true; |
55 | return true; | 59 | return true; |
56 | } | 60 | } |
@@ -63,9 +67,19 @@ public class ModelGenerator extends ModelFacade { | |||
63 | 67 | ||
64 | @Override | 68 | @Override |
65 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | 69 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { |
70 | checkSuccessfulGeneration(); | ||
71 | return super.getPartialInterpretation(partialSymbol); | ||
72 | } | ||
73 | |||
74 | public Problem serializeSolution() { | ||
75 | checkSuccessfulGeneration(); | ||
76 | var serializer = solutionSerializerProvider.get(); | ||
77 | return serializer.serializeSolution(getProblemTrace(), getModel()); | ||
78 | } | ||
79 | |||
80 | private void checkSuccessfulGeneration() { | ||
66 | if (!lastGenerationSuccessful) { | 81 | if (!lastGenerationSuccessful) { |
67 | throw new IllegalStateException("No generated model is available"); | 82 | throw new IllegalStateException("No generated model is available"); |
68 | } | 83 | } |
69 | return super.getPartialInterpretation(partialSymbol); | ||
70 | } | 84 | } |
71 | } | 85 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java index 6642d591..587601f2 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorFactory.java | |||
@@ -9,6 +9,7 @@ import com.google.inject.Inject; | |||
9 | import com.google.inject.Provider; | 9 | import com.google.inject.Provider; |
10 | import tools.refinery.language.model.problem.Problem; | 10 | import tools.refinery.language.model.problem.Problem; |
11 | import tools.refinery.language.semantics.ModelInitializer; | 11 | import tools.refinery.language.semantics.ModelInitializer; |
12 | import tools.refinery.language.semantics.SolutionSerializer; | ||
12 | import tools.refinery.store.dse.propagation.PropagationAdapter; | 13 | import tools.refinery.store.dse.propagation.PropagationAdapter; |
13 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | 14 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; |
14 | import tools.refinery.store.model.ModelStore; | 15 | import tools.refinery.store.model.ModelStore; |
@@ -25,6 +26,9 @@ public final class ModelGeneratorFactory { | |||
25 | @Inject | 26 | @Inject |
26 | private Provider<ModelInitializer> initializerProvider; | 27 | private Provider<ModelInitializer> initializerProvider; |
27 | 28 | ||
29 | @Inject | ||
30 | private Provider<SolutionSerializer> solutionSerializerProvider; | ||
31 | |||
28 | private CancellationToken cancellationToken = CancellationToken.NONE; | 32 | private CancellationToken cancellationToken = CancellationToken.NONE; |
29 | 33 | ||
30 | private boolean debugPartialInterpretations; | 34 | private boolean debugPartialInterpretations; |
@@ -53,7 +57,8 @@ public final class ModelGeneratorFactory { | |||
53 | .requiredInterpretations(getRequiredInterpretations())); | 57 | .requiredInterpretations(getRequiredInterpretations())); |
54 | initializer.configureStoreBuilder(storeBuilder); | 58 | initializer.configureStoreBuilder(storeBuilder); |
55 | var store = storeBuilder.build(); | 59 | var store = storeBuilder.build(); |
56 | return new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed()); | 60 | return new ModelGenerator(initializer.getProblemTrace(), store, initializer.getModelSeed(), |
61 | solutionSerializerProvider); | ||
57 | } | 62 | } |
58 | 63 | ||
59 | private Collection<Concreteness> getRequiredInterpretations() { | 64 | private Collection<Concreteness> getRequiredInterpretations() { |
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 bc02c887..7207a509 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java | |||
@@ -11,7 +11,7 @@ import tools.refinery.store.reasoning.literal.Concreteness; | |||
11 | import tools.refinery.store.reasoning.seed.ModelSeed; | 11 | import tools.refinery.store.reasoning.seed.ModelSeed; |
12 | 12 | ||
13 | public class ModelSemantics extends ModelFacade { | 13 | public class ModelSemantics extends ModelFacade { |
14 | public ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | 14 | ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { |
15 | super(problemTrace, store, modelSeed, Concreteness.PARTIAL); | 15 | super(problemTrace, store, modelSeed, Concreteness.PARTIAL); |
16 | } | 16 | } |
17 | } | 17 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java index 2d93a5ad..abfbe7e6 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ProblemLoader.java | |||
@@ -48,21 +48,29 @@ public class ProblemLoader { | |||
48 | return this; | 48 | return this; |
49 | } | 49 | } |
50 | 50 | ||
51 | public Problem loadString(String problemString) throws IOException { | 51 | public Problem loadString(String problemString, URI uri) throws IOException { |
52 | try (var stream = new LazyStringInputStream(problemString)) { | 52 | try (var stream = new LazyStringInputStream(problemString)) { |
53 | return loadStream(stream); | 53 | return loadStream(stream, uri); |
54 | } | 54 | } |
55 | } | 55 | } |
56 | 56 | ||
57 | public Problem loadStream(InputStream inputStream) throws IOException { | 57 | public Problem loadString(String problemString) throws IOException { |
58 | return loadString(problemString, null); | ||
59 | } | ||
60 | |||
61 | public Problem loadStream(InputStream inputStream, URI uri) throws IOException { | ||
58 | var resourceSet = resourceSetProvider.get(); | 62 | var resourceSet = resourceSetProvider.get(); |
59 | var uri = URI.createFileURI("__synthetic." + fileExtension); | 63 | var resourceUri = uri == null ? URI.createFileURI("__synthetic." + fileExtension) : uri; |
60 | var resource = resourceFactory.createResource(uri); | 64 | var resource = resourceFactory.createResource(resourceUri); |
61 | resourceSet.getResources().add(resource); | 65 | resourceSet.getResources().add(resource); |
62 | resource.load(inputStream, Map.of()); | 66 | resource.load(inputStream, Map.of()); |
63 | return loadResource(resource); | 67 | return loadResource(resource); |
64 | } | 68 | } |
65 | 69 | ||
70 | public Problem loadStream(InputStream inputStream) throws IOException { | ||
71 | return loadStream(inputStream, null); | ||
72 | } | ||
73 | |||
66 | public Problem loadFile(File file) throws IOException { | 74 | public Problem loadFile(File file) throws IOException { |
67 | return loadFile(file.getAbsolutePath()); | 75 | return loadFile(file.getAbsolutePath()); |
68 | } | 76 | } |