From 53bfa0734fff9a70b992d6effde3a6cbac9ea946 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 27 Sep 2017 17:40:00 +0200 Subject: Transitive closure support for relation definitions in Alloy --- .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 8 +- .../builder/Logic2AlloyLanguageMapper.xtend | 31 ++++++- .../builder/Logic2AlloyLanguageMapperTrace.xtend | 9 +- .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 92 ++++++++++++++++++- ...apper_TypeMapper_InheritanceAndHorizontal.xtend | 101 +++++++++++---------- 5 files changed, 182 insertions(+), 59 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend index 65539155..b9723d18 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend @@ -1,13 +1,13 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes -import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.MonitoredAlloySolution +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner @@ -16,8 +16,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace -import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution -import java.util.List class AlloySolver extends LogicReasoner{ @@ -27,7 +25,7 @@ class AlloySolver extends LogicReasoner{ x.createInjectorAndDoEMFRegistration } - val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) + val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal) val AlloyHandler handler = new AlloyHandler val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index ee2f49ed..d6c62f54 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend @@ -64,6 +64,8 @@ import java.util.Collection import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation class Logic2AlloyLanguageMapper { private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE @@ -102,10 +104,12 @@ class Logic2AlloyLanguageMapper { trace.constantDefinitions = problem.collectConstantDefinitions trace.functionDefinitions = problem.collectFunctionDefinitions trace.relationDefinitions = problem.collectRelationDefinitions + val calledInTransitiveClosure = problem.collectTransitiveRelationCalls - problem.constants.forEach[this.constantMapper.transformConstant(it,trace)] + problem.constants.forEach[this.constantMapper.transformConstant(it, trace)] problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + calledInTransitiveClosure.forEach[this.relationMapper.prepareTransitiveClosure(it, trace)] problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] @@ -143,6 +147,8 @@ class Logic2AlloyLanguageMapper { return new TracedOutput(specification,trace) } + + def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { val a = assertion.inverseA val b = assertion.inverseB @@ -213,15 +219,21 @@ class Logic2AlloyLanguageMapper { return ALSMultiplicity::SOME } else if(multiplicity === ALSMultiplicity::LONE) { return ALSMultiplicity::ONE + } else if(multiplicity == ALSMultiplicity::ONE) { + return ALSMultiplicity::ONE } else { throw new IllegalArgumentException('''Lower multiplicity is already set!''') } } private def addUpper(ALSMultiplicity multiplicity) { - if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { + if(multiplicity === ALSMultiplicity::ALL) { + return ALSMultiplicity::LONE + } else if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { return ALSMultiplicity::LONE } else if(multiplicity === ALSMultiplicity::SOME) { return ALSMultiplicity::ONE + } else if(multiplicity == ALSMultiplicity::ONE) { + return ALSMultiplicity::ONE } else { throw new IllegalArgumentException('''Upper multiplicity is already set!''') } @@ -254,6 +266,9 @@ class Logic2AlloyLanguageMapper { ] return res } + private def collectTransitiveRelationCalls(LogicProblem problem) { + return problem.eAllContents.filter(TransitiveClosure).map[it.relation].toSet + } //////////////////// // Type References @@ -380,11 +395,21 @@ class Logic2AlloyLanguageMapper { ] } + def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map variables) { + return this.relationMapper.transformTransitiveRelationReference( + tc.relation, + tc.leftOperand.transformTerm(trace,variables), + tc.rightOperand.transformTerm(trace,variables), + trace + ) + } + def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map variables) { symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { - typeMapper.transformReference(referred,trace)} + typeMapper.transformReference(referred,trace) + } def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { if(trace.constantDefinitions.containsKey(constant)) { return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend index 22f49c98..9a16ddf2 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend @@ -17,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import java.util.HashMap import java.util.Map import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation interface Logic2AlloyLanguageMapper_TypeMapperTrace {} @@ -39,11 +40,17 @@ class Logic2AlloyLanguageMapperTrace { public val Map functionDeclaration2LanguageField = new HashMap public val Map functionDefinition2Function = new HashMap - public val Map relationDeclaration2Global = new HashMap + public val Map relationDeclaration2Global = new HashMap public val Map relationDeclaration2Field = new HashMap public val Map relationDefinition2Predicate = new HashMap + public val Map transitiveClosureTarget2Global = new HashMap + public val Map transitiveClosureTarget2Field = new HashMap + public var Map constantDefinitions public var Map functionDefinitions public var Map relationDefinitions + + public var Map relationInTransitiveToGlobalField = new HashMap + public var Map relationInTransitiveToHosterField = new HashMap } \ 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_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend index 9dd4da2f..0762efce 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend @@ -9,6 +9,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition import java.util.HashMap import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm class Logic2AlloyLanguageMapper_RelationMapper { private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE @@ -18,7 +22,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { this.base = base } - def dispatch protected void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + def dispatch public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { if(!trace.relationDefinitions.containsKey(r)) { if(r.transformToHostedField(trace)) { transformRelationDeclarationToHostedField(r,trace) @@ -28,6 +32,15 @@ class Logic2AlloyLanguageMapper_RelationMapper { } } + def public createRelationDeclaration(String name, List paramTypes, Logic2AlloyLanguageMapperTrace trace) { + val field = createALSFieldDeclaration => [ + it.name = support.toID(name) + it.type = support.unfoldReferenceDirectProduct(base,paramTypes,trace) + ] + trace.logicLanguageBody.fields += field + return field + } + def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { val first = r.parameters.get(0) if(r.parameters.size == 2) { @@ -64,7 +77,7 @@ class Logic2AlloyLanguageMapper_RelationMapper { trace.relationDeclaration2Global.put(r, field) } - def dispatch protected void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { + def dispatch public void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { val res = createALSRelationDefinition => [ name = support.toID(r.name) // fill the variables later @@ -108,4 +121,79 @@ class Logic2AlloyLanguageMapper_RelationMapper { return relation.lookup(trace.relationDeclaration2Global) } } + + public def dispatch void prepareTransitiveClosure(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { + // There is nothing to do, relation can be used in ^relation expressions + if(transformToHostedField(relation,trace)) { + trace.relationInTransitiveToHosterField.put(relation,relation.lookup(trace.relationDeclaration2Field)) + } else { + trace.relationInTransitiveToGlobalField.put(relation,relation.lookup(trace.relationDeclaration2Global)) + } + } + public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { + if(relation.parameters.size === 2) { + /** 1. Create a relation that can be used in ^relation expressions */ + val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) + trace.relationInTransitiveToHosterField.put(relation,declaration) + /** 2. Add fact that the declaration corresponds to the definition */ + val fact = createALSFactDeclaration => [ + it.name = '''EqualsAsDeclaration «relation.name»''' + it.term = createALSQuantifiedEx => [ + val a = createALSVariableDeclaration => [ + it.name = "a" + it.range = base.transformTypeReference(relation.parameters.get(0),trace) + ] + val b = createALSVariableDeclaration => [ + it.name = "b" + it.range = base.transformTypeReference(relation.parameters.get(1),trace) + ] + it.variables += a + it.variables += b + it.type = ALSMultiplicity::ALL + it.expression = createALSIff => [ + it.leftOperand = createALSFunctionCall => [ + it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) + it.params += createALSReference => [ it.referred = a ] + it.params += createALSReference => [ it.referred = b ] + ] + it.rightOperand = createALSSubset => [ + it.leftOperand = createALSJoin => [ + it.leftOperand = createALSReference => [ referred = a ] + it.rightOperand = createALSReference => [ referred = b ] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = declaration ] + ] + ] + ] + ] + ] + trace.specification.factDeclarations += fact + return + } else { + throw new AssertionError('''A non-binary relation "«relation.name»" is used in transitive clousure!''') + } + } + + def public transformTransitiveRelationReference(Relation relation, ALSTerm source, ALSTerm target, Logic2AlloyLanguageMapperTrace trace) { + val alsTargetRelation = if(trace.relationInTransitiveToGlobalField.containsKey(relation)) { + createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] + ] + } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ + createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] + } else { + throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') + } + return createALSSubset => [ + it.leftOperand = createALSJoin => [ + it.leftOperand = source + it.rightOperand = target + ] + it.rightOperand = createAlSTransitiveClosure => [it.operand = alsTargetRelation] + + ] + } } \ 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_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend index 4d7b50e8..92ac27df 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend @@ -30,58 +30,62 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L } override transformTypes(Collection types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { - if(types.exists[hasDefinedSupertype]) { - throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''') - } else { - - val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal - trace.typeMapperTrace = typeTrace + val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal + 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] + body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) - // 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 + trace.specification.signatureBodies += body + typeTrace.type2ALSType.put(type,sig) - // 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] - body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) - - trace.specification.signatureBodies += body - typeTrace.type2ALSType.put(type,sig) - - if(type instanceof TypeDefinition) { - val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig] - for(element : type.elements) { - val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] - elementContainer.declarations += signature - - } - trace.specification.signatureBodies += elementContainer - } - - typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) + typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) + } + + for(element : elements) { + val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty] + if(mostSpecificTypes.size== 1) { + val mostSpecificSubtype = mostSpecificTypes.head + val elementContainer = createALSSignatureBody => [ + it.multiplicity = ALSMultiplicity::ONE + it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype) + ] + val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] + elementContainer.declarations += signature + typeTrace.definedElement2Declaration.put(element,signature) + trace.specification.signatureBodies += elementContainer + } else { + throw new UnsupportedOperationException } - - // 6. Each inheritance is modeled by extend keyword - for(type : types) { - if(type.supertypes.size == 1) { - val alsType = typeTrace.type2ALSType.get(type.supertypes.head) - (type.eContainer as ALSSignatureBody).supertype = alsType - } else if(type.supertypes.size > 1){ - val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) - (type.eContainer as ALSSignatureBody).supertype = alsMainType - for(otherType : type.supertypes.filter[it != alsMainType]) { - typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType)) - } + } + + // 6. Each inheritance is modeled by extend keyword + for(type : types) { + if(type.supertypes.size == 0) { + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass + }if(type.supertypes.size == 1) { + val alsType = typeTrace.type2ALSType.get(type.supertypes.head) + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType + + } else if(type.supertypes.size > 1){ + val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType + for(otherType : type.supertypes.filter[it != alsMainType]) { + typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type)) } } - } } @@ -114,7 +118,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L } override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { - createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)] + val r = trace.typeTrace.definedElement2Declaration.get(referred) + return createALSReference => [it.referred =r] } override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { -- cgit v1.2.3-54-g00ecf