diff options
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend')
-rw-r--r-- | Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend | 46 |
1 files changed, 36 insertions, 10 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend index 1127f01a..973c3d13 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend | |||
@@ -54,6 +54,7 @@ import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandalone | |||
54 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions | 54 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions |
55 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | 55 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory |
56 | import org.eclipse.xtend.lib.annotations.Data | 56 | import org.eclipse.xtend.lib.annotations.Data |
57 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
57 | 58 | ||
58 | class MeasurementScriptRunner { | 59 | class MeasurementScriptRunner { |
59 | static val MODEL_SIZE_GAP = 0 | 60 | static val MODEL_SIZE_GAP = 0 |
@@ -75,9 +76,12 @@ class MeasurementScriptRunner { | |||
75 | metamodelLoader = switch (script.domain) { | 76 | metamodelLoader = switch (script.domain) { |
76 | case fs: new FileSystemLoader(inputWorkspace) | 77 | case fs: new FileSystemLoader(inputWorkspace) |
77 | case ecore: new EcoreLoader(inputWorkspace) | 78 | case ecore: new EcoreLoader(inputWorkspace) |
79 | case ecoreUnsat: new EcoreLoader(inputWorkspace, false) | ||
78 | case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true] | 80 | case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true] |
81 | case YakinduUnsat: new YakinduLoader(inputWorkspace, false) => [useSynchronization = false; useComplexStates = true] | ||
79 | case FAM: new FAMLoader(inputWorkspace) | 82 | case FAM: new FAMLoader(inputWorkspace) |
80 | case satellite: new SatelliteLoader(inputWorkspace) | 83 | case satellite: new SatelliteLoader(inputWorkspace) |
84 | case satelliteUnsat: new SatelliteLoader(inputWorkspace, false) | ||
81 | default: throw new IllegalArgumentException("Unsupported domain: " + script.domain) | 85 | default: throw new IllegalArgumentException("Unsupported domain: " + script.domain) |
82 | } | 86 | } |
83 | } | 87 | } |
@@ -191,15 +195,17 @@ class MeasurementScriptRunner { | |||
191 | config | 195 | config |
192 | } | 196 | } |
193 | 197 | ||
194 | private def createAlloyConfig() { | 198 | private def createAlloyConfig(AlloyBackendSolver backendSolver) { |
195 | val config = new AlloySolverConfiguration | 199 | val config = new AlloySolverConfiguration |
200 | config.solver = backendSolver | ||
196 | config | 201 | config |
197 | } | 202 | } |
198 | 203 | ||
199 | private def createConfig(int modelSize) { | 204 | private def createConfig(int modelSize) { |
200 | val config = switch (solver : script.solver) { | 205 | val config = switch (solver : script.solver) { |
201 | case ViatraSolver: createViatraConfig() | 206 | case ViatraSolver: createViatraConfig() |
202 | case AlloySolver: createAlloyConfig() | 207 | case AlloySolver: createAlloyConfig(AlloyBackendSolver.SAT4J) |
208 | case AlloyMiniSat: createAlloyConfig(AlloyBackendSolver.MiniSatJNI) | ||
203 | default: throw new IllegalArgumentException("Unknown solver: " + solver) | 209 | default: throw new IllegalArgumentException("Unknown solver: " + solver) |
204 | } | 210 | } |
205 | config.solutionScope.numberOfRequiredSolutions = 1 | 211 | config.solutionScope.numberOfRequiredSolutions = 1 |
@@ -243,7 +249,8 @@ class MeasurementScriptRunner { | |||
243 | 249 | ||
244 | val solver = switch (solver : script.solver) { | 250 | val solver = switch (solver : script.solver) { |
245 | case ViatraSolver: new ViatraReasoner | 251 | case ViatraSolver: new ViatraReasoner |
246 | case AlloySolver: new AlloySolver | 252 | case AlloySolver, |
253 | case AlloyMiniSat: new AlloySolver | ||
247 | default: throw new IllegalArgumentException("Unknown solver: " + solver) | 254 | default: throw new IllegalArgumentException("Unknown solver: " + solver) |
248 | } | 255 | } |
249 | val result = solver.solve(problem, config, outputWorkspace) | 256 | val result = solver.solve(problem, config, outputWorkspace) |
@@ -284,14 +291,31 @@ class MeasurementScriptRunner { | |||
284 | } else { | 291 | } else { |
285 | val numberOfKnownElements = knownElements.values.flatten.toSet.size | 292 | val numberOfKnownElements = knownElements.values.flatten.toSet.size |
286 | val newElementCount = modelSize - numberOfKnownElements | 293 | val newElementCount = modelSize - numberOfKnownElements |
287 | config.typeScopes.minNewElements = newElementCount | 294 | switch (script.scope) { |
288 | config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP | 295 | case upperOnly: |
296 | config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP | ||
297 | case exactly: { | ||
298 | config.typeScopes.minNewElements = newElementCount | ||
299 | config.typeScopes.maxNewElements = newElementCount | ||
300 | } | ||
301 | default: { | ||
302 | config.typeScopes.minNewElements = newElementCount | ||
303 | config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP | ||
304 | } | ||
305 | } | ||
289 | } | 306 | } |
290 | switch (script.scope) { | 307 | switch (scope : script.scope) { |
291 | case none: | 308 | case none, |
309 | case exactly: | ||
292 | return | 310 | return |
293 | case quantiles: { | 311 | case quantiles, |
294 | val quantiles = metamodelLoader.typeQuantiles | 312 | case unsat, |
313 | case upperOnly: { | ||
314 | val quantiles = if (scope == Scope.unsat) { | ||
315 | metamodelLoader.unsatTypeQuantiles | ||
316 | } else { | ||
317 | metamodelLoader.typeQuantiles | ||
318 | } | ||
295 | for (eClassInScope : eClassMapper.allClassesInScope(trace)) { | 319 | for (eClassInScope : eClassMapper.allClassesInScope(trace)) { |
296 | val quantile = quantiles.get(eClassInScope.name) | 320 | val quantile = quantiles.get(eClassInScope.name) |
297 | if (quantile !== null) { | 321 | if (quantile !== null) { |
@@ -301,7 +325,9 @@ class MeasurementScriptRunner { | |||
301 | val lowCount = Math.floor(modelSize * quantile.low) as int | 325 | val lowCount = Math.floor(modelSize * quantile.low) as int |
302 | val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int | 326 | val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int |
303 | // println('''«type.name» «lowCount» «highCount»''') | 327 | // println('''«type.name» «lowCount» «highCount»''') |
304 | config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0)) | 328 | if (script.scope != Scope.upperOnly) { |
329 | config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0)) | ||
330 | } | ||
305 | config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount) | 331 | config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount) |
306 | } | 332 | } |
307 | } | 333 | } |