Transitive closure support for relation definitions in Alloy

4 files changed, 179 insertions, 54 deletions

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<Variable, ALSVariableDeclaration> 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<Variable, ALSVariableDeclaration> variables) {

                 symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }

         

         def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) {

-                typeMapper.transformReference(referred,trace)}

+                typeMapper.transformReference(referred,trace)

+        }

         def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List<Term> parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> 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<FunctionDeclaration,ALSFieldDeclaration> functionDeclaration2LanguageField = new HashMap

         public val Map<FunctionDefinition,ALSFunctionDefinition> functionDefinition2Function = new HashMap

         

-        public val Map<RelationDeclaration,ALSFieldDeclaration> relationDeclaration2Global = new HashMap

+        public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Global = new HashMap

         public val Map<RelationDeclaration, ALSFieldDeclaration> relationDeclaration2Field = new HashMap

         public val Map<RelationDefinition,ALSRelationDefinition> relationDefinition2Predicate = new HashMap

         

+        public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Global = new HashMap

+        public val Map<RelationDeclaration, ALSFieldDeclaration> transitiveClosureTarget2Field = new HashMap

+        

         public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions

         public var Map<FunctionDeclaration, FunctionDefinition> functionDefinitions

         public var Map<RelationDeclaration, RelationDefinition> relationDefinitions

+        

+        public var Map<Relation, ALSFieldDeclaration> relationInTransitiveToGlobalField = new HashMap

+        public var Map<Relation, ALSFieldDeclaration> 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<TypeReference> 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<Type> types, Collection<DefinedElement> 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) {