Migrating Additional projects

author: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
committer: OszkarSemerath <oszka@152.66.252.189> 2017-06-10 19:05:05 +0200
commit: 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree: 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
parent: Initial commit, migrating from SVN (diff)
download: VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst
VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip
1 files changed, 331 insertions, 0 deletions
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
new file mode 100644
index 00000000..d00291e0
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -0,0 +1,331 @@
+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.Field
+import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import java.util.Arrays
+import java.util.HashMap
+import java.util.LinkedList
+import java.util.List
+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<ExprVar> objectAtoms, 
+                A4Solution solution,
+                Logic2AlloyLanguageMapperTrace forwardTrace,
+                Map<String, Sig> name2AlloySig,
+                Map<String, Field> name2AlloyField,
+                Map<String,DefinedElement> expression2DefinedElement,
+                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
+}
+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)
+                        }
+                }
+        }
+}
+/*
+class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        
+        override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) {
+                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;
+                
+                //TMP sig maps to identify alloy signatures by their names
+                val Map<String,Type> sigName2LogicType =
+                        forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name]
+                //val Map<String,DefinedElement> 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{
+        
+        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
+        protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator
+                
+        protected val Logic2AlloyLanguageMapper forwardMapper
+        protected val Logic2AlloyLanguageMapperTrace forwardTrace;
+        
+        private var ExprVar logicLanguage;
+        
+        private var String logicBooleanTrue;
+        private var String logicBooleanFalse;
+                
+        private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
+        private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
+        
+        private val Map<ConstantDeclaration, Object> constant2Value
+        private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
+        private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
+        
+        private val int minInt
+        private val int maxInt
+        
+        public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
+                this.typeInterpretator = typeInterpretator
+                this.forwardMapper = forwardMapper
+                this.forwardTrace = trace
+                
+                // Maps to trace language elements to the parsed problem.
+                val Map<String, Sig> name2AlloySig = new HashMap
+                val Map<String, Field> name2AlloyField = new HashMap
+                // exploring signatures
+                for(sig:solution.allReachableSigs) {
+                        name2AlloySig.put(sig.label,sig)
+                        for(field : sig.fields) {
+                                name2AlloyField.put(field.label,field)
+                        }
+                }
+                
+                val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms)
+                this.typeInterpretator.resolveUnknownAtoms(
+                        unknownAtoms,
+                        solution,
+                        forwardTrace,
+                        name2AlloySig,
+                        name2AlloyField,
+                        alloyAtom2LogicElement,
+                        interpretationOfUndefinedType)
+                
+                // eval consants
+                constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
+                        solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
+                ]
+                // eval functions
+                val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function |
+                        newHashMap(
+                                solution.eval(function.name.lookup(name2AlloyField))
+                                        .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
+                
+                val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function |
+                        val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
+                        val paramIndexes = 1..(function.parameters.size)
+                        return newHashMap(
+                                solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t |
+                                        new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
+                                                ->
+                                        t.atom(function.parameters.size + 1).atomLabel2Term
+                                ])]
+                this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
+                // eval relations
+                val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
+                val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation |
+                        solution.eval(relation.name.lookup(name2AlloyField)).map[ t |
+                                new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet]
+                this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
+                
+                //Int limits
+                this.minInt = solution.min
+                this.maxInt = solution.max
+                
+                //print(trace)
+        }
+        
+        def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) {
+                val List<ExprVar> unknownAtoms = new LinkedList
+                
+                for(atom: allAtoms) {
+                        val typeName = getName(atom.type)
+                        val atomName = atom.name
+                        //println(atom.toString + "  < -  " + typeName)
+                        if(typeName == forwardTrace.logicLanguage.name) {
+                                this.logicLanguage = atom
+                        } else if(typeName == "Int" || typeName == "seq/Int") {
+                                // do nothing, integers will be parsed from the string
+                        } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
+                                if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
+                                else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
+                                else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
+                        }
+                        else unknownAtoms += atom
+                }
+                
+                return unknownAtoms
+        }
+        
+        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("\\$") }
+        
+        def print(Logic2AlloyLanguageMapperTrace trace) {
+                println('''Undefined-----''')
+                interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')]
+                //println('''Defined-----''')
+                //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')]
+                
+                println('''Constants-----''')
+                constant2Value.forEach[k, v|println('''«k.name» : «v»''')]
+                println('''Functions-----''')
+                function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]]
+                println('''Relations-----''')
+                relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]]
+        }
+        override getElements(Type type) { getElementsDispatch(type) }
+        def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
+        def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
+        
+        override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
+                val transformedParams = new ParameterSubstitution(parameterSubstitution)
+                return transformedParams.lookup(
+                        function.lookup(this.function2Value)
+                )
+        }
+        
+        override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
+                relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
+        }
+        
+        override getInterpretation(ConstantDeclaration constant) {
+                constant.lookup(this.constant2Value)
+        }
+        
+        override getMinimalInteger() { this.minInt }
+        override getMaximalInteger() { this.maxInt }
+        
+        // Alloy term -> logic term
+        def private atomLabel2Term(String label) {
+                if(label.number) return Integer.parseInt(label)
+                else if(label == this.logicBooleanTrue) return true
+                else if(label == this.logicBooleanFalse) return false
+                else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
+                else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
+        }
+        def private isNumber(String s) {
+                try{
+                        Integer.parseInt(s)
+                        return true
+                }catch(NumberFormatException e) {
+                        return false
+                }
+        }
+}
+/**
+ * Helper class for efficiently matching parameter substitutions for functions and relations.
+ */
+class ParameterSubstitution{
+        val Object[] data;
+        
+        new(Object[] data) { this.data = data }
+        
+        override equals(Object obj) {
+                if(obj === this) return true
+                else if(obj == null) return false
+                if(obj instanceof ParameterSubstitution) {
+                        return Arrays.equals(this.data,obj.data)
+                }
+                return false
+        }
+        
+        override hashCode() {
+                Arrays.hashCode(data)
+        }
+}
+\ No newline at end of file
author	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
committer	OszkarSemerath <oszka@152.66.252.189>	2017-06-10 19:05:05 +0200
commit	60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree	5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
parent	Initial commit, migrating from SVN (diff)
download	VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip

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 new file mode 100644 index 00000000..d00291e0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -0,0 +1,331 @@
	1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
	2
	3	import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
	4	import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
	5	import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
	6	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
	7	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
	8	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
	9	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
	10	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
	11	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
	12	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	13	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
	14	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
	15	import java.util.Arrays
	16	import java.util.HashMap
	17	import java.util.LinkedList
	18	import java.util.List
	19	import java.util.Map
	20	import java.util.Set
	21
	22	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
	23	import edu.mit.csail.sdg.alloy4compiler.ast.Sig
	24	import java.util.ArrayList
	25
	26	interface AlloyModelInterpretation_TypeInterpretation {
	27	def void resolveUnknownAtoms(
	28	Iterable<ExprVar> objectAtoms,
	29	A4Solution solution,
	30	Logic2AlloyLanguageMapperTrace forwardTrace,
	31	Map<String, Sig> name2AlloySig,
	32	Map<String, Field> name2AlloyField,
	33	Map<String,DefinedElement> expression2DefinedElement,
	34	Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
	35	}
	36
	37	class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{
	38	protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
	39
	40	override resolveUnknownAtoms(
	41	Iterable<ExprVar> objectAtoms,
	42	A4Solution solution,
	43	Logic2AlloyLanguageMapperTrace forwardTrace,
	44	Map<String, Sig> name2AlloySig,
	45	Map<String, Field> name2AlloyField,
	46	Map<String,DefinedElement> expression2DefinedElement,
	47	Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
	48	{
	49	/*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()
	50	val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/
	51
	52	val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes
	53
	54	// 1. Evaluate the defined elements
	55	for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {
	56	val name = definedElementMappingEntry.value.name
	57	val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
	58	val elementsOfSingletonSignature = solution.eval(matchingSig)
	59	if(elementsOfSingletonSignature.size != 1) {
	60	throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')
	61	} else {
	62	val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar
	63	expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)
	64	}
	65	}
	66
	67	// 2. evaluate the signatures and create new elements if necessary
	68	for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {
	69	val type = type2SingatureEntry.key
	70	if(type instanceof TypeDeclaration) {
	71	val name = type2SingatureEntry.value.name
	72	val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
	73	val elementsOfSignature = solution.eval(matchingSig)
	74	val elementList = new ArrayList(elementsOfSignature.size)
	75	var newVariableIndex = 1;
	76	for(elementOfSignature : elementsOfSignature) {
	77	val expressionOfDefinedElement = elementOfSignature.atom(0)
	78	if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {
	79	elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)
	80	} else {
	81	val newElementName = '''newObject «newVariableIndex.toString»'''
	82	val newRepresentation = createDefinedElement => [
	83	it.name = newElementName
	84	]
	85	elementList += newRepresentation
	86	expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)
	87	}
	88	}
	89	interpretationOfUndefinedType.put(type,elementList)
	90	}
	91	}
	92	}
	93	}
	94	/*
	95	class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{
	96	protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
	97
	98	override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) {
	99	val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;
	100
	101	//TMP sig maps to identify alloy signatures by their names
	102	val Map<String,Type> sigName2LogicType =
	103	forwardTrace.type2ALSType.keySet.toMap[x\|forwardTrace.type2ALSType.get(x).name]
	104	//val Map<String,DefinedElement> elementNameNamel2DefinedElement =
	105	// forwardTrace.definedElement2Declaration.keySet.toMap[x\|forwardTrace.definedElement2Declaration.get(x).name]
	106
	107	// Fill the interpretation map with empty lists
	108	forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x\|interpretationOfUndefinedType.put(x,new LinkedList)]
	109
	110	// exporing individuals
	111	for(atom: objectAtoms) {
	112	val typeName = getName(atom.type)
	113	//val atomName = atom.name
	114
	115	if(sigName2LogicType.containsKey(typeName)) {
	116	val type = sigName2LogicType.get(typeName)
	117	val elementsOfType = interpretationOfUndefinedType.get(type)
	118	val element = createDefinedElement => [
	119	it.name += type.name
	120	it.name += (elementsOfType.size+1).toString
	121	]
	122	alloyAtom2LogicElement.put(atom.label,element)
	123	elementsOfType+=element
	124	}
	125	else throw new UnsupportedOperationException('''Unknown atom: «atom»''')
	126	}
	127
	128	return interpretationOfUndefinedType
	129	}
	130
	131	def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
	132	val name = type.toString
	133	if(name.startsWith("{this/") && name.endsWith("}")) {
	134	return type.toString.replaceFirst("\\{this\\/","").replace("}","")
	135	}
	136	else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
	137	}
	138	//def private getName(ExprVar atom) { atom.toString.split("\\$") }
	139	}*/
	140
	141	class AlloyModelInterpretation implements LogicModelInterpretation{
	142
	143	protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
	144	protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator
	145
	146	protected val Logic2AlloyLanguageMapper forwardMapper
	147	protected val Logic2AlloyLanguageMapperTrace forwardTrace;
	148
	149	private var ExprVar logicLanguage;
	150
	151	private var String logicBooleanTrue;
	152	private var String logicBooleanFalse;
	153
	154	private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap
	155	private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap
	156
	157	private val Map<ConstantDeclaration, Object> constant2Value
	158	private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value
	159	private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value
	160
	161	private val int minInt
	162	private val int maxInt
	163
	164	public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) {
	165	this.typeInterpretator = typeInterpretator
	166	this.forwardMapper = forwardMapper
	167	this.forwardTrace = trace
	168
	169	// Maps to trace language elements to the parsed problem.
	170	val Map<String, Sig> name2AlloySig = new HashMap
	171	val Map<String, Field> name2AlloyField = new HashMap
	172	// exploring signatures
	173	for(sig:solution.allReachableSigs) {
	174	name2AlloySig.put(sig.label,sig)
	175	for(field : sig.fields) {
	176	name2AlloyField.put(field.label,field)
	177	}
	178	}
	179
	180	val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms)
	181	this.typeInterpretator.resolveUnknownAtoms(
	182	unknownAtoms,
	183	solution,
	184	forwardTrace,
	185	name2AlloySig,
	186	name2AlloyField,
	187	alloyAtom2LogicElement,
	188	interpretationOfUndefinedType)
	189
	190	// eval consants
	191	constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[
	192	solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term
	193	]
	194	// eval functions
	195	val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function \|
	196	newHashMap(
	197	solution.eval(function.name.lookup(name2AlloyField))
	198	.map[t \| new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])]
	199
	200	val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function \|
	201	val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField)
	202	val paramIndexes = 1..(function.parameters.size)
	203	return newHashMap(
	204	solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t \|
	205	new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term])
	206	->
	207	t.atom(function.parameters.size + 1).atomLabel2Term
	208	])]
	209	this.function2Value = Union(hostedfunction2Value,globalfunction2Value)
	210	// eval relations
	211	val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation \|
	212	solution.eval(relation.name.lookup(name2AlloyField)).map[ t \|
	213	new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet]
	214	val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation \|
	215	solution.eval(relation.name.lookup(name2AlloyField)).map[ t \|
	216	new ParameterSubstitution((1..<t.arity).map[int a\|t.atom(a).atomLabel2Term])].toSet]
	217	this.relation2Value = Union(hostedRelation2Value,globalRelation2Value)
	218
	219	//Int limits
	220	this.minInt = solution.min
	221	this.maxInt = solution.max
	222
	223	//print(trace)
	224	}
	225
	226	def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) {
	227	val List<ExprVar> unknownAtoms = new LinkedList
	228
	229	for(atom: allAtoms) {
	230	val typeName = getName(atom.type)
	231	val atomName = atom.name
	232	//println(atom.toString + " < - " + typeName)
	233	if(typeName == forwardTrace.logicLanguage.name) {
	234	this.logicLanguage = atom
	235	} else if(typeName == "Int" \|\| typeName == "seq/Int") {
	236	// do nothing, integers will be parsed from the string
	237	} else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) {
	238	if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label }
	239	else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label}
	240	else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''')
	241	}
	242	else unknownAtoms += atom
	243	}
	244
	245	return unknownAtoms
	246	}
	247
	248	def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {
	249	val name = type.toString
	250	if(name.startsWith("{this/") && name.endsWith("}")) {
	251	return type.toString.replaceFirst("\\{this\\/","").replace("}","")
	252	}
	253	else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')
	254	}
	255	def private getName(ExprVar atom) { atom.toString.split("\\$") }
	256
	257	def print(Logic2AlloyLanguageMapperTrace trace) {
	258	println('''Undefined-----''')
	259	interpretationOfUndefinedType.forEach[k,v\|println('''«k.name» -> «v.map[name]»''')]
	260	//println('''Defined-----''')
	261	//trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')]
	262
	263	println('''Constants-----''')
	264	constant2Value.forEach[k, v\|println('''«k.name» : «v»''')]
	265	println('''Functions-----''')
	266	function2Value.forEach[f,m\|m.forEach[k,v\| println('''«f.name» : «k» \|-> «v»''')]]
	267	println('''Relations-----''')
	268	relation2Value.forEach[r,s\|s.forEach[t \| println('''«r.name»: («t»)''')]]
	269	}
	270
	271	override getElements(Type type) { getElementsDispatch(type) }
	272	def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) }
	273	def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements }
	274
	275	override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) {
	276	val transformedParams = new ParameterSubstitution(parameterSubstitution)
	277	return transformedParams.lookup(
	278	function.lookup(this.function2Value)
	279	)
	280	}
	281
	282	override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) {
	283	relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution))
	284	}
	285
	286	override getInterpretation(ConstantDeclaration constant) {
	287	constant.lookup(this.constant2Value)
	288	}
	289
	290	override getMinimalInteger() { this.minInt }
	291	override getMaximalInteger() { this.maxInt }
	292
	293	// Alloy term -> logic term
	294	def private atomLabel2Term(String label) {
	295	if(label.number) return Integer.parseInt(label)
	296	else if(label == this.logicBooleanTrue) return true
	297	else if(label == this.logicBooleanFalse) return false
	298	else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement)
	299	else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''')
	300	}
	301	def private isNumber(String s) {
	302	try{
	303	Integer.parseInt(s)
	304	return true
	305	}catch(NumberFormatException e) {
	306	return false
	307	}
	308	}
	309	}
	310
	311	/**
	312	* Helper class for efficiently matching parameter substitutions for functions and relations.
	313	*/
	314	class ParameterSubstitution{
	315	val Object[] data;
	316
	317	new(Object[] data) { this.data = data }
	318
	319	override equals(Object obj) {
	320	if(obj === this) return true
	321	else if(obj == null) return false
	322	if(obj instanceof ParameterSubstitution) {
	323	return Arrays.equals(this.data,obj.data)
	324	}
	325	return false
	326	}
	327
	328	override hashCode() {
	329	Arrays.hashCode(data)
	330	}
	331	} \ No newline at end of file