From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- ...yLanguageMapper_TypeMapper_Horizontal.xtend_old | 428 +++++++++++++++++++++ 1 file changed, 428 insertions(+) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old') 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 definedElement2Declaration = new HashMap + + public val Map definition2definition = new HashMap + public val Map declaration2definition = new HashMap + public val Map undefined2definition = new HashMap + public val Map new2declaration = new HashMap + + def getAllDefinedTypes() { + return (definition2definition.values) + + (declaration2definition.values) + + (undefined2definition.values) + } + def getAllDeclaredTypes() { + return new2declaration.values + } + + public val Map> type2AllSignatures = new HashMap; +} + +@Data +class DynamicTypeConstraints { + List> positiveCNF + LinkedHashSet negative + public new() { + this.positiveCNF = new LinkedList + this.negative = new LinkedHashSet + } + def public void addPositiveTypeOptions(List typeDisjunction) { + this.positiveCNF.add(typeDisjunction) + } + def public void addNegativeTypes(Iterable 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 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 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 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> 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> 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 typeConstraints(List elements, Map> typeToConcreteSubtypes) { + val Map 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 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 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 -- cgit v1.2.3-54-g00ecf