1 files changed, 53 insertions, 48 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_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 4d7b50e8..92ac27df 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
@@ -30,58 +30,62 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
        }
        
        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
-                if(types.exists[hasDefinedSupertype]) {
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
-                        throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''')
+                trace.typeMapperTrace = typeTrace
-                } else {
+                
-                        
+                // 1. A global type for Objects is created
-                        val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
+                val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
-                        trace.typeMapperTrace = typeTrace
+                val objectBody = createALSSignatureBody => [
+                        it.declarations += objectSig
+                        it.abstract = true
+                ]
+                typeTrace.objectSupperClass = objectSig
+                trace.specification.signatureBodies += objectBody
+                
+                // 2. Each type is mapped to a unique sig
+                for(type : types) {
+                        val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
+                        val body = createALSSignatureBody => [it.declarations += sig]
+                        body.abstract = type.isIsAbstract || (type instanceof TypeDefinition)
                        
-                        // 1. A global type for Objects is created
+                        trace.specification.signatureBodies += body
-                        val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
+                        typeTrace.type2ALSType.put(type,sig)
-                        val objectBody = createALSSignatureBody => [
-                                it.declarations += objectSig
-                                it.abstract = true
-                        ]
-                        typeTrace.objectSupperClass = objectSig
-                        trace.specification.signatureBodies += objectBody
                        
-                        // 2. Each type is mapped to a unique sig
+                        typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
-                        for(type : types) {
+                }
-                                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
+                
-                                val body = createALSSignatureBody => [it.declarations += sig]
+                for(element : elements) {
-                                body.abstract = type.isIsAbstract || (type instanceof TypeDefinition)
+                        val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty]
-                                
+                        if(mostSpecificTypes.size== 1) {
-                                trace.specification.signatureBodies += body
+                                val mostSpecificSubtype = mostSpecificTypes.head
-                                typeTrace.type2ALSType.put(type,sig)
+                                val elementContainer = createALSSignatureBody => [
-                                
+                                        it.multiplicity = ALSMultiplicity::ONE
-                                if(type instanceof TypeDefinition) {
+                                        it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype)
-                                        val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig]
+                                ]
-                                        for(element : type.elements) {
+                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
-                                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
+                                elementContainer.declarations += signature
-                                                elementContainer.declarations += signature
+                                typeTrace.definedElement2Declaration.put(element,signature)
-                                                
+                                trace.specification.signatureBodies += elementContainer
-                                        }
+                        } else {
-                                        trace.specification.signatureBodies += elementContainer
+                                throw new UnsupportedOperationException
-                                }
-                                
-                                typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
                        }
-                        
+                }
-                        // 6. Each inheritance is modeled by extend keyword
+                
-                        for(type : types) {
+                // 6. Each inheritance is modeled by extend keyword
-                                if(type.supertypes.size == 1) {
+                for(type : types) {
-                                        val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
+                        if(type.supertypes.size == 0) {
-                                        (type.eContainer as ALSSignatureBody).supertype = alsType
+                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass
-                                } else if(type.supertypes.size > 1){
+                        }if(type.supertypes.size == 1) {
-                                        val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
+                                val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
-                                        (type.eContainer as ALSSignatureBody).supertype = alsMainType
+                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType
-                                        for(otherType : type.supertypes.filter[it != alsMainType]) {
+                                
-                                                typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType))
+                        } else if(type.supertypes.size > 1){
-                                        }
+                                val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
+                                (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType
+                                for(otherType : type.supertypes.filter[it != alsMainType]) {
+                                        typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type))
                                }
                        }
-                                
                }
        }
        
@@ -114,7 +118,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
        }
        
        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
-                createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)]
+                val r =  trace.typeTrace.definedElement2Declaration.get(referred)
+                return createALSReference => [it.referred =r]
        }
        
        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {

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 4d7b50e8..92ac27df 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
@@ -30,58 +30,62 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
30	}	30	}
31		31
32	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) {
33	if(types.exists[hasDefinedSupertype]) {	33	val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
34	throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''')	34	trace.typeMapperTrace = typeTrace
35	} else {	35
36		36	// 1. A global type for Objects is created
37	val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal	37	val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
38	trace.typeMapperTrace = typeTrace	38	val objectBody = createALSSignatureBody => [
		39	it.declarations += objectSig
		40	it.abstract = true
		41	]
		42	typeTrace.objectSupperClass = objectSig
		43	trace.specification.signatureBodies += objectBody
		44
		45	// 2. Each type is mapped to a unique sig
		46	for(type : types) {
		47	val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
		48	val body = createALSSignatureBody => [it.declarations += sig]
		49	body.abstract = type.isIsAbstract \|\| (type instanceof TypeDefinition)
39		50
40	// 1. A global type for Objects is created	51	trace.specification.signatureBodies += body
41	val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]	52	typeTrace.type2ALSType.put(type,sig)
42	val objectBody = createALSSignatureBody => [
43	it.declarations += objectSig
44	it.abstract = true
45	]
46	typeTrace.objectSupperClass = objectSig
47	trace.specification.signatureBodies += objectBody
48		53
49	// 2. Each type is mapped to a unique sig	54	typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
50	for(type : types) {	55	}
51	val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]	56
52	val body = createALSSignatureBody => [it.declarations += sig]	57	for(element : elements) {
53	body.abstract = type.isIsAbstract \|\| (type instanceof TypeDefinition)	58	val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty]
54		59	if(mostSpecificTypes.size== 1) {
55	trace.specification.signatureBodies += body	60	val mostSpecificSubtype = mostSpecificTypes.head
56	typeTrace.type2ALSType.put(type,sig)	61	val elementContainer = createALSSignatureBody => [
57		62	it.multiplicity = ALSMultiplicity::ONE
58	if(type instanceof TypeDefinition) {	63	it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype)
59	val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig]	64	]
60	for(element : type.elements) {	65	val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
61	val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]	66	elementContainer.declarations += signature
62	elementContainer.declarations += signature	67	typeTrace.definedElement2Declaration.put(element,signature)
63		68	trace.specification.signatureBodies += elementContainer
64	}	69	} else {
65	trace.specification.signatureBodies += elementContainer	70	throw new UnsupportedOperationException
66	}
67
68	typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
69	}	71	}
70		72	}
71	// 6. Each inheritance is modeled by extend keyword	73
72	for(type : types) {	74	// 6. Each inheritance is modeled by extend keyword
73	if(type.supertypes.size == 1) {	75	for(type : types) {
74	val alsType = typeTrace.type2ALSType.get(type.supertypes.head)	76	if(type.supertypes.size == 0) {
75	(type.eContainer as ALSSignatureBody).supertype = alsType	77	(typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass
76	} else if(type.supertypes.size > 1){	78	}if(type.supertypes.size == 1) {
77	val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)	79	val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
78	(type.eContainer as ALSSignatureBody).supertype = alsMainType	80	(typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType
79	for(otherType : type.supertypes.filter[it != alsMainType]) {	81
80	typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType))	82	} else if(type.supertypes.size > 1){
81	}	83	val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
		84	(typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType
		85	for(otherType : type.supertypes.filter[it != alsMainType]) {
		86	typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type))
82	}	87	}
83	}	88	}
84
85	}	89	}
86	}	90	}
87		91
@@ -114,7 +118,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
114	}	118	}
115		119
116	override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {	120	override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
117	createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)]	121	val r = trace.typeTrace.definedElement2Declaration.get(referred)
		122	return createALSReference => [it.referred =r]
118	}	123	}
119		124
120	override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {	125	override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {