diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-25 04:15:39 -0400 |
commit | 25a4b1b53add70e268c3083682f8a3508c618ec2 (patch) | |
tree | 6d46e62be49cfe6c5640e2e9af80aae90da6a212 /Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |
parent | mid-measurement push (diff) | |
download | VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.gz VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.tar.zst VIATRA-Generator-25a4b1b53add70e268c3083682f8a3508c618ec2.zip |
VAMPIRE: post-submission push
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend')
-rw-r--r-- | Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend new file mode 100644 index 00000000..dcb4bb32 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |||
@@ -0,0 +1,249 @@ | |||
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 | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
16 | import java.util.Arrays | ||
17 | import java.util.HashMap | ||
18 | import java.util.LinkedList | ||
19 | import java.util.List | ||
20 | import java.util.Map | ||
21 | import java.util.Set | ||
22 | import java.util.SortedSet | ||
23 | import java.util.TreeSet | ||
24 | |||
25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
26 | |||
27 | class AlloyModelInterpretation implements LogicModelInterpretation{ | ||
28 | |||
29 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
30 | protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator | ||
31 | |||
32 | protected val Logic2AlloyLanguageMapper forwardMapper | ||
33 | protected val Logic2AlloyLanguageMapperTrace forwardTrace; | ||
34 | |||
35 | private var ExprVar logicLanguage; | ||
36 | |||
37 | private var String logicBooleanTrue; | ||
38 | private var String logicBooleanFalse; | ||
39 | private SortedSet<Integer> integerAtoms = new TreeSet | ||
40 | private SortedSet<String> stringAtoms = new TreeSet | ||
41 | |||
42 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap | ||
43 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | ||
44 | |||
45 | private val Map<ConstantDeclaration, Object> constant2Value | ||
46 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | ||
47 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | ||
48 | |||
49 | //private val int minInt | ||
50 | //private val int maxInt | ||
51 | |||
52 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | ||
53 | this.typeInterpretator = typeInterpretator | ||
54 | this.forwardMapper = forwardMapper | ||
55 | this.forwardTrace = trace | ||
56 | |||
57 | // Maps to trace language elements to the parsed problem. | ||
58 | val Map<String, Sig> name2AlloySig = new HashMap | ||
59 | val Map<String, Field> name2AlloyField = new HashMap | ||
60 | // exploring signatures | ||
61 | for(sig:solution.allReachableSigs) { | ||
62 | name2AlloySig.put(sig.label,sig) | ||
63 | for(field : sig.fields) { | ||
64 | name2AlloyField.put(field.label,field) | ||
65 | } | ||
66 | } | ||
67 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) | ||
68 | this.typeInterpretator.resolveUnknownAtoms( | ||
69 | unknownAtoms, | ||
70 | solution, | ||
71 | forwardTrace, | ||
72 | name2AlloySig, | ||
73 | name2AlloyField, | ||
74 | alloyAtom2LogicElement, | ||
75 | interpretationOfUndefinedType) | ||
76 | |||
77 | // eval consants | ||
78 | constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ | ||
79 | solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term | ||
80 | ] | ||
81 | // eval functions | ||
82 | val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | | ||
83 | newHashMap( | ||
84 | solution.eval(function.name.lookup(name2AlloyField)) | ||
85 | .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] | ||
86 | |||
87 | val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | | ||
88 | val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) | ||
89 | val paramIndexes = 1..(function.parameters.size) | ||
90 | return newHashMap( | ||
91 | solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | | ||
92 | new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) | ||
93 | -> | ||
94 | t.atom(function.parameters.size + 1).atomLabel2Term | ||
95 | ])] | ||
96 | this.function2Value = Union(hostedfunction2Value,globalfunction2Value) | ||
97 | // eval relations | ||
98 | val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | | ||
99 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
100 | new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] | ||
101 | val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | | ||
102 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
103 | new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet] | ||
104 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | ||
105 | |||
106 | //Int limits | ||
107 | //this.minInt = solution.min | ||
108 | //this.maxInt = solution.max | ||
109 | |||
110 | //print(trace) | ||
111 | } | ||
112 | |||
113 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) { | ||
114 | val Iterable<ExprVar> allAtoms = solution.allAtoms | ||
115 | val List<ExprVar> unknownAtoms = new LinkedList | ||
116 | |||
117 | for(atom: allAtoms) { | ||
118 | val typeName = getName(atom.type) | ||
119 | val atomName = atom.name | ||
120 | println(atom.toString + " < - " + typeName) | ||
121 | if(typeName == forwardTrace.logicLanguage.name) { | ||
122 | this.logicLanguage = atom | ||
123 | } else if(typeName == "Int" || typeName == "seq/Int") { | ||
124 | val value = Integer.parseInt(atomName.join) | ||
125 | this.integerAtoms.add(value) | ||
126 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | ||
127 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | ||
128 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | ||
129 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | ||
130 | } else if(typeName == "String") { | ||
131 | val value = parseString(atomName.join) | ||
132 | this.stringAtoms.add(value) | ||
133 | } else { | ||
134 | unknownAtoms += atom | ||
135 | } | ||
136 | } | ||
137 | val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head | ||
138 | for(i : solution.eval(integerSignature)) { | ||
139 | val value = Integer.parseInt(i.atom(0)) | ||
140 | this.integerAtoms.add(value) | ||
141 | } | ||
142 | val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head | ||
143 | for(i : solution.eval(stringSignature)) { | ||
144 | val value = parseString(i.atom(0)) | ||
145 | this.stringAtoms.add(value) | ||
146 | } | ||
147 | return unknownAtoms | ||
148 | } | ||
149 | |||
150 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
151 | val name = type.toString | ||
152 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
153 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
154 | } | ||
155 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
156 | } | ||
157 | def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
158 | |||
159 | def print(Logic2AlloyLanguageMapperTrace trace) { | ||
160 | println('''Undefined-----''') | ||
161 | interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')] | ||
162 | //println('''Defined-----''') | ||
163 | //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')] | ||
164 | |||
165 | println('''Constants-----''') | ||
166 | constant2Value.forEach[k, v|println('''«k.name» : «v»''')] | ||
167 | println('''Functions-----''') | ||
168 | function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] | ||
169 | println('''Relations-----''') | ||
170 | relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] | ||
171 | } | ||
172 | |||
173 | override getElements(Type type) { getElementsDispatch(type) } | ||
174 | def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } | ||
175 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | ||
176 | |||
177 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
178 | val transformedParams = new ParameterSubstitution(parameterSubstitution) | ||
179 | return transformedParams.lookup( | ||
180 | function.lookup(this.function2Value) | ||
181 | ) | ||
182 | } | ||
183 | |||
184 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
185 | relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) | ||
186 | } | ||
187 | |||
188 | override getInterpretation(ConstantDeclaration constant) { | ||
189 | constant.lookup(this.constant2Value) | ||
190 | } | ||
191 | |||
192 | // Alloy term -> logic term | ||
193 | def private atomLabel2Term(String label) { | ||
194 | if(label.number) return Integer.parseInt(label) | ||
195 | else if(label == this.logicBooleanTrue) return true | ||
196 | else if(label == this.logicBooleanFalse) return false | ||
197 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | ||
198 | else if(label.isString) return parseString(label) | ||
199 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | ||
200 | } | ||
201 | def private isNumber(String s) { | ||
202 | try{ | ||
203 | Integer.parseInt(s) | ||
204 | return true | ||
205 | }catch(NumberFormatException e) { | ||
206 | return false | ||
207 | } | ||
208 | } | ||
209 | def private isString(String label) { | ||
210 | label.startsWith("\"") && label.endsWith("\"") | ||
211 | } | ||
212 | def private parseString(String label) { | ||
213 | label.substring(1,label.length-1) | ||
214 | } | ||
215 | |||
216 | override getAllIntegersInStructure() { | ||
217 | this.integerAtoms | ||
218 | } | ||
219 | |||
220 | override getAllRealsInStructure() { | ||
221 | new TreeSet | ||
222 | } | ||
223 | |||
224 | override getAllStringsInStructure() { | ||
225 | this.stringAtoms | ||
226 | } | ||
227 | } | ||
228 | |||
229 | /** | ||
230 | * Helper class for efficiently matching parameter substitutions for functions and relations. | ||
231 | */ | ||
232 | class ParameterSubstitution{ | ||
233 | val Object[] data; | ||
234 | |||
235 | new(Object[] data) { this.data = data } | ||
236 | |||
237 | override equals(Object obj) { | ||
238 | if(obj === this) return true | ||
239 | else if(obj == null) return false | ||
240 | if(obj instanceof ParameterSubstitution) { | ||
241 | return Arrays.equals(this.data,obj.data) | ||
242 | } | ||
243 | return false | ||
244 | } | ||
245 | |||
246 | override hashCode() { | ||
247 | Arrays.hashCode(data) | ||
248 | } | ||
249 | } \ No newline at end of file | ||