aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_')
-rw-r--r--Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_212
1 files changed, 0 insertions, 212 deletions
diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
deleted file mode 100644
index 264e3ff8..00000000
--- a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_
+++ /dev/null
@@ -1,212 +0,0 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
4import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
5import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
15import java.util.Arrays
16import java.util.HashMap
17import java.util.LinkedList
18import java.util.List
19import java.util.Map
20import java.util.Set
21
22import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
23
24class 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 //print
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
195class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-05-25 19:38:03 +0000