From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 263 +++++++++++++++++++++ 1 file changed, 263 insertions(+) create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend') 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 types, Collection 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> + 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.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..=2) { + for(type1Index: 0.. [ + 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 operands, + Logic2AlloyLanguageMapperTrace trace + ) { + if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} + else { + val notEquals = new ArrayList(operands.size*operands.size/2) + for(i:0..[ + 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 -- cgit v1.2.3-70-g09d2