1 files changed, 90 insertions, 2 deletions

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