From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../Logic2AlloyLanguageMapper_Containment.xtend | 260 +++++++++++++++++++++ 1 file changed, 260 insertions(+) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend new file mode 100644 index 00000000..fd519c1e --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend @@ -0,0 +1,260 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import java.util.HashMap + +class Logic2AlloyLanguageMapper_Containment { + val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper base; + public new(Logic2AlloyLanguageMapper base) { + this.base = base + } + + def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + // Single root + val rootField = createALSFieldDeclaration => [ + it.name= support.toID(#["util", "root"]) + it.multiplicity = ALSMultiplicity.ONE + it.type = typesOrderedInContainment(containment,trace) + ] + trace.logicLanguageBody.fields += rootField + + val contains = createALSFieldDeclaration => [ + it.name = support.toID(#["util", "contains"]) + //it.multiplicity = ALSMultiplicity::SET + it.type = createALSDirectProduct => [ + it.leftMultiplicit = ALSMultiplicity::LONE + it.rightMultiplicit = ALSMultiplicity::SET + it.leftOperand = typesOrderedInContainment(containment,trace) + it.rightOperand = typesOrderedInContainment(containment,trace) + ] + ] + trace.logicLanguageBody.fields += contains + + val containmentRelationDefinition = createALSFactDeclaration => [ + it.name = support.toID(#["util", "containmentDefinition"]) + ] + + if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) { + val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation| + base.relationMapper.transformRelationReference(relation,trace) + ].toList + + containmentRelationDefinition.term = createALSEquals => [ + leftOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ]] + rightOperand = support.unfoldPlus(containmentRelations) + ] + } else { + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment, trace) + ] + val child = createALSVariableDeclaration => [ + it.name = "child" + it.range = typesOrderedInContainment(containment, trace) + ] + + val logicFactory = LogiclanguageFactory.eINSTANCE + val logicParentVariable = logicFactory.createVariable + val logicChildVariable = logicFactory.createVariable + val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable] + val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable] + val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)] + val possibleRelations = containment.containmentRelations.map[relation | + base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap) + ] + + containmentRelationDefinition.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity.ALL + it.variables += parent + it.variables += child + it.expression = createALSIff => [ + it.leftOperand = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = child] + it.rightOperand = createALSReference => [it.referred = parent] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + it.rightOperand = support.unfoldOr(possibleRelations,trace) + ] + ] + } + + trace.specification.factDeclarations += containmentRelationDefinition + + // With the exception of the root, every object has at least one parent + // No parent for root + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "noParentForRoot"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::NO + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += parent + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = parent] + it.rightOperand = createALSJoin => [ + it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] + it.rightOperand = createALSReference => [it.referred = rootField] + ] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + // Parent for nonroot + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "atLeastOneParent"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::ALL + val child = createALSVariableDeclaration => [ + it.name = "child" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += child + it.expression = createALSOr => [ + it.leftOperand = createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = child] + it.rightOperand = createALSJoin => [ + it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] + it.rightOperand = createALSReference => [it.referred = rootField] + ] + ] + it.rightOperand = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::SOME + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment, trace) + ] + it.variables += parent + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = parent] + it.rightOperand = createALSReference => [it.referred = child] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + ] + ] + + // Every object has at most one parent +// trace.specification.factDeclarations += createALSFactDeclaration => [ +// it.name = support.toID(#["util", "atMostOneParent"]) +// it.term = createALSQuantifiedEx => [ +// it.type = ALSMultiplicity::ALL +// val child = createALSVariableDeclaration => [ +// it.name = "child" +// it.range = typesOrderedInContainment(containment,trace) +// ] +// it.variables += child +// it.expression = createALSQuantifiedEx => [ +// it.type = ALSMultiplicity::LONE +// val parent = createALSVariableDeclaration => [ +// it.name = "parent" +// it.range = typesOrderedInContainment(containment, trace) +// ] +// it.variables += parent +// it.expression = createALSFunctionCall => [ +// it.referredDefinition = containmentRelation +// it.params += createALSReference => [ +// it.referred = parent +// it.referred = child +// ] +// ] +// ] +// ] +// ] + + // No circle in containment + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "noCircularContainment"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::NO + val variable = createALSVariableDeclaration => [ + it.name = "circle" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += variable + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = variable] + it.rightOperand = createALSReference => [it.referred = variable] + ] + it.rightOperand = createAlSTransitiveClosure => [ + it.operand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + ] + + } + + /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + val types = containment.typesOrderedInHierarchy + val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList +// val uncoveredSignatures = new ArrayList(signaturesInContainment) +// val coveringSignatures = new LinkedList +// + val engine = ViatraQueryEngine.on(new EMFScope(trace.specification)) + //val directSubsetMatcher = DirectSubsetMatcher.on(engine) + // x <= y + val subsetMatcher = SubsetMatcher.on(engine) + + if() + }*/ + + /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List signaturesInContainment, SubsetMatcher matcher) { + for(signatureInContainment : signaturesInContainment) { + if(!matcher.hasMatch(signatureInContainment,target)) { + return false + } + } + return true + }*/ + + /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List signaturesInContainment, SubsetMatcher matcher) { + val subtypes = matcher.getAllValuesOfx(target); + for(subType : subtypes) { + val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained | + matcher.hasMatch(subType,contained) + ] + if(!isSubtypeOfASignatureInContainment) { + return false + } + } + return true + }*/ + + def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + val types = containment.typesOrderedInHierarchy + val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten + // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten + val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList + return support.unfoldPlus(typeReferences) + } +} \ No newline at end of file -- cgit v1.2.3-70-g09d2