1 files changed, 1 insertions, 117 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
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<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{

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 @@
1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder	1	package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2		2
3	import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar	3	import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
		4	import edu.mit.csail.sdg.alloy4compiler.ast.Sig
4	import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field	5	import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
5	import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution	6	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.builder.LogicModelInterpretation
@@ -20,123 +21,6 @@ import java.util.Map
20	import java.util.Set	21	import java.util.Set
21		22
22	import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*	23	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		24
141	class AlloyModelInterpretation implements LogicModelInterpretation{	25	class AlloyModelInterpretation implements LogicModelInterpretation{
142		26