From 6a3ff9bb588bf47242a56b91e35479dbba38eb19 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 7 May 2020 17:26:07 +0200 Subject: Scope unsat benchmarks --- .../dslreasoner/run/script/MeasurementScript.xtend | 13 ++++-- .../run/script/MeasurementScriptRunner.xtend | 46 +++++++++++++++++----- 2 files changed, 46 insertions(+), 13 deletions(-) (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script') diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend index 56a65091..f842afb5 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend @@ -29,19 +29,26 @@ class MeasurementScript { enum Domain { fs, ecore, + ecoreUnsat, Yakindu, + YakinduUnsat, FAM, - satellite + satellite, + satelliteUnsat } enum Scope { none, - quantiles + quantiles, + upperOnly, + unsat, + exactly } enum Solver { ViatraSolver, - AlloySolver + AlloySolver, + AlloyMiniSat } enum ScopePropagator { 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 import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory import org.eclipse.xtend.lib.annotations.Data +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver class MeasurementScriptRunner { static val MODEL_SIZE_GAP = 0 @@ -75,9 +76,12 @@ class MeasurementScriptRunner { metamodelLoader = switch (script.domain) { case fs: new FileSystemLoader(inputWorkspace) case ecore: new EcoreLoader(inputWorkspace) + case ecoreUnsat: new EcoreLoader(inputWorkspace, false) case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true] + case YakinduUnsat: new YakinduLoader(inputWorkspace, false) => [useSynchronization = false; useComplexStates = true] case FAM: new FAMLoader(inputWorkspace) case satellite: new SatelliteLoader(inputWorkspace) + case satelliteUnsat: new SatelliteLoader(inputWorkspace, false) default: throw new IllegalArgumentException("Unsupported domain: " + script.domain) } } @@ -191,15 +195,17 @@ class MeasurementScriptRunner { config } - private def createAlloyConfig() { + private def createAlloyConfig(AlloyBackendSolver backendSolver) { val config = new AlloySolverConfiguration + config.solver = backendSolver config } private def createConfig(int modelSize) { val config = switch (solver : script.solver) { case ViatraSolver: createViatraConfig() - case AlloySolver: createAlloyConfig() + case AlloySolver: createAlloyConfig(AlloyBackendSolver.SAT4J) + case AlloyMiniSat: createAlloyConfig(AlloyBackendSolver.MiniSatJNI) default: throw new IllegalArgumentException("Unknown solver: " + solver) } config.solutionScope.numberOfRequiredSolutions = 1 @@ -243,7 +249,8 @@ class MeasurementScriptRunner { val solver = switch (solver : script.solver) { case ViatraSolver: new ViatraReasoner - case AlloySolver: new AlloySolver + case AlloySolver, + case AlloyMiniSat: new AlloySolver default: throw new IllegalArgumentException("Unknown solver: " + solver) } val result = solver.solve(problem, config, outputWorkspace) @@ -284,14 +291,31 @@ class MeasurementScriptRunner { } else { val numberOfKnownElements = knownElements.values.flatten.toSet.size val newElementCount = modelSize - numberOfKnownElements - config.typeScopes.minNewElements = newElementCount - config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP + switch (script.scope) { + case upperOnly: + config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP + case exactly: { + config.typeScopes.minNewElements = newElementCount + config.typeScopes.maxNewElements = newElementCount + } + default: { + config.typeScopes.minNewElements = newElementCount + config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP + } + } } - switch (script.scope) { - case none: + switch (scope : script.scope) { + case none, + case exactly: return - case quantiles: { - val quantiles = metamodelLoader.typeQuantiles + case quantiles, + case unsat, + case upperOnly: { + val quantiles = if (scope == Scope.unsat) { + metamodelLoader.unsatTypeQuantiles + } else { + metamodelLoader.typeQuantiles + } for (eClassInScope : eClassMapper.allClassesInScope(trace)) { val quantile = quantiles.get(eClassInScope.name) if (quantile !== null) { @@ -301,7 +325,9 @@ class MeasurementScriptRunner { val lowCount = Math.floor(modelSize * quantile.low) as int val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int // println('''«type.name» «lowCount» «highCount»''') - config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0)) + if (script.scope != Scope.upperOnly) { + config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0)) + } config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount) } } -- cgit v1.2.3-70-g09d2