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 | 47 |
1 files changed, 32 insertions, 15 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 95216835..107aa001 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 | |||
@@ -19,6 +19,8 @@ import java.util.LinkedList | |||
19 | import java.util.List | 19 | import java.util.List |
20 | import java.util.Map | 20 | import java.util.Map |
21 | import java.util.Set | 21 | import java.util.Set |
22 | import java.util.SortedSet | ||
23 | import java.util.TreeSet | ||
22 | 24 | ||
23 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
24 | 26 | ||
@@ -34,6 +36,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
34 | 36 | ||
35 | private var String logicBooleanTrue; | 37 | private var String logicBooleanTrue; |
36 | private var String logicBooleanFalse; | 38 | private var String logicBooleanFalse; |
39 | private SortedSet<Integer> integerAtoms = new TreeSet | ||
40 | private SortedSet<String> stringAtoms = new TreeSet | ||
37 | 41 | ||
38 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap | 42 | private val Map<String, DefinedElement> alloyAtom2LogicElement = new HashMap |
39 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | 43 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap |
@@ -42,8 +46,8 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
42 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | 46 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value |
43 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | 47 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value |
44 | 48 | ||
45 | private val int minInt | 49 | //private val int minInt |
46 | private val int maxInt | 50 | //private val int maxInt |
47 | 51 | ||
48 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | 52 | public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { |
49 | this.typeInterpretator = typeInterpretator | 53 | this.typeInterpretator = typeInterpretator |
@@ -60,8 +64,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
60 | name2AlloyField.put(field.label,field) | 64 | name2AlloyField.put(field.label,field) |
61 | } | 65 | } |
62 | } | 66 | } |
63 | 67 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) | |
64 | val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution.allAtoms) | ||
65 | this.typeInterpretator.resolveUnknownAtoms( | 68 | this.typeInterpretator.resolveUnknownAtoms( |
66 | unknownAtoms, | 69 | unknownAtoms, |
67 | solution, | 70 | solution, |
@@ -101,31 +104,46 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
101 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | 104 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) |
102 | 105 | ||
103 | //Int limits | 106 | //Int limits |
104 | this.minInt = solution.min | 107 | //this.minInt = solution.min |
105 | this.maxInt = solution.max | 108 | //this.maxInt = solution.max |
106 | 109 | ||
107 | //print(trace) | 110 | //print(trace) |
108 | } | 111 | } |
109 | 112 | ||
110 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(Iterable<ExprVar> allAtoms) { | 113 | def List<ExprVar> collectUnknownAndResolveKnownAtoms(A4Solution solution) { |
114 | val Iterable<ExprVar> allAtoms = solution.allAtoms | ||
111 | val List<ExprVar> unknownAtoms = new LinkedList | 115 | val List<ExprVar> unknownAtoms = new LinkedList |
112 | 116 | ||
113 | for(atom: allAtoms) { | 117 | for(atom: allAtoms) { |
114 | val typeName = getName(atom.type) | 118 | val typeName = getName(atom.type) |
115 | val atomName = atom.name | 119 | val atomName = atom.name |
116 | //println(atom.toString + " < - " + typeName) | 120 | println(atom.toString + " < - " + typeName) |
117 | if(typeName == forwardTrace.logicLanguage.name) { | 121 | if(typeName == forwardTrace.logicLanguage.name) { |
118 | this.logicLanguage = atom | 122 | this.logicLanguage = atom |
119 | } else if(typeName == "Int" || typeName == "seq/Int") { | 123 | } else if(typeName == "Int" || typeName == "seq/Int") { |
120 | // do nothing, integers will be parsed from the string | 124 | val value = Integer.parseInt(atomName.join) |
125 | this.integerAtoms.add(value) | ||
121 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | 126 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { |
122 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | 127 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } |
123 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | 128 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} |
124 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | 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 | ||
125 | } | 135 | } |
126 | else unknownAtoms += atom | ||
127 | } | 136 | } |
128 | 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 | } | ||
129 | return unknownAtoms | 147 | return unknownAtoms |
130 | } | 148 | } |
131 | 149 | ||
@@ -196,17 +214,16 @@ class AlloyModelInterpretation implements LogicModelInterpretation{ | |||
196 | } | 214 | } |
197 | 215 | ||
198 | override getAllIntegersInStructure() { | 216 | override getAllIntegersInStructure() { |
199 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 217 | this.integerAtoms |
200 | } | 218 | } |
201 | 219 | ||
202 | override getAllRealsInStructure() { | 220 | override getAllRealsInStructure() { |
203 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 221 | new TreeSet |
204 | } | 222 | } |
205 | 223 | ||
206 | override getAllStringsInStructure() { | 224 | override getAllStringsInStructure() { |
207 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 225 | this.stringAtoms |
208 | } | 226 | } |
209 | |||
210 | } | 227 | } |
211 | 228 | ||
212 | /** | 229 | /** |