Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
1 files changed, 268 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_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
new file mode 100644
index 00000000..ade9860b
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,268 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import java.util.ArrayList
+import java.util.Collection
+import java.util.HashMap
+import java.util.List
+import java.util.Map
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace
+{
+        public var ALSSignatureDeclaration objectSupperClass;
+        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+}
+/**
+ * Each object is an element of an Object set, and types are subsets of the objects.
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        new() {
+                // Initialize package
+                LogicproblemPackage.eINSTANCE.class
+        }
+        
+        override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
+                trace.typeMapperTrace = typeTrace
+                
+                // 1. A global type for Objects is created
+                val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
+                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]
+                        trace.specification.signatureBodies += body
+                        typeTrace.type2ALSType.put(type,sig)
+                }
+                
+                // 3. The elements of a defined type is mapped to singleton signatures
+                // 3.1 Collect the elements
+                val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine)
+                val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>>
+                for(element : elements) {
+                        val topmostTypes = elementMatcher.getAllValuesOftype(element)
+                        var ALSSignatureDeclaration selectedTopmostType;
+                        if(topmostTypes.empty) {
+                                selectedTopmostType = objectSig
+                        } else{
+                                selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType)
+                        }
+                        topmostType2Elements.putOrAddToList(selectedTopmostType,element)
+                }
+                
+                // 4. For each topmost types several singleton classes are generated, which represents the elements.
+                // For the sake of clarity, common bodies are used.
+                for(topmostEntry : topmostType2Elements.entrySet) {
+                        
+                        for(element : topmostEntry.value) {
+                                val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
+                                typeTrace.definedElement2Declaration.put(element,signature)
+                        }
+                        
+                        val body = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity.ONE
+                                it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)]
+                        ]
+                        
+                        val containerLogicType = topmostEntry.key
+                        body.superset += containerLogicType
+                        
+                        trace.specification.signatureBodies+=body
+                }
+                
+                // 5.1 Each Defined Type is specified as the union of its elements
+                for(definedType : types.filter(TypeDefinition)) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("typedefinition",definedType.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(definedType.elements.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]])
+                                ]
+                        ]
+                }
+                // 5.2 Each Defined Element is unique
+                for(definedType : types.filter(TypeDefinition)) {
+                        val allElementsIncludingSubtypes = 
+                                definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition)
+                                        .map[elements].flatten.toSet.toList
+                        if(allElementsIncludingSubtypes.size>=2) {
+                                trace.specification.factDeclarations += createALSFactDeclaration => [
+                                        it.name = support.toIDMultiple("typeElementsUnique",definedType.name)
+                                        it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace)
+                                ]
+                        }
+                }
+                
+                // 6. Each inheritance is modeled by subset operator 'in'
+                for(type : types) {
+                        val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody
+                        if(type.supertypes.empty)  {
+                                sigBody.superset += typeTrace.objectSupperClass
+                        } else {
+                                sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)]
+                        }
+                }
+                
+                
+                // 7. Each type is in the intersection of the supertypes
+                for(type : types.filter[it.supertypes.size>=2]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                
+                // 8. Each abstract type is equal to the union of the subtypes
+                for(type : types.filter[isIsAbstract]) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("abstract",type.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
+                                        it.rightOperand = support.unfoldPlus(type.subtypes.map[e|
+                                                createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                                ]
+                        ]
+                }
+                // 8.1 The object type is the union of the root types.
+                val rootTypes = types.filter[it.supertypes.empty].toList
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toIDMultiple(#["ObjectTypeDefinition"])
+                        it.term = createALSEquals => [
+                                it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ]
+                                it.rightOperand = support.unfoldPlus(rootTypes.map[e|
+                                        createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
+                        ]
+                ]
+                
+                // 9. For each type X (including Object)
+                //    only the common subtypes are in the intersection
+                //    of the two subtype.
+                // 9.1. for the object
+                {
+                        val rootTypeList = types.filter[it.supertypes.empty].toList
+                        for(type1Index: 0..<rootTypeList.size) {
+                                for(type2Index: 0..<type1Index) {
+                                        trace.specification.factDeclarations += 
+                                                commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace)
+                                }
+                        }
+                }
+                
+                //9.3 for the subtypes of each objects
+                {
+                        for(inScope : types) {
+                                val subtypeList = inScope.subtypes//.toList
+                                if(subtypeList.size>=2) {
+                                        for(type1Index: 0..<subtypeList.size) {
+                                                for(type2Index: 0..<type1Index) {
+                                                        trace.specification.factDeclarations += 
+                                                                commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace)
+                                                }
+                                        }
+                                }
+                        }
+                }
+        }
+        
+        private def isEnumlikeType(Type type) {
+                if(type instanceof TypeDefinition) {
+                        val elements = type.elements
+                        return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type]
+                }
+                return false
+        }
+        
+        private def isEnumlikeElement(DefinedElement d) {
+                d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType 
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) {
+                val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine)
+                val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList
+                return createALSFactDeclaration => [
+                                it.name = support.toIDMultiple("common","types",t1.name,t2.name)
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSIntersection => [
+                                                it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)]
+                                                it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)]
+                                        ]
+                                        it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]])
+                                ]
+                        ]
+        }
+        
+        def private unfoldDistinctElements(
+                List<DefinedElement> operands,
+                Logic2AlloyLanguageMapperTrace trace
+        ) {
+                if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);}
+                else {
+                        val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
+                        for(i:0..<operands.size) {
+                                for(j: i+1..<operands.size) {
+                                        notEquals+=createALSNotEquals=>[
+                                                leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ]
+                                                rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ]
+                                        ]
+                                }
+                        }
+                        return support.unfoldAnd(notEquals)
+                }
+        }
+        
+        override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                return #[trace.typeTrace.type2ALSType.get(referred)]
+        }
+        
+        override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.objectSupperClass
+        }
+        
+        override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
+                createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)]
+        }
+        
+        override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
+                return undefinedScope + trace.typeTrace.definedElement2Declaration.size
+        }
+        
+}
+\ No newline at end of file
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..ade9860b --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,268 @@
	1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
	2
	3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries
	4	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
	5	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
	6	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
	7	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
	8	import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
	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.TypeDefinition
	12	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
	13	import java.util.ArrayList
	14	import java.util.Collection
	15	import java.util.HashMap
	16	import java.util.List
	17	import java.util.Map
	18
	19	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
	20
	21	class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
	22	implements Logic2AlloyLanguageMapper_TypeMapperTrace
	23	{
	24	public var ALSSignatureDeclaration objectSupperClass;
	25	public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
	26	public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
	27	}
	28	/**
	29	* Each object is an element of an Object set, and types are subsets of the objects.
	30	*/
	31	class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{
	32	private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
	33	private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
	34
	35	new() {
	36	// Initialize package
	37	LogicproblemPackage.eINSTANCE.class
	38	}
	39
	40	override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
	41	val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
	42	trace.typeMapperTrace = typeTrace
	43
	44	// 1. A global type for Objects is created
	45	val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
	46	val objectBody = createALSSignatureBody => [
	47	it.declarations += objectSig
	48	it.abstract = true
	49	]
	50	typeTrace.objectSupperClass = objectSig
	51	trace.specification.signatureBodies += objectBody
	52
	53	// 2. Each type is mapped to a unique sig
	54	for(type : types) {
	55	val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
	56	val body = createALSSignatureBody => [it.declarations += sig]
	57	trace.specification.signatureBodies += body
	58	typeTrace.type2ALSType.put(type,sig)
	59	}
	60
	61	// 3. The elements of a defined type is mapped to singleton signatures
	62	// 3.1 Collect the elements
	63	val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine)
	64	val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>>
	65	for(element : elements) {
	66	val topmostTypes = elementMatcher.getAllValuesOftype(element)
	67	var ALSSignatureDeclaration selectedTopmostType;
	68	if(topmostTypes.empty) {
	69	selectedTopmostType = objectSig
	70	} else{
	71	selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType)
	72	}
	73	topmostType2Elements.putOrAddToList(selectedTopmostType,element)
	74	}
	75
	76	// 4. For each topmost types several singleton classes are generated, which represents the elements.
	77	// For the sake of clarity, common bodies are used.
	78	for(topmostEntry : topmostType2Elements.entrySet) {
	79
	80	for(element : topmostEntry.value) {
	81	val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
	82	typeTrace.definedElement2Declaration.put(element,signature)
	83	}
	84
	85	val body = createALSSignatureBody => [
	86	it.multiplicity = ALSMultiplicity.ONE
	87	it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)]
	88	]
	89
	90	val containerLogicType = topmostEntry.key
	91	body.superset += containerLogicType
	92
	93	trace.specification.signatureBodies+=body
	94	}
	95
	96	// 5.1 Each Defined Type is specified as the union of its elements
	97	for(definedType : types.filter(TypeDefinition)) {
	98	trace.specification.factDeclarations += createALSFactDeclaration => [
	99	it.name = support.toIDMultiple("typedefinition",definedType.name)
	100	it.term = createALSEquals => [
	101	it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ]
	102	it.rightOperand = support.unfoldPlus(definedType.elements.map[e\|
	103	createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]])
	104	]
	105	]
	106	}
	107	// 5.2 Each Defined Element is unique
	108	for(definedType : types.filter(TypeDefinition)) {
	109	val allElementsIncludingSubtypes =
	110	definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition)
	111	.map[elements].flatten.toSet.toList
	112	if(allElementsIncludingSubtypes.size>=2) {
	113	trace.specification.factDeclarations += createALSFactDeclaration => [
	114	it.name = support.toIDMultiple("typeElementsUnique",definedType.name)
	115	it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace)
	116	]
	117	}
	118	}
	119
	120	// 6. Each inheritance is modeled by subset operator 'in'
	121	for(type : types) {
	122	val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody
	123	if(type.supertypes.empty) {
	124	sigBody.superset += typeTrace.objectSupperClass
	125	} else {
	126	sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)]
	127	}
	128	}
	129
	130
	131	// 7. Each type is in the intersection of the supertypes
	132	for(type : types.filter[it.supertypes.size>=2]) {
	133	trace.specification.factDeclarations += createALSFactDeclaration => [
	134	it.name = support.toIDMultiple("abstract",type.name)
	135	it.term = createALSEquals => [
	136	it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
	137	it.rightOperand = support.unfoldIntersection(type.supertypes.map[e\|
	138	createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
	139	]
	140	]
	141	}
	142
	143	// 8. Each abstract type is equal to the union of the subtypes
	144	for(type : types.filter[isIsAbstract]) {
	145	trace.specification.factDeclarations += createALSFactDeclaration => [
	146	it.name = support.toIDMultiple("abstract",type.name)
	147	it.term = createALSEquals => [
	148	it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
	149	it.rightOperand = support.unfoldPlus(type.subtypes.map[e\|
	150	createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
	151	]
	152	]
	153	}
	154	// 8.1 The object type is the union of the root types.
	155	val rootTypes = types.filter[it.supertypes.empty].toList
	156	trace.specification.factDeclarations += createALSFactDeclaration => [
	157	it.name = support.toIDMultiple(#["ObjectTypeDefinition"])
	158	it.term = createALSEquals => [
	159	it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ]
	160	it.rightOperand = support.unfoldPlus(rootTypes.map[e\|
	161	createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
	162	]
	163	]
	164
	165	// 9. For each type X (including Object)
	166	// only the common subtypes are in the intersection
	167	// of the two subtype.
	168	// 9.1. for the object
	169	{
	170	val rootTypeList = types.filter[it.supertypes.empty].toList
	171	for(type1Index: 0..<rootTypeList.size) {
	172	for(type2Index: 0..<type1Index) {
	173	trace.specification.factDeclarations +=
	174	commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace)
	175	}
	176	}
	177	}
	178
	179	//9.3 for the subtypes of each objects
	180	{
	181	for(inScope : types) {
	182	val subtypeList = inScope.subtypes//.toList
	183	if(subtypeList.size>=2) {
	184	for(type1Index: 0..<subtypeList.size) {
	185	for(type2Index: 0..<type1Index) {
	186	trace.specification.factDeclarations +=
	187	commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace)
	188	}
	189	}
	190	}
	191	}
	192	}
	193	}
	194
	195	private def isEnumlikeType(Type type) {
	196	if(type instanceof TypeDefinition) {
	197	val elements = type.elements
	198	return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type]
	199	}
	200	return false
	201	}
	202
	203	private def isEnumlikeElement(DefinedElement d) {
	204	d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType
	205	}
	206
	207	def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
	208	val res = trace.typeMapperTrace
	209	if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) {
	210	return res
	211	} else {
	212	throw new IllegalArgumentException('''
	213	Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
	214	but found «res.class.name»''')
	215	}
	216	}
	217
	218	def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) {
	219	val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine)
	220	val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList
	221	return createALSFactDeclaration => [
	222	it.name = support.toIDMultiple("common","types",t1.name,t2.name)
	223	it.term = createALSEquals => [
	224	it.leftOperand = createALSIntersection => [
	225	it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)]
	226	it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)]
	227	]
	228	it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t\|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]])
	229	]
	230	]
	231	}
	232
	233	def private unfoldDistinctElements(
	234	List<DefinedElement> operands,
	235	Logic2AlloyLanguageMapperTrace trace
	236	) {
	237	if(operands.size == 1 \|\| operands.size == 0) {support.unfoldTrueStatement(trace);}
	238	else {
	239	val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2)
	240	for(i:0..<operands.size) {
	241	for(j: i+1..<operands.size) {
	242	notEquals+=createALSNotEquals=>[
	243	leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ]
	244	rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ]
	245	]
	246	}
	247	}
	248	return support.unfoldAnd(notEquals)
	249	}
	250	}
	251
	252	override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
	253	return #[trace.typeTrace.type2ALSType.get(referred)]
	254	}
	255
	256	override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
	257	trace.typeTrace.objectSupperClass
	258	}
	259
	260	override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
	261	createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)]
	262	}
	263
	264	override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
	265	return undefinedScope + trace.typeTrace.definedElement2Declaration.size
	266	}
	267
	268	} \ No newline at end of file