Alloy type mapping fix

3 files changed, 10 insertions, 5 deletions

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 432651af..f6b0b4a5 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
@@ -16,6 +16,9 @@ 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 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper

+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal

 

 class AlloySolver extends LogicReasoner{

         

@@ -25,7 +28,9 @@ class AlloySolver extends LogicReasoner{
                 x.createInjectorAndDoEMFRegistration

         }

         

-        val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes)

+        val Logic2AlloyLanguageMapper_TypeMapper typeMapper = new Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal//Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes

+        

+        val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(typeMapper)

         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/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
index 107aa001..bbee35fc 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -117,7 +117,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
                 for(atom: allAtoms) {

                         val typeName = getName(atom.type)

                         val atomName = atom.name

-                        println(atom.toString + "  < -  " + typeName)

+                        //println(atom.toString + "  < -  " + typeName)

                         if(typeName == forwardTrace.logicLanguage.name) {

                                 this.logicLanguage = atom

                         } else if(typeName == "Int" || typeName == "seq/Int") {

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
index 397fb84b..3379ba20 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -123,8 +123,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
                 // 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.name = support.toIDMultiple("supertypeIsInIntersection",type.name)

+                                it.term = createALSSubset => [

                                         it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]

                                         it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|

                                                 createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])

@@ -135,7 +135,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
                 // 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.name = support.toIDMultiple("abstractIsUnion",type.name)

                                 it.term = createALSEquals => [

                                         it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]

                                         it.rightOperand = support.unfoldPlus(type.subtypes.map[e|