diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip |
Migrating Additional projects
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend')
-rw-r--r-- | Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | 268 |
1 files changed, 268 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..ade9860b --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,268 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | ||
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody | ||
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | ||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
13 | import java.util.ArrayList | ||
14 | import java.util.Collection | ||
15 | import java.util.HashMap | ||
16 | import java.util.List | ||
17 | import java.util.Map | ||
18 | |||
19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
20 | |||
21 | class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
22 | implements Logic2AlloyLanguageMapper_TypeMapperTrace | ||
23 | { | ||
24 | public var ALSSignatureDeclaration objectSupperClass; | ||
25 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
26 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
27 | } | ||
28 | /** | ||
29 | * Each object is an element of an Object set, and types are subsets of the objects. | ||
30 | */ | ||
31 | class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{ | ||
32 | private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; | ||
33 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | ||
34 | |||
35 | new() { | ||
36 | // Initialize package | ||
37 | LogicproblemPackage.eINSTANCE.class | ||
38 | } | ||
39 | |||
40 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
41 | val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
42 | trace.typeMapperTrace = typeTrace | ||
43 | |||
44 | // 1. A global type for Objects is created | ||
45 | val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] | ||
46 | val objectBody = createALSSignatureBody => [ | ||
47 | it.declarations += objectSig | ||
48 | it.abstract = true | ||
49 | ] | ||
50 | typeTrace.objectSupperClass = objectSig | ||
51 | trace.specification.signatureBodies += objectBody | ||
52 | |||
53 | // 2. Each type is mapped to a unique sig | ||
54 | for(type : types) { | ||
55 | val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] | ||
56 | val body = createALSSignatureBody => [it.declarations += sig] | ||
57 | trace.specification.signatureBodies += body | ||
58 | typeTrace.type2ALSType.put(type,sig) | ||
59 | } | ||
60 | |||
61 | // 3. The elements of a defined type is mapped to singleton signatures | ||
62 | // 3.1 Collect the elements | ||
63 | val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine) | ||
64 | val topmostType2Elements = new HashMap<ALSSignatureDeclaration,List<DefinedElement>> | ||
65 | for(element : elements) { | ||
66 | val topmostTypes = elementMatcher.getAllValuesOftype(element) | ||
67 | var ALSSignatureDeclaration selectedTopmostType; | ||
68 | if(topmostTypes.empty) { | ||
69 | selectedTopmostType = objectSig | ||
70 | } else{ | ||
71 | selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType) | ||
72 | } | ||
73 | topmostType2Elements.putOrAddToList(selectedTopmostType,element) | ||
74 | } | ||
75 | |||
76 | // 4. For each topmost types several singleton classes are generated, which represents the elements. | ||
77 | // For the sake of clarity, common bodies are used. | ||
78 | for(topmostEntry : topmostType2Elements.entrySet) { | ||
79 | |||
80 | for(element : topmostEntry.value) { | ||
81 | val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] | ||
82 | typeTrace.definedElement2Declaration.put(element,signature) | ||
83 | } | ||
84 | |||
85 | val body = createALSSignatureBody => [ | ||
86 | it.multiplicity = ALSMultiplicity.ONE | ||
87 | it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)] | ||
88 | ] | ||
89 | |||
90 | val containerLogicType = topmostEntry.key | ||
91 | body.superset += containerLogicType | ||
92 | |||
93 | trace.specification.signatureBodies+=body | ||
94 | } | ||
95 | |||
96 | // 5.1 Each Defined Type is specified as the union of its elements | ||
97 | for(definedType : types.filter(TypeDefinition)) { | ||
98 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
99 | it.name = support.toIDMultiple("typedefinition",definedType.name) | ||
100 | it.term = createALSEquals => [ | ||
101 | it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ] | ||
102 | it.rightOperand = support.unfoldPlus(definedType.elements.map[e| | ||
103 | createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]]) | ||
104 | ] | ||
105 | ] | ||
106 | } | ||
107 | // 5.2 Each Defined Element is unique | ||
108 | for(definedType : types.filter(TypeDefinition)) { | ||
109 | val allElementsIncludingSubtypes = | ||
110 | definedType.<Type>transitiveClosureStar[it.subtypes].filter(TypeDefinition) | ||
111 | .map[elements].flatten.toSet.toList | ||
112 | if(allElementsIncludingSubtypes.size>=2) { | ||
113 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
114 | it.name = support.toIDMultiple("typeElementsUnique",definedType.name) | ||
115 | it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace) | ||
116 | ] | ||
117 | } | ||
118 | } | ||
119 | |||
120 | // 6. Each inheritance is modeled by subset operator 'in' | ||
121 | for(type : types) { | ||
122 | val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody | ||
123 | if(type.supertypes.empty) { | ||
124 | sigBody.superset += typeTrace.objectSupperClass | ||
125 | } else { | ||
126 | sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)] | ||
127 | } | ||
128 | } | ||
129 | |||
130 | |||
131 | // 7. Each type is in the intersection of the supertypes | ||
132 | for(type : types.filter[it.supertypes.size>=2]) { | ||
133 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
134 | it.name = support.toIDMultiple("abstract",type.name) | ||
135 | it.term = createALSEquals => [ | ||
136 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
137 | it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| | ||
138 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
139 | ] | ||
140 | ] | ||
141 | } | ||
142 | |||
143 | // 8. Each abstract type is equal to the union of the subtypes | ||
144 | for(type : types.filter[isIsAbstract]) { | ||
145 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
146 | it.name = support.toIDMultiple("abstract",type.name) | ||
147 | it.term = createALSEquals => [ | ||
148 | it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] | ||
149 | it.rightOperand = support.unfoldPlus(type.subtypes.map[e| | ||
150 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
151 | ] | ||
152 | ] | ||
153 | } | ||
154 | // 8.1 The object type is the union of the root types. | ||
155 | val rootTypes = types.filter[it.supertypes.empty].toList | ||
156 | trace.specification.factDeclarations += createALSFactDeclaration => [ | ||
157 | it.name = support.toIDMultiple(#["ObjectTypeDefinition"]) | ||
158 | it.term = createALSEquals => [ | ||
159 | it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ] | ||
160 | it.rightOperand = support.unfoldPlus(rootTypes.map[e| | ||
161 | createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) | ||
162 | ] | ||
163 | ] | ||
164 | |||
165 | // 9. For each type X (including Object) | ||
166 | // only the common subtypes are in the intersection | ||
167 | // of the two subtype. | ||
168 | // 9.1. for the object | ||
169 | { | ||
170 | val rootTypeList = types.filter[it.supertypes.empty].toList | ||
171 | for(type1Index: 0..<rootTypeList.size) { | ||
172 | for(type2Index: 0..<type1Index) { | ||
173 | trace.specification.factDeclarations += | ||
174 | commonSubtypeOnlyInDiamonds(rootTypeList.get(type1Index),rootTypeList.get(type2Index),trace) | ||
175 | } | ||
176 | } | ||
177 | } | ||
178 | |||
179 | //9.3 for the subtypes of each objects | ||
180 | { | ||
181 | for(inScope : types) { | ||
182 | val subtypeList = inScope.subtypes//.toList | ||
183 | if(subtypeList.size>=2) { | ||
184 | for(type1Index: 0..<subtypeList.size) { | ||
185 | for(type2Index: 0..<type1Index) { | ||
186 | trace.specification.factDeclarations += | ||
187 | commonSubtypeOnlyInDiamonds(subtypeList.get(type1Index),subtypeList.get(type2Index),trace) | ||
188 | } | ||
189 | } | ||
190 | } | ||
191 | } | ||
192 | } | ||
193 | } | ||
194 | |||
195 | private def isEnumlikeType(Type type) { | ||
196 | if(type instanceof TypeDefinition) { | ||
197 | val elements = type.elements | ||
198 | return elements.forall[it.definedInType.size === 1 && it.definedInType.head === type] | ||
199 | } | ||
200 | return false | ||
201 | } | ||
202 | |||
203 | private def isEnumlikeElement(DefinedElement d) { | ||
204 | d.definedInType.size === 1 && d.definedInType.head.isEnumlikeType | ||
205 | } | ||
206 | |||
207 | def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { | ||
208 | val res = trace.typeMapperTrace | ||
209 | if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes) { | ||
210 | return res | ||
211 | } else { | ||
212 | throw new IllegalArgumentException(''' | ||
213 | Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», | ||
214 | but found «res.class.name»''') | ||
215 | } | ||
216 | } | ||
217 | |||
218 | def private commonSubtypeOnlyInDiamonds(Type t1, Type t2, Logic2AlloyLanguageMapperTrace trace) { | ||
219 | val topmostCommonSubtypes = TypeQueries.instance.getTopmostCommonSubtypes(trace.incqueryEngine) | ||
220 | val allTopmostCommon = topmostCommonSubtypes.getAllValuesOfcommon(t1,t2).toList | ||
221 | return createALSFactDeclaration => [ | ||
222 | it.name = support.toIDMultiple("common","types",t1.name,t2.name) | ||
223 | it.term = createALSEquals => [ | ||
224 | it.leftOperand = createALSIntersection => [ | ||
225 | it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)] | ||
226 | it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)] | ||
227 | ] | ||
228 | it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]]) | ||
229 | ] | ||
230 | ] | ||
231 | } | ||
232 | |||
233 | def private unfoldDistinctElements( | ||
234 | List<DefinedElement> operands, | ||
235 | Logic2AlloyLanguageMapperTrace trace | ||
236 | ) { | ||
237 | if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} | ||
238 | else { | ||
239 | val notEquals = new ArrayList<ALSTerm>(operands.size*operands.size/2) | ||
240 | for(i:0..<operands.size) { | ||
241 | for(j: i+1..<operands.size) { | ||
242 | notEquals+=createALSNotEquals=>[ | ||
243 | leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ] | ||
244 | rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ] | ||
245 | ] | ||
246 | } | ||
247 | } | ||
248 | return support.unfoldAnd(notEquals) | ||
249 | } | ||
250 | } | ||
251 | |||
252 | override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { | ||
253 | return #[trace.typeTrace.type2ALSType.get(referred)] | ||
254 | } | ||
255 | |||
256 | override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { | ||
257 | trace.typeTrace.objectSupperClass | ||
258 | } | ||
259 | |||
260 | override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { | ||
261 | createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)] | ||
262 | } | ||
263 | |||
264 | override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { | ||
265 | return undefinedScope + trace.typeTrace.definedElement2Declaration.size | ||
266 | } | ||
267 | |||
268 | } \ No newline at end of file | ||