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/run/MetamodelLoader.xtend | |
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/run/MetamodelLoader.xtend')
-rw-r--r-- | Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend | 63 |
1 files changed, 60 insertions, 3 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 | } |