diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src')
2 files changed, 86 insertions, 441 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old deleted file mode 100644 index 7383904d..00000000 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old +++ /dev/null | |||
@@ -1,428 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher | ||
15 | import java.util.HashMap | ||
16 | import java.util.LinkedHashSet | ||
17 | import java.util.LinkedList | ||
18 | import java.util.List | ||
19 | import java.util.Map | ||
20 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
21 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
22 | import org.eclipse.xtend.lib.annotations.Data | ||
23 | |||
24 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
25 | |||
26 | class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal | ||
27 | implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
28 | public var ALSSignatureDeclaration declaredSupertype | ||
29 | public var ALSSignatureDeclaration definedSupertype | ||
30 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
31 | |||
32 | public val Map<TypeDefinition, ALSSignatureDeclaration> definition2definition = new HashMap | ||
33 | public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap | ||
34 | public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap | ||
35 | public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap | ||
36 | |||
37 | def getAllDefinedTypes() { | ||
38 | return (definition2definition.values) + | ||
39 | (declaration2definition.values) + | ||
40 | (undefined2definition.values) | ||
41 | } | ||
42 | def getAllDeclaredTypes() { | ||
43 | return new2declaration.values | ||
44 | } | ||
45 | |||
46 | public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap; | ||
47 | } | ||
48 | |||
49 | @Data | ||
50 | class DynamicTypeConstraints { | ||
51 | List<List<Type>> positiveCNF | ||
52 | LinkedHashSet<Type> negative | ||
53 | public new() { | ||
54 | this.positiveCNF = new LinkedList | ||
55 | this.negative = new LinkedHashSet | ||
56 | } | ||
57 | def public void addPositiveTypeOptions(List<Type> typeDisjunction) { | ||
58 | this.positiveCNF.add(typeDisjunction) | ||
59 | } | ||
60 | def public void addNegativeTypes(Iterable<Type> negativeTypes) { | ||
61 | this.negative.addAll(negativeTypes) | ||
62 | } | ||
63 | } | ||
64 | |||
65 | /** | ||
66 | * Dynamic types are represented by disjoint sets, and | ||
67 | * static types are represented by the union of the dynamic type sets. | ||
68 | * | ||
69 | * Definition Declaration | ||
70 | * | / \ | ||
71 | * | W/DefinedSuper Wo/DefinedSuper | ||
72 | * | | / \ | ||
73 | * | | undefined2declaration new2declaration | ||
74 | * definition2definition definition2declaration | ||
75 | * +----------------------------------------------------+ +-------------+ | ||
76 | * Defined Declared | ||
77 | */ | ||
78 | class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
79 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
80 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
81 | |||
82 | override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
83 | // 0. Creating the traces | ||
84 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal | ||
85 | trace.typeMapperTrace = typeTrace | ||
86 | /** | ||
87 | * Static type -> list of possible dynamic type map | ||
88 | */ | ||
89 | val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace) | ||
90 | |||
91 | |||
92 | |||
93 | // 1. Transforming the types | ||
94 | |||
95 | // There are two kind of types: | ||
96 | // A: one with defined supertypes (including itself), that only has defined elements | ||
97 | // Those types can have instances only from the defined elements, ie they are subset of problem.elements | ||
98 | // B: one without defined supertypes | ||
99 | // Those types can have instances from two sources | ||
100 | // B.1 from elements that dont have definitions | ||
101 | // B.2 from newly created elements | ||
102 | val allConcreteTypes = problem.types.filter[!it.isAbstract] | ||
103 | val definitions = allConcreteTypes.filter(TypeDefinition).toList | ||
104 | val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList | ||
105 | val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList | ||
106 | |||
107 | // 2. If there are defined elements | ||
108 | if(trace.typeTrace.definedSupertype != null) { | ||
109 | // 3 mapping the elements | ||
110 | problem.elements.transformDefinedSupertype(trace) | ||
111 | // 4. if there are elements that are added to types, then it have to be mapped to defined parts | ||
112 | if(problem.elements.exists[!it.definedInType.empty]) { | ||
113 | definitions.forEach[it.transformDefinition2Definition(trace)] | ||
114 | declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)] | ||
115 | } | ||
116 | // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions | ||
117 | if(problem.elements.exists[it.definedInType.empty]) { | ||
118 | declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)] | ||
119 | } | ||
120 | |||
121 | definedConcreteTypesAreFull(trace) | ||
122 | definedConcreteTypesAreDisjoint(trace) | ||
123 | problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace) | ||
124 | } | ||
125 | |||
126 | // Transforming the declared and defined concrete types | ||
127 | problem.elements.transformDefinedSupertype(trace) | ||
128 | if(trace.typeTrace.definedSupertype != null) { | ||
129 | problem.elements.transformDefinedElements(trace) | ||
130 | declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)] | ||
131 | } | ||
132 | |||
133 | // 2: Caching the types by filling type2AllSignatures | ||
134 | for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) { | ||
135 | val type = typeToConcreteSubtypesEntry.key | ||
136 | val List<ALSSignatureDeclaration> signatures = new LinkedList | ||
137 | |||
138 | } | ||
139 | } | ||
140 | |||
141 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
142 | val res = trace.typeMapperTrace | ||
143 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) { | ||
144 | return res | ||
145 | } else { | ||
146 | throw new IllegalArgumentException(''' | ||
147 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name», | ||
148 | but found «res.class.name»''') | ||
149 | } | ||
150 | } | ||
151 | |||
152 | private def boolean hasDefinedSupertype(Type type) { | ||
153 | if(type instanceof TypeDefinition) { | ||
154 | return true | ||
155 | } else { | ||
156 | if(type.supertypes.empty) return false | ||
157 | else return type.supertypes.exists[it.hasDefinedSupertype] | ||
158 | } | ||
159 | } | ||
160 | |||
161 | private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) { | ||
162 | trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [ | ||
163 | it.name = support.toID(#["util","defined","Object"]) | ||
164 | ] | ||
165 | trace.specification.signatureBodies += createALSSignatureBody => [ | ||
166 | it.abstract = true | ||
167 | it.declarations += trace.typeTrace.definedSupertype | ||
168 | ] | ||
169 | } | ||
170 | |||
171 | private def transformDefinedElements(List<DefinedElement> elements, | ||
172 | Logic2AlloyLanguageMapperTrace trace){ | ||
173 | if(trace.typeTrace.definedSupertype != null) { | ||
174 | // 2. Create elements as singleton signatures subtype of definedSupertype | ||
175 | val elementBodies = createALSSignatureBody => [ | ||
176 | it.multiplicity = ALSMultiplicity::ONE | ||
177 | it.supertype = trace.typeTrace.definedSupertype | ||
178 | ] | ||
179 | trace.specification.signatureBodies += elementBodies | ||
180 | for(element : elements) { | ||
181 | val elementDeclaration = createALSSignatureDeclaration => [ | ||
182 | it.name = support.toIDMultiple(#["element"],element.name) | ||
183 | ] | ||
184 | elementBodies.declarations += elementDeclaration | ||
185 | trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration) | ||
186 | } | ||
187 | // 3. Specify that definedSupertype is equal to the union of specified | ||
188 | /*trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
189 | it.name = support.toID(#["util","typehierarchy","definitionOfElements"]) | ||
190 | it.term = createALSEquals => [ | ||
191 | it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] | ||
192 | it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[ | ||
193 | it.referred = element.lookup(trace.typeTrace.definedElement2Declaration) | ||
194 | ]]) | ||
195 | ] | ||
196 | ]*/ | ||
197 | } | ||
198 | } | ||
199 | |||
200 | ///// Type definitions | ||
201 | |||
202 | protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) { | ||
203 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)] | ||
204 | val body = createALSSignatureBody => [ | ||
205 | it.declarations += sig | ||
206 | it.superset += trace.typeTrace.definedSupertype | ||
207 | ] | ||
208 | trace.specification.signatureBodies += body | ||
209 | trace.typeTrace.definition2definition.put(type,sig) | ||
210 | } | ||
211 | protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
212 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)] | ||
213 | val body = createALSSignatureBody => [ | ||
214 | it.declarations += sig | ||
215 | it.superset += trace.typeTrace.definedSupertype | ||
216 | ] | ||
217 | trace.specification.signatureBodies += body | ||
218 | trace.typeTrace.declaration2definition.put(type,sig) | ||
219 | } | ||
220 | protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
221 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)] | ||
222 | val body = createALSSignatureBody => [ | ||
223 | it.declarations += sig | ||
224 | it.supertype = trace.typeTrace.definedSupertype | ||
225 | ] | ||
226 | trace.specification.signatureBodies += body | ||
227 | trace.typeTrace.undefined2definition.put(type,sig) | ||
228 | } | ||
229 | protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { | ||
230 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)] | ||
231 | val body = createALSSignatureBody => [ | ||
232 | it.declarations += sig | ||
233 | it.supertype = trace.typeTrace.declaredSupertype | ||
234 | ] | ||
235 | trace.specification.signatureBodies += body | ||
236 | trace.typeTrace.new2declaration.put(type,sig) | ||
237 | } | ||
238 | |||
239 | /** | ||
240 | * The dynamic types cover each concrete types | ||
241 | */ | ||
242 | protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) { | ||
243 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
244 | it.name = support.toID(#["util","typehierarchy","elementFull"]) | ||
245 | it.term = createALSEquals => [ | ||
246 | it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] | ||
247 | it.rightOperand = support.unfoldPlus( | ||
248 | trace.typeTrace.allDefinedTypes.map[type| | ||
249 | createALSReference=>[referred = type] | ||
250 | ].toList | ||
251 | ) | ||
252 | ] | ||
253 | ] | ||
254 | |||
255 | } | ||
256 | /** | ||
257 | * The dynamic types are disjoint | ||
258 | */ | ||
259 | protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) { | ||
260 | val types = trace.getTypeTrace.allDefinedTypes.toList | ||
261 | if (types.size >= 2) { | ||
262 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
263 | it.name = support.toID(#["util", "typehierarchy", "elementFull"]) | ||
264 | it.term = types.disjointSets | ||
265 | ] | ||
266 | } | ||
267 | } | ||
268 | /** | ||
269 | * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not | ||
270 | */ | ||
271 | protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) { | ||
272 | val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes) | ||
273 | for(constraintOnElement : constraintOnElements.entrySet) { | ||
274 | val element = constraintOnElement.key | ||
275 | val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration) | ||
276 | val constraint = constraintOnElement.value | ||
277 | |||
278 | var ALSTerm negativeConstraints; | ||
279 | if(constraint.negative.isEmpty) { | ||
280 | negativeConstraints = null | ||
281 | } else { | ||
282 | negativeConstraints = support.unfoldAnd(constraint.negative.map[type| | ||
283 | createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ] | ||
284 | ].toList) | ||
285 | } | ||
286 | |||
287 | var ALSTerm positiveTypeConstraints | ||
288 | if(constraint.positiveCNF.isEmpty) { | ||
289 | positiveTypeConstraints = null | ||
290 | } else { | ||
291 | positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition | | ||
292 | support.unfoldOr(typeConstraintFromDefinition.map[type | | ||
293 | elementInDefinedType(elementSignature,type,trace) | ||
294 | ].toList,trace) | ||
295 | ]) | ||
296 | } | ||
297 | |||
298 | var ALSTerm typeConstraint | ||
299 | if(negativeConstraints != null && positiveTypeConstraints == null) { | ||
300 | typeConstraint = negativeConstraints | ||
301 | } else if (negativeConstraints == null && positiveTypeConstraints != null) { | ||
302 | typeConstraint = positiveTypeConstraints | ||
303 | } else if (negativeConstraints != null && positiveTypeConstraints != null) { | ||
304 | val and = createALSAnd | ||
305 | and.leftOperand = positiveTypeConstraints | ||
306 | and.rightOperand = negativeConstraints | ||
307 | typeConstraint = and | ||
308 | } else { | ||
309 | typeConstraint = null | ||
310 | } | ||
311 | |||
312 | if(typeConstraint != null) { | ||
313 | val fact = createALSFactDeclaration => [ | ||
314 | name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name) | ||
315 | ] | ||
316 | fact.term = typeConstraint | ||
317 | trace.specification.factDeclarations +=fact | ||
318 | } | ||
319 | // otherwise there is no type constraint on element | ||
320 | } | ||
321 | } | ||
322 | |||
323 | private def elementInDefinedType( | ||
324 | ALSSignatureDeclaration elementSignature, | ||
325 | Type type, | ||
326 | Logic2AlloyLanguageMapperTrace trace) | ||
327 | { | ||
328 | var ALSSignatureDeclaration signature | ||
329 | if(type instanceof TypeDeclaration) { | ||
330 | if(trace.typeTrace.declaration2definition.containsKey(type)) { | ||
331 | signature = type.lookup(trace.typeTrace.declaration2definition) | ||
332 | } else if(trace.typeTrace.undefined2definition.containsKey(type)) { | ||
333 | signature = type.lookup(trace.typeTrace.undefined2definition) | ||
334 | } else { | ||
335 | return null | ||
336 | } | ||
337 | } else if(type instanceof TypeDefinition) { | ||
338 | if(trace.typeTrace.definition2definition.containsKey(type)) { | ||
339 | signature = type.lookup(trace.typeTrace.definition2definition) | ||
340 | } else { | ||
341 | return null | ||
342 | } | ||
343 | } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''') | ||
344 | |||
345 | val finalSignature = signature | ||
346 | return createALSSubset => [ | ||
347 | leftOperand = createALSReference => [ | ||
348 | referred = elementSignature | ||
349 | ] | ||
350 | rightOperand = createALSReference => [ | ||
351 | referred = finalSignature | ||
352 | ] | ||
353 | ] | ||
354 | } | ||
355 | |||
356 | def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) { | ||
357 | if(trace.incqueryEngine == null) { | ||
358 | trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) | ||
359 | } | ||
360 | val matcher = SupertypeStarMatcher.on(trace.incqueryEngine) | ||
361 | val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap | ||
362 | for(supertype : problem.types) { | ||
363 | typeToConcreteSubtypes.put( | ||
364 | supertype, | ||
365 | matcher.getAllValuesOfsubtype(supertype) | ||
366 | .filter[!it.isIsAbstract].toList) | ||
367 | } | ||
368 | return typeToConcreteSubtypes | ||
369 | } | ||
370 | |||
371 | /** | ||
372 | * Gives type constraints in a form of CNF | ||
373 | */ | ||
374 | def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) { | ||
375 | val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap | ||
376 | elements.forEach[constraints.put(it,new DynamicTypeConstraints)] | ||
377 | |||
378 | for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) { | ||
379 | val subtypes = type.lookup(typeToConcreteSubtypes) | ||
380 | for(elementInType:type.elements) { | ||
381 | elementInType.lookup(constraints).addPositiveTypeOptions(subtypes) | ||
382 | } | ||
383 | for(elementNotInType:elements.filter[!type.elements.contains(it)]) { | ||
384 | elementNotInType.lookup(constraints).addNegativeTypes(subtypes) | ||
385 | } | ||
386 | } | ||
387 | |||
388 | return constraints | ||
389 | } | ||
390 | |||
391 | private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) { | ||
392 | if(signatures.size >= 2){ | ||
393 | val top = createALSEquals => [ | ||
394 | it.leftOperand = signatures.intersectionOfTypes | ||
395 | it.rightOperand = createALSNone | ||
396 | ] | ||
397 | if(signatures.size > 2) { | ||
398 | return createALSAnd => [ | ||
399 | it.leftOperand = top | ||
400 | it.rightOperand = signatures.subList(1,signatures.size).disjointSets | ||
401 | ] | ||
402 | } else{ | ||
403 | return top | ||
404 | } | ||
405 | } else { | ||
406 | throw new UnsupportedOperationException() | ||
407 | } | ||
408 | } | ||
409 | |||
410 | private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) { | ||
411 | if(signatures.size == 2) { | ||
412 | return createALSIntersection => [ | ||
413 | leftOperand = createALSReference => [it.referred = signatures.get(0)] | ||
414 | rightOperand = createALSReference => [it.referred = signatures.get(1)] | ||
415 | ] | ||
416 | } else if(signatures.size > 2) { | ||
417 | return createALSIntersection => [ | ||
418 | leftOperand = createALSReference => [it.referred = signatures.get(0)] | ||
419 | rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes | ||
420 | ] | ||
421 | } else throw new UnsupportedOperationException() | ||
422 | } | ||
423 | |||
424 | |||
425 | override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
426 | //trace.typeTrace. | ||
427 | } | ||
428 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend index 6533ad36..4d7b50e8 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend | |||
@@ -1,26 +1,88 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
11 | import java.util.Collection | ||
9 | import java.util.HashMap | 12 | import java.util.HashMap |
13 | import java.util.LinkedList | ||
14 | import java.util.List | ||
10 | import java.util.Map | 15 | import java.util.Map |
11 | import java.util.Collection | ||
12 | 16 | ||
13 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { | 17 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { |
14 | val Map<TypeDeclaration,ALSSignatureDeclaration> newElementTypes = new HashMap | 18 | public var ALSSignatureDeclaration objectSupperClass; |
15 | val Map<Type,ALSSignatureDeclaration> definedElementTypes = new HashMap | 19 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; |
16 | var ALSSignatureDeclaration undefinedSupertype | 20 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap |
17 | var ALSSignatureDeclaration definedSupertype | 21 | public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap |
18 | } | 22 | } |
19 | 23 | ||
20 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ | 24 | class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ |
25 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
26 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
27 | |||
28 | new() { | ||
29 | LogicproblemPackage.eINSTANCE.class | ||
30 | } | ||
21 | 31 | ||
22 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | 32 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { |
23 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 33 | if(types.exists[hasDefinedSupertype]) { |
34 | throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''') | ||
35 | } else { | ||
36 | |||
37 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal | ||
38 | trace.typeMapperTrace = typeTrace | ||
39 | |||
40 | // 1. A global type for Objects is created | ||
41 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
42 | val objectBody = createALSSignatureBody => [ | ||
43 | it.declarations += objectSig | ||
44 | it.abstract = true | ||
45 | ] | ||
46 | typeTrace.objectSupperClass = objectSig | ||
47 | trace.specification.signatureBodies += objectBody | ||
48 | |||
49 | // 2. Each type is mapped to a unique sig | ||
50 | for(type : types) { | ||
51 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
52 | val body = createALSSignatureBody => [it.declarations += sig] | ||
53 | body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) | ||
54 | |||
55 | trace.specification.signatureBodies += body | ||
56 | typeTrace.type2ALSType.put(type,sig) | ||
57 | |||
58 | if(type instanceof TypeDefinition) { | ||
59 | val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig] | ||
60 | for(element : type.elements) { | ||
61 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
62 | elementContainer.declarations += signature | ||
63 | |||
64 | } | ||
65 | trace.specification.signatureBodies += elementContainer | ||
66 | } | ||
67 | |||
68 | typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) | ||
69 | } | ||
70 | |||
71 | // 6. Each inheritance is modeled by extend keyword | ||
72 | for(type : types) { | ||
73 | if(type.supertypes.size == 1) { | ||
74 | val alsType = typeTrace.type2ALSType.get(type.supertypes.head) | ||
75 | (type.eContainer as ALSSignatureBody).supertype = alsType | ||
76 | } else if(type.supertypes.size > 1){ | ||
77 | val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) | ||
78 | (type.eContainer as ALSSignatureBody).supertype = alsMainType | ||
79 | for(otherType : type.supertypes.filter[it != alsMainType]) { | ||
80 | typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType)) | ||
81 | } | ||
82 | } | ||
83 | } | ||
84 | |||
85 | } | ||
24 | } | 86 | } |
25 | 87 | ||
26 | private def boolean hasDefinedSupertype(Type type) { | 88 | private def boolean hasDefinedSupertype(Type type) { |
@@ -30,21 +92,32 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L | |||
30 | if(type.supertypes.empty) return false | 92 | if(type.supertypes.empty) return false |
31 | else return type.supertypes.exists[it.hasDefinedSupertype] | 93 | else return type.supertypes.exists[it.hasDefinedSupertype] |
32 | } | 94 | } |
33 | } | 95 | } |
96 | |||
97 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
98 | val res = trace.typeMapperTrace | ||
99 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) { | ||
100 | return res | ||
101 | } else { | ||
102 | throw new IllegalArgumentException(''' | ||
103 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
104 | but found «res.class.name»''') | ||
105 | } | ||
106 | } | ||
34 | 107 | ||
35 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | 108 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { |
36 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 109 | trace.typeTrace.typeSelection.get(referred) |
37 | } | 110 | } |
38 | 111 | ||
39 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | 112 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { |
40 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 113 | trace.typeTrace.objectSupperClass |
41 | } | 114 | } |
42 | 115 | ||
43 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | 116 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { |
44 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 117 | createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)] |
45 | } | 118 | } |
46 | 119 | ||
47 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | 120 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { |
48 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 121 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size |
49 | } | 122 | } |
50 | } \ No newline at end of file | 123 | } \ No newline at end of file |