diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | 331 |
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 @@ | |||
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 | ||