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 --- ..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 ------ .../configs/Yakindu.json | 13 +++++ ..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 17 ------ .../configs/ecore.json | 17 ++++++ ..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 ------ ..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 16 ------ .../configs/satellite.json | 17 ++++++ ..._ViatraSolver_polyhedral_typeHierarchy_Clp.json | 17 ------ .../mit/inf/dslreasoner/run/MetamodelLoader.xtend | 63 ++++++++++++++++++++-- .../dslreasoner/run/script/MeasurementScript.xtend | 13 +++-- .../run/script/MeasurementScriptRunner.xtend | 46 ++++++++++++---- 11 files changed, 153 insertions(+), 98 deletions(-) delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json create mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json delete mode 100644 Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json (limited to 'Tests') diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json deleted file mode 100644 index 1e2d4dd4..00000000 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/FAM_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json +++ /dev/null @@ -1,16 +0,0 @@ -{ - "inputPath": "initialModels", - "outputPath": "outputModels", - "timeout": 1200, - "saveModels": true, - "warmupIterations": 0, - "iterations": 5, - "domain": "FAM", - "scope": "none", - "sizes": [500], - "solver": "ViatraSolver", - "scopePropagator": "polyhedral", - "propagatedConstraints": "hints", - "polyhedronSolver": "Clp", - "scopeHeuristics": "polyhedral" -} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json new file mode 100644 index 00000000..b602f2fe --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu.json @@ -0,0 +1,13 @@ +{ + "inputPath": "initialModels", + "outputPath": "outputModels", + "timeout": 300, + "saveModels": true, + "saveTemporaryFiles": false, + "warmupIterations": 0, + "iterations": 30, + "domain": "Yakindu", + "scope": "unsat", + "sizes": [20], + "solver": "AlloySolver" +} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json deleted file mode 100644 index b4d51684..00000000 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/Yakindu_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json +++ /dev/null @@ -1,17 +0,0 @@ -{ - "inputPath": "initialModels", - "outputPath": "outputModels", - "timeout": 1200, - "saveModels": false, - "saveTemporaryFiles": true, - "warmupIterations": 0, - "iterations": 5, - "domain": "Yakindu", - "scope": "none", - "sizes": [100], - "solver": "ViatraSolver", - "scopePropagator": "polyhedral", - "propagatedConstraints": "hints", - "polyhedronSolver": "Clp", - "scopeHeuristic": "polyhedral" -} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json new file mode 100644 index 00000000..36fb0ea2 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore.json @@ -0,0 +1,17 @@ +{ + "inputPath": "initialModels", + "outputPath": "outputModels", + "timeout": 300, + "saveModels": true, + "saveTemporaryFiles": false, + "warmupIterations": 0, + "iterations": 1, + "domain": "ecoreUnsat", + "scope": "none", + "sizes": [5, 10, 20, 30, 40, 50], + "solver": "ViatraSolver", + "scopePropagator": "polyhedral", + "propagatedConstraints": "hints", + "polyhedronSolver": "Clp", + "scopeHeuristic": "polyhedral" +} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json deleted file mode 100644 index 72e97957..00000000 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/ecore_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json +++ /dev/null @@ -1,16 +0,0 @@ -{ - "inputPath": "initialModels", - "outputPath": "outputModels", - "timeout": 1200, - "saveModels": true, - "warmupIterations": 0, - "iterations": 5, - "domain": "ecore", - "scope": "quantiles", - "sizes": [50], - "solver": "ViatraSolver", - "scopePropagator": "polyhedral", - "propagatedConstraints": "hints", - "polyhedronSolver": "Clp", - "scopeHeuristic": "polyhedral" -} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json deleted file mode 100644 index a7e29a22..00000000 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/fs_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json +++ /dev/null @@ -1,16 +0,0 @@ -{ - "inputPath": "initialModels", - "outputPath": "outputModels", - "timeout": 1200, - "saveModels": true, - "warmupIterations": 1, - "iterations": 1, - "domain": "fs", - "scope": "none", - "sizes": [50, 100, 150, 200, 250, 300, 350, 400, 450, 500], - "solver": "ViatraSolver", - "scopePropagator": "polyhedral", - "propagatedConstraints": "hints", - "polyhedronSolver": "Clp", - "scopeHeuristic": "polyhedral" -} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json new file mode 100644 index 00000000..16abb5d0 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite.json @@ -0,0 +1,17 @@ +{ + "inputPath": "initialModels", + "outputPath": "outputModels", + "timeout": 300, + "saveModels": true, + "saveTemporaryFiles": false, + "warmupIterations": 0, + "iterations": 30, + "domain": "satelliteUnsat", + "scope": "none", + "sizes": [10], + "solver": "ViatraSolver", + "scopePropagator": "polyhedral", + "propagatedConstraints": "hints", + "polyhedronSolver": "Clp", + "scopeHeuristic": "polyhedral" +} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json b/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json deleted file mode 100644 index d5469948..00000000 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/configs/satellite_useful_ViatraSolver_polyhedral_typeHierarchy_Clp.json +++ /dev/null @@ -1,17 +0,0 @@ -{ - "inputPath": "initialModels", - "outputPath": "outputModels", - "timeout": 120, - "saveModels": true, - "saveTemporaryFiles": true, - "warmupIterations": 0, - "iterations": 1, - "domain": "Yakindu", - "scope": "quantiles", - "sizes": [10, 20, 30, 40, 50, 60, 70, 80, 90, 100], - "solver": "ViatraSolver", - "scopePropagator": "polyhedral", - "propagatedConstraints": "hints", - "polyhedronSolver": "Clp", - "scopeHeuristic": "polyhedral" -} diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend index 1be03eed..bf9ca274 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend @@ -40,6 +40,8 @@ class TypeQuantiles { } abstract class MetamodelLoader { + public static val UNSAT_PREFIX = "unsat_" + protected val ReasonerWorkspace workspace new(ReasonerWorkspace workspace) { @@ -61,6 +63,10 @@ abstract class MetamodelLoader { def Map getTypeQuantiles() { emptyMap } + + def Map getUnsatTypeQuantiles() { + throw new UnsupportedOperationException("This domain has no type quantiles for unsatisfiable problems") + } def List getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { emptyList @@ -136,9 +142,15 @@ class YakinduLoader extends MetamodelLoader { public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing", "choiceHasNoIncoming"] + val boolean satisfiable + new(ReasonerWorkspace workspace) { + this(workspace, true) + } + + new(ReasonerWorkspace workspace, boolean satisfiable) { super(workspace) - YakindummPackage.eINSTANCE.eClass + this.satisfiable = satisfiable } def setUseSynchronization(boolean useSynchronization) { @@ -173,6 +185,8 @@ class YakinduLoader extends MetamodelLoader { useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] ].filter [ spec | useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)] + ].filter [ + !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX) ].toList val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet val derivedFeatures = new LinkedHashMap @@ -213,6 +227,19 @@ class YakinduLoader extends MetamodelLoader { "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581) } } + + override getUnsatTypeQuantiles() { + #{ + "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979), + "Entry" -> new TypeQuantiles(0.2, 0.4), + "Exit" -> new TypeQuantiles(0, 0), + "FinalState" -> new TypeQuantiles(0, 0), + "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422), + "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926), +// "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043), + "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581) + } + } override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { #[new SGraphHint(ecore2Logic, trace)] @@ -276,9 +303,15 @@ class FileSystemLoader extends MetamodelLoader { } class EcoreLoader extends MetamodelLoader { + val boolean satisfiable new(ReasonerWorkspace workspace) { + this(workspace, true) + } + + new(ReasonerWorkspace workspace, boolean satisfiable) { super(workspace) + this.satisfiable = satisfiable } override loadMetamodel() { @@ -307,7 +340,12 @@ class EcoreLoader extends MetamodelLoader { override loadQueries(EcoreMetamodelDescriptor metamodel) { val patternGroup = Ecore.instance val patterns = patternGroup.specifications.toList - val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet + val allWfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet + val wfPatterns = if (satisfiable) { + allWfPatterns.filter[!it.simpleName.startsWith(UNSAT_PREFIX)].toSet + } else { + allWfPatterns + } val derivedFeatures = new HashMap return new ViatraQuerySetDescriptor( patterns, @@ -346,9 +384,15 @@ class EcoreLoader extends MetamodelLoader { } class SatelliteLoader extends MetamodelLoader { + val boolean satisfiable new(ReasonerWorkspace workspace) { + this(workspace, true) + } + + new(ReasonerWorkspace workspace, boolean satisfiable) { super(workspace) + this.satisfiable = satisfiable } override loadMetamodel() { @@ -371,7 +415,9 @@ class SatelliteLoader extends MetamodelLoader { override loadQueries(EcoreMetamodelDescriptor metamodel) { val i = SatelliteQueriesAll.instance - val patterns = i.specifications.toList + val patterns = i.specifications.filter [ + !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX) + ].toList val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet val derivedFeatures = new LinkedHashMap val res = new ViatraQuerySetDescriptor( @@ -404,4 +450,15 @@ class SatelliteLoader extends MetamodelLoader { } } + override getUnsatTypeQuantiles() { + #{ + "CubeSat3U" -> new TypeQuantiles(0.1, 0.25), + "CubeSat6U" -> new TypeQuantiles(0.1, 0.25), + "SmallSat" -> new TypeQuantiles(0.1, 0.25), + "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.1), + "XCommSubsystem" -> new TypeQuantiles(0, 0.1), + "KaCommSubsystem" -> new TypeQuantiles(0, 0.05), + "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25) + } + } } 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-54-g00ecf