diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-07 17:26:07 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-05-07 17:26:07 +0200 |
commit | 6a3ff9bb588bf47242a56b91e35479dbba38eb19 (patch) | |
tree | 0432ecd0edafb99dc9f017d0a8cfee31a931583a /Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner | |
parent | Fix concurrency bug in AlloyHandler (diff) | |
download | VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.tar.gz VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.tar.zst VIATRA-Generator-6a3ff9bb588bf47242a56b91e35479dbba38eb19.zip |
Scope unsat benchmarks
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner')
3 files changed, 106 insertions, 16 deletions
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 { | |||
40 | } | 40 | } |
41 | 41 | ||
42 | abstract class MetamodelLoader { | 42 | abstract class MetamodelLoader { |
43 | public static val UNSAT_PREFIX = "unsat_" | ||
44 | |||
43 | protected val ReasonerWorkspace workspace | 45 | protected val ReasonerWorkspace workspace |
44 | 46 | ||
45 | new(ReasonerWorkspace workspace) { | 47 | new(ReasonerWorkspace workspace) { |
@@ -61,6 +63,10 @@ abstract class MetamodelLoader { | |||
61 | def Map<String, TypeQuantiles> getTypeQuantiles() { | 63 | def Map<String, TypeQuantiles> getTypeQuantiles() { |
62 | emptyMap | 64 | emptyMap |
63 | } | 65 | } |
66 | |||
67 | def Map<String, TypeQuantiles> getUnsatTypeQuantiles() { | ||
68 | throw new UnsupportedOperationException("This domain has no type quantiles for unsatisfiable problems") | ||
69 | } | ||
64 | 70 | ||
65 | def List<LinearTypeConstraintHint> getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { | 71 | def List<LinearTypeConstraintHint> getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { |
66 | emptyList | 72 | emptyList |
@@ -136,9 +142,15 @@ class YakinduLoader extends MetamodelLoader { | |||
136 | public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing", | 142 | public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing", |
137 | "choiceHasNoIncoming"] | 143 | "choiceHasNoIncoming"] |
138 | 144 | ||
145 | val boolean satisfiable | ||
146 | |||
139 | new(ReasonerWorkspace workspace) { | 147 | new(ReasonerWorkspace workspace) { |
148 | this(workspace, true) | ||
149 | } | ||
150 | |||
151 | new(ReasonerWorkspace workspace, boolean satisfiable) { | ||
140 | super(workspace) | 152 | super(workspace) |
141 | YakindummPackage.eINSTANCE.eClass | 153 | this.satisfiable = satisfiable |
142 | } | 154 | } |
143 | 155 | ||
144 | def setUseSynchronization(boolean useSynchronization) { | 156 | def setUseSynchronization(boolean useSynchronization) { |
@@ -173,6 +185,8 @@ class YakinduLoader extends MetamodelLoader { | |||
173 | useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] | 185 | useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] |
174 | ].filter [ spec | | 186 | ].filter [ spec | |
175 | useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)] | 187 | useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)] |
188 | ].filter [ | ||
189 | !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX) | ||
176 | ].toList | 190 | ].toList |
177 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet | 191 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet |
178 | val derivedFeatures = new LinkedHashMap | 192 | val derivedFeatures = new LinkedHashMap |
@@ -213,6 +227,19 @@ class YakinduLoader extends MetamodelLoader { | |||
213 | "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581) | 227 | "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581) |
214 | } | 228 | } |
215 | } | 229 | } |
230 | |||
231 | override getUnsatTypeQuantiles() { | ||
232 | #{ | ||
233 | "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979), | ||
234 | "Entry" -> new TypeQuantiles(0.2, 0.4), | ||
235 | "Exit" -> new TypeQuantiles(0, 0), | ||
236 | "FinalState" -> new TypeQuantiles(0, 0), | ||
237 | "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422), | ||
238 | "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926), | ||
239 | // "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043), | ||
240 | "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581) | ||
241 | } | ||
242 | } | ||
216 | 243 | ||
217 | override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { | 244 | override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { |
218 | #[new SGraphHint(ecore2Logic, trace)] | 245 | #[new SGraphHint(ecore2Logic, trace)] |
@@ -276,9 +303,15 @@ class FileSystemLoader extends MetamodelLoader { | |||
276 | } | 303 | } |
277 | 304 | ||
278 | class EcoreLoader extends MetamodelLoader { | 305 | class EcoreLoader extends MetamodelLoader { |
306 | val boolean satisfiable | ||
279 | 307 | ||
280 | new(ReasonerWorkspace workspace) { | 308 | new(ReasonerWorkspace workspace) { |
309 | this(workspace, true) | ||
310 | } | ||
311 | |||
312 | new(ReasonerWorkspace workspace, boolean satisfiable) { | ||
281 | super(workspace) | 313 | super(workspace) |
314 | this.satisfiable = satisfiable | ||
282 | } | 315 | } |
283 | 316 | ||
284 | override loadMetamodel() { | 317 | override loadMetamodel() { |
@@ -307,7 +340,12 @@ class EcoreLoader extends MetamodelLoader { | |||
307 | override loadQueries(EcoreMetamodelDescriptor metamodel) { | 340 | override loadQueries(EcoreMetamodelDescriptor metamodel) { |
308 | val patternGroup = Ecore.instance | 341 | val patternGroup = Ecore.instance |
309 | val patterns = patternGroup.specifications.toList | 342 | val patterns = patternGroup.specifications.toList |
310 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet | 343 | val allWfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet |
344 | val wfPatterns = if (satisfiable) { | ||
345 | allWfPatterns.filter[!it.simpleName.startsWith(UNSAT_PREFIX)].toSet | ||
346 | } else { | ||
347 | allWfPatterns | ||
348 | } | ||
311 | val derivedFeatures = new HashMap | 349 | val derivedFeatures = new HashMap |
312 | return new ViatraQuerySetDescriptor( | 350 | return new ViatraQuerySetDescriptor( |
313 | patterns, | 351 | patterns, |
@@ -346,9 +384,15 @@ class EcoreLoader extends MetamodelLoader { | |||
346 | } | 384 | } |
347 | 385 | ||
348 | class SatelliteLoader extends MetamodelLoader { | 386 | class SatelliteLoader extends MetamodelLoader { |
387 | val boolean satisfiable | ||
349 | 388 | ||
350 | new(ReasonerWorkspace workspace) { | 389 | new(ReasonerWorkspace workspace) { |
390 | this(workspace, true) | ||
391 | } | ||
392 | |||
393 | new(ReasonerWorkspace workspace, boolean satisfiable) { | ||
351 | super(workspace) | 394 | super(workspace) |
395 | this.satisfiable = satisfiable | ||
352 | } | 396 | } |
353 | 397 | ||
354 | override loadMetamodel() { | 398 | override loadMetamodel() { |
@@ -371,7 +415,9 @@ class SatelliteLoader extends MetamodelLoader { | |||
371 | 415 | ||
372 | override loadQueries(EcoreMetamodelDescriptor metamodel) { | 416 | override loadQueries(EcoreMetamodelDescriptor metamodel) { |
373 | val i = SatelliteQueriesAll.instance | 417 | val i = SatelliteQueriesAll.instance |
374 | val patterns = i.specifications.toList | 418 | val patterns = i.specifications.filter [ |
419 | !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX) | ||
420 | ].toList | ||
375 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet | 421 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet |
376 | val derivedFeatures = new LinkedHashMap | 422 | val derivedFeatures = new LinkedHashMap |
377 | val res = new ViatraQuerySetDescriptor( | 423 | val res = new ViatraQuerySetDescriptor( |
@@ -404,4 +450,15 @@ class SatelliteLoader extends MetamodelLoader { | |||
404 | } | 450 | } |
405 | } | 451 | } |
406 | 452 | ||
453 | override getUnsatTypeQuantiles() { | ||
454 | #{ | ||
455 | "CubeSat3U" -> new TypeQuantiles(0.1, 0.25), | ||
456 | "CubeSat6U" -> new TypeQuantiles(0.1, 0.25), | ||
457 | "SmallSat" -> new TypeQuantiles(0.1, 0.25), | ||
458 | "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.1), | ||
459 | "XCommSubsystem" -> new TypeQuantiles(0, 0.1), | ||
460 | "KaCommSubsystem" -> new TypeQuantiles(0, 0.05), | ||
461 | "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25) | ||
462 | } | ||
463 | } | ||
407 | } | 464 | } |
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 { | |||
29 | enum Domain { | 29 | enum Domain { |
30 | fs, | 30 | fs, |
31 | ecore, | 31 | ecore, |
32 | ecoreUnsat, | ||
32 | Yakindu, | 33 | Yakindu, |
34 | YakinduUnsat, | ||
33 | FAM, | 35 | FAM, |
34 | satellite | 36 | satellite, |
37 | satelliteUnsat | ||
35 | } | 38 | } |
36 | 39 | ||
37 | enum Scope { | 40 | enum Scope { |
38 | none, | 41 | none, |
39 | quantiles | 42 | quantiles, |
43 | upperOnly, | ||
44 | unsat, | ||
45 | exactly | ||
40 | } | 46 | } |
41 | 47 | ||
42 | enum Solver { | 48 | enum Solver { |
43 | ViatraSolver, | 49 | ViatraSolver, |
44 | AlloySolver | 50 | AlloySolver, |
51 | AlloyMiniSat | ||
45 | } | 52 | } |
46 | 53 | ||
47 | enum ScopePropagator { | 54 | 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 | |||
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 | } |