diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend | 260 |
1 files changed, 260 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend new file mode 100644 index 00000000..fd519c1e --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend | |||
@@ -0,0 +1,260 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy | ||
8 | import java.util.HashMap | ||
9 | |||
10 | class Logic2AlloyLanguageMapper_Containment { | ||
11 | val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
12 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
13 | val Logic2AlloyLanguageMapper base; | ||
14 | public new(Logic2AlloyLanguageMapper base) { | ||
15 | this.base = base | ||
16 | } | ||
17 | |||
18 | def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
19 | // Single root | ||
20 | val rootField = createALSFieldDeclaration => [ | ||
21 | it.name= support.toID(#["util", "root"]) | ||
22 | it.multiplicity = ALSMultiplicity.ONE | ||
23 | it.type = typesOrderedInContainment(containment,trace) | ||
24 | ] | ||
25 | trace.logicLanguageBody.fields += rootField | ||
26 | |||
27 | val contains = createALSFieldDeclaration => [ | ||
28 | it.name = support.toID(#["util", "contains"]) | ||
29 | //it.multiplicity = ALSMultiplicity::SET | ||
30 | it.type = createALSDirectProduct => [ | ||
31 | it.leftMultiplicit = ALSMultiplicity::LONE | ||
32 | it.rightMultiplicit = ALSMultiplicity::SET | ||
33 | it.leftOperand = typesOrderedInContainment(containment,trace) | ||
34 | it.rightOperand = typesOrderedInContainment(containment,trace) | ||
35 | ] | ||
36 | ] | ||
37 | trace.logicLanguageBody.fields += contains | ||
38 | |||
39 | val containmentRelationDefinition = createALSFactDeclaration => [ | ||
40 | it.name = support.toID(#["util", "containmentDefinition"]) | ||
41 | ] | ||
42 | |||
43 | if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) { | ||
44 | val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation| | ||
45 | base.relationMapper.transformRelationReference(relation,trace) | ||
46 | ].toList | ||
47 | |||
48 | containmentRelationDefinition.term = createALSEquals => [ | ||
49 | leftOperand = createALSJoin => [ | ||
50 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
51 | rightOperand = createALSReference => [ referred = contains ]] | ||
52 | rightOperand = support.unfoldPlus(containmentRelations) | ||
53 | ] | ||
54 | } else { | ||
55 | val parent = createALSVariableDeclaration => [ | ||
56 | it.name = "parent" | ||
57 | it.range = typesOrderedInContainment(containment, trace) | ||
58 | ] | ||
59 | val child = createALSVariableDeclaration => [ | ||
60 | it.name = "child" | ||
61 | it.range = typesOrderedInContainment(containment, trace) | ||
62 | ] | ||
63 | |||
64 | val logicFactory = LogiclanguageFactory.eINSTANCE | ||
65 | val logicParentVariable = logicFactory.createVariable | ||
66 | val logicChildVariable = logicFactory.createVariable | ||
67 | val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable] | ||
68 | val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable] | ||
69 | val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)] | ||
70 | val possibleRelations = containment.containmentRelations.map[relation | | ||
71 | base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap) | ||
72 | ] | ||
73 | |||
74 | containmentRelationDefinition.term = createALSQuantifiedEx => [ | ||
75 | it.type = ALSMultiplicity.ALL | ||
76 | it.variables += parent | ||
77 | it.variables += child | ||
78 | it.expression = createALSIff => [ | ||
79 | it.leftOperand = createALSSubset => [ | ||
80 | it.leftOperand = createALSDirectProduct => [ | ||
81 | it.leftOperand = createALSReference => [it.referred = child] | ||
82 | it.rightOperand = createALSReference => [it.referred = parent] | ||
83 | ] | ||
84 | it.rightOperand = createALSJoin => [ | ||
85 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
86 | rightOperand = createALSReference => [ referred = contains ] | ||
87 | ] | ||
88 | ] | ||
89 | it.rightOperand = support.unfoldOr(possibleRelations,trace) | ||
90 | ] | ||
91 | ] | ||
92 | } | ||
93 | |||
94 | trace.specification.factDeclarations += containmentRelationDefinition | ||
95 | |||
96 | // With the exception of the root, every object has at least one parent | ||
97 | // No parent for root | ||
98 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
99 | it.name = support.toID(#["util", "noParentForRoot"]) | ||
100 | it.term = createALSQuantifiedEx => [ | ||
101 | it.type = ALSMultiplicity::NO | ||
102 | val parent = createALSVariableDeclaration => [ | ||
103 | it.name = "parent" | ||
104 | it.range = typesOrderedInContainment(containment,trace) | ||
105 | ] | ||
106 | it.variables += parent | ||
107 | it.expression = createALSSubset => [ | ||
108 | it.leftOperand = createALSDirectProduct => [ | ||
109 | it.leftOperand = createALSReference => [it.referred = parent] | ||
110 | it.rightOperand = createALSJoin => [ | ||
111 | it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] | ||
112 | it.rightOperand = createALSReference => [it.referred = rootField] | ||
113 | ] | ||
114 | ] | ||
115 | it.rightOperand = createALSJoin => [ | ||
116 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
117 | rightOperand = createALSReference => [ referred = contains ] | ||
118 | ] | ||
119 | ] | ||
120 | ] | ||
121 | ] | ||
122 | // Parent for nonroot | ||
123 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
124 | it.name = support.toID(#["util", "atLeastOneParent"]) | ||
125 | it.term = createALSQuantifiedEx => [ | ||
126 | it.type = ALSMultiplicity::ALL | ||
127 | val child = createALSVariableDeclaration => [ | ||
128 | it.name = "child" | ||
129 | it.range = typesOrderedInContainment(containment,trace) | ||
130 | ] | ||
131 | it.variables += child | ||
132 | it.expression = createALSOr => [ | ||
133 | it.leftOperand = createALSEquals => [ | ||
134 | it.leftOperand = createALSReference => [it.referred = child] | ||
135 | it.rightOperand = createALSJoin => [ | ||
136 | it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] | ||
137 | it.rightOperand = createALSReference => [it.referred = rootField] | ||
138 | ] | ||
139 | ] | ||
140 | it.rightOperand = createALSQuantifiedEx => [ | ||
141 | it.type = ALSMultiplicity::SOME | ||
142 | val parent = createALSVariableDeclaration => [ | ||
143 | it.name = "parent" | ||
144 | it.range = typesOrderedInContainment(containment, trace) | ||
145 | ] | ||
146 | it.variables += parent | ||
147 | it.expression = createALSSubset => [ | ||
148 | it.leftOperand = createALSDirectProduct => [ | ||
149 | it.leftOperand = createALSReference => [it.referred = parent] | ||
150 | it.rightOperand = createALSReference => [it.referred = child] | ||
151 | ] | ||
152 | it.rightOperand = createALSJoin => [ | ||
153 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
154 | rightOperand = createALSReference => [ referred = contains ] | ||
155 | ] | ||
156 | ] | ||
157 | ] | ||
158 | ] | ||
159 | ] | ||
160 | ] | ||
161 | |||
162 | // Every object has at most one parent | ||
163 | // trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
164 | // it.name = support.toID(#["util", "atMostOneParent"]) | ||
165 | // it.term = createALSQuantifiedEx => [ | ||
166 | // it.type = ALSMultiplicity::ALL | ||
167 | // val child = createALSVariableDeclaration => [ | ||
168 | // it.name = "child" | ||
169 | // it.range = typesOrderedInContainment(containment,trace) | ||
170 | // ] | ||
171 | // it.variables += child | ||
172 | // it.expression = createALSQuantifiedEx => [ | ||
173 | // it.type = ALSMultiplicity::LONE | ||
174 | // val parent = createALSVariableDeclaration => [ | ||
175 | // it.name = "parent" | ||
176 | // it.range = typesOrderedInContainment(containment, trace) | ||
177 | // ] | ||
178 | // it.variables += parent | ||
179 | // it.expression = createALSFunctionCall => [ | ||
180 | // it.referredDefinition = containmentRelation | ||
181 | // it.params += createALSReference => [ | ||
182 | // it.referred = parent | ||
183 | // it.referred = child | ||
184 | // ] | ||
185 | // ] | ||
186 | // ] | ||
187 | // ] | ||
188 | // ] | ||
189 | |||
190 | // No circle in containment | ||
191 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
192 | it.name = support.toID(#["util", "noCircularContainment"]) | ||
193 | it.term = createALSQuantifiedEx => [ | ||
194 | it.type = ALSMultiplicity::NO | ||
195 | val variable = createALSVariableDeclaration => [ | ||
196 | it.name = "circle" | ||
197 | it.range = typesOrderedInContainment(containment,trace) | ||
198 | ] | ||
199 | it.variables += variable | ||
200 | it.expression = createALSSubset => [ | ||
201 | it.leftOperand = createALSDirectProduct => [ | ||
202 | it.leftOperand = createALSReference => [it.referred = variable] | ||
203 | it.rightOperand = createALSReference => [it.referred = variable] | ||
204 | ] | ||
205 | it.rightOperand = createAlSTransitiveClosure => [ | ||
206 | it.operand = createALSJoin => [ | ||
207 | leftOperand = createALSReference => [referred = trace.logicLanguage] | ||
208 | rightOperand = createALSReference => [ referred = contains ] | ||
209 | ] | ||
210 | ] | ||
211 | ] | ||
212 | ] | ||
213 | ] | ||
214 | |||
215 | } | ||
216 | |||
217 | /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
218 | val types = containment.typesOrderedInHierarchy | ||
219 | val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList | ||
220 | // val uncoveredSignatures = new ArrayList(signaturesInContainment) | ||
221 | // val coveringSignatures = new LinkedList | ||
222 | // | ||
223 | val engine = ViatraQueryEngine.on(new EMFScope(trace.specification)) | ||
224 | //val directSubsetMatcher = DirectSubsetMatcher.on(engine) | ||
225 | // x <= y | ||
226 | val subsetMatcher = SubsetMatcher.on(engine) | ||
227 | |||
228 | if() | ||
229 | }*/ | ||
230 | |||
231 | /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) { | ||
232 | for(signatureInContainment : signaturesInContainment) { | ||
233 | if(!matcher.hasMatch(signatureInContainment,target)) { | ||
234 | return false | ||
235 | } | ||
236 | } | ||
237 | return true | ||
238 | }*/ | ||
239 | |||
240 | /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List<ALSSignatureDeclaration> signaturesInContainment, SubsetMatcher matcher) { | ||
241 | val subtypes = matcher.getAllValuesOfx(target); | ||
242 | for(subType : subtypes) { | ||
243 | val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained | | ||
244 | matcher.hasMatch(subType,contained) | ||
245 | ] | ||
246 | if(!isSubtypeOfASignatureInContainment) { | ||
247 | return false | ||
248 | } | ||
249 | } | ||
250 | return true | ||
251 | }*/ | ||
252 | |||
253 | def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { | ||
254 | val types = containment.typesOrderedInHierarchy | ||
255 | val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten | ||
256 | // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten | ||
257 | val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList | ||
258 | return support.unfoldPlus(typeReferences) | ||
259 | } | ||
260 | } \ No newline at end of file | ||