blob: 3a7c5041774ac468cb0e68a5f6c0fb7fc4aa581b (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
package hu.bme.mit.inf.dslreasoner.run
import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint
import org.eclipse.viatra.dse.base.ThreadContext
import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
class SGraphInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstraint {
var PartialInterpretation partialInterpretation
var ViatraQueryMatcher<?> noEntry
var ViatraQueryMatcher<?> entryHasNoOutgoing
var ViatraQueryMatcher<?> synchronizationHasNoOutgoing
var ViatraQueryMatcher<?> noSynch
var ViatraQueryMatcher<?> synchronizedSiblingRegions
var ViatraQueryMatcher<?> noStateInRegion
new(ModelGenerationMethod method) {
super(method)
}
override getName() {
return SGraphInconsistencyDetector.simpleName
}
override init(ThreadContext context) {
partialInterpretation = context.model as PartialInterpretation
try{
this.noEntry = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion")
].head.getMatcher(context.queryEngine)
this.entryHasNoOutgoing = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry")
].head.getMatcher(context.queryEngine)
this.synchronizationHasNoOutgoing = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_hasNoOutgoing")
].head.getMatcher(context.queryEngine)
this.noSynch = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noSynch")
].head.getMatcher(context.queryEngine)
this.synchronizedSiblingRegions = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_SynchronizedRegionDoesNotHaveMultipleRegions")
].head.getMatcher(context.queryEngine)
this.noStateInRegion = method.unfinishedWF.filter[
it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion")
].head.getMatcher(context.queryEngine)
} catch(Exception e) { }
}
override checkGlobalConstraint(ThreadContext context) {
if(noEntry !== null) {
val requiredNewObjects =
noEntry.countMatches*2 +
entryHasNoOutgoing.countMatches +
synchronizationHasNoOutgoing.countMatches +
noSynch.countMatches*2 +
synchronizedSiblingRegions.countMatches*4
noStateInRegion.countMatches
val availableNewObjects = partialInterpretation.maxNewElements
val res = availableNewObjects >= requiredNewObjects
//println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''')
return res
} else {
true
}
}
override createNew() {
return new SGraphInconsistencyDetector(this.method)
}
//
// def hasSynchronization() {
// this.partialInterpretation.partialtypeinterpratation.
// }
}
|
