diff options
Diffstat (limited to 'Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution')
3 files changed, 147 insertions, 59 deletions
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend index 35ffaf65..8ea674d3 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/GenerationTaskExecutor.xtend | |||
@@ -133,7 +133,9 @@ class GenerationTaskExecutor { | |||
133 | // 5. create a solver and a configuration | 133 | // 5. create a solver and a configuration |
134 | // 5.1 initialize | 134 | // 5.1 initialize |
135 | val solver = solverLoader.loadSolver(task.solver,configurationMap) | 135 | val solver = solverLoader.loadSolver(task.solver,configurationMap) |
136 | val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,console) | 136 | val objectiveSpecification = scriptExecutor.getObjectiveSpecification(task.objectives) |
137 | val objectiveEntries = objectiveSpecification?.entries ?: emptyList | ||
138 | val solverConfig = solverLoader.loadSolverConfig(task.solver,configurationMap,objectiveEntries,console) | ||
137 | 139 | ||
138 | 140 | ||
139 | // 5.2 set values that defined directly | 141 | // 5.2 set values that defined directly |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend index 0512a5ee..25036df6 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/ScriptExecutor.xtend | |||
@@ -30,6 +30,8 @@ import org.eclipse.core.runtime.Status | |||
30 | import org.eclipse.core.runtime.jobs.Job | 30 | import org.eclipse.core.runtime.jobs.Job |
31 | import org.eclipse.emf.common.util.URI | 31 | import org.eclipse.emf.common.util.URI |
32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
33 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveSpecification | ||
34 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveReference | ||
33 | 35 | ||
34 | @FinalFieldsConstructor | 36 | @FinalFieldsConstructor |
35 | class ScriptExecutor { | 37 | class ScriptExecutor { |
@@ -40,7 +42,7 @@ class ScriptExecutor { | |||
40 | /** | 42 | /** |
41 | * Executes a script | 43 | * Executes a script |
42 | */ | 44 | */ |
43 | public def executeScript(URI uri) { | 45 | def executeScript(URI uri) { |
44 | val job = new Job('''Model Generation: «uri.lastSegment»''') { | 46 | val job = new Job('''Model Generation: «uri.lastSegment»''') { |
45 | override protected run(IProgressMonitor monitor) { | 47 | override protected run(IProgressMonitor monitor) { |
46 | try{ | 48 | try{ |
@@ -57,7 +59,7 @@ class ScriptExecutor { | |||
57 | job.schedule(); | 59 | job.schedule(); |
58 | } | 60 | } |
59 | 61 | ||
60 | public def executeScript(ConfigurationScript script, IProgressMonitor monitor) { | 62 | def executeScript(ConfigurationScript script, IProgressMonitor monitor) { |
61 | script.activateAllEPackageReferences | 63 | script.activateAllEPackageReferences |
62 | val tasks = script.commands.filter(Task) | 64 | val tasks = script.commands.filter(Task) |
63 | 65 | ||
@@ -94,12 +96,12 @@ class ScriptExecutor { | |||
94 | // } | 96 | // } |
95 | } | 97 | } |
96 | 98 | ||
97 | def public dispatch execute(GenerationTask task, IProgressMonitor monitor) { | 99 | def dispatch void execute(GenerationTask task, IProgressMonitor monitor) { |
98 | val generationTaskExecutor = new GenerationTaskExecutor | 100 | val generationTaskExecutor = new GenerationTaskExecutor |
99 | generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) | 101 | generationTaskExecutor.executeGenerationTask(task,this,scriptConsoleFactory,monitor) |
100 | } | 102 | } |
101 | 103 | ||
102 | def public dispatch execute(Task task, IProgressMonitor monitor) { | 104 | def dispatch void execute(Task task, IProgressMonitor monitor) { |
103 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') | 105 | throw new IllegalArgumentException('''Unsupported task type: «task.class.simpleName»!''') |
104 | } | 106 | } |
105 | 107 | ||
@@ -174,6 +176,16 @@ class ScriptExecutor { | |||
174 | null | 176 | null |
175 | } | 177 | } |
176 | 178 | ||
179 | def dispatch getObjectiveSpecification(ObjectiveSpecification config) { | ||
180 | config | ||
181 | } | ||
182 | def dispatch getObjectiveSpecification(ObjectiveReference config) { | ||
183 | config.referred.specification | ||
184 | } | ||
185 | def dispatch getObjectiveSpecification(Void config) { | ||
186 | null | ||
187 | } | ||
188 | |||
177 | def dispatch getConfiguration(ConfigSpecification config) { | 189 | def dispatch getConfiguration(ConfigSpecification config) { |
178 | config | 190 | config |
179 | } | 191 | } |
diff --git a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend index 9eceef5f..f769d46f 100644 --- a/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend +++ b/Application/hu.bme.mit.inf.dslreasoner.application/src/hu/bme/mit/inf/dslreasoner/application/execution/SolverLoader.xtend | |||
@@ -1,44 +1,47 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.application.execution | 1 | package hu.bme.mit.inf.dslreasoner.application.execution |
2 | 2 | ||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver |
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
5 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CostObjectiveFunction | ||
6 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ObjectiveEntry | ||
7 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.OptimizationEntry | ||
6 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver | 8 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.Solver |
9 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ThresholdEntry | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
8 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver | 11 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver |
9 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration | 12 | import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | ||
20 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
21 | import java.util.List | ||
12 | import java.util.Map | 22 | import java.util.Map |
13 | import java.util.Optional | 23 | import java.util.Optional |
24 | import org.eclipse.viatra.query.patternlanguage.emf.vql.PatternModel | ||
25 | import org.eclipse.xtext.EcoreUtil2 | ||
14 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 26 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
15 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | ||
17 | 27 | ||
18 | class SolverLoader { | 28 | class SolverLoader { |
19 | def loadSolver(Solver solver, Map<String, String> config) { | 29 | def loadSolver(Solver solver, Map<String, String> config) { |
20 | switch(solver) { | 30 | switch (solver) { |
21 | case ALLOY_SOLVER: return new AlloySolver | 31 | case ALLOY_SOLVER: return new AlloySolver |
22 | case SMT_SOLVER: return new SMTSolver | 32 | case SMT_SOLVER: return new SMTSolver |
23 | case VIATRA_SOLVER: return new ViatraReasoner | 33 | case VIATRA_SOLVER: return new ViatraReasoner |
24 | } | 34 | } |
25 | } | 35 | } |
26 | 36 | ||
27 | 37 | private def <Type> Optional<Type> getAsType(Map<String, String> config, String key, ScriptConsole console, | |
28 | 38 | Function1<String, Type> parser, Class<Type> requestedType) { | |
29 | private def <Type> Optional<Type> getAsType( | 39 | if (config.containsKey(key)) { |
30 | Map<String, String> config, | ||
31 | String key, | ||
32 | ScriptConsole console, | ||
33 | Function1<String,Type> parser, | ||
34 | Class<Type> requestedType) | ||
35 | { | ||
36 | if(config.containsKey(key)) { | ||
37 | val stringValue = config.get(key) | 40 | val stringValue = config.get(key) |
38 | try{ | 41 | try { |
39 | val parsedValue = parser.apply(stringValue) | 42 | val parsedValue = parser.apply(stringValue) |
40 | return Optional.of(parsedValue) | 43 | return Optional.of(parsedValue) |
41 | } catch(Exception e) { | 44 | } catch (Exception e) { |
42 | console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') | 45 | console.writeError('''Unable to parse configuration value for "«key»" to «requestedType.simpleName»!''') |
43 | return Optional::empty | 46 | return Optional::empty |
44 | } | 47 | } |
@@ -46,60 +49,131 @@ class SolverLoader { | |||
46 | return Optional::empty | 49 | return Optional::empty |
47 | } | 50 | } |
48 | } | 51 | } |
52 | |||
49 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { | 53 | private def getAsInteger(Map<String, String> config, String key, ScriptConsole console) { |
50 | return getAsType(config,key,console,[x|Integer.parseInt(x)],Integer) | 54 | return getAsType(config, key, console, [x|Integer.parseInt(x)], Integer) |
51 | } | 55 | } |
56 | |||
52 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { | 57 | private def getAsBoolean(Map<String, String> config, String key, ScriptConsole console) { |
53 | return getAsType(config,key,console,[x|Boolean.parseBoolean(x)],Boolean) | 58 | return getAsType(config, key, console, [x|Boolean.parseBoolean(x)], Boolean) |
54 | } | 59 | } |
60 | |||
55 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { | 61 | private def getAsDouble(Map<String, String> config, String key, ScriptConsole console) { |
56 | return getAsType(config,key,console,[x|Double.parseDouble(x)],Double) | 62 | return getAsType(config, key, console, [x|Double.parseDouble(x)], Double) |
57 | } | 63 | } |
58 | 64 | ||
59 | def loadSolverConfig( | 65 | def loadSolverConfig(Solver solver, Map<String, String> config, List<ObjectiveEntry> objectiveEntries, |
60 | Solver solver, | 66 | ScriptConsole console) { |
61 | Map<String, String> config, | 67 | switch (solver) { |
62 | ScriptConsole console) | 68 | case ALLOY_SOLVER: { |
63 | { | 69 | if (!objectiveEntries.empty) { |
64 | if(solver === Solver::ALLOY_SOLVER) { | 70 | throw new IllegalArgumentException("Objectives are not supported by Alloy.") |
65 | return new AlloySolverConfiguration => [c| | 71 | } |
66 | config.getAsInteger("symmetry",console) | 72 | val c = new SmtSolverConfiguration |
67 | .ifPresent[c.symmetry = it] | 73 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
68 | config.getAsType("solver",console,[x|AlloyBackendSolver::valueOf(x)],AlloyBackendSolver) | 74 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
69 | .ifPresent[c.solver = it] | 75 | c |
70 | ] | 76 | } |
71 | } else if(solver === Solver::SMT_SOLVER) { | 77 | case SMT_SOLVER: { |
72 | return new SmtSolverConfiguration => [c| | 78 | if (!objectiveEntries.empty) { |
73 | config.getAsBoolean("fixRandomSeed",console).ifPresent[c.fixRandomSeed = it] | 79 | throw new IllegalArgumentException("Objectives are not supported by Z3.") |
74 | config.getAsType("path",console,[it],String).ifPresent[c.solverPath = it] | 80 | } |
75 | ] | 81 | val c = new SmtSolverConfiguration |
76 | } else if(solver === Solver::VIATRA_SOLVER) { | 82 | config.getAsBoolean("fixRandomSeed", console).ifPresent[c.fixRandomSeed = it] |
77 | return new ViatraReasonerConfiguration => [c| | 83 | config.getAsType("path", console, [it], String).ifPresent[c.solverPath = it] |
84 | c | ||
85 | } | ||
86 | case VIATRA_SOLVER: { | ||
87 | val c = new ViatraReasonerConfiguration | ||
78 | c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser | 88 | c.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser |
79 | if(config.containsKey("diversity-range")) { | 89 | if (config.containsKey("diversity-range")) { |
80 | val stringValue = config.get("diversity-range") | 90 | val stringValue = config.get("diversity-range") |
81 | try{ | 91 | try { |
82 | val range = Integer.parseInt(stringValue) | 92 | val range = Integer.parseInt(stringValue) |
83 | c.diversityRequirement = new DiversityDescriptor => [ | 93 | c.diversityRequirement = new DiversityDescriptor => [ |
84 | it.ensureDiversity = true | 94 | it.ensureDiversity = true |
85 | it.range = range | 95 | it.range = range |
86 | ] | 96 | ] |
87 | } catch (NumberFormatException e) {console.writeError('''Malformed number format: «e.message»''')} | 97 | } catch (NumberFormatException e) { |
98 | console.writeError('''Malformed number format: «e.message»''') | ||
99 | } | ||
88 | } | 100 | } |
89 | ] | 101 | for (objectiveEntry : objectiveEntries) { |
90 | } else { | 102 | val costObjectiveConfig = new CostObjectiveConfiguration |
91 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | 103 | switch (objectiveEntry) { |
104 | OptimizationEntry: { | ||
105 | costObjectiveConfig.findExtremum = true | ||
106 | costObjectiveConfig.kind = switch (direction : objectiveEntry.direction) { | ||
107 | case MAXIMIZE: | ||
108 | ObjectiveKind.HIGHER_IS_BETTER | ||
109 | case MINIMIZE: | ||
110 | ObjectiveKind.LOWER_IS_BETTER | ||
111 | default: | ||
112 | throw new IllegalArgumentException("Unknown direction: " + direction) | ||
113 | } | ||
114 | costObjectiveConfig.threshold = ObjectiveThreshold.NO_THRESHOLD | ||
115 | } | ||
116 | ThresholdEntry: { | ||
117 | costObjectiveConfig.findExtremum = false | ||
118 | val threshold = objectiveEntry.threshold.doubleValue | ||
119 | switch (operator : objectiveEntry.operator) { | ||
120 | case LESS: { | ||
121 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
122 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
123 | } | ||
124 | case GREATER: { | ||
125 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
126 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
127 | } | ||
128 | case LESS_EQUALS: { | ||
129 | costObjectiveConfig.kind = ObjectiveKind.LOWER_IS_BETTER | ||
130 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
131 | } | ||
132 | case GREATER_EQUALS: { | ||
133 | costObjectiveConfig.kind = ObjectiveKind.HIGHER_IS_BETTER | ||
134 | costObjectiveConfig.threshold = new ObjectiveThreshold.Exclusive(threshold) | ||
135 | } | ||
136 | default: | ||
137 | throw new IllegalArgumentException("Unknown operator: " + operator) | ||
138 | } | ||
139 | } | ||
140 | } | ||
141 | val function = objectiveEntry.function | ||
142 | if (function instanceof CostObjectiveFunction) { | ||
143 | for (costEntry : function.entries) { | ||
144 | val element = new CostObjectiveElementConfiguration | ||
145 | val pattern = costEntry.patternElement.pattern | ||
146 | val packageName = costEntry.patternElement.package?.packageName ?: | ||
147 | EcoreUtil2.getContainerOfType(pattern, PatternModel)?.packageName | ||
148 | element.patternQualifiedName = if (packageName.nullOrEmpty) { | ||
149 | pattern.name | ||
150 | } else { | ||
151 | packageName + "." + pattern.name | ||
152 | } | ||
153 | costObjectiveConfig.elements += element | ||
154 | } | ||
155 | } else { | ||
156 | throw new IllegalArgumentException("Only cost objectives are supported by VIATRA.") | ||
157 | } | ||
158 | c.costObjectives += costObjectiveConfig | ||
159 | } | ||
160 | c | ||
161 | } | ||
162 | default: | ||
163 | throw new UnsupportedOperationException('''Unknown solver: «solver»''') | ||
92 | } | 164 | } |
93 | } | 165 | } |
94 | 166 | ||
95 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 167 | def dispatch void setRunIndex(AlloySolverConfiguration config, Map<String, String> parameters, int runIndex, |
96 | parameters.getAsBoolean("randomize",console).ifPresent[ | 168 | ScriptConsole console) { |
97 | if(it) { | 169 | parameters.getAsBoolean("randomize", console).ifPresent [ |
98 | config.randomise = runIndex-1 | 170 | if (it) { |
171 | config.randomise = runIndex - 1 | ||
99 | } | 172 | } |
100 | ] | 173 | ] |
101 | } | 174 | } |
102 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, ScriptConsole console) { | 175 | |
103 | 176 | def dispatch void setRunIndex(LogicSolverConfiguration config, Map<String, String> parameters, int runIndex, | |
177 | ScriptConsole console) { | ||
104 | } | 178 | } |
105 | } \ No newline at end of file | 179 | } |