1 files changed, 428 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_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
new file mode 100644
index 00000000..7383904d
--- /dev/null
+++ 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
@@ -0,0 +1,428 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection
+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
+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.ComplexTypeReference
+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.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
+import java.util.HashMap
+import java.util.LinkedHashSet
+import java.util.LinkedList
+import java.util.List
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import org.eclipse.xtend.lib.annotations.Data
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+        implements Logic2AlloyLanguageMapper_TypeMapperTrace {
+        public var ALSSignatureDeclaration declaredSupertype
+        public var ALSSignatureDeclaration definedSupertype
+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
+        
+        public val Map<TypeDefinition,  ALSSignatureDeclaration> definition2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap
+        public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap
+        
+        def getAllDefinedTypes() {
+                return (definition2definition.values) +
+                       (declaration2definition.values) +
+                       (undefined2definition.values)
+        }
+        def getAllDeclaredTypes() {
+                return new2declaration.values
+        }
+        
+        public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap;
+}
+@Data
+class DynamicTypeConstraints {
+        List<List<Type>> positiveCNF
+        LinkedHashSet<Type> negative
+        public new() {
+                this.positiveCNF = new LinkedList
+                this.negative = new LinkedHashSet
+        }
+        def public void addPositiveTypeOptions(List<Type> typeDisjunction) {
+                this.positiveCNF.add(typeDisjunction)
+        }
+        def public void addNegativeTypes(Iterable<Type> negativeTypes) {
+                this.negative.addAll(negativeTypes)
+        }
+}
+/**
+ * Dynamic types are represented by disjoint sets, and 
+ * static types are represented by the union of the dynamic type sets.
+ * 
+ * Definition                         Declaration
+ *     |                              /         \
+ *     |                  W/DefinedSuper       Wo/DefinedSuper
+ *     |                     |                  /           \
+ *     |                     |      undefined2declaration  new2declaration
+ * definition2definition  definition2declaration
+ * +----------------------------------------------------+  +-------------+
+ *        Defined                                              Declared
+ */
+class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{
+        private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
+        private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
+        
+        override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                // 0. Creating the traces
+                val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
+                trace.typeMapperTrace = typeTrace
+                /**
+                 * Static type -> list of possible dynamic type map
+                 */
+                val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace)
+                
+                
+                
+                // 1. Transforming the types
+                
+                // There are two kind of types:
+                // A: one with defined supertypes (including itself), that only has defined elements
+                // Those types can have instances only from the defined elements, ie they are subset of problem.elements
+                // B: one without defined supertypes 
+                // Those types can have instances from two sources
+                // B.1 from elements that dont have definitions
+                // B.2 from newly created elements
+                val allConcreteTypes = problem.types.filter[!it.isAbstract]
+                val definitions = allConcreteTypes.filter(TypeDefinition).toList
+                val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList
+                val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList
+                
+                // 2. If there are defined elements
+                if(trace.typeTrace.definedSupertype != null) {
+                        // 3 mapping the elements
+                        problem.elements.transformDefinedSupertype(trace)
+                        // 4. if there are elements that are added to types, then it have to be mapped to defined parts
+                        if(problem.elements.exists[!it.definedInType.empty]) {
+                                definitions.forEach[it.transformDefinition2Definition(trace)]
+                                declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)]
+                        }
+                        // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions
+                        if(problem.elements.exists[it.definedInType.empty]) {
+                                declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)]
+                        }
+                        
+                        definedConcreteTypesAreFull(trace)
+                        definedConcreteTypesAreDisjoint(trace)
+                        problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace)
+                }
+                
+                // Transforming the declared and defined concrete types
+                problem.elements.transformDefinedSupertype(trace)
+                if(trace.typeTrace.definedSupertype != null) {
+                        problem.elements.transformDefinedElements(trace)
+                        declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)]
+                }
+                
+                // 2: Caching the types by filling type2AllSignatures
+                for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) {
+                        val type = typeToConcreteSubtypesEntry.key
+                        val List<ALSSignatureDeclaration> signatures = new LinkedList
+                        
+                }
+        }
+        
+        def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
+                val res = trace.typeMapperTrace
+                if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) {
+                        return res
+                } else {
+                        throw new IllegalArgumentException('''
+                        Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name»,
+                        but found «res.class.name»''')
+                }
+        }
+        
+        private def boolean hasDefinedSupertype(Type type) {
+                if(type instanceof TypeDefinition) {
+                        return true
+                } else {
+                        if(type.supertypes.empty) return false
+                        else return type.supertypes.exists[it.hasDefinedSupertype]
+                }
+        }
+        
+        private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) {
+                trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [
+                        it.name = support.toID(#["util","defined","Object"])
+                ]
+                trace.specification.signatureBodies += createALSSignatureBody => [
+                        it.abstract = true
+                        it.declarations += trace.typeTrace.definedSupertype
+                ]
+        }
+        
+        private def transformDefinedElements(List<DefinedElement> elements,
+                Logic2AlloyLanguageMapperTrace trace){
+                if(trace.typeTrace.definedSupertype != null) {                  
+                        // 2. Create elements as singleton signatures subtype of definedSupertype
+                        val elementBodies = createALSSignatureBody => [
+                                it.multiplicity = ALSMultiplicity::ONE
+                                it.supertype = trace.typeTrace.definedSupertype
+                        ]
+                        trace.specification.signatureBodies += elementBodies
+                        for(element : elements) {
+                                val elementDeclaration = createALSSignatureDeclaration => [
+                                        it.name = support.toIDMultiple(#["element"],element.name)
+                                ]
+                                elementBodies.declarations += elementDeclaration
+                                trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration)
+                        }
+                        // 3. Specify that definedSupertype is equal to the union of specified
+                        /*trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util","typehierarchy","definitionOfElements"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[
+                                                it.referred = element.lookup(trace.typeTrace.definedElement2Declaration)
+                                        ]])
+                                ]
+                        ]*/
+                }
+        }
+        
+        ///// Type definitions
+        
+        protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.definition2definition.put(type,sig)
+        }
+        protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.superset += trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.declaration2definition.put(type,sig)
+        }
+        protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.definedSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.undefined2definition.put(type,sig)
+        }
+        protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
+                val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)]
+                val body = createALSSignatureBody => [
+                        it.declarations += sig
+                        it.supertype = trace.typeTrace.declaredSupertype
+                ]
+                trace.specification.signatureBodies += body
+                trace.typeTrace.new2declaration.put(type,sig)
+        }
+        
+        /**
+         * The dynamic types cover each concrete types
+         */
+        protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) {
+                trace.specification.factDeclarations += createALSFactDeclaration => [
+                        it.name = support.toID(#["util","typehierarchy","elementFull"])
+                                it.term = createALSEquals => [
+                                        it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
+                                        it.rightOperand = support.unfoldPlus(
+                                                trace.typeTrace.allDefinedTypes.map[type|
+                                                        createALSReference=>[referred = type]
+                                                ].toList
+                                        )
+                                ]
+                ]
+                
+        }
+        /**
+         * The dynamic types are disjoint
+         */
+        protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) {
+                val types = trace.getTypeTrace.allDefinedTypes.toList
+                if (types.size >= 2) {
+                        trace.specification.factDeclarations += createALSFactDeclaration => [
+                                it.name = support.toID(#["util", "typehierarchy", "elementFull"])
+                                it.term = types.disjointSets
+                        ]
+                }
+        }
+        /**
+         * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not
+         */
+        protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) {
+                val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes)
+                for(constraintOnElement : constraintOnElements.entrySet) {
+                        val element = constraintOnElement.key
+                        val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration)
+                        val constraint = constraintOnElement.value
+                        
+                        var ALSTerm negativeConstraints;
+                        if(constraint.negative.isEmpty) {
+                                negativeConstraints = null
+                        } else {
+                                negativeConstraints = support.unfoldAnd(constraint.negative.map[type|
+                                        createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ]
+                                ].toList)
+                        }
+                        
+                        var ALSTerm positiveTypeConstraints
+                        if(constraint.positiveCNF.isEmpty) {
+                                positiveTypeConstraints = null
+                        } else {
+                                positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition |
+                                        support.unfoldOr(typeConstraintFromDefinition.map[type |
+                                                elementInDefinedType(elementSignature,type,trace)
+                                        ].toList,trace)
+                                ])
+                        }
+                        
+                        var ALSTerm typeConstraint
+                        if(negativeConstraints != null && positiveTypeConstraints == null) {
+                                typeConstraint = negativeConstraints
+                        } else if (negativeConstraints == null && positiveTypeConstraints != null) {
+                                typeConstraint = positiveTypeConstraints
+                        } else if (negativeConstraints != null && positiveTypeConstraints != null) {
+                                val and = createALSAnd
+                                and.leftOperand = positiveTypeConstraints
+                                and.rightOperand = negativeConstraints
+                                typeConstraint = and
+                        } else {
+                                typeConstraint = null
+                        }
+                        
+                        if(typeConstraint != null) {
+                                val fact =  createALSFactDeclaration => [
+                                        name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name)
+                                ]
+                                fact.term = typeConstraint
+                                trace.specification.factDeclarations +=fact
+                        }
+                        // otherwise there is no type constraint on element
+                }
+        }
+        
+        private def elementInDefinedType(
+                ALSSignatureDeclaration elementSignature,
+                Type type,
+                Logic2AlloyLanguageMapperTrace trace)
+        {
+                var ALSSignatureDeclaration signature
+                if(type instanceof TypeDeclaration) {
+                        if(trace.typeTrace.declaration2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.declaration2definition)
+                        } else if(trace.typeTrace.undefined2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.undefined2definition)
+                        } else {
+                                return null
+                        }
+                } else if(type instanceof TypeDefinition) {
+                        if(trace.typeTrace.definition2definition.containsKey(type)) {
+                                signature = type.lookup(trace.typeTrace.definition2definition)
+                        } else {
+                                return null
+                        }
+                } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''')
+                
+                val finalSignature = signature
+                return createALSSubset => [
+                        leftOperand = createALSReference => [
+                                referred = elementSignature
+                        ]
+                        rightOperand = createALSReference => [
+                                referred = finalSignature
+                        ]
+                ]
+        }
+        
+        def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) {
+                if(trace.incqueryEngine == null) {
+                        trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
+                }
+                val matcher = SupertypeStarMatcher.on(trace.incqueryEngine)
+                val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap
+                for(supertype : problem.types) {
+                        typeToConcreteSubtypes.put(
+                                supertype,
+                                matcher.getAllValuesOfsubtype(supertype)
+                                        .filter[!it.isIsAbstract].toList)
+                }
+                return typeToConcreteSubtypes
+        }
+        
+        /**
+         * Gives type constraints in a form of CNF 
+         */
+        def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) {
+                val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap
+                elements.forEach[constraints.put(it,new DynamicTypeConstraints)]
+                
+                for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) {
+                        val subtypes = type.lookup(typeToConcreteSubtypes)
+                        for(elementInType:type.elements) {
+                                elementInType.lookup(constraints).addPositiveTypeOptions(subtypes)
+                        }
+                        for(elementNotInType:elements.filter[!type.elements.contains(it)]) {
+                                elementNotInType.lookup(constraints).addNegativeTypes(subtypes)
+                        }
+                }
+                
+                return constraints
+        }
+        
+        private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size >= 2){
+                        val top = createALSEquals => [
+                                it.leftOperand = signatures.intersectionOfTypes
+                                it.rightOperand = createALSNone
+                        ]
+                        if(signatures.size > 2) {
+                                return createALSAnd => [
+                                        it.leftOperand = top
+                                        it.rightOperand = signatures.subList(1,signatures.size).disjointSets
+                                ]
+                        } else{
+                                return top
+                        }
+                } else {
+                        throw new UnsupportedOperationException()
+                }
+        }
+        
+        private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) {
+                if(signatures.size == 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = createALSReference => [it.referred = signatures.get(1)]
+                        ]
+                } else if(signatures.size > 2) {
+                        return createALSIntersection => [
+                                leftOperand = createALSReference => [it.referred = signatures.get(0)]
+                                rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes
+                        ]
+                } else throw new UnsupportedOperationException()
+        }
+        
+        
+        override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
+                //trace.typeTrace.
+        }
+}
+\ 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_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 new file mode 100644 index 00000000..7383904d --- /dev/null +++ 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
@@ -0,0 +1,428 @@
	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