diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-10-13 13:32:46 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-10-13 13:32:46 +0200 |
commit | e9338be10e5453a7a026bbc16ddaa30abe9fa5be (patch) | |
tree | c33155d6110dc4cf2c99eda427cfb04ceff1511d /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend | |
parent | Visualisation for all models in a directory (diff) | |
download | VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.tar.gz VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.tar.zst VIATRA-Generator-e9338be10e5453a7a026bbc16ddaa30abe9fa5be.zip |
Refactoring of Alloy type mapping and interpretation.
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 | 118 |
1 files changed, 1 insertions, 117 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 53674ca3..abedf9e4 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 | |||
@@ -1,6 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | 3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar |
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | 5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field |
5 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | 6 | 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.builder.LogicModelInterpretation |
@@ -20,123 +21,6 @@ import java.util.Map | |||
20 | import java.util.Set | 21 | import java.util.Set |
21 | 22 | ||
22 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 23 | 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 | 24 | ||
141 | class AlloyModelInterpretation implements LogicModelInterpretation{ | 25 | class AlloyModelInterpretation implements LogicModelInterpretation{ |
142 | 26 | ||