:lipstick:

7 files changed, 151 insertions, 11 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend
new file mode 100644
index 00000000..f7603cf9
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend
@@ -0,0 +1,21 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

+

+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig

+import java.util.Map

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

+import java.util.List

+

+interface AlloyModelInterpretation_TypeInterpretation {

+        def void resolveUnknownAtoms(

+                Iterable<ExprVar> objectAtoms, 

+                A4Solution solution,

+                Logic2AlloyLanguageMapperTrace forwardTrace,

+                Map<String, Sig> name2AlloySig,

+                Map<String, Field> name2AlloyField,

+                Map<String,DefinedElement> expression2DefinedElement,

+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)

+}
\ 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/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend
new file mode 100644
index 00000000..934a863a
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend
@@ -0,0 +1,72 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

+

+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field

+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

+import java.util.ArrayList

+import java.util.List

+import java.util.Map

+

+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

+

+class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{

+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

+        

+        override resolveUnknownAtoms(

+                Iterable<ExprVar> objectAtoms, 

+                A4Solution solution,

+                Logic2AlloyLanguageMapperTrace forwardTrace,

+                Map<String, Sig> name2AlloySig,

+                Map<String, Field> name2AlloyField,

+                Map<String,DefinedElement> expression2DefinedElement,

+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)

+        {

+                /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()

+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/

+                

+                val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes

+                

+                // 1. Evaluate the defined elements

+                for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {

+                        val name = definedElementMappingEntry.value.name

+                        val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)

+                        val elementsOfSingletonSignature = solution.eval(matchingSig)

+                        if(elementsOfSingletonSignature.size != 1) {

+                                throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')

+                        } else {

+                                val expressionOfDefinedElement  = elementsOfSingletonSignature.head.atom(0)// as ExprVar

+                                expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)

+                        }

+                }

+                

+                // 2. evaluate the signatures and create new elements if necessary

+                for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {

+                        val type = type2SingatureEntry.key

+                        if(type instanceof TypeDeclaration) {

+                                val name = type2SingatureEntry.value.name

+                                val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)

+                                val elementsOfSignature = solution.eval(matchingSig)

+                                val elementList = new ArrayList(elementsOfSignature.size)

+                                var newVariableIndex = 1;

+                                for(elementOfSignature : elementsOfSignature) {

+                                        val expressionOfDefinedElement  = elementOfSignature.atom(0)

+                                        if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {

+                                                elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)

+                                        } else {

+                                                val newElementName = '''newObject «newVariableIndex.toString»'''

+                                                val newRepresentation = createDefinedElement => [

+                                                        it.name = newElementName

+                                                ]

+                                                elementList += newRepresentation

+                                                expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)

+                                        }

+                                }

+                                interpretationOfUndefinedType.put(type,elementList)

+                        }

+                }

+        }

+}
\ 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/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
new file mode 100644
index 00000000..8019c6b5
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
@@ -0,0 +1,20 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

+

+import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

+import java.util.Map

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

+import java.util.List

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory

+

+class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{

+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

+        

+        override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) {

+                throw new UnsupportedOperationException("TODO: auto-generated method stub")

+        }

+        

+}
\ 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.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
index d6c62f54..ee7c092a 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
@@ -1,6 +1,7 @@
 package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

 

 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration

+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity

@@ -8,6 +9,9 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory

+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion

+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion

+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And

@@ -46,8 +50,12 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

+import java.util.Collection

 import java.util.Collections

 import java.util.HashMap

 import java.util.List

@@ -57,15 +65,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
 import org.eclipse.xtend.lib.annotations.Accessors

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation

-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation

-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

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
new file mode 100644
index 00000000..8cdb7769
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend
@@ -0,0 +1,15 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

+

+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

+import java.util.HashMap

+import java.util.Map

+

+class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes

+        implements Logic2AlloyLanguageMapper_TypeMapperTrace

+{

+        public var ALSSignatureDeclaration objectSupperClass;

+        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;

+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = 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_TypeMapperTrace_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend
new file mode 100644
index 00000000..8377aca4
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend
@@ -0,0 +1,15 @@
+package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

+

+import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

+import java.util.HashMap

+import java.util.List

+import java.util.Map

+

+class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {

+        public var ALSSignatureDeclaration objectSupperClass;

+        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;

+        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap

+        public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap 

+}

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 3b2e3390..397fb84b 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
@@ -14,11 +14,9 @@ import java.util.ArrayList
 import java.util.Collection

 import java.util.HashMap

 import java.util.List

-import java.util.Map

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

 

-

 /**

  * Each object is an element of an Object set, and types are subsets of the objects.

  */