diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ new file mode 100644 index 00000000..05b97b0c --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ | |||
@@ -0,0 +1,212 @@ | |||
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 | |||
24 | class AlloyModelInterpretation implements LogicModelInterpretation{ | ||
25 | |||
26 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
27 | //protected val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
28 | |||
29 | protected val Logic2AlloyLanguageMapper forwardMapper | ||
30 | protected val Logic2AlloyLanguageMapperTrace forwardTrace; | ||
31 | |||
32 | private var ExprVar logicLanguage; | ||
33 | private var String logicBooleanTrue; | ||
34 | private var String logicBooleanFalse; | ||
35 | |||
36 | val Map<String,DefinedElement> alloyAtom2LogicElement = new HashMap | ||
37 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | ||
38 | |||
39 | private val Map<ConstantDeclaration, Object> constant2Value | ||
40 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | ||
41 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | ||
42 | |||
43 | private val int minInt | ||
44 | private val int maxInt | ||
45 | |||
46 | public new (A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | ||
47 | |||
48 | this.forwardMapper = forwardMapper | ||
49 | this.forwardTrace = trace | ||
50 | |||
51 | //TMP sig maps to identify alloy signatures by their names | ||
52 | val Map<String,Type> sigName2LogicType = | ||
53 | forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] | ||
54 | val Map<String,DefinedElement> elementNameNamel2DefinedElement = | ||
55 | forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] | ||
56 | |||
57 | // Fill the interpretation map with empty lists | ||
58 | forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] | ||
59 | |||
60 | // exporing individuals | ||
61 | for(atom: solution.allAtoms) { | ||
62 | val typeName = getName(atom.type) | ||
63 | val atomName = atom.name | ||
64 | //println(atom.toString + " < - " + typeName) | ||
65 | if(typeName == forwardTrace.logicLanguage.name) { | ||
66 | this.logicLanguage = atom | ||
67 | } else if(typeName == "Int" || typeName == "seq/Int") { | ||
68 | // do nothing | ||
69 | } else if(sigName2LogicType.containsKey(typeName) && typeName.lookup(sigName2LogicType) instanceof TypeDefinition) { | ||
70 | val element = elementNameNamel2DefinedElement.get(atomName.head) | ||
71 | alloyAtom2LogicElement.put(atom.label,element) | ||
72 | } else if(sigName2LogicType.containsKey(typeName)) { | ||
73 | val type = sigName2LogicType.get(typeName) | ||
74 | val elementsOfType = interpretationOfUndefinedType.get(type) | ||
75 | val element = createDefinedElement => [ | ||
76 | it.name += type.name | ||
77 | it.name += (elementsOfType.size+1).toString | ||
78 | ] | ||
79 | alloyAtom2LogicElement.put(atom.label,element) | ||
80 | elementsOfType+=element | ||
81 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | ||
82 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | ||
83 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | ||
84 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | ||
85 | } | ||
86 | else throw new UnsupportedOperationException('''Unknown atom: «atom»''') | ||
87 | } | ||
88 | |||
89 | //TMP field maps | ||
90 | val Map<String, Field> name2AlloyField = new HashMap | ||
91 | // exploring signatures | ||
92 | for(sig:solution.allReachableSigs) { | ||
93 | for(field : sig.fields) { | ||
94 | name2AlloyField.put(field.label,field) | ||
95 | } | ||
96 | } | ||
97 | |||
98 | // eval consants | ||
99 | constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ | ||
100 | solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term | ||
101 | ] | ||
102 | // eval functions | ||
103 | val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | | ||
104 | newHashMap( | ||
105 | solution.eval(function.name.lookup(name2AlloyField)) | ||
106 | .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] | ||
107 | |||
108 | val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | | ||
109 | val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) | ||
110 | val paramIndexes = 1..(function.parameters.size) | ||
111 | return newHashMap( | ||
112 | solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | | ||
113 | new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) | ||
114 | -> | ||
115 | t.atom(function.parameters.size + 1).atomLabel2Term | ||
116 | ])] | ||
117 | this.function2Value = Union(hostedfunction2Value,globalfunction2Value) | ||
118 | // eval relations | ||
119 | val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | | ||
120 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
121 | new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] | ||
122 | val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | | ||
123 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
124 | new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet] | ||
125 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | ||
126 | |||
127 | //Int limits | ||
128 | this.minInt = solution.min | ||
129 | this.maxInt = solution.max | ||
130 | |||
131 | |||
132 | } | ||
133 | |||
134 | def print() { | ||
135 | println('''Elements-----''') | ||
136 | interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v»''')] | ||
137 | |||
138 | println('''Constants-----''') | ||
139 | constant2Value.forEach[k, v|println('''«k.name» : «v»''')] | ||
140 | println('''Functions-----''') | ||
141 | function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] | ||
142 | println('''Relations-----''') | ||
143 | relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] | ||
144 | } | ||
145 | |||
146 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
147 | val name = type.toString | ||
148 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
149 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
150 | } | ||
151 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
152 | } | ||
153 | def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
154 | |||
155 | override getElements(Type type) { getElementsDispatch(type) } | ||
156 | def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } | ||
157 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | ||
158 | |||
159 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
160 | val transformedParams = new ParameterSubstitution(parameterSubstitution) | ||
161 | return transformedParams.lookup( | ||
162 | function.lookup(this.function2Value) | ||
163 | ) | ||
164 | } | ||
165 | |||
166 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
167 | relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) | ||
168 | } | ||
169 | |||
170 | override getInterpretation(ConstantDeclaration constant) { | ||
171 | constant.lookup(this.constant2Value) | ||
172 | } | ||
173 | |||
174 | override getMinimalInteger() { this.minInt } | ||
175 | override getMaximalInteger() { this.maxInt } | ||
176 | |||
177 | // Alloy term -> logic term | ||
178 | def private atomLabel2Term(String label) { | ||
179 | if(label.number) return Integer.parseInt(label) | ||
180 | else if(label == this.logicBooleanTrue) return true | ||
181 | else if(label == this.logicBooleanFalse) return false | ||
182 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | ||
183 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | ||
184 | } | ||
185 | def isNumber(String s) { | ||
186 | try{ | ||
187 | Integer.parseInt(s) | ||
188 | return true | ||
189 | }catch(NumberFormatException e) { | ||
190 | return false | ||
191 | } | ||
192 | } | ||
193 | } | ||
194 | |||
195 | class ParameterSubstitution{ | ||
196 | val Object[] data; | ||
197 | |||
198 | new(Object[] data) { this.data = data } | ||
199 | |||
200 | override equals(Object obj) { | ||
201 | if(obj === this) return true | ||
202 | else if(obj == null) return false | ||
203 | if(obj instanceof ParameterSubstitution) { | ||
204 | return Arrays.equals(this.data,obj.data) | ||
205 | } | ||
206 | return false | ||
207 | } | ||
208 | |||
209 | override hashCode() { | ||
210 | Arrays.hashCode(data) | ||
211 | } | ||
212 | } \ No newline at end of file | ||