1 files changed, 263 insertions, 0 deletions

diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver2/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..9e548ab6
--- /dev/null
+++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -0,0 +1,263 @@
+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 static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+/**
+ * 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) {
+                if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size
+        }
+        
+        override getTypeInterpreter() {
+                return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes
+        }
+}
\ No newline at end of file