From e9338be10e5453a7a026bbc16ddaa30abe9fa5be Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 13 Oct 2017 13:32:46 +0200 Subject: Refactoring of Alloy type mapping and interpretation. --- .../builder/AlloyModelInterpretation.xtend | 118 +-------------------- .../Logic2AlloyLanguageMapper_TypeMapper.xtend | 2 + ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 11 +- ...apper_TypeMapper_InheritanceAndHorizontal.xtend | 16 +-- 4 files changed, 12 insertions(+), 135 deletions(-) (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit') 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 53674ca3..abedf9e4 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 @@ -1,6 +1,7 @@ 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.builder.LogicModelInterpretation @@ -20,123 +21,6 @@ import java.util.Map import java.util.Set import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import edu.mit.csail.sdg.alloy4compiler.ast.Sig -import java.util.ArrayList - -interface AlloyModelInterpretation_TypeInterpretation { - def void resolveUnknownAtoms( - Iterable objectAtoms, - A4Solution solution, - Logic2AlloyLanguageMapperTrace forwardTrace, - Map name2AlloySig, - Map name2AlloyField, - Map expression2DefinedElement, - Map> interpretationOfUndefinedType) -} - -class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ - protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE - - override resolveUnknownAtoms( - Iterable objectAtoms, - A4Solution solution, - Logic2AlloyLanguageMapperTrace forwardTrace, - Map name2AlloySig, - Map name2AlloyField, - Map expression2DefinedElement, - Map> interpretationOfUndefinedType) - { - /*val Map expression2DefinedElement = new HashMap() - val Map> 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) - } - } - } -} -/* -class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{ - protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE - - override resolveUnknownAtoms(Iterable objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map alloyAtom2LogicElement) { - val Map> interpretationOfUndefinedType = new HashMap; - - //TMP sig maps to identify alloy signatures by their names - val Map sigName2LogicType = - forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] - //val Map elementNameNamel2DefinedElement = - // forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] - - // Fill the interpretation map with empty lists - forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] - - // exporing individuals - for(atom: objectAtoms) { - val typeName = getName(atom.type) - //val atomName = atom.name - - if(sigName2LogicType.containsKey(typeName)) { - val type = sigName2LogicType.get(typeName) - val elementsOfType = interpretationOfUndefinedType.get(type) - val element = createDefinedElement => [ - it.name += type.name - it.name += (elementsOfType.size+1).toString - ] - alloyAtom2LogicElement.put(atom.label,element) - elementsOfType+=element - } - else throw new UnsupportedOperationException('''Unknown atom: «atom»''') - } - - return interpretationOfUndefinedType - } - - def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { - val name = type.toString - if(name.startsWith("{this/") && name.endsWith("}")) { - return type.toString.replaceFirst("\\{this\\/","").replace("}","") - } - else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') - } - //def private getName(ExprVar atom) { atom.toString.split("\\$") } -}*/ class AlloyModelInterpretation implements LogicModelInterpretation{ diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend index 9927f1cc..49268b42 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend @@ -13,4 +13,6 @@ interface Logic2AlloyLanguageMapper_TypeMapper { def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace) def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace) + + def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter() } 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 ade9860b..3b2e3390 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 @@ -18,13 +18,7 @@ import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes - implements Logic2AlloyLanguageMapper_TypeMapperTrace -{ - public var ALSSignatureDeclaration objectSupperClass; - public val Map type2ALSType = new HashMap; - public val Map definedElement2Declaration = new HashMap -} + /** * Each object is an element of an Object set, and types are subsets of the objects. */ @@ -265,4 +259,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL return undefinedScope + trace.typeTrace.definedElement2Declaration.size } + override getTypeInterpreter() { + return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes + } } \ 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_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend index 92ac27df..be840e30 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend @@ -2,24 +2,13 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody -import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import java.util.Collection -import java.util.HashMap import java.util.LinkedList -import java.util.List -import java.util.Map - -class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { - public var ALSSignatureDeclaration objectSupperClass; - public val Map type2ALSType = new HashMap; - public val Map definedElement2Declaration = new HashMap - public val Map> typeSelection = new HashMap -} class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE @@ -125,4 +114,9 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { return undefinedScope + trace.typeTrace.definedElement2Declaration.size } + + override getTypeInterpreter() { + return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal + } + } \ No newline at end of file -- cgit v1.2.3-54-g00ecf