Fix bug for ignored-attributes + better logic problem creation

4 files changed, 159 insertions, 53 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
index 5457d70c..e57b595a 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
@@ -1,17 +1,17 @@
 <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
---><plugin>

-  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" point="org.eclipse.viatra.query.runtime.queryspecification">

-    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries">

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.directSubset"/>

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.subset"/>

-    </group>

-  </extension>

-  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" point="org.eclipse.viatra.query.runtime.queryspecification">

-    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries">

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.supertype"/>

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.topmostCommonSubtypes"/>

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowermostCommonSupertype"/>

-      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowestCommonSupertypeOfAllOccuranceOfElement"/>

-    </group>

-  </extension>

-</plugin>

+--><plugin>
+  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries">
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.directSubset"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.subset"/>
+    </group>
+  </extension>
+  <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
+    <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries">
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.supertype"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.topmostCommonSubtypes"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowermostCommonSupertype"/>
+      <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowestCommonSupertypeOfAllOccuranceOfElement"/>
+    </group>
+  </extension>
+</plugin>
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
index f74c2ab4..1e2bbe6d 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend
@@ -25,6 +25,8 @@ import org.eclipse.emf.ecore.EObject
 import org.eclipse.emf.ecore.resource.Resource

 

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

+import org.eclipse.emf.ecore.EClass

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 

 class InstanceModel2PartialInterpretation {

         val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

@@ -123,26 +125,31 @@ class InstanceModel2PartialInterpretation {
                         // Transforming the attributes

                         for(attribute : source.eClass.EAllAttributes.filter[attributesUsed.contains(it) && !it.derived]) {

                                 val isIgnored = checkIfIgnored(source, attribute, ignoredAttribs)

-                                if (!isIgnored) {

-                                        val type = ecore2Logic.relationOfAttribute(ecore2LogicTrace,attribute)

-                                        val interpretation = type.lookup(partialInterpretationTrace.relation2Interpretation)

-                                        val sourceElement = source.lookup(object2DefinedElement)

-                                        if(attribute.isMany) {

-                                                val listOfTargets = source.eGet(attribute) as List<? extends EObject>

-                                                for(target : listOfTargets) {

-                                                        val value = translateValue(target,ecore2LogicTrace,partialInterpretationTrace)

-                                                        if(value !== null) {

-                                                                translateLink(interpretation,sourceElement,value)

-                                                        }

+                                val type = ecore2Logic.relationOfAttribute(ecore2LogicTrace, attribute)

+                                val interpretation = type.lookup(partialInterpretationTrace.relation2Interpretation)

+                                val sourceElement = source.lookup(object2DefinedElement)

+                                if (attribute.isMany) {

+                                        val listOfTargets = source.eGet(attribute) as List<? extends EObject>

+                                        for (target : listOfTargets) {

+                                                var DefinedElement value = null

+                                                if (!isIgnored) value = translateValue(target, ecore2LogicTrace, partialInterpretationTrace)

+                                                else value = createUnknownElement(partialInterpretation, target)

+                                                if (value !== null) {

+                                                        translateLink(interpretation, sourceElement, value)

                                                 }

-                                        } else {

-                                                val target = source.eGet(attribute)

-                                                if(target !== null) {

-                                                        val value = translateValue(target,ecore2LogicTrace,partialInterpretationTrace)

-                                                        if(value !== null) {

-                                                                translateLink(interpretation,sourceElement,value)

+                                        }

+                                } else {

+                                        val target = source.eGet(attribute)

+                                        if (target !== null) {

+                                                if (!isIgnored) {

+                                                        val value = translateValue(target, ecore2LogicTrace, partialInterpretationTrace)

+                                                        if (value !== null) {

+                                                                translateLink(interpretation, sourceElement, value)

                                                         }

                                                 }

+                                                else translateLink(interpretation, sourceElement, createUnknownElement(partialInterpretation, target))

+//                                              else value = null

+

                                         }

                                 }

                         }

@@ -190,11 +197,18 @@ class InstanceModel2PartialInterpretation {
         ) {

                 val classInIgnored = ignoredAttribs.get(object.eClass.name)

                 val mayIgnored = (

+                                        classInIgnored !== null && classInIgnored.containsKey("*")

+                                        ||

                                         classInIgnored !== null && classInIgnored.containsKey(attribute.name))

 

                 var isIgnored = false

                 if (mayIgnored) {

-                        val specificIgnoredValue = classInIgnored.get(attribute.name)

+                        var String specificIgnoredValue = null

+                        if (classInIgnored.containsKey("*")) 

+                                specificIgnoredValue = classInIgnored.get("*")

+                        else

+                                specificIgnoredValue = classInIgnored.get(attribute.name)

+                                

                         if (specificIgnoredValue.equals("*"))

                                 isIgnored = true

                         else {

@@ -208,10 +222,10 @@ class InstanceModel2PartialInterpretation {
                 }

                 // DEBUG

                 if (isIgnored) {
-                println("IGNORED")
-                println(object)
-                println(attribute)
-                println(object.eGet(attribute))

+//              println("IGNORED")
+//              println(object)
+//              println(attribute)
+//              println(object.eGet(attribute))

                 }

                 // END DEBUG

                 return isIgnored

@@ -276,4 +290,45 @@ class InstanceModel2PartialInterpretation {
         dispatch protected def translateValue(String value, Ecore2Logic_Trace ecore2LogicTrace, Problem2PartialInterpretationTrace partialInterpretationTrace) {

                 value.lookup(partialInterpretationTrace.primitiveValues.stringMap)

         }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Enumerator value) {

+                throw new UnsupportedOperationException("Currently we do not support ignored Enums")

+                //TODO Unsure about this

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Boolean value) {

+                val e = createBooleanElement => [valueSet = false]

+                p.newElements += e

+                return e

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Integer value) {

+                val e = createIntegerElement => [valueSet = false]

+                p.newElements += e

+                return e

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Short value) {

+                val e = createIntegerElement => [valueSet = false]

+                p.newElements += e

+                return e

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Double value) {

+                val e = createRealElement => [it.valueSet = false]

+                p.newElements += e

+                return e

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, Float value) {

+                val e = createRealElement => [valueSet = false]

+                p.newElements += e

+                return e

+        }

+        

+        dispatch protected def createUnknownElement(PartialInterpretation p, String value) {

+                val e = createStringElement => [valueSet = false]

+                p.newElements += e

+                return e

+        }

 }
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
index f15f5787..a2d2f625 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/PartialInterpretation2Logic.xtend
@@ -162,12 +162,22 @@ class PartialInterpretation2Logic {
         

         def private createLink(RelationLink link, SymbolicDeclaration relationDeclaration) {

                 if(link instanceof BinaryElementRelationLink) {

-                        if((link.param1 !== null) && (link.param2 !== null)) {

-                                return createSymbolicValue=>[

-                                        it.symbolicReference=relationDeclaration

-                                        it.parameterSubstitutions += createValueInLink(link.param1)

-                                        it.parameterSubstitutions += createValueInLink(link.param2)

-                                ]

+                        if ((link.param1 !== null) && (link.param2 !== null)) {

+                                if (typeof(PrimitiveElement).isAssignableFrom(link.param2.class) &&

+                                        !(link.param2 as PrimitiveElement).valueSet) {

+                                        return createSymbolicValue => [

+                                                it.symbolicReference = relationDeclaration

+                                                it.parameterSubstitutions += createValueInLink(link.param1)

+                                                it.parameterSubstitutions += createUnkownValueInLink(link.param2)

+                                        ]

+                                } else {

+                                        return createSymbolicValue => [

+                                                it.symbolicReference = relationDeclaration

+                                                it.parameterSubstitutions += createValueInLink(link.param1)

+                                                it.parameterSubstitutions += createValueInLink(link.param2)

+                                        ]

+                                }

+

                         } else {

                                 throw new IllegalArgumentException

                         }

@@ -189,4 +199,20 @@ class PartialInterpretation2Logic {
         def private dispatch createValueInLink(DefinedElement element) {

                 return createSymbolicValue => [it.symbolicReference = element]

         }

+        

+        def private dispatch createUnkownValueInLink(BooleanElement element) {

+                Exists[addVar(createBoolTypeReference)]

+        }

+        def private dispatch createUnkownValueInLink(IntegerElement element) {

+                Exists[addVar(createIntTypeReference)]

+        }

+        def private dispatch createUnkownValueInLink(RealElement element) {

+                Exists[addVar(createRealTypeReference)]

+        }

+        def private dispatch createUnkownValueInLink(StringElement element) {

+                throw new UnsupportedOperationException("Currently cannot create an unknown String")

+        }

+        def private dispatch createUnkownValueInLink(DefinedElement element) {

+                Exists[addVar(createComplexTypeReference => [it.referred = element.definedInType.get(0)])]

+        }

 }
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
index 92db5c18..28fc6e31 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage/PartialInterpretationInitialiser.xtend
@@ -4,10 +4,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
 import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes

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

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

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

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

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

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

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

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

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

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

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

 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.StringLiteral

@@ -31,7 +36,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement

-import java.math.BigDecimal

 import java.util.HashMap

 import java.util.Map

 import java.util.SortedSet

@@ -40,6 +44,7 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope
 import org.eclipse.xtend.lib.annotations.Data

 

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

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

 

 @Data class Problem2PartialInterpretationTrace {

         Map<TypeDeclaration, PartialComplexTypeInterpretation> type2Interpretation

@@ -253,7 +258,7 @@ class PartialInterpretationInitialiser {
                                 throw new UnsupportedOperationException('''Assertion describing partial model of "«r.interpretationOf.name»" contains unsupported constructs''')

                         }

                         for(link:links) {

-                                r.relationlinks += createLink(link,trace)

+                                r.relationlinks += createLink(interpretation, link,trace)

                         }

                 }

                 

@@ -264,8 +269,8 @@ class PartialInterpretationInitialiser {
 

                 return relation2Interpretation

         }

-        def private createLink(SymbolicValue v, PrimitiveValueTrace trace) {

-                val translatedValues = v.parameterSubstitutions.map[getElement(trace)].toList

+        def private createLink(PartialInterpretation interpretation, SymbolicValue v, PrimitiveValueTrace trace) {

+                val translatedValues = v.parameterSubstitutions.map[getElement(interpretation, trace)].toList

                 if(translatedValues.size == 1) {

                         return createUnaryElementRelationLink => [it.param1 = translatedValues.get(0)]

                 } else if(translatedValues.size == 2) {

@@ -282,21 +287,27 @@ class PartialInterpretationInitialiser {
                 }

         }

 

-        def private dispatch getElement(SymbolicValue element, PrimitiveValueTrace trace) {

+        def private dispatch getElement(SymbolicValue element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

                 return element.symbolicReference as DefinedElement

         }

-        def private dispatch getElement(BoolLiteral element, PrimitiveValueTrace trace) {

+        def private dispatch getElement(BoolLiteral element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

                 element.value.lookup(trace.booleanMap)

         }

-        def private dispatch getElement(IntLiteral element, PrimitiveValueTrace trace) {

+        def private dispatch getElement(IntLiteral element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

                 element.value.lookup(trace.integerMap)

         }

-        def private dispatch getElement(RealLiteral element, PrimitiveValueTrace trace) {

+        def private dispatch getElement(RealLiteral element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

                 element.value.lookup(trace.realMap)

         }

-        def private dispatch getElement(StringLiteral element, PrimitiveValueTrace trace) {

+        def private dispatch getElement(StringLiteral element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

                 element.value.lookup(trace.stringMap)

         }

+        def private dispatch getElement(Exists element, PartialInterpretation interpretation, PrimitiveValueTrace trace) {

+                val type = element.quantifiedVariables.get(0).range

+                val e = createUnknownValueElement(type)

+                interpretation.newElements += e

+                return e

+        }

         

         def private initialisePartialTypeInterpretation(TypeDeclaration t, ViatraQueryEngine engine) {

                 val supertypeMatcher = SupertypeStar.Matcher.on(engine)

@@ -319,4 +330,18 @@ class PartialInterpretationInitialiser {
                 ]

                 return res

         }

+                

+        def private dispatch createUnknownValueElement(BoolTypeReference element) {

+                createRealElement => [it.valueSet = false]

+        }

+        def private dispatch createUnknownValueElement(IntTypeReference element) {

+                createRealElement => [it.valueSet = false]

+        }

+        def private dispatch createUnknownValueElement(RealTypeReference element) {

+                createRealElement => [it.valueSet = false]

+        }

+        def private dispatch createUnknownValueElement(ComplexTypeReference element) {

+                //TODO Enum handling

+        }

+        

 }
\ No newline at end of file