From 181d6443766d7b2212218b57183dce6af038c199 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 24 Jan 2021 01:49:37 +0100 Subject: Fix bug for ignored-attributes + better logic problem creation --- .../plugin.xml | 32 +++---- .../InstanceModel2PartialInterpretation.xtend | 99 +++++++++++++++++----- .../PartialInterpretation2Logic.xtend | 38 +++++++-- .../PartialInterpretationInitialiser.xtend | 43 ++++++++-- 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 @@ - - - - - - - - - - - - - - - +--> + + + + + + + + + + + + + + + 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 - 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 + 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 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 -- cgit v1.2.3-54-g00ecf