From fe2881fe9c09372ac4a5cc54e96b439d024dffd9 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 13 Oct 2017 13:35:03 +0200 Subject: :lipstick: --- ...loyModelInterpretation_TypeInterpretation.xtend | 21 +++++++ ...retation_TypeInterpretation_FilteredTypes.xtend | 72 ++++++++++++++++++++++ ...peInterpretation_InheritanceAndHorizontal.xtend | 20 ++++++ .../builder/Logic2AlloyLanguageMapper.xtend | 17 +++-- ...guageMapper_TypeMapperTrace_FilteredTypes.xtend | 15 +++++ ..._TypeMapperTrace_InheritanceAndHorizontal.xtend | 15 +++++ ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 2 - 7 files changed, 151 insertions(+), 11 deletions(-) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner') 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 objectAtoms, + A4Solution solution, + Logic2AlloyLanguageMapperTrace forwardTrace, + Map name2AlloySig, + Map name2AlloyField, + Map expression2DefinedElement, + Map> 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 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) + } + } + } +} \ 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 objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map name2AlloySig, Map name2AlloyField, Map expression2DefinedElement, Map> 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 type2ALSType = new HashMap; + public val Map 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 type2ALSType = new HashMap; + public val Map definedElement2Declaration = new HashMap + public val Map> 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. */ -- cgit v1.2.3-54-g00ecf