aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend
blob: 230bb69285dedda143ddf1b61dc5a58d144c9be9 (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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
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<?>  choiceHasNoOutgiong
	var ViatraQueryMatcher<?>  choiceHasNoIncoming
	//var ViatraQueryMatcher<?> noSynch
	var ViatraQueryMatcher<?> synchronizationHasNoOutgoing
	
	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.noStateInRegion = method.unfinishedWF.filter[
				it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion")
			].head.getMatcher(context.queryEngine)
			
			this.choiceHasNoOutgiong = method.unfinishedWF.filter[
				it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoOutgoing")
			].head.getMatcher(context.queryEngine)
			
//			this.choiceHasNoIncoming = method.unfinishedWF.filter[
//				it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoIncoming")
//			].head.getMatcher(context.queryEngine)
		} catch(Exception e) {	}
		try{
//			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.synchronizationHasNoOutgoing = method.unfinishedWF.filter[
				it.fullyQualifiedName.equals("unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_synchHasNoOutgoing")
			].head.getMatcher(context.queryEngine)
		} catch(Exception e) {	}
	}
	
	override checkGlobalConstraint(ThreadContext context) {
		if(noEntry !== null) {
			var requiredNewObjects = 
				noEntry.countMatches*2 +
				entryHasNoOutgoing.countMatches + 
				choiceHasNoOutgiong.countMatches+
				//choiceHasNoIncoming.countMatches+
				noStateInRegion.countMatches
			if(synchronizationHasNoOutgoing!= null) {
				requiredNewObjects += 
					//noSynch.countMatches*2 + 
					synchronizationHasNoOutgoing.countMatches +
					synchronizedSiblingRegions.countMatches*4 
			}
				
			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.
//	}
}